Changeset 3541


Ignore:
Timestamp:
Mar 18, 2015, 11:28:30 AM (5 years ago)
Author:
pellitta
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3539 r3541  
    5555   Eq: expr → expr → condition
    5656 | Not: condition → condition.
     57 
     58  (* technical lemmas for expr_eq*)
    5759
    5860let rec expr_eq (e1:expr) (e2:expr):bool≝
     
    6668#e elim e [1,2: #v change with (v==v = true); @(\b ?) %
    6769|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
     70
     71  (* the predicate expr_eq corresponds to syntactical equality on the type expr *)
    6872
    6973lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
     
    8185    #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.
    8286
     87(* for the syntactical record in Language.ma *)
     88
     89  (* seq_i: type of sequential instructions *)
     90
    8391inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i.
     92
    8493definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
    8594 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
     
    8796|sInc v ⇒ match s2 with [sInc v' ⇒ (v==v')| _⇒ false]
    8897].
     98
     99  (* technical lemma(s) for seq_i_eq *)
    89100
    90101lemma seq_i_eq_refl:∀s.seq_i_eq s s=true.
     
    104115qed.
    105116
     117  (* cond_i: type of (guards of) conditional instructions,
     118             i.e., possible conditions of IfThenElse *)
     119
    106120definition cond_i:Type[0]≝condition.
    107121
     
    111125|Not e⇒ match c2 with [Not f⇒ cond_i_eq e f|_⇒ false]].
    112126
    113 (*
    114 lemma expr_eq_sym:∀e1,e2.expr_eq e1 e2=expr_eq e2 e1.
    115 #e1 elim e1 [1,2:#n #e2 cases e2 [1,2:#n' try %
    116  change with (n==n' = (n'==n)) inversion (n==n') #H
    117  [ lapply(\P H) // |
    118 |#f1 #f2 normalize %|4,5,7,8:#f1 try(#f2) normalize %
    119 |#n normalize //]
    120 |3,4:#f1 #f2 #H1 #H2 #e2 cases e2 normalize [1,2,5,6:#_ %|3,8:#g1 #g2 >(H1 g1) >(H2 g2) %
    121 |4,7:#_ #_ %] qed. *)
     127  (* technical lemma(s) for cond_i *)
    122128
    123129lemma condition_eq_refl:∀c:condition.cond_i_eq c c=true.
     
    139145qed.
    140146
     147  (* cond_i: type of (guards of) loop instructions,
     148             i.e., possible conditions of While *)
     149
     150definition loop_i:Type[0]≝condition.
     151
     152definition loop_i_eq:loop_i → loop_i → bool ≝cond_i_eq.
     153
     154lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.@cond_i_eq_equality qed.
     155
     156  (* io_i: type of I/O instructions (none in the language considered) *)
     157
     158definition io_i ≝ False.
     159
     160definition io_i_eq ≝ λi1,i2:False. true.
     161
     162lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
     163
     164  (* syntactical record *)
     165
     166definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
     167[@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
     168|@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
     169|@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
     170|@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
     171|@(mk_DeqSet expr expr_eq expr_eq_equality)
     172|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
     173
    141174(* | IfThenElse: condition → command → command → command*)
    142175(* | For: variable → expr → list command → command*)
     
    154187definition program ≝ list command.
    155188
    156 (* NO, modificare: serve solo la guardia del while (senza la roba qui sopra),
    157 di fatto come per l'IfThenElse ho considerato solo Eq e Not *)
    158 inductive loop_i:Type[0]≝lWhile: condition → program → loop_i.
    159 definition loop_i_eq:loop_i → loop_i → bool ≝λl1,l2:loop_i.match l1 with
    160 [lWhile c1 p1 ⇒ match l2 with [lWhile c2 p2 ⇒ (andb (c1==c2) (p1==p2))]].
    161 
    162 lemma loop_i_eq_equality:∀l1,l2.loop_i_eq l1 l2=true ↔ l1=l2.#l1 #l2
    163 cases l1 cases l2 % #_ % qed.
    164 
    165 definition io_i ≝ False.
    166 
    167 definition io_i_eq ≝ λi1,i2:False. true.
    168 
    169 lemma io_i_eq_equality: ∀i1,i2. io_i_eq i1 i2 = true ↔ i1=i2. * qed.
    170 
    171 (*
    172 let rec neqb n m ≝
    173 match n with
    174   [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
    175   | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
    176   ].
    177 axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
    178 *)
    179 
    180 definition imp_instr_params: instr_params ≝ mk_instr_params ? ? ? ? ? ?.
    181 [@(mk_DeqSet seq_i seq_i_eq seq_i_eq_equality)
    182 |@(mk_DeqSet io_i io_i_eq io_i_eq_equality)
    183 |@(mk_DeqSet cond_i cond_i_eq cond_i_eq_equality)
    184 |@(mk_DeqSet loop_i loop_i_eq loop_i_eq_equality)
    185 |@(mk_DeqSet expr expr_eq expr_eq_equality)
    186 |@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
    187 
    188 
    189 
    190189(* Big step, operational semantics of expressions and conditions *)
    191190
     
    358357*)
    359358
    360 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
    361 [lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].
     359definition 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.
     360(*λl,s.match l with
     361[lWhile g l⇒ match (sem_condition g) with [None ⇒ None ?|Some b⇒ Some ? (mk_Prod b s)]].*)
    362362
    363363definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
Note: See TracChangeset for help on using the changeset viewer.