Changeset 3538 for LTS/imp.ma
 Timestamp:
 Mar 16, 2015, 7:01:08 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3536 r3538 17 17 include "basics/bool.ma". 18 18 include "Language.ma". 19 include "basics/finset.ma". 19 20 20 21 (* Tools *) … … 34 35 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true. 35 36 #b #b' cases b normalize #H destruct % qed. 36 37 let rec neqb n m ≝38 match n with39 [ O ⇒ match m with [ O ⇒ true  S q ⇒ false]40  S p ⇒ match m with [ O ⇒ false  S q ⇒ neqb p q]41 ].42 43 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.44 45 definition DeqNat:DeqSet≝mk_DeqSet nat neqb neqb_true_to_eq.46 47 lemma neqb_refl:∀n.neqb n n=true.48 #n elim n [%#n' normalize * %]qed.49 50 lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.51 #n1 elim n1 [#n2 cases n2 [%#n' normalize %]#n2' #IH #n2 cases n2 normalize [2: #m >IH]52 % qed.53 37 54 38 (* Syntax *) … … 67 51 68 52 let rec expr_eq (e1:expr) (e2:expr):bool≝ 69 match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1v2_⇒ false]70 Const v1⇒ match e2 with [Const v2⇒ neqb v1v2_⇒ false]53 match e1 with [Var v1⇒ match e2 with [Var v2⇒ v1==v2_⇒ false] 54 Const v1⇒ match e2 with [Const v2⇒ v1==v2_⇒ false] 71 55 Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)_⇒ false] 72 56 Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)_⇒ false] … … 74 58 75 59 lemma expr_eq_refl:∀e:expr.expr_eq e e=true. 76 #e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * #_ *%60 #e elim e [1,2: #v change with (v==v = true); @(\b ?) % 77 61 3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 78 62 79 63 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2. 80 64 #e1 #e2 % [2:* lapply e2 e2 elim e1 81 [1,2:#n #_ normalize >neqb_refl%65 [1,2:#n #_ change with (n==n = true) @(\b ?) % 82 66 3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl] 83 67 lapply e2 e2 elim e1 84 [1,2: #v1 #e2 cases e2 normalize 85 [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) * #A destruct >(A H) #_ % 86 3,4,7,8: #e #f #ABS destruct] 68 [1,2: #v1 #e2 cases e2 69 [1,6: #v2 #H >(\P H) % 70 2,5: #v2 #H normalize in H; destruct 71 3,4,7,8: #e #f normalize #ABS destruct] 87 72 3,4: #e #e2 #H #K #f cases f 88 73 [1,2,5,6: #v2 normalize #ABS destruct … … 93 78 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [ 94 79 sNop ⇒ match s2 with [sNop ⇒ true _⇒ false] 95 sAss ⇒ match s2 with [sAss ⇒ true _⇒ false]96 sInc ⇒ match s2 with [sInc ⇒ true _⇒ false]80 sAss v e ⇒ match s2 with [sAss v' e' ⇒ (andb (v==v') (expr_eq e e')) _⇒ false] 81 sInc v ⇒ match s2 with [sInc v' ⇒ (v==v') _⇒ false] 97 82 ]. 98 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2 99 cases s1 cases s2 normalize % #H destruct % qed. 100 101 inductive io_i:Type[0]≝. 102 definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true. 103 lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2 104 cases i1 qed. 105 106 (*axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m. 107 axiom neqb_true_to_eq2: ∀n,m:nat. neqb n m = true ↔ n = m.*) 108 lemma neqb_refl:∀n.neqb n n=true. 109 #n elim n [%#n' normalize * %]qed. 110 lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1. 111 #n1 elim n1 [#n2 cases n2 [%#n' normalize %]#n2' #IH #n2 cases n2 normalize [2: #m >IH] 112 % qed. 83 84 lemma seq_i_eq_refl:∀s.seq_i_eq s s=true. 85 #s cases s try(#v) try(#e) try % 86 [ whd in ⊢ (??%?); >(\b (refl … v)) >expr_eq_refl % 87  change with (v==v = true); >(\b ?) %] qed. 88 89 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2. 90 #s1 #s2 % [2: * elim s1 [2,3:#v try(#e)] @seq_i_eq_refl 91 lapply s2 s2 elim s1 [2,3:#v] [#e] #s2 cases s2 [2,3,5,6,8,9:#v'] [1,3,5: #e'] 92 [2,3,4,6,7,8: normalize #H destruct 93 1: whd in ⊢ (??%? → ?); inversion (v==v') [2: normalize #_ #H destruct] 94 #EQ inversion (expr_eq e e') [2: normalize #_ #H destruct] #H #_ 95 >(proj1 … (expr_eq_equality …) H) >(\P EQ) % 96 5: #H >(\P H) % 97  // ] 98 qed. 113 99 114 100 definition cond_i:Type[0]≝condition. 115 let rec expr_eq (e1:expr) (e2:expr):bool≝ 116 match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2_⇒ false] 117 Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2_⇒ false] 118 Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)_⇒ false] 119 Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)_⇒ false] 120 ]. 101 121 102 let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝ 122 103 match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ … … 124 105 Not e⇒ match c2 with [Not f⇒ cond_i_eq e f_⇒ false]]. 125 106 126 lemma expr_eq_aux:∀e:expr.expr_eq e e=true.127 #e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * @neqb_refl128 3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.129 130 131 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).132 #e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)133 inversion(expr_eq e2 f2)] [1,3:#_ %2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.134 135 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).136 #e1 #e2 #f1 #f2 #H normalize in H; % [inversion(expr_eq e1 f1)137 inversion(expr_eq e2 f2)] [1,3:#_ %2,4:#K >K in H; normalize * [2:>ifthenelse_aux] % qed.138 139 140 lemma expr_eq_equality_one:∀e1,e2:expr.expr_eq e1 e2=true → e1=e2.141 #e1 elim e1142 [1,2: #v1 * normalize143 [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) #A destruct >(A H) %144 3,4,7,8: #e #f #ABS destruct]145 3,4: #e *146 [1,2,5: #v2 #H #K * [1,2,5,6,9,10:#n #ABS normalize in ABS; destruct147 3,4,7,8,11,12:#f1 #f2 #T [2,4,5: normalize in T; destruct1,3,6: >(H f1) >(K f2)148 [1,5,9:%149 2,4,10,12: inversion(f2) [2,6,10,14:#n #Hf2 >Hf2 in T;150 inversion(expr_eq e f1) #Heqef1 normalize >Heqef1 normalize #ABS destruct(ABS)151 3,4,7,8,11,12,15,16:#f1 #f2 #_ #H1 #H2152 >H2 in T; normalize >ifthenelse_aux * %153 1,5,9,13:#v #H2 >H2 in T; normalize #Hite >(ifthenelse_mm (expr_eq e f1) (neqb v2 v))154 [1,3,5,7:%2,4,6,8:assumption]]155 3:lapply(expr_eq_plus e (Var v2) f1 f2)6,7,8:lapply(expr_eq_plus e (Const v2) f1 f2)156 11:lapply(expr_eq_minus e (Var v2) f1 f2)]* try(#H1 #H2) assumption]]157 6:#n #H #K #f cases f [1,2:#k3,4:#f1 #f2] #T normalize in T; destruct(T)158 >(K f2) [>(H f1) [%inversion (expr_eq e f1) #II try(%) >II in T; #ABS normalize in ABS; destruct]159 inversion(f2) [#v #IHf >IHf in T; normalize >ifthenelse_aux * %160 #v #IHf >IHf in T; normalize inversion(neqb n v) #IHnenv #T try (%) >ifthenelse_aux in T; * %161 3,4: #g1 #g2 #Hg1 #Hg2 #Hf2 >Hf2 in T; normalize >ifthenelse_aux * %]]162 3,4,7,8:#f1 #f2 #H #K * [1,2,5,6,9,10:#n #T normalize in T; destruct163 3,4,7,8,9,11,12,15,16: #g1 #g213,14:#n] #T normalize in T; destruct164 >(H g1) [1,3,5: >(K g2) [1,3,5:%2,4,6: /2 by sym_eq, ifthenelse_mm/]165 2,4,6,8: /2 by ifthenelse_mm2/7:>(K g2) [%/2 by ifthenelse_mm/ qed.166 167 lemma expr_eq_equality_two:∀e1,e2.e1=e2→ expr_eq e1 e2=true.168 #e1 #e2 * elim e1 [1,2:#n normalize >neqb_refl %3,4:#f1 #f2 normalize169 #H1 >H1 #H2 >H2 normalize %]qed.170 171 lemma expr_eq_equality:∀e1,e2.expr_eq e1 e2=true ↔ e1=e2.172 #e1 #e2 % [@expr_eq_equality_one@expr_eq_equality_two] qed.173 174 107 (* 175 lemma expr_eq_equality_two':∀e1,e2.e1≠e2→ expr_eq e1 e2=false.176 #e1 #e2 * lapply e2 e2 #e2 elim e1 [1,2:#n normalize /3 by _/3,4:#f1 #f2 normalize177 #H1 >H1 #H2 >H2 normalize %]qed.178 *)179 lemma expr_eq_refl:∀e.expr_eq e e=true.180 #e >expr_eq_equality_two % qed.181 182 108 lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1. 183 #e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' normalize >neqb_sym % 109 #e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' try % 110 change with (n==n' = (n'==n)) inversion (n==n') #H 111 [ lapply(\P H) //  184 112 #f1 #f2 normalize %4,5,7,8:#f1 try(#f2) normalize % 185 113 #n normalize //] 186 114 3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %3,8:#g1 #g2 >(H1 g1) >(H2 g2) % 187 4,7:#_ #_ %] qed. 188 189 (* 190 191 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2. 192 #e1 elim e1 193 [ #v1 * 194 [ #v2 normalize % #H cases (neqb_true_to_eq v1 v2) #H1 #H2 195 >H1 // destruct /2/ 196  #c normalize % #H destruct 197 *: cases daemon ] 198  199  #e1 #e2 #IH1 #IH2 * 200 [3: #f1 #f2 normalize % 201 [ inversion (expr_eq e1 f1) normalize #H1 #H2 [2: destruct ] 202 cases (IH1 f1) cases (IH2 f2) /4 by eq_f2, sym_eq/ 203  #H destruct cases (IH1 f1) cases (IH2 f2) #H1 #H2 #H3 #H4 204 >H4/2 by / 205 *) 206 207 lemma condition_eq_sym:∀c:condition.cond_i_eq c c=true. 208 #c elim c [#e #f normalize >expr_eq_aux >expr_eq_aux normalize % 115 4,7:#_ #_ %] qed. *) 116 117 lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true. 118 #c elim c [#e #f whd in ⊢ (??%?); >expr_eq_refl >expr_eq_refl normalize % 209 119 #c' normalize * %] qed. 210 120 211 121 lemma cond_i_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2. 212 #c1 #c2 % [2: * @condition_eq_sym 213  lapply c2 c2 elim c1 normalize 214 [ #e1 #e2 * normalize 215 [ #f1 #f2 inversion(expr_eq f1 e1) normalize cases f1 cases e1 [1,2,5,6,17,18,21,22:#n1 #n2 normalize 216 #H destruct [1,2:>(neqb_true_to_eq n2 n1 H) cases f2 cases e2 217 [1,2,5,6,17,18,21,22:#k1 #k2 >neqb_refl normalize #K destruct >(neqb_true_to_eq k1 k2 K) % 218 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 219 #ABS destruct5,6,7,8,13,14,15,16:#h1 #h2 normalize [2,3:#ABS destruct 220 1,4,5,6,7,8: inversion(expr_eq h1 g1) #INV1 >INV1 normalize #INV2 destruct 221 c1 try(c2) e1 e2 f1 f2 H >INV1 in INV2; >neqb_refl >INV1 normalize 222 #INV2 >expr_eq_sym in INV1; #INV1 >INV1 in INV2; normalize #INV2 >expr_eq_sym in INV1; 223 #INV1 destruct >(expr_eq_equality_one g2 h2 INV2) >expr_eq_sym in INV1; #INV1 224 >(expr_eq_equality_one g1 h1 INV1) %] >neqb_refl in ABS; normalize #ABS destruct] 225 >neqb_refl in ABS; normalize #ABS destruct 226 9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS >neqb_refl in ABS; normalize #ABS destruct] 227 3,4,5,6:#ABS destruct >neqb_sym in H; #H >H in ABS; normalize #ABS destruct] 228 9,10,13,14,25,26,29,30:#n #h1 #h2 normalize #ABS1 #ABS2 destruct 229 11,12,15,16,27,28,31,32:#g1 #g2 #h1 #h2 normalize inversion(expr_eq h1 g1) 230 #INV1 >INV1 normalize #INV2 #E destruct >INV1 in E; normalize #E >expr_eq_sym in INV1; #INV1; >INV1 in E; 231 normalize #E destruct >expr_eq_sym in INV1; #INV1 >(expr_eq_equality_one h1 g1 INV1) 232 >expr_eq_sym in INV2; #INV2 >INV2 in E; normalize #E destruct >expr_eq_sym in INV2; #INV2 233 >(expr_eq_equality_one h2 g2 INV2) >expr_eq_sym in E; #E >(expr_eq_equality_one f2 e2 E) % 234 ]#f1 #f2 #n normalize #ABS1 #ABS2 destruct 235 #c2 #ABS destruct]#c2 #H #c' cases c' [#e1 #e2 normalize #ABS destruct#c3 normalize #K 236 >(H c3 K) % qed. 237 238 239 (* 240 inductive cond_i:Type[0]≝cIfThenElse: cond_i. 241 definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true. 242 lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2 243 cases c1 cases c2 % #_ % qed. 244 *) 122 #c1 #c2 % [2: * // ] 123 lapply c2 c2 elim c1 [ #e1 #e2 * 124 [ #f1 #f2 whd in ⊢ (??%? → ?); 125 inversion(expr_eq e1 f1) [2: #_ normalize #EQ destruct ] #H1 126 >(proj1 … (expr_eq_equality …) … H1) 127 inversion(expr_eq e2 f2) [2: #_ normalize #EQ destruct ] #H2 #_ 128 >(proj1 … (expr_eq_equality …) … H2) % 129  normalize #c #H destruct 130 ] #c2 #IH * 131 [ normalize #e1 #e2 #H destruct 132  #c3 #H >(IH … H) % ]] 133 qed. 245 134 246 135 inductive loop_i:Type[0]≝lWhile: loop_i. … … 248 137 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2 249 138 cases l1 cases l2 % #_ % qed. 139 140 definition io_i ≝ False. 141 142 definition io_i_eq ≝ λi1,i2:False. true. 143 144 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed. 250 145 251 146 (* … … 336 231 337 232 definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?. 338 normalize #s inversion(s) #INV #env [@(Some ? n)@(Some ? n)@(Some ? (S n))]qed.233 normalize * [ 2: #v #e 3: #v ] #env [@(Some ? env)@(Some ? n)@(Some ? (S n))]qed. 339 234 340 235 definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
Note: See TracChangeset
for help on using the changeset viewer.