Changeset 3547 for LTS


Ignore:
Timestamp:
Mar 21, 2015, 3:57:18 PM (5 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3546 r3547  
    3939#b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
    4040
     41(* it does not seem to be useful at all (rewriting does not simplify) *)
     42lemma ifthenelse_match:∀T:Type[0].∀t1,t2:T.∀b.if b then t1 else t2=match b with [true⇒ t1|false⇒ t2].
     43#T #t1 #t2 * [>ifthenelse_true|>ifthenelse_false] % qed.
     44
     45(* are these two really needed now? *)
    4146lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
    4247#b #b' cases b normalize #H destruct % qed.
     
    4550#b #b' cases b normalize #H destruct % qed.
    4651
    47 
     52(* is ex_falso in the standard libary? *)
     53lemma ex_falso_quodlibet:∀P:Prop.False→ P.
     54#P #F cases F qed.
     55
     56(* what about this? *)
     57lemma contradiction:∀A:Prop.∀P.P→¬P→ A.
     58#A #P #H #Hn @(ex_falso_quodlibet ?) @(absurd P H Hn). qed.
     59
     60lemma 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
     63lemma 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.
    4867
    4968(* Syntax *)
    50 
    5169
    5270definition variable ≝ DeqNat.
     
    304322whd in match (read (〈v,val〉::env') v2); >INV2 [>ifthenelse_true|>ifthenelse_false]
    305323whd in match (read (〈v,n〉::env') v2); try %
    306 lapply (\P INV2) #ABS elim E #ABS2 lapply (ABS2 ABS) #F cases F
     324lapply (\P INV2) #ABS @ex_falso_quodlibet @(absurd ? ABS E)
     325(*elim E #ABS2 lapply (ABS2 ABS) #F cases F*)
    307326|whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??);
    308327inversion(v2==v) #INV2 [>ifthenelse_true|>ifthenelse_false]
     
    310329|>IH whd in match (read (〈v,n〉::env') v2);  >INV2 >ifthenelse_false %
    311330qed.
     331
     332lemma 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_true|whd 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);
     340inversion(v2==v) #INV2 [>ifthenelse_true|>ifthenelse_false] >(\b INV2) #H
     341whd in match (assign ???);
     342
     343 inversion(v1==v) #INV'
     344[1,3:>ifthenelse_true|2,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.
    312348
    313349let rec sem_expr (env:environment) (e: expr) on e : (option nat) ≝
Note: See TracChangeset for help on using the changeset viewer.