Skip to content

Commit b16af89

Browse files
author
Thomas Dinsdale-Young
committed
More CAP stuff
1 parent 0922fae commit b16af89

File tree

3 files changed

+247
-91
lines changed

3 files changed

+247
-91
lines changed

‎CAPModel.v

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Require Import CountableFiniteMaps.
1010
Require Import SeparationAlgebras.
1111
Require Import Setof.
1212
Require Import HeapSeparationAlgebra.
13+
Require Import SeparationAlgebraProduct.
1314

1415
Module CAPModel (ht : HeapTypes) .
1516
Module Export TheHeap := MHeaps ht.
@@ -42,20 +43,19 @@ Module CAPModel (ht : HeapTypes) .
4243

4344
Definition Cap := CapSA.S.
4445

45-
Record LState := {
46-
ls_hp : store;
47-
ls_cap : Cap
48-
}.
46+
Definition LState := (store * Cap)%type.
4947

50-
Definition ls_sepop : partial_op LState :=
51-
fun ls ls' =>
52-
let (lsh, lsc) := ls in
53-
let (lsh', lsc') := ls' in
54-
let (hd, hv) := HSA.sepop lsh lsh' in
55-
let (cd, cv) := CapSA.sepop lsc lsc' in
56-
{| defined := hd /\ cd; val := {| ls_hp := hv; ls_cap := cv |} |}.
48+
Existing Instance prod_setoid.
49+
Existing Instance prod_SA.
50+
Definition ls_sepop := prod_sepop _ HSA.sepop _ CapSA.sepop.
51+
Instance ls_SA : SepAlg ls_sepop := prod_SA _ _ _ _.
5752

5853
Definition SState := CFMap RID LState.
54+
55+
Definition lcol (l : LState) (s : SState) : partial_val (T:=LState) :=
56+
cfm_dom_fold s (fun (o : partial_val (T:=LState))
57+
(a :
58+
5959
Definition Act := SState -> LState -> Prop.
6060
Definition AMod := Token -> option Act.
6161

‎CountableFiniteMaps.v

Lines changed: 112 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -1,80 +1,112 @@
1-
2-
Require Import SetoidClass.
3-
4-
Section Countable.
5-
6-
Context (A : Type) {A_Setoid : Setoid A}.
7-
Class Countable := {
8-
cnt_count :> A -> nat;
9-
cnt_choose :> nat -> A;
10-
cnt_inverse1 : forall a, a == cnt_choose (cnt_count a);
11-
cnt_inverse2 : forall n, n = cnt_count (cnt_choose n)
12-
}.
13-
Coercion cnt_count : Countable >-> Funclass.
14-
End Countable.
15-
16-
17-
(*
18-
Program Instance nat_setoid : Setoid nat.
19-
20-
Program Instance nat_count : Countable nat.
21-
*)
22-
Section NatFMap.
23-
Set Implicit Arguments.
24-
Context (Codom : Type).
25-
Record NatFMap := {
26-
nfm :> nat -> option Codom;
27-
nfm_bound : nat;
28-
nfm_bounded : forall a, a > nfm_bound -> nfm a = None
29-
}.
30-
31-
Require Import Max.
32-
33-
34-
Program Definition nfm_set (n : nat) (v : Codom) (m : NatFMap) : NatFMap :=
35-
{| nfm x := if Peano_dec.eq_nat_dec x n then Some v else nfm m x;
36-
nfm_bound := max n (nfm_bound m) |}.
37-
Obligation 1.
38-
remember (Peano_dec.eq_nat_dec a n) as s.
39-
destruct s; subst.
40-
contradict H.
41-
generalize (le_max_l n (nfm_bound m)); intro.
42-
auto with *.
43-
44-
apply nfm_bounded.
45-
generalize (le_max_r n (nfm_bound m)); intro.
46-
unfold gt in *.
47-
unfold lt in *.
48-
generalize (Le.le_n_S _ _ H0); intro.
49-
rewrite H1.
50-
trivial.
51-
Qed.
52-
Definition nfm_fresh (m : NatFMap) := S (nfm_bound m).
53-
Hint Resolve nfm_bounded.
54-
Lemma nfm_fresh_is_fresh (m : NatFMap) : nfm m (nfm_fresh m) = None.
55-
auto.
56-
Qed.
57-
Unset Implicit Arguments.
58-
End NatFMap.
59-
60-
61-
Definition CFMap A `{Countable A} codom := NatFMap codom.
62-
63-
Section CountableFiniteMaps.
64-
65-
Context (A : Type) {A_Setoid : Setoid A} {A_Countable : Countable A}.
66-
Variable R : Type.
67-
Set Implicit Arguments.
68-
Definition cfm : CFMap A R -> A -> option R :=
69-
fun m a => m (A_Countable a).
70-
Definition cfm_set (a : A) (v : R) (m : CFMap A R) : CFMap A R :=
71-
nfm_set (A_Countable a) v m.
72-
Definition cfm_fresh (m : CFMap A R) : A :=
73-
(cnt_choose _ (nfm_fresh m)).
74-
Lemma cfm_fresh_is_fresh (m : CFMap A R) : cfm m (cfm_fresh m) = None.
75-
cbv [cfm_fresh cfm].
76-
rewrite <- cnt_inverse2.
77-
apply nfm_fresh_is_fresh.
78-
Qed.
79-
80-
End CountableFiniteMaps.
1+
2+
Require Import SetoidClass.
3+
4+
Section Countable.
5+
6+
Context (A : Type) {A_Setoid : Setoid A}.
7+
Class Countable := {
8+
cnt_count :> A -> nat;
9+
cnt_choose :> nat -> A;
10+
cnt_inverse1 : forall a, a == cnt_choose (cnt_count a);
11+
cnt_inverse2 : forall n, n = cnt_count (cnt_choose n)
12+
}.
13+
Coercion cnt_count : Countable >-> Funclass.
14+
End Countable.
15+
16+
17+
(*
18+
Program Instance nat_setoid : Setoid nat.
19+
20+
Program Instance nat_count : Countable nat.
21+
*)
22+
Section NatFMap.
23+
Set Implicit Arguments.
24+
Context (Codom : Type).
25+
Record NatFMap := {
26+
nfm :> nat -> option Codom;
27+
nfm_bound : nat;
28+
nfm_bounded : forall a, a > nfm_bound -> nfm a = None
29+
}.
30+
31+
Require Import Max.
32+
33+
34+
Program Definition nfm_set (n : nat) (v : Codom) (m : NatFMap) : NatFMap :=
35+
{| nfm x := if Peano_dec.eq_nat_dec x n then Some v else nfm m x;
36+
nfm_bound := max n (nfm_bound m) |}.
37+
Obligation 1.
38+
remember (Peano_dec.eq_nat_dec a n) as s.
39+
destruct s; subst.
40+
contradict H.
41+
generalize (le_max_l n (nfm_bound m)); intro.
42+
auto with *.
43+
44+
apply nfm_bounded.
45+
generalize (le_max_r n (nfm_bound m)); intro.
46+
unfold gt in *.
47+
unfold lt in *.
48+
generalize (Le.le_n_S _ _ H0); intro.
49+
rewrite H1.
50+
trivial.
51+
Qed.
52+
Definition nfm_fresh (m : NatFMap) := S (nfm_bound m).
53+
Hint Resolve nfm_bounded.
54+
Lemma nfm_fresh_is_fresh (m : NatFMap) : nfm m (nfm_fresh m) = None.
55+
auto.
56+
Qed.
57+
Unset Implicit Arguments.
58+
End NatFMap.
59+
60+
61+
Definition CFMap A `{Countable A} codom := NatFMap codom.
62+
63+
Section CountableFiniteMaps.
64+
65+
Context (A : Type) {A_Setoid : Setoid A} {A_Countable : Countable A}.
66+
Variable R : Type.
67+
Set Implicit Arguments.
68+
Definition cfm : CFMap A R -> A -> option R :=
69+
fun m a => m (A_Countable a).
70+
Definition cfm_set (a : A) (v : R) (m : CFMap A R) : CFMap A R :=
71+
nfm_set (A_Countable a) v m.
72+
Definition cfm_fresh (m : CFMap A R) : A :=
73+
(cnt_choose _ (nfm_fresh m)).
74+
Lemma cfm_fresh_is_fresh (m : CFMap A R) : cfm m (cfm_fresh m) = None.
75+
cbv [cfm_fresh cfm].
76+
rewrite <- cnt_inverse2.
77+
apply nfm_fresh_is_fresh.
78+
Qed.
79+
Inductive cfm_def_at (m : CFMap A R) : A -> Prop :=
80+
| cfm_def_witness : forall a v, Some v = cfm m a -> cfm_def_at m a.
81+
Definition cfm_make_def_at (m : CFMap A R) (a : A) : option (cfm_def_at m a) :=
82+
match (cfm m a) as o return (o = cfm m a -> option (cfm_def_at m a)) with
83+
| Some r => fun H : Some r = cfm m a => Some (cfm_def_witness m a H)
84+
| None => fun _ => None
85+
end eq_refl.
86+
Fixpoint cfm_dom_fold_to
87+
(m : CFMap A R) (T : Type) (f : T -> forall a, cfm_def_at m a -> T) (o : T) (n : nat) : T :=
88+
match n with
89+
| O => o
90+
| S n' => let t' := (cfm_dom_fold_to f o n') in
91+
match (cfm_make_def_at m (cnt_choose A n)) with
92+
| Some da => f t' (cnt_choose A n) da
93+
| _ => t' end
94+
end.
95+
96+
Definition cfm_dom_fold (m : CFMap A R) (T : Type)
97+
(f : T -> forall a, cfm_def_at m a -> T) (o : T) : T :=
98+
cfm_dom_fold_to f o (nfm_bound m).
99+
Definition cfm_def_get (m : CFMap A R) (a : A) (P : cfm_def_at m a) : R.
100+
remember (cfm m a).
101+
destruct (o).
102+
exact r.
103+
contradict P.
104+
intro.
105+
destruct H.
106+
rewrite <- Heqo in H.
107+
inversion H.
108+
Defined.
109+
110+
End CountableFiniteMaps.
111+
112+

‎SeparationAlgebraProduct.v

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
Add LoadPath "C:\td202\GitHub\coq\views".
2+
3+
4+
Require Import SeparationAlgebras.
5+
Require Import SetoidClass.
6+
Require Import Tactics.
7+
Require Import Setof.
8+
9+
Instance defined_morphism {A} `{Setoid A} :
10+
Proper (equiv ==> equiv) defined.
11+
destruct x; destruct y.
12+
firstorder.
13+
Qed.
14+
15+
16+
Section SeparationAlgebraProduct.
17+
Context A
18+
{A_setoid : Setoid A}
19+
(aop :partial_op A)
20+
{A_SA : SepAlg aop}.
21+
Context B
22+
{B_setoid : Setoid B}
23+
(bop :partial_op B)
24+
{B_SA : SepAlg bop}.
25+
26+
Program Instance prod_setoid : Setoid (A*B) :=
27+
{| equiv := fun c c' =>
28+
let (a, b) := c in
29+
let (a', b') := c' in
30+
a == a' /\ b == b' |}.
31+
Obligation 1.
32+
split; cbv.
33+
destruct x; firstorder.
34+
destruct x; destruct y; firstorder.
35+
destruct x; destruct y; destruct z.
36+
firstorder; rewr auto.
37+
Qed.
38+
39+
Program Definition prod_SA_unit : @Setof (A*B) _ :=
40+
{| elem := (fun c =>
41+
let (a,b) := c in sa_unit a /\ sa_unit b) |}.
42+
Obligation 1.
43+
destruct x; destruct y.
44+
firstorder; rewr trivial.
45+
Qed.
46+
47+
Definition prod_sepop : partial_op (A*B) :=
48+
fun c c' =>
49+
let (a, b) := c in
50+
let (a', b') := c' in
51+
let a'' := aop a a' in let b'' := bop b b' in
52+
{|
53+
defined := defined a'' /\ defined b'';
54+
val := (val a'', val b'')
55+
|}.
56+
57+
Instance prod_sepop_morphism : Proper
58+
(equiv ==> equiv ==> equiv) prod_sepop.
59+
repeat intro.
60+
unfold prod_sepop.
61+
repeat match goal with
62+
| c : prod A B |- _ => destruct c
63+
| P : (_,_) == (_,_) |- _ => destruct P
64+
end.
65+
destruct (sa_morph _ _ H _ _ H0).
66+
destruct (sa_morph _ _ H2 _ _ H1).
67+
split; simpl; intuition; try rewr auto.
68+
Qed.
69+
70+
Lemma prod_sepop_comm : forall c c',
71+
prod_sepop c c' == prod_sepop c' c.
72+
intuition.
73+
generalize (sa_comm a a0).
74+
generalize (sa_comm b b0).
75+
split; simpl.
76+
rewr auto.
77+
destruct H.
78+
destruct H0.
79+
intuition.
80+
Qed.
81+
82+
Lemma prod_sepop_assoc : forall c c' c'',
83+
lift_op prod_sepop (prod_sepop c c') (lift_val c'')
84+
== lift_op prod_sepop (lift_val c) (prod_sepop c' c'').
85+
intuition.
86+
generalize (sa_assoc a a0 a1).
87+
generalize (sa_assoc b b0 b1).
88+
intros H H0; split;
89+
destruct H; destruct H0;
90+
unfold lift_op in *; simpl in *;
91+
intuition.
92+
Qed.
93+
94+
Lemma prod_sepop_unit_exists : forall c, exists i,
95+
elem prod_SA_unit i /\ prod_sepop i c == lift_val c.
96+
intuition.
97+
destruct (sa_unit_exists a).
98+
destruct (sa_unit_exists b).
99+
exists (x,x0).
100+
simpl; firstorder.
101+
Qed.
102+
103+
Lemma prod_sepop_unit_min : forall c c' i,
104+
elem prod_SA_unit i ->
105+
(prod_sepop i c) == lift_val c' ->
106+
c == c'.
107+
intuition.
108+
destruct i as [ia ib].
109+
generalize (sa_unit_min b b0 ib).
110+
generalize (sa_unit_min a a0 ia).
111+
intros.
112+
simpl in *; unfold prod_prop_equiv in *; simpl in *.
113+
intuition.
114+
Qed.
115+
116+
Instance prod_SA : SepAlg prod_sepop :=
117+
{| sa_morph := prod_sepop_morphism;
118+
sa_comm := prod_sepop_comm;
119+
sa_assoc := prod_sepop_assoc;
120+
sa_unit := prod_SA_unit;
121+
sa_unit_exists := prod_sepop_unit_exists;
122+
sa_unit_min := prod_sepop_unit_min
123+
|}.
124+
End SeparationAlgebraProduct.

0 commit comments

Comments
 (0)