Changeset 3553
 Timestamp:
 Apr 10, 2015, 3:08:55 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3548 r3553 54 54 55 55 (* is ex_falso in the standard libary? *) 56 lemma ex_falso_quodlibet:∀P:Prop.False→ P. 57 #P #F cases F qed. 56 (*lemma ex_falso_quodlibet:∀P:Prop.False→ P. 57 #P #F cases F qed.*) 58 lemma ex_falso_quodlibet:False→ ∀P:Prop.P. 59 #F cases F qed. 58 60 59 61 (* what about this? *) … … 62 64 63 65 lemma contradiction:∀P.P→¬P→ (∀A:Prop.A). 64 #P #H #Hn #A @(ex_falso_quodlibet A(absurd P H Hn)) qed.66 #P #H #Hn #A @(ex_falso_quodlibet (absurd P H Hn)) qed. 65 67 66 68 (* … … 75 77 @(contradiction (?=?) (refl …) H) qed. 76 78 79 lemma neq_bool:∀b1,b2.b1=(notb b2)→(b1≠b2).* * normalize #H /2 by sym_not_eq/ qed. 80 77 81 lemma eqb_refl:∀T:DeqSet.∀t:T.(t==t)=true. 78 82 #T #t @(\b ?) % qed. (* inversion(t==t) #H try(%) lapply(\Pf H) #ABS @(contradiction …) [@(t=t)@refl@ABS] qed.*) … … 80 84 lemma eqb_sym:∀T:DeqSet.∀t1,t2:T.(t1==t2)=(t2==t1). 81 85 #T #t1 #t2 inversion(t1==t2) #INV [lapply(\P INV)lapply(\Pf INV)] #H [>H >eqb_refl % 82  elim H #H'inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?)86 inversion(t2==t1) #INV2 [lapply(\P INV2) #ABS destruct @(contradiction ((t1==t1)=true) INV2 ?) 83 87 /2 by /%] qed. 88 89 lemma neq_refl_false:∀T.∀t:T.(t≠t)→ ∀P:Prop.P. 90 #T #t #H @(contradiction (t=t) (refl …) H) qed. 91 92 lemma neqb_refl_false:∀T:DeqSet.∀t:T.(t==t)=false→ ∀P:Prop.P. 93 #T #t #ABS @(contradiction ((t==t)=true) (eqb_refl …) ?) @neq_bool whd in match(¬true); 94 assumption qed. 84 95 85 96 (* Syntax *) … … 559 570 definition Lt:expr → expr → condition≝λe1,e2.Not (Geq e2 e1). 560 571 572 (* Abitare tipo Program *) 573 574 (* Abitare tipo Instructions *) 575 576 definition imp_Instructions≝Instructions imp_state_params. 577 578 definition imp_signature≝signature imp_state_params imp_state_params. 579 580 check CallCostLabel 581 582 definition imp_envitem:(env_item imp_env_params imp_instr_params)≝ 561 583 562 584 (*  mIfThenElse1:
Note: See TracChangeset
for help on using the changeset viewer.