Changeset 3529

Timestamp:

Mar 12, 2015, 3:38:10 PM (5 years ago)

Author:

pellitta

Message:

abitazione tipo instr_params in corso

File:

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

LTS/imp.ma

@@ -15 +15 @@
 include "basics/lists/list.ma".
 include "arithmetics/nat.ma".
+include "basics/bool.ma".
+include "Language.ma".
 
 (* Syntax *)
@@ -30 +32 @@
    Eq: expr → expr → condition
  | Not: condition → condition.
+ 
+inductive seq_i:Type[0]≝sNop: seq_i|sAss: seq_i|sInc: 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]
+|sAss ⇒ match s2 with [sAss ⇒ true| _⇒ false]
+|sInc ⇒ match s2 with [sInc ⇒ true| _⇒ false]
+].
+lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2
+cases s1 cases s2 normalize % #H destruct % qed.
+
+inductive io_i:Type[0]≝.
+definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true.
+lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2
+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.
+
+definition cond_i:Type[0]≝condition.
+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]
+].
+let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
+match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ 
+(andb (expr_eq e1 f1) (expr_eq e2 f2))|_⇒ false]
+|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
+
+lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2.
+#e1 #e2 elim e1 elim e2 normalize [#v #v' % #H elim v elim v' normalize in H; 
+[%|#v2 #H' destruct
+lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2.
+#c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H;
+(*
+inductive cond_i:Type[0]≝cIfThenElse: cond_i.
+definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true.
+lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2
+cases c1 cases c2 % #_ % qed.
+*)
+
+(*
+inductive loop_i:Type[0]≝lWhile: loop_i.
+definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true.
+lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
+cases l1 cases l2 % #_ % 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 nat neqb neqb_true_to_eq)
+|@(mk_DeqSet nat neqb neqb_true_to_eq)].qed.
 
 (* | IfThenElse: condition → command → command → command*)