Changeset 1977 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 May 22, 2012, 12:05:22 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1975 r1977 134 134 qed. 135 135 136 lemma pair_as_replace:137 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. 〈a, b〉 = c'→ T. ∀EQc: c'= c.138 c ≃ 〈a,b〉 →139 P ( let 〈a, b〉 as H ≝ c in t a b ?) → P (let 〈a',b'〉 as H ≝ c' in t a' b' H).136 lemma jmpair_as_replace: 137 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. c' ≃ 〈a, b〉 → T. ∀EQc: c'= c. 138 ∀EQ:c ≃ 〈a,b〉. 139 P (t a b ?) → P ((let 〈a',b'〉 (*as H*) ≝ c' in λH. t a' b' H) (refl_jmeq ? c')). 140 140 [2: 141 >EQc assumption141 >EQc @EQ 142 142 1: 143 #A #B #T #P #a #b * #x #y * #x' #y' #t #H1 #H2 destruct // 144 ] 143 #A #B #T #P #a #b 144 #c #c' #t #EQc >EQc in t; c' #f #EQ normalize lapply f lapply EQ EQ f cases c 145 cases daemon (* CSC: extremely difficult to prove... 146 normalize #a' #b' @(pose … 〈a,b〉) #H #f 147 @(pose … 〈a,b〉) 148 @(jmeq_elim ?? (λab.λH.P (f (\fst ab) (\snd ab) H)) ?? H) 149 check(E ????? H) 150 cut (a=a' ∧ b=b') 151 [ destruct /2/ 152  * #EQa #EQb >EQa in H; >EQb #H check (E ????? H) 153 #H cut (a=a') [2: #Eqa >Eqa in H; #H 154 155 156 * #x #y * #x' #y' #t #H1 #H2 cases H1 in H2; normalize 157 #X H1 destruct(X) destruct // 158 ]*) 145 159 qed. 146 160 … … 644 658 (* XXX: work on sigma commutation *) 645 659 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 646 (* XXX: work on ticks (of all kinds) *)647 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks648 660 (* XXX: work on both sides *) 649 661 [1,2,3,4,5: … … 655 667 ] 656 668 <EQaddr normalize nodelta #irrelevant 657 [1: 658 @(pair_as_replace ??? (λx. pi1 ?? x = ?) ???? (λx. λy. λ_. half_add ???) ? p) 659 669 try @(jmpair_as_replace ?????????? p) 670 [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ] 671 normalize nodelta 672 (* XXX: work on ticks (of all kinds) *) 673 >EQticks' ticks' <instr_refl in EQticks; #EQticks >EQticks 660 674 (* XXX: removes status 's' *) 661 675 normalize nodelta >EQs s ticks 662 676 whd in ⊢ (??%%); 663 677 (* XXX: simplify the left hand side *) 664 678 cases daemon 665 679 (* XXX: work on both sides *) 666 680 1,2,3,9,51,53,54,55: (* ADD, ADDC, SUBB, DEC, POP, XCHD, RET, RETI *)
Note: See TracChangeset
for help on using the changeset viewer.