-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathstate.v
142 lines (102 loc) · 3.05 KB
/
state.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
Require Import util.
Require Import Coq.Arith.Arith.
Require Import Coq.Bool.Bool.
Require Import Coq.Strings.String.
Require Import Coq.Logic.FunctionalExtensionality.
Definition store := id -> nat.
Definition heap := nat -> option nat.
Axiom finite_heap : forall h: heap, exists n: nat,
forall n' v: nat, h n' = Some v -> n' < n.
Definition emp_heap : heap :=
fun (n: nat) => None.
Definition in_dom (l: nat) (h: heap) : Prop :=
exists n, h l = Some n.
Definition not_in_dom (l: nat) (h: heap) : Prop :=
h l = None.
Theorem in_not_in_dec :
forall l h, {in_dom l h} + {not_in_dom l h}.
Proof.
intros l h. unfold in_dom. unfold not_in_dom.
destruct (h l).
left. exists n. auto.
right. auto.
Qed.
Definition disjoint (h1 h2: heap) : Prop :=
forall l, not_in_dom l h1 \/ not_in_dom l h2.
Definition h_union (h1 h2: heap) : heap :=
fun l =>
if (in_not_in_dec l h1) then h1 l else h2 l.
(* h1 is a subset of h2 *)
Definition h_subset (h1 h2: heap) : Prop :=
forall l n, h1 l = Some n -> h2 l = Some n.
(* store update *)
Definition st_update (s: store) (x: id) (n: nat) : store :=
fun x' => if beq_id x x' then n else s x'.
(* heap update *)
Definition h_update (h: heap) (l: nat) (n: nat) : heap :=
fun l' => if beq_nat l l' then Some n else h l'.
Definition state : Type := (store * heap).
(* since program may abort, we extend our state
definition to add a special state Abt *)
Inductive ext_state : Type :=
| St: state -> ext_state (* normal state *)
| Abt: ext_state. (* abort *)
(* Lemma *)
Lemma h_update_equal : forall x h l n,
in_dom x h ->
h l = None ->
h x = (h_update h l n) x.
Proof.
intros.
unfold h_update, in_dom in *.
destruct (l =? x) eqn:Ha.
-apply beq_nat_true in Ha. subst. destruct H.
rewrite H in H0. inversion H0.
-reflexivity.
Qed.
Lemma disjoint_comm : forall h1 h2,
disjoint h1 h2 <-> disjoint h2 h1.
Proof.
intros. unfold disjoint. split.
-intros. destruct H with l.
+right. assumption.
+left. assumption.
-intros. destruct H with l.
+right. assumption.
+left. assumption.
Qed.
Lemma disjoint_elim_union_a : forall h1 h2 h3,
disjoint h1 (h_union h2 h3) ->
disjoint h1 h2.
Proof.
intros. unfold disjoint in *.
intros. destruct H with l.
-left. assumption.
-right. unfold h_union, not_in_dom in *.
destruct (in_not_in_dec l h2).
+assumption.
+unfold not_in_dom in *. assumption.
Qed.
Lemma disjoint_elim_union_b : forall h1 h2 h3,
disjoint h1 (h_union h2 h3) ->
disjoint h1 h3.
Proof.
intros. unfold disjoint in *.
intros. destruct H with l.
-left. assumption.
-right. unfold h_union, not_in_dom in *.
destruct (in_not_in_dec l h2).
+unfold in_dom in *. destruct i. rewrite H1 in H0.
inversion H0.
+assumption.
Qed.
Lemma h_union_emp_heap : forall h,
h_union emp_heap h = h.
Proof.
intros. unfold h_union.
apply functional_extensionality. intros.
destruct (in_not_in_dec x emp_heap).
-unfold in_dom in *. destruct i. unfold emp_heap in *.
inversion H.
-reflexivity.
Qed.