 Timestamp:
 Mar 21, 2015, 3:57:18 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3546 r3547 39 39 #b #T #t1 #t2 cases b #H normalize in H; destruct [%2%1] % qed. 40 40 41 (* it does not seem to be useful at all (rewriting does not simplify) *) 42 lemma ifthenelse_match:∀T:Type[0].∀t1,t2:T.∀b.if b then t1 else t2=match b with [true⇒ t1false⇒ t2]. 43 #T #t1 #t2 * [>ifthenelse_true>ifthenelse_false] % qed. 44 45 (* are these two really needed now? *) 41 46 lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true. 42 47 #b #b' cases b normalize #H destruct % qed. … … 45 50 #b #b' cases b normalize #H destruct % qed. 46 51 47 52 (* is ex_falso in the standard libary? *) 53 lemma ex_falso_quodlibet:∀P:Prop.False→ P. 54 #P #F cases F qed. 55 56 (* 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. 59 60 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. 62 63 lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1). 64 #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 ?) 66 /2 by /%] qed. 48 67 49 68 (* Syntax *) 50 51 69 52 70 definition variable ≝ DeqNat. … … 304 322 whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true>ifthenelse_false] 305 323 whd in match (read (〈v,n〉::env') v2); try % 306 lapply (\P INV2) #ABS elim E #ABS2 lapply (ABS2 ABS) #F cases F 324 lapply (\P INV2) #ABS @ex_falso_quodlibet @(absurd ? ABS E) 325 (*elim E #ABS2 lapply (ABS2 ABS) #F cases F*) 307 326 whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??); 308 327 inversion(v2==v) #INV2 [>ifthenelse_true>ifthenelse_false] … … 310 329 >IH whd in match (read (〈v,n〉::env') v2); >INV2 >ifthenelse_false % 311 330 qed. 331 332 lemma assign_miss2: ∀env,v1,v2,val. v2 ≠ v1 → (read (assign env v1 val) v2)= (read env v2). 333 #env #v1 #v2 #val #E elim env [whd in match (assign ???); whd in match(read ??); 334 >(\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' 344 [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) ? ?) 347 [assumption/2 by /]whd in match (read ??); >INV2 >ifthenelse_true % qed. 312 348 313 349 let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝
Note: See TracChangeset
for help on using the changeset viewer.