Changeset 3541

Timestamp:

Mar 18, 2015, 11:28:30 AM (6 years ago)

Author:

pellitta

Message:

 

File:

• LTS/imp.ma (modified) (9 diffs)

LTS/imp.ma

@@ -55 +55 @@
    Eq: expr → expr → condition
  | Not: condition → condition.
+ 
+  (* technical lemmas for expr_eq*)
 
 let rec expr_eq (e1:expr) (e2:expr):bool≝
@@ -66 +68 @@
 #e elim e [1,2: #v change with (v==v = true); @(\b ?) %
 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
+
+  (* the predicate expr_eq corresponds to syntactical equality on the type expr *)
 
 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.
 
+(* for the syntactical record in Language.ma *)
+
+  (* seq_i: type of sequential instructions *)
+
 inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i.
+
 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
  sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
@@ -87 +96 @@
 |sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false]
 ].
+
+  (* technical lemma(s) for seq_i_eq *)
 
 lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
@@ -104 +115 @@
 qed.
 
+  (* cond_i: type of (guards of) conditional instructions,
+             i.e., possible conditions of IfThenElse *)
+
 definition cond_i:Type[0]≝condition.
 
@@ -111 +125 @@
 |Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
 
-(*
-lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1.
-#e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' try % 
- change with (n==n' = (n'==n)) inversion (n==n') #H
- [ lapply(\P H) // | 
-|#f1 #f2 normalize %|4,5,7,8:#f1 try(#f2) normalize %
-|#n normalize //]
-|3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %|3,8:#g1 #g2 >(H1 g1) >(H2 g2) %
-|4,7:#_ #_ %] qed. *)
+  (* technical lemma(s) for cond_i *)
 
 lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true.
@@ -139 +145 @@
 qed.
 
+  (* cond_i: type of (guards of) loop instructions,
+             i.e., possible conditions of While *)
+
+definition loop_i:Type[0]≝condition.
+
+definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq.
+
+lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.@cond_i_eq_equality qed.
+
+  (* io_i: type of I/O instructions (none in the language considered) *)
+
+definition io_i ≝ False.
+
+definition io_i_eq ≝ λi1,i2:False. true.
+
+lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
+
+  (* syntactical record *)
+
+definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
+[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
+|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
+|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
+|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
+|@(mk_DeqSet expr expr_eq expr_eq_equality)
+|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
+
 (* | IfThenElse: condition → command → command → command*)
 (* | For: variable → expr → list command → command*)
@@ -154 +187 @@
 definition program ≝ list command.
 
-(* NO, modificare: serve solo la guardia del while (senza la roba qui sopra), 
-di fatto come per l'IfThenElse ho considerato solo Eq e Not *)
-inductive loop_i:Type[0]≝lWhile: condition → program → loop_i.
-definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.match l1 with
-[lWhile c1 p1 ⇒ match l2 with [lWhile c2 p2 ⇒ (andb (c1==c2) (p1==p2))]].
-
-lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
-cases l1 cases l2 % #_ % qed.
-
-definition io_i ≝ False.
-
-definition io_i_eq ≝ λi1,i2:False. true.
-
-lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
-
-(*
-let rec neqb n m ≝ 
-match n with 
-  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] 
-  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
-  ].
-axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
-*)
-
-definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
-[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
-|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
-|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
-|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
-|@(mk_DeqSet expr expr_eq expr_eq_equality)
-|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
-
-
-
 (* Big step, operational semantics of expressions and conditions *)
 
@@ -358 +357 @@
 *)
 
-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
-[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].
+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.
+(*λl,s.match l with
+[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)
 
 definition imp_sem_state_params≝mk_sem_state_params imp_instr_.