Changeset 3529
 Timestamp:
 Mar 12, 2015, 3:38:10 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/imp.ma
r3528 r3529 15 15 include "basics/lists/list.ma". 16 16 include "arithmetics/nat.ma". 17 include "basics/bool.ma". 18 include "Language.ma". 17 19 18 20 (* Syntax *) … … 30 32 Eq: expr → expr → condition 31 33  Not: condition → condition. 34 35 inductive seq_i:Type[0]≝sNop: seq_isAss: seq_isInc: seq_i. 36 definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [ 37 sNop ⇒ match s2 with [sNop ⇒ true _⇒ false] 38 sAss ⇒ match s2 with [sAss ⇒ true _⇒ false] 39 sInc ⇒ match s2 with [sInc ⇒ true _⇒ false] 40 ]. 41 lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2 42 cases s1 cases s2 normalize % #H destruct % qed. 43 44 inductive io_i:Type[0]≝. 45 definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true. 46 lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2 47 cases i1 qed. 48 49 let rec neqb n m ≝ 50 match n with 51 [ O ⇒ match m with [ O ⇒ true  S q ⇒ false] 52  S p ⇒ match m with [ O ⇒ false  S q ⇒ neqb p q] 53 ]. 54 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. 55 56 definition cond_i:Type[0]≝condition. 57 let rec expr_eq (e1:expr) (e2:expr):bool≝ 58 match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2_⇒ false] 59 Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2_⇒ false] 60 Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)_⇒ false] 61 Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)_⇒ false] 62 ]. 63 let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝ 64 match c1 with [Eq e1 e2⇒ match c2 with [Eq f1 f2 ⇒ 65 (andb (expr_eq e1 f1) (expr_eq e2 f2))_⇒ false] 66 Not e⇒ match c2 with [Not f⇒ cond_i_eq e f_⇒ false]]. 67 68 lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔e1=e2. 69 #e1 #e2 elim e1 elim e2 normalize [#v #v' % #H elim v elim v' normalize in H; 70 [%#v2 #H' destruct 71 lemma condition_eq_equality:∀c1,c2:condition.cond_i_eq c1 c2=true ↔ c1=c2. 72 #c1 #c2 elim c1 elim c2 [#H1 #H2 #H3 #H4 % #H normalize in H; 73 (* 74 inductive cond_i:Type[0]≝cIfThenElse: cond_i. 75 definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true. 76 lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2 77 cases c1 cases c2 % #_ % qed. 78 *) 79 80 (* 81 inductive loop_i:Type[0]≝lWhile: loop_i. 82 definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true. 83 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2 84 cases l1 cases l2 % #_ % qed. 85 *) 86 87 (* 88 let rec neqb n m ≝ 89 match n with 90 [ O ⇒ match m with [ O ⇒ true  S q ⇒ false] 91  S p ⇒ match m with [ O ⇒ false  S q ⇒ neqb p q] 92 ]. 93 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m. 94 *) 95 96 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?. 97 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality) 98 @(mk_DeqSet io_i io_i_eq io_i_eq_equality) 99 @(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality) 100 @(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality) 101 @(mk_DeqSet nat neqb neqb_true_to_eq) 102 @(mk_DeqSet nat neqb neqb_true_to_eq)].qed. 32 103 33 104 (*  IfThenElse: condition → command → command → command*)
Note: See TracChangeset
for help on using the changeset viewer.