-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathassertion.v
95 lines (74 loc) · 2.64 KB
/
assertion.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
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import language.
Require Import state.
Require Import util.
Require Import semantic.
Definition assertion := state -> Prop.
Definition emp : assertion :=
fun st: state => snd st = emp_heap.
Definition point_to (e1 e2: aexp): assertion :=
fun st: state =>
match st with
| (s,h) => h = h_update emp_heap (aeval s e1) (aeval s e2)
end.
Notation "e1 '|->' e2" := (point_to e1 e2) (at level 60).
Definition sep_conj (p q : assertion) : assertion :=
fun st: state =>
match st with
| (s, h) =>
exists h1, exists h2,
disjoint h1 h2 /\ h_union h1 h2 = h /\ p (s, h1) /\ q (s, h2)
end.
Notation "p '**' q" := (sep_conj p q) (at level 70).
Definition sep_disj (p q: assertion) : assertion :=
fun (st : state) =>
match st with
| (s, h) =>
forall h', disjoint h' h -> p (s, h') -> q (s, h_union h h')
end.
Notation "p '--*' q" := (sep_disj p q) (at level 80).
Definition s_conj (p q: assertion) : assertion :=
fun (s: state) => p s /\ q s.
Notation "p '//\\' q" := (s_conj p q) (at level 75).
Definition s_disj (p q: assertion) : assertion :=
fun (s: state) => p s \/ q s.
Notation "p '\\//' q" := (s_disj p q) (at level 78).
Definition s_imp (p q: assertion) : assertion :=
fun (s: state) => p s -> q s.
Notation "p '-->' q" := (s_imp p q) (at level 85).
Definition strongerThan (p q: assertion) : Prop :=
forall s: state, s_imp p q s.
Notation "p '==>' q" := (strongerThan p q) (at level 90).
Definition spEquiv (p q: assertion) : Prop :=
(p ==> q) /\ (q ==> p).
Notation "p '<==>' q" := (spEquiv p q) (at level 90).
(* theorems of assertion *)
Lemma disj_star_distr: forall (p q r: assertion),
(p \\// q) ** r <==> (p ** r) \\// (q ** r).
Proof.
intros.
unfold spEquiv. split.
-unfold strongerThan, s_imp. intros.
destruct s. destruct H. destruct H. destruct H. destruct H0.
destruct H1. unfold s_disj in *. destruct H1.
+left. unfold sep_conj. exists x. exists x0. auto.
+right. unfold sep_conj. exists x. exists x0. auto.
-unfold strongerThan, s_imp. intros.
destruct s. unfold s_disj in *. destruct H.
+simpl. repeat destruct H. destruct H0. destruct H1.
exists x. exists x0. auto.
+simpl. repeat destruct H. destruct H0. destruct H1.
exists x. exists x0. auto.
Qed.
Lemma conj2disj : forall p1 p2 p3,
p1 ** p2 ==> p3 ->
p1 ==> p2 --* p3.
Proof.
unfold strongerThan, s_imp. intros. destruct s.
unfold sep_disj. intros. unfold sep_conj in *.
apply H. exists h. exists h'. split.
-apply disjoint_comm. assumption.
-split. +reflexivity. +split; assumption.
Qed.