Set Implicit Arguments.
Require Import MyTactics.
Require Import Resources.
In this file, we investigate the definition of a resource that corresponds
directly to an ML store typing and that could be used in a direct proof of
type soundness for weak references.
This file represents an experiment and is not used as part of the main
development.
-------------------------------------------------------------------------
The discrete star is defined by the axiom forall a, star a a a. This
intuitively means that all information is duplicable, or, in other words,
that all threads share full knowledge of the information.
Definition discrete_star (
A :
Type) (
a1 a2 a :
A) :=
a1 =
a /\
a2 =
a.
-------------------------------------------------------------------------
We now construct a function discrete_add that is commutative, associative,
and coincides with discrete_star where the latter is defined. The idea is
that discrete_add a1 a2 should coincide with a1 and a2 if a1 and a2
are equal, and should otherwise be default -- a fixed default element. To
express this idea, we use the excluded middle and Hilbert's epsilon operator.
One could perhaps go even further and remove the requirement that A be
inhabited: indeed, if A is void, then it should be easy to define a
suitable discrete_add. But, in all practical applications, it is easy
to prove that A is inhabited, so this does not seem worth the trouble.
Require Import Epsilon.
Require Import Classical.
The following is a relational specification of the function discrete_add
that we would like to define.
Definition discrete_add_spec A (
default a1 a2 a :
A) :=
(
a1 =
a2 ->
discrete_star a1 a2 a) /\ (
a1 <>
a2 ->
a =
default).
The following lemmas spell out what this specification means.
Lemma discrete_add_spec_eq:
forall A (
default a b :
A),
discrete_add_spec default a a b ->
a =
b.
Proof.
unfold discrete_add_spec, discrete_star. tauto.
Qed.
Lemma discrete_add_spec_neq:
forall A (
default a1 a2 b :
A),
a1 <>
a2 ->
discrete_add_spec default a1 a2 b ->
default =
b.
Proof.
unfold discrete_add_spec, discrete_star. intuition auto.
Qed.
We now define discrete_add as the function that corresponds to the
above relational specification.
Definition discrete_add A (
default a1 a2 :
A) :=
@
epsilon A (
inhabits default) (
discrete_add_spec default a1 a2).
We check that this function does behave in the desired manner.
Adding a with a yields a.
Lemma discrete_add_eq:
forall A (
default a :
A),
a =
discrete_add default a a.
Proof.
unfold discrete_add.
intros.
eapply discrete_add_spec_eq with (
default :=
default).
eapply epsilon_spec.
exists a.
unfold discrete_add_spec,
discrete_star.
tauto.
Qed.
Adding a1 with a2 yields default if a1 and a2 are distinct.
Lemma discrete_add_neq:
forall A (
default a1 a2 :
A),
a1 <>
a2 ->
default =
discrete_add default a1 a2.
Proof.
unfold discrete_add.
intros.
eapply discrete_add_spec_neq with (
default :=
default).
eassumption.
eapply epsilon_spec.
exists default.
unfold discrete_add_spec,
discrete_star.
tauto.
Qed.
Adding default with anything yields default.
Lemma discrete_add_default:
forall A (
default a :
A),
default =
discrete_add default default a.
Proof.
Lemma discrete_add_default_symmetric:
forall A (
default a :
A),
default =
discrete_add default a default.
Proof.
The function discrete_add coincides with discrete_star where the latter
is defined.
Lemma discrete_add_matches_discrete_star:
forall A (
default :
A),
forall a1 a2 a,
discrete_star a1 a2 a ->
a =
discrete_add default a1 a2.
Proof.
unfold discrete_star.
intros.
unpack.
subst.
eauto using discrete_add_eq.
Qed.
This horrible tactic considers the cases a1 = a2 and a1 <> a2, and
in each case simplifies applications of discrete_add to a1 and a2.
Ltac discrete_add_by_cases a1 a2 :=
destruct (
classic (
a1 =
a2));
subst;
repeat rewrite <-
discrete_add_eq;
repeat match goal with h: ?
a1 <> ?
a2 |-
_ =>
first [
rewrite <- (@
discrete_add_neq _ _ a1 a2); [
idtac |
solve [
eauto ] ]
|
rewrite <- (@
discrete_add_neq _ _ a2 a1); [
idtac |
solve [
eauto ] ]
]
end.
discrete_add is commutative and associative.
Lemma discrete_add_commutative:
forall A (
default :
A),
forall a1 a2,
discrete_add default a1 a2 =
discrete_add default a2 a1.
Proof.
intros. discrete_add_by_cases a1 a2; eauto.
Qed.
Lemma discrete_add_associative:
forall A (
default :
A),
forall a1 a2 a3,
discrete_add default a1 (
discrete_add default a2 a3) =
discrete_add default (
discrete_add default a1 a2)
a3.
Proof.
-------------------------------------------------------------------------
Any type A forms a monotonic separation algebra, known as the discrete
monotonic separation algebra, where all information is duplicable, that is,
the separating conjunction is defined by star a a a for every element
a. Dockins et al. introduce this concept.
In this case, the orderings rxo and rio must coincide: because all
information is shared, whatever change an active thread decides to make
is visible by a passive thread. Any ordering will do; the ordering does
not have to be the identity.
Program Instance discrete_resource
(
A :
Type)
(
IA :
Inhabited A)
(
ordering :
A ->
A ->
Prop)
(
_ :
forall a,
ordering a a)
(
_ :
forall a1 a2 a3 :
A,
ordering a1 a2 ->
ordering a2 a3 ->
ordering a1 a3)
:
STAR A := {
star := @
discrete_star A;
add := @
discrete_add A inhabitant;
neutral a :=
a;
rxo :=
ordering;
rio :=
ordering
}.
Next Obligation.
unfold discrete_star. tauto.
Qed.
Next Obligation.
unfold discrete_star. intuition (subst; eauto).
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
unfold discrete_star.
introv star_deterministic star_commutative star_associative.
intros;
unpack;
subst;
subst.
generalize discrete_add_eq;
intro.
intuition congruence.
Qed.
Next Obligation.
unfold discrete_star. eauto.
Qed.
Next Obligation.
unfold discrete_star. intuition congruence.
Qed.
Next Obligation.
unfold discrete_star. eauto.
Qed.
Next Obligation.
unfold discrete_star. intuition (subst; eauto 6).
Qed.
Next Obligation.
unfold discrete_star. intuition (subst; eauto 6).
Qed.
-------------------------------------------------------------------------
A store typing in the style of ML maps locations to types: it is an
allocation map over (discrete) types.
We have to use intensional equality over types, as opposed to tyeq,
because the latter is reflexive and transitive only at well-formed
types. Or perhaps the image of a store typing should be restricted
to consist only of well-formed types.
Require Import Types.
Definition store_typing :=
aMap ty.
Program Definition store_typing_resource :
STAR store_typing :=
map_resource _ (
discrete_resource _ _ (@
eq ty)
_ _).
Next Obligation.
econstructor.
exact (
TyVar 0).
Qed.
Every store typing is compatible with itself.
Lemma store_typing_duplicable:
forall R :
store_typing,
@
star _ store_typing_resource R R R.
Proof.
simpl. unfold discrete_star. intuition eauto.
Qed.