1 | include "Common.ma". |
---|
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 |
---|
19 | | Cio: label → label → cmd |
---|
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. |
---|
41 | cmd × continuation × ((list (nat × ident × ((option label) × continuation))) × S). |
---|
42 | |
---|
43 | definition fetchT ≝ fname → cmd. |
---|
44 | |
---|
45 | inductive step (S: storeT) (fetch: fetchT) : state S → state S → list label → Prop := |
---|
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)〉 |
---|
50 | [] |
---|
51 | | step_skip: ∀c,k,K,s. |
---|
52 | step … |
---|
53 | 〈Cskip, c::k, K, s〉 |
---|
54 | 〈c, k, K, s〉 |
---|
55 | [] |
---|
56 | | step_seq: ∀c,c',k,K,s. |
---|
57 | step … |
---|
58 | 〈Cseq c c', k, K, s〉 |
---|
59 | 〈 c, c'::k, K, s〉 |
---|
60 | [] |
---|
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〉 |
---|
65 | 〈 c1, k, K, s〉 |
---|
66 | [l1] |
---|
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〉 |
---|
71 | 〈 c2, k, K, s〉 |
---|
72 | [l2] |
---|
73 | | step_while_true: ∀b,l1,c,l2,k,K,s. eval_bool_expr ? s b = true → |
---|
74 | step … |
---|
75 | 〈Cwhile b l1 c l2, k, K,s〉 |
---|
76 | 〈 c, (Cwhile b l1 c l2)::k, K, s〉 |
---|
77 | [l1] |
---|
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〉 |
---|
81 | 〈 Cskip, k, K, s〉 |
---|
82 | [l2] |
---|
83 | | step_label: ∀l1,l2,k,K,s. |
---|
84 | step … |
---|
85 | 〈Cio l1 l2, k, K, s〉 |
---|
86 | 〈 Cskip, k, K, s〉 |
---|
87 | [l1;l2] |
---|
88 | | step_call: ∀x,f,e,l,c,k,K,s. fetch f = c → |
---|
89 | step … |
---|
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] |
---|
93 | | step_return: ∀e,k1,v,x,l,k2,K,s. |
---|
94 | step … |
---|
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]]). |
---|
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 | *) |
---|