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