Changeset 3529


Ignore:
Timestamp:
Mar 12, 2015, 3:38:10 PM (5 years ago)
Author:
pellitta
Message:

abitazione tipo instr_params in corso

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3528 r3529  
    1515include "basics/lists/list.ma".
    1616include "arithmetics/nat.ma".
     17include "basics/bool.ma".
     18include "Language.ma".
    1719
    1820(* Syntax *)
     
    3032   Eq: expr → expr → condition
    3133 | Not: condition → condition.
     34 
     35inductive seq_i:Type[0]≝sNop: seq_i|sAss: seq_i|sInc: seq_i.
     36definition 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].
     41lemma seq_i_eq_equality:∀s1,s2.seq_i_eq s1 s2=true ↔ s1=s2.#s1 #s2
     42cases s1 cases s2 normalize % #H destruct % qed.
     43
     44inductive io_i:Type[0]≝.
     45definition io_i_eq:io_i→ io_i→ bool≝λi1,i2:io_i.true.
     46lemma io_i_eq_equality:∀i1,i2.io_i_eq i1 i2=true ↔ i1=i2.#i1 #i2
     47cases i1 qed.
     48
     49let rec neqb n m ≝
     50match 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  ].
     54axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
     55
     56definition cond_i:Type[0]≝condition.
     57let rec expr_eq (e1:expr) (e2:expr):bool≝
     58match 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].
     63let rec cond_i_eq (c1:cond_i) (c2:cond_i):bool ≝
     64match 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
     68lemma 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
     71lemma 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(*
     74inductive cond_i:Type[0]≝cIfThenElse: cond_i.
     75definition cond_i_eq:cond_i → cond_i → bool ≝λc1,c2:cond_i.true.
     76lemma cond_i_eq_equality:∀c1,c2.cond_i_eq c1 c2=true ↔ c1=c2.#c1 #c2
     77cases c1 cases c2 % #_ % qed.
     78*)
     79
     80(*
     81inductive loop_i:Type[0]≝lWhile: loop_i.
     82definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.true.
     83lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
     84cases l1 cases l2 % #_ % qed.
     85*)
     86
     87(*
     88let rec neqb n m ≝
     89match 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  ].
     93axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
     94*)
     95
     96definition 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.
    32103
    33104(* | IfThenElse: condition → command → command → command*)
Note: See TracChangeset for help on using the changeset viewer.