Changeset 3541
- Timestamp:
- Mar 18, 2015, 11:28:30 AM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/imp.ma
r3539 r3541 55 55 Eq: expr → expr → condition 56 56 | Not: condition → condition. 57 58 (* technical lemmas for expr_eq*) 57 59 58 60 let rec expr_eq (e1:expr) (e2:expr):bool≝ … … 66 68 #e elim e [1,2: #v change with (v==v = true); @(\b ?) % 67 69 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed. 70 71 (* the predicate expr_eq corresponds to syntactical equality on the type expr *) 68 72 69 73 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2. … … 81 85 #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed. 82 86 87 (* for the syntactical record in Language.ma *) 88 89 (* seq_i: type of sequential instructions *) 90 83 91 inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i. 92 84 93 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [ 85 94 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false] … … 87 96 |sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false] 88 97 ]. 98 99 (* technical lemma(s) for seq_i_eq *) 89 100 90 101 lemma seq_i_eq_refl:∀s.seq_i_eq s s=true. … … 104 115 qed. 105 116 117 (* cond_i: type of (guards of) conditional instructions, 118 i.e., possible conditions of IfThenElse *) 119 106 120 definition cond_i:Type[0]≝condition. 107 121 … … 111 125 |Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]]. 112 126 113 (* 114 lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1. 115 #e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' try % 116 change with (n==n' = (n'==n)) inversion (n==n') #H 117 [ lapply(\P H) // | 118 |#f1 #f2 normalize %|4,5,7,8:#f1 try(#f2) normalize % 119 |#n normalize //] 120 |3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %|3,8:#g1 #g2 >(H1 g1) >(H2 g2) % 121 |4,7:#_ #_ %] qed. *) 127 (* technical lemma(s) for cond_i *) 122 128 123 129 lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true. … … 139 145 qed. 140 146 147 (* cond_i: type of (guards of) loop instructions, 148 i.e., possible conditions of While *) 149 150 definition loop_i:Type[0]≝condition. 151 152 definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq. 153 154 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.@cond_i_eq_equality qed. 155 156 (* io_i: type of I/O instructions (none in the language considered) *) 157 158 definition io_i ≝ False. 159 160 definition io_i_eq ≝ λi1,i2:False. true. 161 162 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed. 163 164 (* syntactical record *) 165 166 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?. 167 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality) 168 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality) 169 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality) 170 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality) 171 |@(mk_DeqSet expr expr_eq expr_eq_equality) 172 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed. 173 141 174 (* | IfThenElse: condition → command → command → command*) 142 175 (* | For: variable → expr → list command → command*) … … 154 187 definition program ≝ list command. 155 188 156 (* NO, modificare: serve solo la guardia del while (senza la roba qui sopra),157 di fatto come per l'IfThenElse ho considerato solo Eq e Not *)158 inductive loop_i:Type[0]≝lWhile: condition → program → loop_i.159 definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.match l1 with160 [lWhile c1 p1 ⇒ match l2 with [lWhile c2 p2 ⇒ (andb (c1==c2) (p1==p2))]].161 162 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2163 cases l1 cases l2 % #_ % qed.164 165 definition io_i ≝ False.166 167 definition io_i_eq ≝ λi1,i2:False. true.168 169 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.170 171 (*172 let rec neqb n m ≝173 match n with174 [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]175 | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]176 ].177 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.178 *)179 180 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.181 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)182 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality)183 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)184 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)185 |@(mk_DeqSet expr expr_eq expr_eq_equality)186 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.187 188 189 190 189 (* Big step, operational semantics of expressions and conditions *) 191 190 … … 358 357 *) 359 358 360 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝λl,s.match l with 361 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]]. 359 definition imp_eval_loop_cond:(loop_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝imp_eval_cond_cond. 360 (*λl,s.match l with 361 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*) 362 362 363 363 definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
Note: See TracChangeset
for help on using the changeset viewer.