Changeset 3548 for LTS/imp.ma


Ignore:
Timestamp:
Mar 24, 2015, 2:18:28 PM (5 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3547 r3548  
    2727#b #T #t cases b % qed.
    2828
     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;" *)
    2932lemma ifthenelse_true:∀T:Type[0].∀t1,t2:T.if true then t1 else t2=t1.
    3033#T #t1 #t2 % qed.
     
    5558
    5659(* 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
     63lemma contradiction:∀P.P→¬P→ (∀A:Prop.A).
     64#P #H #Hn #A @(ex_falso_quodlibet A (absurd P H Hn)) qed.
     65
     66(*
     67lemma not_true:∀b.(b≠true)→ (b=false).#b cases b #H try(%)
     68@(contradiction (true=true) (refl …) H) qed.
     69
     70lemma not_false:∀b.(b≠false)→ (b=true).#b cases b #H try(%)
     71@(contradiction (false=false) (refl …) H) qed.
     72*)
     73
     74lemma not_bool:∀b1,b2.(b1≠b2)→ b1=(notb b2).* * normalize #H try(%)
     75@(contradiction (?=?) (refl …) H) qed.
    5976
    6077lemma 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.*)
    6279
    6380lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1).
    6481#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 ?)
    6683/2 by /|%] qed.
    6784
     
    325342(*elim E #ABS2 lapply (ABS2 ABS) #F cases F*)
    326343|whd in match (assign ???); >INV >ifthenelse_false whd in match (read ??);
    327 inversion(v2==v) #INV2 [>ifthenelse_true|>ifthenelse_false]
     344inversion(v2==v) #INV2 whd in match(if ? then ? else ?);
    328345[whd in match (read ??); >INV2 >ifthenelse_true %
    329346|>IH whd in match (read (〈v,n〉::env') v2);  >INV2 >ifthenelse_false %
     
    333350 #env #v1 #v2 #val #E elim env [whd in match (assign ???); whd in match(read ??);
    334351 >(\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);
    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 …) ?) % assumption|lapply (\Pf INV) #K whd in match (assign ???);
     357whd 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'
    344359[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) ? ?)
     360>eqb_sym in INV; #INV @(contradiction ((v1==v)=true) ? ?) [@INV'|/2 by /]
     361|>INV2 >ifthenelse_false %]|@(contradiction ((v1==v)=true) ? ?)
    347362[assumption|/2 by /]|whd in match (read ??); >INV2 >ifthenelse_true % qed.
    348363
     
    543558
    544559definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1).
     560
    545561
    546562(* | mIfThenElse1:
Note: See TracChangeset for help on using the changeset viewer.