Changeset 3536


Ignore:
Timestamp:
Mar 16, 2015, 5:02:57 PM (5 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:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/imp.ma

    r3534 r3536  
    1818include "Language.ma".
    1919
     20(* Tools *)
     21
     22lemma ifthenelse_elim:∀b,T.∀t:T.if b then t else t=t.
     23#b #T #t cases b % qed.
     24
     25lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
     26#b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
     27
     28lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
     29#b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
     30
     31lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
     32#b #b' cases b normalize #H destruct % qed.
     33
     34lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
     35#b #b' cases b normalize #H destruct % qed.
     36
     37let rec neqb n m ≝
     38match n with
     39  [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
     40  | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q]
     41  ].
     42 
     43axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true ↔ n = m.
     44
     45definition DeqNat:DeqSet≝mk_DeqSet nat neqb neqb_true_to_eq.
     46
     47lemma neqb_refl:∀n.neqb n n=true.
     48#n elim n [%|#n' normalize * %]qed.
     49
     50lemma neqb_sym:∀n1,n2.neqb n1 n2=neqb n2 n1.
     51#n1 elim n1 [#n2 cases n2 [%|#n' normalize %]|#n2' #IH #n2 cases n2 normalize [2: #m >IH]
     52% qed.
     53
    2054(* Syntax *)
    2155
    22 definition variable ≝ nat.
    23 axiom label:Type[0].
     56definition variable ≝ DeqNat.
    2457
    2558inductive expr: Type[0] ≝
    2659   Var: variable → expr
    27  | Const: nat → expr
     60 | Const: DeqNat → expr
    2861 | Plus: expr → expr → expr
    2962 | Minus: expr → expr → expr.
     
    3265   Eq: expr → expr → condition
    3366 | Not: condition → condition.
    34  
    35 inductive seq_i:Type[0]≝sNop: seq_i|sAss: seq_i|sInc: seq_i.
     67
     68let rec expr_eq (e1:expr) (e2:expr):bool≝
     69match e1 with [Var v1⇒ match e2 with [Var v2⇒ neqb v1 v2|_⇒ false]
     70|Const v1⇒ match e2 with [Const v2⇒ neqb v1 v2|_⇒ false]
     71|Plus le1 re1 ⇒ match e2 with [Plus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
     72|Minus le1 re1 ⇒ match e2 with [Minus le2 re2 ⇒ andb (expr_eq le1 le2) (expr_eq re1 re2)|_⇒ false]
     73].
     74
     75lemma expr_eq_refl:∀e:expr.expr_eq e e=true.
     76#e elim e [1,2: #v normalize lapply(neqb_true_to_eq v v) * #_ * %
     77|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
     78
     79lemma expr_eq_equality:∀e1,e2:expr.expr_eq e1 e2=true ↔ e1=e2.
     80#e1 #e2 % [2:* lapply e2 -e2 elim e1
     81  [1,2:#n #_ normalize >neqb_refl %
     82  |3,4:#f1 #f2 #H1 #H2 #e2 @expr_eq_refl]
     83|lapply e2 -e2 elim e1
     84  [1,2: #v1 #e2 cases e2 normalize
     85    [1,2,5,6: #v2 #H lapply(neqb_true_to_eq v1 v2) * #A destruct >(A H) #_ %
     86    |3,4,7,8: #e #f #ABS destruct]
     87  |3,4: #e #e2 #H #K #f cases f
     88    [1,2,5,6: #v2 normalize #ABS destruct
     89    |3,4,7,8:#f1 #f2 normalize inversion(expr_eq e f1) #INV1 >INV1 inversion(expr_eq e2 f2)
     90    #INV2 >INV2 normalize #T destruct >(H ? INV1) >(K ? INV2) % qed.
     91
     92inductive seq_i:Type[0]≝sNop: seq_i|sAss: variable → expr → seq_i|sInc: variable → seq_i.
    3693definition seq_i_eq:seq_i→ seq_i → bool≝λs1,s2:seq_i.match s1 with [
    3794 sNop ⇒ match s2 with [sNop ⇒ true| _⇒ false]
     
    47104cases i1 qed.
    48105
    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.
     106(*axiom neqb_true_to_eq: ∀n,m:nat. neqb n m = true → n = m.
     107axiom neqb_true_to_eq2: ∀n,m:nat. neqb n m = true ↔ n = m.*)
    55108lemma neqb_refl:∀n.neqb n n=true.
    56109#n elim n [%|#n' normalize * %]qed.
     
    75128|3,4: #f1 #f2 normalize #H1 >H1 #H2 >H2 %]qed.
    76129
    77 lemma ifthenelse_aux:∀b,T.∀t:T.if b then t else t=t.
    78 #b #T #t cases b % qed.
    79 
    80 lemma ifthenelse_left:∀b,T.∀t1,t2:T.if b then t1 else t2=t1→ (b=true ∨ t1=t2).
    81 #b #T #t1 #t2 cases b #H normalize in H; destruct [%1|%2] % qed.
    82 
    83 lemma ifthenelse_right:∀b,T.∀t1,t2:T.if b then t1 else t2=t2→ (b=false ∨ t1=t2).
    84 #b #T #t1 #t2 cases b #H normalize in H; destruct [%2|%1] % qed.
    85 
    86 lemma ifthenelse_mm:∀b,b':bool.if b then b' else false=true→ b'=true.
    87 #b #b' cases b normalize #H destruct % qed.
    88 
    89 lemma ifthenelse_mm2:∀b,b':bool.if b then b' else false=true→ b=true.
    90 #b #b' cases b normalize #H destruct % qed.
    91130
    92131lemma 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).
     
    227266|@(mk_DeqSet expr expr_eq expr_eq_equality)].qed.
    228267
     268
    229269(* | IfThenElse: condition → command → command → command*)
    230270(* | For: variable → expr → list command → command*)
     
    264304
    265305lemma assign_hit: ∀env,v,val. assign env v val v = val.
    266  #env #v #val normalize >eqb_n_n normalize %
     306 #env #v #val normalize >(eqb_n_n v) normalize %
    267307qed.
    268308
    269309lemma assign_miss: ∀env,v1,v2,val. v1 ≠ v2 → assign env v1 val v2 = env v2.
    270  #env #v1 #v2 #val #E normalize >not_eq_to_eqb_false /2/
     310 #env #v1 #v2 #val #E normalize >(not_eq_to_eqb_false v2 v1) /2 by refl, not_to_not/
    271311qed.
    272312
     
    282322   [ Eq e1 e2 ⇒ eqb (sem_expr env e1) (sem_expr env e2)
    283323   | Not c ⇒ notb (sem_condition env c) ].
     324
     325(*CERCO*)
     326
     327
     328
     329definition imp_env_params:env_params≝mk_env_params environment.
     330
     331axiom env_eq:environment→ environment → bool.
     332axiom env_eq_to_true:∀e1,e2.env_eq e1 e2=true ↔ e1 =e2.
     333definition DeqEnv:DeqSet≝mk_DeqSet environment env_eq env_eq_to_true.
     334
     335definition imp_state_params:state_params≝mk_state_params imp_instr_params imp_env_params DeqEnv.
     336
     337definition imp_eval_seq:(seq_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
     338normalize #s inversion(s) #INV #env [@(Some ? n)|@(Some ? n)|@(Some ? (S n))]qed.
     339
     340definition imp_eval_io:(io_instr imp_state_params)→(store_type imp_state_params)→ option (store_type imp_state_params)≝?.
     341// qed.
     342
     343definition imp_eval_cond_cond:(cond_instr imp_state_params)→ (store_type imp_state_params)→ option (bool × (store_type imp_state_params))≝?.
     344normalize #c cases c [(*case Eq e1 e2*) #e1 #e2 #n |(*case Not g*) #g]
     345
     346(*
     347let rec imp_eval_cond_cond (c: (cond_instr imp_state_params)) (s:(store_type imp_state_params)):option (bool × (store_type imp_state_params))≝
     348match c with
     349[Eq e1 e2⇒ ?
     350|Not c' ⇒ ?
     351].
     352*)
     353
     354definition imp_sem_state_params≝mk_sem_state_params imp_instr_.
     355
     356
     357
    284358
    285359(* Big step, declarative semantics of programs *)
Note: See TracChangeset for help on using the changeset viewer.