[3375] | 1 | include "arithmetics/nat.ma". |
---|
| 2 | include "basics/types.ma". |
---|
| 3 | include "basics/lists/list.ma". |
---|
| 4 | |
---|
| 5 | (*************************) |
---|
| 6 | |
---|
| 7 | axiom ltb: nat → nat → bool. |
---|
| 8 | |
---|
| 9 | (*************************) |
---|
| 10 | |
---|
| 11 | record label: Type[0] ≝ {label_name: nat}. |
---|
| 12 | |
---|
| 13 | record ident: Type[0] ≝ {ident_name: nat}. |
---|
| 14 | |
---|
| 15 | record fname: Type[0] ≝ {function_name: nat}. |
---|
| 16 | |
---|
| 17 | definition label_of_fname: fname → label ≝ |
---|
| 18 | λf. mk_label (function_name f). |
---|
| 19 | |
---|
| 20 | coercion label_of_fname. |
---|
| 21 | |
---|
| 22 | record storeT: Type[1] ≝ |
---|
| 23 | { store:> Type[0] |
---|
| 24 | ; get: store → option ident → nat |
---|
| 25 | ; set: store → option ident → nat → store |
---|
| 26 | ; get_set_hit: ∀s,x,v. get (set s x v) x = v |
---|
| 27 | ; get_set_miss: ∀s,x,y,v. get (set s x v) y = get s y |
---|
| 28 | }. |
---|
| 29 | |
---|
| 30 | inductive expr : Type[0] := |
---|
| 31 | | Evar: option ident → expr |
---|
| 32 | | Econst: nat → expr |
---|
| 33 | | Eadd: expr → expr → expr |
---|
| 34 | | Esub: expr → expr → expr. |
---|
| 35 | |
---|
| 36 | inductive bool_expr : Type[0] := |
---|
| 37 | | Bequal: expr → expr → bool_expr |
---|
| 38 | | Bless: expr → expr → bool_expr. |
---|
| 39 | |
---|
| 40 | inductive cmd : Type[0] := |
---|
| 41 | | Cskip: cmd |
---|
| 42 | | Cassign: ident → expr → cmd |
---|
| 43 | | Cseq: cmd → cmd → cmd |
---|
| 44 | | Cifthenelse: bool_expr → label → cmd → label → cmd → cmd |
---|
| 45 | | Cwhile: bool_expr → label → cmd → label → cmd |
---|
| 46 | | Clabel: label → cmd → cmd |
---|
| 47 | | Ccall: ident → fname → expr → option label → cmd |
---|
| 48 | | Cret: expr → cmd. |
---|
| 49 | |
---|
| 50 | let rec eval_expr (S: storeT) (s: S) (e: expr) on e : nat := |
---|
| 51 | match e with |
---|
| 52 | [ Evar x ⇒ get S s x |
---|
| 53 | | Econst n ⇒ n |
---|
| 54 | | Eadd e1 e2 ⇒ eval_expr S s e1 + eval_expr S s e2 |
---|
| 55 | | Esub e1 e2 ⇒ eval_expr S s e1 - eval_expr S s e2 |
---|
| 56 | ]. |
---|
| 57 | |
---|
| 58 | definition eval_bool_expr: ∀S:storeT. ∀s:S. ∀b:bool_expr. bool ≝ |
---|
| 59 | λS,s,b. |
---|
| 60 | match b with |
---|
| 61 | [ Bequal e1 e2 => eqb (eval_expr S s e1) (eval_expr S s e2) |
---|
| 62 | | Bless e1 e2 => ltb (eval_expr S s e1) (eval_expr S s e2) |
---|
| 63 | ]. |
---|
| 64 | |
---|
| 65 | definition continuation: Type[0] ≝ list cmd. |
---|
| 66 | |
---|
| 67 | definition state: storeT → Type[0] ≝ λS. |
---|
| 68 | cmd × continuation × ((list (ident × (option label) × continuation)) × S). |
---|
| 69 | |
---|
| 70 | definition fetchT ≝ fname → cmd. |
---|
| 71 | |
---|
| 72 | inductive step (S: storeT) (fetch: fetchT) : state S → state S → option label → Prop := |
---|
| 73 | | step_assign: ∀x,e,k,K,s. |
---|
| 74 | step … |
---|
| 75 | 〈Cassign x e, k, K, s〉 |
---|
| 76 | 〈Cskip, k, K, set … s (Some … x) (eval_expr … s e)〉 |
---|
| 77 | (None …) |
---|
| 78 | | step_skip: ∀c,k,K,s. |
---|
| 79 | step … |
---|
| 80 | 〈Cskip, c::k, K, s〉 |
---|
| 81 | 〈c, k, K, s〉 |
---|
| 82 | (None …) |
---|
| 83 | | step_seq: ∀c,c',k,K,s. |
---|
| 84 | step … |
---|
| 85 | 〈Cseq c c', k, K, s〉 |
---|
| 86 | 〈c, c'::k, K, s〉 |
---|
| 87 | (None …) |
---|
| 88 | | step_if_true: |
---|
| 89 | ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = true → |
---|
| 90 | step … |
---|
| 91 | 〈Cifthenelse b l1 c1 l2 c2, k, K, s〉 |
---|
| 92 | 〈c1, k, K, s〉 |
---|
| 93 | (Some … l1) |
---|
| 94 | | step_if_false: |
---|
| 95 | ∀b,l1,c1,l2,c2,k,K,s. eval_bool_expr ? s b = false → |
---|
| 96 | step … |
---|
| 97 | 〈Cifthenelse b l1 c1 l2 c2, k, K, s〉 |
---|
| 98 | 〈c2, k, K, s〉 |
---|
| 99 | (Some … l2) |
---|
| 100 | | step_while_true: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = true → |
---|
| 101 | step … |
---|
| 102 | 〈Cwhile b l1 c l2, k, K,s〉 |
---|
| 103 | 〈c, (Cwhile b l1 c l2)::k, K, s〉 |
---|
| 104 | (Some … l1) |
---|
| 105 | | step_while_false: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = false → |
---|
| 106 | step … |
---|
| 107 | 〈Cwhile b l1 c l2, k, K, s〉 |
---|
| 108 | 〈Cskip, k, K, s〉 |
---|
| 109 | (Some … l2) |
---|
| 110 | | step_label: ∀c,l,k,K,s. |
---|
| 111 | step … |
---|
| 112 | 〈Clabel l c,k,K,s〉 |
---|
| 113 | 〈c,k,K,s〉 |
---|
| 114 | (Some … l) |
---|
| 115 | | step_call: ∀x,f,e,l,c,k,K,s. fetch f = c → |
---|
| 116 | step … |
---|
| 117 | 〈Ccall x f e l, k, K, s〉 |
---|
| 118 | 〈c, [], 〈x,l,k〉::K, set ? s (None …) (eval_expr ? s e)〉 |
---|
| 119 | (Some … f) |
---|
| 120 | | step_return: ∀e,k1,x,l,k2,K,s. |
---|
| 121 | step … |
---|
| 122 | 〈Cret e, k1, 〈x,l,k2〉::K, s〉 |
---|
| 123 | 〈Cskip, k2, K, set ? s (Some … x) (eval_expr ? s e)〉 |
---|
| 124 | l. |
---|
| 125 | |
---|
| 126 | (* |
---|
| 127 | definition steps: ∀S: storeT) : state S → state S → option label → Prop := star (trans_imp lbl). |
---|
| 128 | |
---|
| 129 | Definition term_imp_lbl (lbl: Type) (c: cmd lbl) (s s': store) (trace: list lbl): Prop := |
---|
| 130 | star_imp lbl (c, Chalt lbl, s) (Cskip lbl, Chalt lbl, s') trace. |
---|
| 131 | |
---|
| 132 | Lemma induction_on_code_imp: |
---|
| 133 | forall (P : code_imp -> Prop), |
---|
| 134 | P (Cskip False) -> |
---|
| 135 | (forall x e, P (Cassign False x e)) -> |
---|
| 136 | (forall S1 S2, P S1 -> P S2 -> P (Cseq False S1 S2)) -> |
---|
| 137 | (forall S1 S2 b, P S1 -> P S2 -> P (Cifthenelse False b S1 S2)) -> |
---|
| 138 | (forall S b, P S -> P (Cwhile False b S)) -> |
---|
| 139 | forall S : code_imp, P S. |
---|
| 140 | Proof. |
---|
| 141 | unfold code_imp; intros. |
---|
| 142 | induction S as [ | | | | | Hfalse ]; auto. |
---|
| 143 | destruct Hfalse. |
---|
| 144 | Qed. |
---|
| 145 | *) |
---|