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 | *) |
---|