Changeset 3548
 Timestamp:
 Mar 24, 2015, 2:18:28 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3547 r3548 27 27 #b #T #t cases b % qed. 28 28 29 (* use "whd in match (if ? then ? else ?);" instead of these two *) 30 (* however, whd fails to rewrite in some cases *) 31 (* to use it on hypothesis H write "whd in match(if ? then ? else ?) in H;" *) 29 32 lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1. 30 33 #T #t1 #t2 % qed. … … 55 58 56 59 (* what about this? *) 57 lemma contradiction:∀A:Prop.∀P.P→¬P→ A. 58 #A #P #H #Hn @(ex_falso_quodlibet ?) @(absurd P H Hn). qed. 60 (*lemma contradiction:∀A:Prop.∀P.P→¬P→ A. 61 #A #P #H #Hn @(ex_falso_quodlibet ?) @(absurd P H Hn). qed.*) 62 63 lemma contradiction:∀P.P→¬P→ (∀A:Prop.A). 64 #P #H #Hn #A @(ex_falso_quodlibet A (absurd P H Hn)) qed. 65 66 (* 67 lemma not_true:∀b.(b≠true)→ (b=false).#b cases b #H try(%) 68 @(contradiction (true=true) (refl …) H) qed. 69 70 lemma not_false:∀b.(b≠false)→ (b=true).#b cases b #H try(%) 71 @(contradiction (false=false) (refl …) H) qed. 72 *) 73 74 lemma not_bool:∀b1,b2.(b1≠b2)→ b1=(notb b2).* * normalize #H try(%) 75 @(contradiction (?=?) (refl …) H) qed. 59 76 60 77 lemma eqb_refl:∀T:DeqSet.∀t:T.(t==t)=true. 61 #T #t inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)@refl@ABS] qed.78 #T #t @(\b ?) % qed. (* inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)@refl@ABS] qed.*) 62 79 63 80 lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1). 64 81 #T #t1 #t2 inversion(t1==t2) #INV [lapply(\P INV)lapply(\Pf INV)] #H [>H >eqb_refl % 65 elim H #H' inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ( false=true) ((t1==t1)=true) INV2 ?)82 elim H #H' inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?) 66 83 /2 by /%] qed. 67 84 … … 325 342 (*elim E #ABS2 lapply (ABS2 ABS) #F cases F*) 326 343 whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??); 327 inversion(v2==v) #INV2 [>ifthenelse_true>ifthenelse_false]344 inversion(v2==v) #INV2 whd in match(if ? then ? else ?); 328 345 [whd in match (read ??); >INV2 >ifthenelse_true % 329 346 >IH whd in match (read (〈v,n〉::env') v2); >INV2 >ifthenelse_false % … … 333 350 #env #v1 #v2 #val #E elim env [whd in match (assign ???); whd in match(read ??); 334 351 >(\bf E) >ifthenelse_false %* #v #n #env' inversion(v==v1) #INV [<(\P INV) 335 #K whd in match (assign ???); >(\b refl …) >ifthenelse_true whd in match(read (〈v,n〉::env') v2); 336 inversion(v2==v) #INV2 [>ifthenelse_true>ifthenelse_false] whd in match(read ??); 337 >INV2 [>ifthenelse_truewhd in match(read ??); %] inversion(E) 338 #ABS #ABS2 destruct <(\P INV) in ABS; >(\P INV2) #ABS cases (ABS (refl …v)) 339 lapply (\Pf INV) #K whd in match (assign ???); whd in match (read (〈v,n〉::env') v2); 340 inversion(v2==v) #INV2 [>ifthenelse_true>ifthenelse_false] >(\b INV2) #H 341 whd in match (assign ???); 342 343 inversion(v1==v) #INV' 352 #K whd in match (assign ???); >(\b refl …) whd in match(if ? then ? else ?); 353 whd in match(read (〈v,n〉::env') v2); inversion(v2==v) #INV2 354 whd in match(if ? then ? else ?); whd in match(if ? then ? else ?); whd in match(read ??); 355 >INV2 try(%) inversion(E) #ABS #ABS2 destruct <(\P INV) in ABS; >(\P INV2) #ABS 356 @(contradiction (v=v) (refl …) ?) % assumptionlapply (\Pf INV) #K whd in match (assign ???); 357 whd in match (read (〈v,n〉::env') v2); inversion(v2==v) #INV2 [>ifthenelse_true>ifthenelse_false] 358 >(\b INV2) #H whd in match (assign ???); inversion(v1==v) #INV' 344 359 [1,3:>ifthenelse_true2,4:>ifthenelse_false] [2,4: <H whd in match(read ??); [ 345 >eqb_sym in INV; #INV @(contradiction ?((v1==v)=true) ? ?) [@INV'/2 by /]346 >INV2 >ifthenelse_false %]@(contradiction ?((v1==v)=true) ? ?)360 >eqb_sym in INV; #INV @(contradiction ((v1==v)=true) ? ?) [@INV'/2 by /] 361 >INV2 >ifthenelse_false %]@(contradiction ((v1==v)=true) ? ?) 347 362 [assumption/2 by /]whd in match (read ??); >INV2 >ifthenelse_true % qed. 348 363 … … 543 558 544 559 definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1). 560 545 561 546 562 (*  mIfThenElse1:
Note: See TracChangeset
for help on using the changeset viewer.