Changeset 3530 for LTS/imp.ma


Ignore:
Timestamp:
Mar 13, 2015, 5:03:17 PM (5 years ago)
Author:
pellitta
Message:

prova in corso lemma che il predicato sul tipo expr corrisponde all'uguaglianza

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3529 r3530  
    5252  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
    5353  ].
    54 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
     54axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m.
     55lemma neqb_sym:∀n.neqb n n=true.
     56#n elim n [%|#n' normalize * %]qed.
    5557
    5658definition cond_i:Type[0]≝condition.
     
    6668|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
    6769
     70lemma expr_eq_aux:∀e:expr.expr_eq e e=true.
     71#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_sym
     72|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
     73
     74lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2.
     75#e1 elim e1
     76[1,2: #v1 * normalize
     77  [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) #A destruct >(A H) %
     78  |3,4,7,8: #e #f #ABS destruct]
     79|3,4: #e *
     80  [1,2,5: #v2 #H #K #f #T normalize in T;
     81  [1,2,5,6: #v2 #H /10 by _/
     82 
     83
     84
    6885lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2.
    69 #e1 #e2 elim e1 elim e2 normalize [#v #v' % #H elim v elim v' normalize in H;
    70 [%|#v2 #H' destruct
     86#e1 elim e1
     87[ #v1 *
     88  [ #v2 normalize % #H cases (neqb_true_to_eq v1 v2) #H1 #H2
     89    >H1 // destruct /2/
     90  | #c normalize % #H destruct
     91  |*: cases daemon ]
     92|
     93| #e1 #e2 #IH1 #IH2 *
     94  [3: #f1 #f2 normalize %
     95      [ inversion (expr_eq e1 f1) normalize #H1 #H2 [2: destruct ]
     96        cases (IH1 f1) cases (IH2 f2) /4 by eq_f2, sym_eq/
     97      | #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4
     98        >H4/2 by /
     99       
     100
     101#e1 #e2 elim e1 elim e2 [#v #v' % elim v elim v' [#_ %|#v2 #IH #H normalize in H; destruct
     102|#v2 #IH #H normalize in H; destruct|#v2 #H #v3 #K #T normalize in T; lapply(neqb_true_to_eq v2 v3)
     103* #A1 >(A1 T) #_ %|#_ %|#v2 #H #ABS destruct|#v2 #H #ABS destruct|#v1 #H #v2
     104#K #J destruct normalize lapply(neqb_true_to_eq v2 v2) * #_ #A >A %]
     105|#n #v % #H normalize in H; destruct|#f1 #f2 #A #B #v % #ABS normalize in ABS; destruct
     106|#f1 #f2 #A #B #v % #ABS normalize in ABS; destruct
     107|#v #n % normalize #ABS destruct|#n1 #n2 % normalize #H destruct [lapply(neqb_true_to_eq n2 n1)
     108* #A >(A H) #_ % | lapply(neqb_true_to_eq n1 n1) * #_ * %] (*end Var *)
     109|#f1 #f2 #_ #_ #n % normalize #ABS destruct
     110|#f1 #f2 #_ #_ #n % normalize #ABS destruct
     111|#v #f1 #f2 #_ #_ % normalize #ABS destruct
     112|#n #f1 #f2 #_ #_ % normalize #ABS destruct (* end Const*)
     113|#f1 #f2 #H1 #H2 #e1' #e2' #IH1 #IH2 % [2:#D destruct(D) normalize
     114elim f1
     115[#v normalize lapply(neqb_true_to_eq v v) * #_ #A >(A …) [2:%] normalize
     116elim f2
     117[#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize %
     118|#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize %
     119|#e #f #IHe #IHf normalize >IHe >IHf normalize %
     120|#e #f #IHe #IHf normalize >IHe >IHf normalize %]
     121|#n normalize lapply(neqb_true_to_eq n n) * #_ #A >(A \dots) [2:%] normalize
     122elim f2
     123[#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize %
     124|#v' normalize lapply(neqb_true_to_eq v' v') * #_ #B >(B …) [2:%] normalize %
     125|#e #f #IHe #IHf normalize >IHe >IHf normalize %
     126|#e #f #IHe #IHf normalize >IHe >IHf normalize %]
     127|#e #f inversion(expr_eq e e) inversion(expr_eq f f) #Hff #Hee normalize >Hff >Hee normalize #H * [%|%
     128|destruct|%]
     129|#e #f inversion(expr_eq e e) inversion(expr_eq f f) #Hff #Hee normalize >Hff >Hee normalize #H * [%|%
     130|destruct|%]]
     131|-IH1 -IH2  #H normalize in H; inversion(expr_eq e1' f1) inversion(expr_eq e2' f2)
     132#I2 #I1 (*[cut((e2'=f2)∧(e1'=f1)) [% [elim e2' elim f2
     133[#v #v'*)
     134>I1 in H; normalize >I2 #B destruct ] (* incompleto *)
     135
     136|#f1 #f2 #_ #_ #e #e' #_ #_ % #H
     137normalize in H; destruct
     138|#v #f1 #f2 #_ #_ % #H normalize in H; destruct
     139|#n #f1 #f2 #_ #_ % #H normalize in H; destruct
     140|#f1 #f2 #_ #_ #e #e' #_ #_ % #H normalize in H; destruct
     141|#f1 #f2 #_ #_ #e #e' #_ #_ % [2:* normalize inversion(expr_eq e e) inversion(expr_eq e' e')
     142#He #He' >He >He' normalize [%|
     143
     144
     145
     146
     147
     148
     149
     150#IHf normalize
     151
     152* #H6 #H7 cut(v2=v3) [@H6 @C|#K >K %]|#_ %|
     153#v2 #H #ABS destruct|#v2 #H #ABS destruct|#v2 #H #v3 #K #T >T normalize elim v3
     154[%|#v4 normalize * %]]|#v1 #v2 % normalize #ABS destruct|#f1 #f2 #H1 #H2 #v
     155% normalize #K destruct|#f1 #f2 #H1 #H2 #v % normalize #K destruct|
     156#v #n % normalize #ABS destruct|#n1 #n2 % normalize #H [2: destruct elim n1 normalize [%|#n * %]| lapply (neqb_true_to_eq n2 n1) #A elim A *
     157[#H22 %|@H]]|#f1 #f2 #H #K #n % normalize #ABS destruct|#f1 #f2 #H #K #n % normalize #ABS destruct
     158|#v #f1 #f2 #H1 #H2 % normalize #ABS destruct|#n #f1 #f2 #H1 #H2 % normalize #ABS destruct
     159|#f1 #f2 #_ #_ #ee1 #ee2 #_ #_ % [2:* normalize cases ee1 [#v normalize cases v normalize
     160[cases ee2 [#v' normalize lapply(neqb_true_to_eq v' v') * #_ * %
     161|#v' normalize lapply(neqb_true_to_eq v' v') * #_ * %
     162|#ff1 #ff2
     163 inversion(expr_eq ee1 f1)
     164[#H1 normalize #H2
     165
     166elim ee1 elim f1 elim ee2 elim f2
     167[#H559 #H560 #H561 #H562 #H563
     168
     169
     170#K [cut((ee1=f1)∧(ee2=f2))[% normalize in K;
     171
     172
     173
     174
    71175lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
    72176#c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H;
Note: See TracChangeset for help on using the changeset viewer.