Changeset 3532
- Timestamp:
- Mar 16, 2015, 11:09:36 AM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/imp.ma
r3530 r3532 72 72 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 73 73 74 lemma ifthenelse_aux:∀b,T.∀t:T.if b then t else t=t. 75 #b #T #t cases b % qed. 76 77 lemma 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 80 lemma 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 83 lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true. 84 #b #b' cases b normalize #H destruct % qed. 85 86 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true. 87 #b #b' cases b normalize #H destruct % qed. 88 89 lemma 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 93 lemma 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 74 98 lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2. 75 99 #e1 elim e1 … … 78 102 |3,4,7,8: #e #f #ABS destruct] 79 103 |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 (* 84 126 85 127 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2. … … 97 139 | #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4 98 140 >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 143 lemma 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. 174 146 175 147 lemma 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) 150 normalize 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 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 183 177 184 (* 178 185 inductive cond_i:Type[0]≝cIfThenElse: cond_i.
Note: See TracChangeset
for help on using the changeset viewer.