Changeset 3536

Timestamp:

Mar 16, 2015, 5:02:57 PM (6 years ago)

Author:

pellitta

Message:

roll-back per avere tipo seq_i con parametri e store_type come environment decidibile (rifatta prova predicato uguaglianza su expr)

File:

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

LTS/imp.ma

@@ -18 +18 @@
 include "Language.ma".
 
+(* Tools *)
+
+lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.
+#b #T #t cases b % qed.
+
+lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
+#b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
+
+lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
+#b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
+
+lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
+#b #b' cases b normalize #H destruct % qed.
+
+lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
+#b #b' cases b normalize #H destruct % 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 DeqNat:DeqSet≝mk_DeqSet nat neqb neqb_true_to_eq.
+
+lemma neqb_refl:∀n.neqb n n=true.
+#n elim n [%|#n' normalize * %]qed.
+
+lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
+#n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
+% qed.
+
 (* Syntax *)
 
-definition variable ≝ nat.
-axiom label:Type[0].
+definition variable ≝ DeqNat.
 
 inductive expr: Type[0] ≝
    Var: variable → expr
- | Const: nat → expr
+ | Const: DeqNat → expr
  | Plus: expr → expr → expr
  | Minus: expr → expr → expr.
@@ -32 +65 @@
    Eq: expr → expr → condition
  | Not: condition → condition.
- 
-inductive seq_i:Type[0]≝sNop: seq_i|sAss: seq_i|sInc: seq_i.
+
+let rec expr_eq (e1:expr) (e2:expr):bool≝
+match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
+|Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
+|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
+|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
+].
+
+lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
+#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * #_ * %
+|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
+
+lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
+#e1 #e2 % [2:* lapply e2 -e2 elim e1
+  [1,2:#n #_ normalize >neqb_refl %
+  |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl]
+|lapply e2 -e2 elim e1
+  [1,2: #v1 #e2 cases e2 normalize
+    [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) * #A destruct >(A H) #_ %
+    |3,4,7,8: #e #f #ABS destruct]
+  |3,4: #e #e2 #H #K #f cases f 
+    [1,2,5,6: #v2 normalize #ABS destruct
+    |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2)
+    #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.
+
+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]
@@ -47 +104 @@
 cases i1 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.
+(*axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m.
+axiom neqb_true_to_eq2: ∀n,m:nat. neqb n m = true ↔ n = m.*)
 lemma neqb_refl:∀n.neqb n n=true.
 #n elim n [%|#n' normalize * %]qed.
@@ -75 +128 @@
 |3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
 
-lemma ifthenelse_aux:∀b,T.∀t:T.if b then t else t=t.
-#b #T #t cases b % qed.
-
-lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
-#b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
-
-lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
-#b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
-
-lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
-#b #b' cases b normalize #H destruct % qed.
-
-lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
-#b #b' cases b normalize #H destruct % qed.
 
 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).
@@ -227 +266 @@
 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
 
+
 (* | IfThenElse: condition → command → command → command*)
 (* | For: variable → expr → list command → command*)
@@ -264 +304 @@
 
 lemma assign_hit: ∀env,v,val. assign env v val v = val.
- #env #v #val normalize >eqb_n_n normalize %
+ #env #v #val normalize >(eqb_n_n v) normalize %
 qed.
 
 lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2.
- #env #v1 #v2 #val #E normalize >not_eq_to_eqb_false /2/
+ #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
 qed.
 
@@ -282 +322 @@
    [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2)
    | Not c ⇒ notb (sem_condition env c) ].
+
+(*CERCO*)
+
+
+
+definition imp_env_params:env_params≝mk_env_params environment.
+
+axiom env_eq:environment→ environment → bool.
+axiom env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2.
+definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true.
+
+definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
+
+definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
+normalize #s inversion(s) #INV #env [@(Some ? n)|@(Some ? n)|@(Some ? (S n))]qed.
+
+definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
+// qed.
+
+definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝?.
+normalize #c cases c [(*case Eq e1 e2*) #e1 #e2 #n |(*case Not g*) #g]
+
+(*
+let rec imp_eval_cond_cond (c: (cond_instr imp_state_params)) (s:(store_type imp_state_params)):option (bool × (store_type imp_state_params))≝
+match c with
+[Eq e1 e2⇒ ?
+|Not c' ⇒ ?
+].
+*)
+
+definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
+
+
+
 
 (* Big step, declarative semantics of programs *)