Changeset 3533 for LTS/imp.ma
 Timestamp:
 Mar 16, 2015, 12:52:30 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3532 r3533 53 53 ]. 54 54 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m. 55 lemma neqb_ sym:∀n.neqb n n=true.55 lemma neqb_refl:∀n.neqb n n=true. 56 56 #n elim n [%#n' normalize * %]qed. 57 lemma 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. 57 60 58 61 definition cond_i:Type[0]≝condition. … … 69 72 70 73 lemma 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_ sym74 #e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_refl 72 75 3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 73 76 … … 123 126 2,4,6,8: /2 by ifthenelse_mm2/7:>(K g2) [%/2 by ifthenelse_mm/ qed. 124 127 128 lemma 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 (* 133 lemma 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 *) 137 lemma expr_eq_refl:∀e.expr_eq e e=true. 138 #e >expr_eq_equality_two % qed. 139 140 lemma 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 125 147 (* 126 148 … … 147 169 lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2. 148 170 #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 151 174 #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 k1K) %175 [1,2,5,6,17,18,21,22:#k1 #k2 >neqb_refl normalize #K destruct >(neqb_true_to_eq k1 k2 K) % 153 176 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 177 #ABS destruct5,6,7,8,13,14,15,16:#h1 #h2 normalize [2,3:#ABS destruct 155 178 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:#c3:#c'] normalize #H try(#K) destruct cut(c=c') 171 [2:* % inversion c inversion c' [1,3:#e #f2,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; 189 normalize #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 183 196 184 197 (*
Note: See TracChangeset
for help on using the changeset viewer.