Changeset 3532


Ignore:
Timestamp:
Mar 16, 2015, 11:09:36 AM (5 years ago)
Author:
pellitta
Message:

prova predicato uguaglianza su tipo expr completata, prova predicato uguaglianza su tipo condition in corso

File:
1 edited

Legend:

Unmodified
Added
Removed

  • LTS/imp.ma

    r3530 r3532  
    7272|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    7373
     74lemma ifthenelse_aux:∀b,T.∀t:T.if b then t else t=t.
     75#b #T #t cases b % qed.
     76
     77lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
     78#b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
     79
     80lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
     81#b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
     82
     83lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
     84#b #b' cases b normalize #H destruct % qed.
     85
     86lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
     87#b #b' cases b normalize #H destruct % qed.
     88
     89lemma expr_eq_plus:∀e1,e2,f1,f2:expr.expr_eq (Plus e1 e2) (Plus f1 f2)=true→ ((expr_eq e1 f1)=true∧(expr_eq e2 f2)=true).
     90#e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
     91|inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
     92
     93lemma expr_eq_minus:∀e1,e2,f1,f2:expr.expr_eq (Minus e1 e2) (Minus f1 f2)=true→ ((expr_eq e1 f1)=true∧(expr_eq e2 f2)=true).
     94#e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)
     95|inversion(expr_eq e2 f2)] [1,3:#_ %|2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.
     96
     97
    7498lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2.
    7599#e1 elim e1
    … …  
    78102  |3,4,7,8: #e #f #ABS destruct]
    79103|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 
     104  [1,2,5: #v2 #H #K * [1,2,5,6,9,10:#n #ABS normalize in ABS; destruct
     105  |3,4,7,8,11,12:#f1 #f2 #T [2,4,5: normalize in T; destruct|1,3,6: >(H f1) >(K f2)
     106  [1,5,9:% 
     107  |2,4,10,12: inversion(f2) [2,6,10,14:#n #Hf2 >Hf2 in T;
     108  inversion(expr_eq e f1) #Heqef1 normalize >Heqef1 normalize #ABS destruct(ABS)
     109  |3,4,7,8,11,12,15,16:#f1 #f2 #_ #H1 #H2
     110  >H2 in T; normalize >ifthenelse_aux * %
     111  |1,5,9,13:#v #H2 >H2 in T; normalize #Hite >(ifthenelse_mm (expr_eq e f1) (neqb v2 v))
     112[1,3,5,7:%|2,4,6,8:assumption]]
     113|3:lapply(expr_eq_plus e (Var v2) f1 f2)|6,7,8:lapply(expr_eq_plus e (Const v2) f1 f2)
     114|11:lapply(expr_eq_minus e (Var v2) f1 f2)]* try(#H1 #H2) assumption]]
     115|6:#n #H #K #f cases f [1,2:#k|3,4:#f1 #f2] #T normalize in T; destruct(T)
     116>(K f2) [>(H f1) [%|inversion (expr_eq e f1) #II try(%) >II in T; #ABS normalize in ABS; destruct]
     117|inversion(f2) [#v #IHf >IHf in T; normalize >ifthenelse_aux * %
     118|#v #IHf >IHf in T; normalize inversion(neqb n v) #IHnenv #T try (%) >ifthenelse_aux in T; * %
     119|3,4: #g1 #g2 #Hg1 #Hg2 #Hf2 >Hf2 in T; normalize >ifthenelse_aux * %]]
     120|3,4,7,8:#f1 #f2 #H #K * [1,2,5,6,9,10:#n #T normalize in T; destruct
     121|3,4,7,8,9,11,12,15,16: #g1 #g2|13,14:#n] #T normalize in T; destruct
     122>(H g1) [1,3,5: >(K g2) [1,3,5:%|2,4,6: /2 by sym_eq, ifthenelse_mm/]
     123|2,4,6,8: /2 by ifthenelse_mm2/|7:>(K g2) [%|/2 by ifthenelse_mm/ qed.
     124
     125(*
    84126
    85127lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2.
    … …  
    97139      | #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4
    98140        >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
    114 elim f1
    115 [#v normalize lapply(neqb_true_to_eq v v) * #_ #A >(A …) [2:%] normalize
    116 elim 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
    122 elim 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
    137 normalize 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 
    166 elim 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 
     141*)     
     142
     143lemma condition_eq_sym:∀c:condition.cond_i_eq c c=true.
     144#c elim c [#e #f normalize >expr_eq_aux >expr_eq_aux normalize %
     145|#c' normalize * %] qed.
    174146
    175147lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
    176 #c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H;
     148#c1 #c2 % [2: * @condition_eq_sym
     149|elim c1 elim c2 [#e1 #e2 #f1 #f2 normalize inversion(expr_eq f1 e1)
     150normalize cases f1 cases e1 [1,2,5,6,17,18,21,22:#n1 #n2 normalize
     151#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) %
     153|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
     154#ABS destruct|5,6,7,8,13,14,15,16:#h1 #h2 normalize [2,3:#ABS destruct
     155|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
     175inversion(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
     183
    177184(*
    178185inductive cond_i:Type[0]≝cIfThenElse: cond_i.
Note: See TracChangeset for help on using the changeset viewer.