Changeset 3533 for LTS


Ignore:
Timestamp:
Mar 16, 2015, 12:52:30 PM (5 years ago)
Author:
pellitta
Message:

prova predicato uguaglianza tipo condition completata

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3532 r3533  
    5353  ].
    5454axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m.
    55 lemma neqb_sym:∀n.neqb n n=true.
     55lemma neqb_refl:∀n.neqb n n=true.
    5656#n elim n [%|#n' normalize * %]qed.
     57lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
     58#n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
     59% qed.
    5760
    5861definition cond_i:Type[0]≝condition.
     
    6972
    7073lemma 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
     74#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_refl
    7275|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    7376
     
    123126|2,4,6,8: /2 by ifthenelse_mm2/|7:>(K g2) [%|/2 by ifthenelse_mm/ qed.
    124127
     128lemma expr_eq_equality_two:∀e1,e2.e1=e2→ expr_eq e1 e2=true.
     129#e1 #e2 * elim e1 [1,2:#n normalize >neqb_refl %|3,4:#f1 #f2 normalize
     130#H1 >H1 #H2 >H2 normalize %]qed.
     131
     132(*
     133lemma expr_eq_equality_two':∀e1,e2.e1≠e2→ expr_eq e1 e2=false.
     134#e1 #e2 * lapply e2 -e2 #e2 elim e1 [1,2:#n normalize /3 by _/|3,4:#f1 #f2 normalize
     135#H1 >H1 #H2 >H2 normalize %]qed.
     136*)
     137lemma expr_eq_refl:∀e.expr_eq e e=true.
     138#e >expr_eq_equality_two % qed.
     139
     140lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1.
     141#e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' normalize >neqb_sym %
     142|#f1 #f2 normalize %|4,5,7,8:#f1 try(#f2) normalize %
     143|#n normalize //]
     144|3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %|3,8:#g1 #g2 >(H1 g1) >(H2 g2) %
     145|4,7:#_ #_ %] qed.
     146
    125147(*
    126148
     
    147169lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
    148170#c1 #c2 % [2: * @condition_eq_sym
    149 |elim c1 elim c2 [#e1 #e2 #f1 #f2 normalize inversion(expr_eq f1 e1)
    150 normalize cases f1 cases e1 [1,2,5,6,17,18,21,22:#n1 #n2 normalize
     171| lapply c2 -c2 elim c1 normalize
     172  [ #e1 #e2 * normalize
     173    [ #f1 #f2 inversion(expr_eq f1 e1) normalize cases f1 cases e1 [1,2,5,6,17,18,21,22:#n1 #n2 normalize
    151174#H destruct [1,2:>(neqb_true_to_eq n2 n1 H) cases f2 cases e2
    152 [1,2,5,6,17,18,21,22:#k1 #k2 normalize #K destruct >(neqb_true_to_eq k2 k1 K) %
     175[1,2,5,6,17,18,21,22:#k1 #k2 >neqb_refl normalize #K destruct >(neqb_true_to_eq k1 k2 K) %
    153176|3,4,7,8,11,12,15,16,19,20,23,24,27,28,31,32:#g1 #g2 [1,2,3,4,9,10,11,12:#n normalize
    154177#ABS destruct|5,6,7,8,13,14,15,16:#h1 #h2 normalize [2,3:#ABS destruct
    155178|1,4,5,6,7,8: inversion(expr_eq h1 g1) #INV1 >INV1 normalize #INV2 destruct
    156 -c1 -c2 -e1 -e2 -f1 -f2 -H >(expr_eq_equality_one h1 g1 INV1)
    157 >(expr_eq_equality_one h2 g2 INV2) %]]
    158 |9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS destruct]
    159 |3,4,5,6:#ABS destruct] |3,4,7,8,9,10:#n #h1 #h2 normalize #ABS destruct
    160 |11,12:#g1 #g2 #h1 #h2 normalize inversion(expr_eq h1 g1)
    161 #INV1 >INV1 normalize #INV2 #E destruct >(expr_eq_equality_one f2 e2 E)
    162 >(expr_eq_equality_one h1 g1 INV1) >(expr_eq_equality_one h2 g2 INV2) %
    163 |13,14:/3 by eq_f2, expr_eq_equality_one/
    164 |15,16,27,28,31,32:#g1 #g2 #h1 #h2 normalize inversion(expr_eq h1 g1)
    165 #INV1 >INV1 normalize #INV2 #E destruct >(expr_eq_equality_one f2 e2 E)
    166 >(expr_eq_equality_one h1 g1 INV1) >(expr_eq_equality_one h2 g2 INV2) %
    167 ]#n #g1 #g2 normalize #_ #ABS destruct
    168 |2,4:#c] #IH [#e #f|#c'|#e #c] normalize #H try(#K) destruct
    169 
    170 [2:#c|3:#c'] normalize #H try(#K) destruct cut(c=c')
    171 [2:* %| inversion c inversion c' [1,3:#e #f|2,4:#c3] #H1
    172 [#g1 #g2 #T
    173 /3 by _/
    174 
    175 inversion(expr_eq f1 e1) #INV1 >INV1 in H; normalize #H destruct
    176 >(expr_eq_equality_one f1 e1 INV1) >(expr_eq_equality_one f2 e2 H) %
    177 |normalize inversion(expr_eq f1 e1) #INV1 normalize nodelta
    178  inversion(expr_eq f2 e2) #INV2 >expr_eq_aux in INV1; normalize
    179  [1,3,5,7:#INV1 >expr_eq_aux in INV2; normalize [1,3,5,7:#INV2
    180  elim f1
    181  normalize in H;
    182  #INV2 destruct
     179-c1 try(-c2) -e1 -e2 -f1 -f2 -H >INV1 in INV2; >neqb_refl >INV1 normalize
     180#INV2 >expr_eq_sym in INV1; #INV1 >INV1 in INV2; normalize #INV2 >expr_eq_sym in INV1;
     181#INV1 destruct >(expr_eq_equality_one g2 h2 INV2) >expr_eq_sym in INV1; #INV1
     182>(expr_eq_equality_one g1 h1 INV1) %] >neqb_refl in ABS; normalize #ABS destruct]
     183>neqb_refl in ABS; normalize #ABS destruct
     184|9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS >neqb_refl in ABS; normalize #ABS destruct]
     185|3,4,5,6:#ABS destruct >neqb_sym in H; #H >H in ABS; normalize #ABS destruct]
     186|9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS1 #ABS2 destruct
     187|11,12,15,16,27,28,31,32:#g1 #g2 #h1 #h2 normalize inversion(expr_eq h1 g1)
     188#INV1 >INV1 normalize #INV2 #E destruct >INV1 in E; normalize #E >expr_eq_sym in INV1; #INV1; >INV1 in E;
     189normalize #E destruct >expr_eq_sym in INV1; #INV1 >(expr_eq_equality_one h1 g1 INV1)
     190>expr_eq_sym in INV2; #INV2 >INV2 in E; normalize #E destruct >expr_eq_sym in INV2; #INV2
     191>(expr_eq_equality_one h2 g2 INV2) >expr_eq_sym in E; #E >(expr_eq_equality_one f2 e2 E) %
     192]#f1 #f2 #n normalize #ABS1 #ABS2 destruct
     193|#c2 #ABS destruct]|#c2 #H #c' cases c' [#e1 #e2 normalize #ABS destruct|#c3 normalize #K
     194>(H c3 K) % qed.
     195
    183196
    184197(*
Note: See TracChangeset for help on using the changeset viewer.