Changeset 3530
 Timestamp:
 Mar 13, 2015, 5:03:17 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3529 r3530 52 52  S p ⇒ match m with [ O ⇒ false  S q ⇒ neqb p q] 53 53 ]. 54 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. 54 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m. 55 lemma neqb_sym:∀n.neqb n n=true. 56 #n elim n [%#n' normalize * %]qed. 55 57 56 58 definition cond_i:Type[0]≝condition. … … 66 68 Not e⇒ match c2 with [Not f⇒ cond_i_eq e f_⇒ false]]. 67 69 70 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_sym 72 3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 73 74 lemma 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 68 85 lemma 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 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 174 71 175 lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2. 72 176 #c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H;
Note: See TracChangeset
for help on using the changeset viewer.