Set Implicit Arguments.
Functional extensionality for stores saves a lot of pollution.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import MyTactics.
Locations are integers.
Definition location :=
nat.
A store is a pair of a reference allocation limit and a mapping of
locations to values. This definition is parameterized with respect
to the nature of values.
Inductive gstore (
A :
Type) :
Type :=
|
Store:
location -> (
location ->
option A) ->
gstore A.
Store modification.
Definition patch (
A :
Type) (
m :
location ->
A) (
point :
location) (
v :
A) :
location ->
A :=
fun l =>
if eq_nat_dec point l then v else m l.
Store extension.
Definition extend (
A :
Type) (
m :
location ->
option A) (
point :
location) (
v :
A) :
location ->
option A :=
patch m point (
Some v).
Store transformation.
Definition transform (
A B :
Type) (
f :
A ->
B) (
m :
location ->
option A) :
location ->
option B :=
fun l :
location =>
match m l with
|
None =>
None
|
Some v =>
Some (
f v)
end.
Basic facts about patch.
Lemma patch_extensional:
forall (
A :
Type)
limit (
m1 m2 :
location ->
A)
point v,
(
forall l,
l <
limit ->
m1 l =
m2 l) ->
(
forall l,
l <
limit ->
patch m1 point v l =
patch m2 point v l).
Proof.
intros. unfold patch. by_cases; auto.
Qed.
Lemma patch_extensional_new:
forall (
A :
Type)
limit (
m1 m2 :
location ->
A)
v,
(
forall l,
l <
limit ->
m1 l =
m2 l) ->
(
forall l,
l <
S limit ->
patch m1 limit v l =
patch m2 limit v l).
Proof.
intros. unfold patch. by_cases; auto.
Qed.
Extension and transformation commute.
Lemma transform_extend:
forall (
A B :
Type) (
f :
A ->
B) (
m :
location ->
option A) (
l :
location) (
v :
A),
transform f (
extend m l v) =
extend (
transform f m)
l (
f v).
Proof.
intros. extensionality x. unfold transform, extend, patch. by_cases; auto.
Qed.
Basic facts about transformation.
Lemma transform_none:
forall (
A B :
Type) (
f :
A ->
B)
m l,
m l =
None ->
transform f m l =
None.
Proof.
introv h. unfold transform. rewrite h. auto.
Qed.
Lemma transform_some:
forall (
A B :
Type) (
f :
A ->
B)
m l v,
m l =
Some v ->
transform f m l =
Some (
f v).
Proof.
introv h. unfold transform. rewrite h. auto.
Qed.
Lemma transform_extensional:
forall (
A B :
Type) (
f :
A ->
B)
m1 m2,
(
forall l,
m1 l =
m2 l) ->
(
forall l,
transform f m1 l =
transform f m2 l).
Proof.
introv h. intro. unfold transform. rewrite h. auto.
Qed.
Hint Resolve transform_none transform_some transform_extensional :
transform.
The predicate everywhere P states that every value in the store satisfies
P.
Inductive everywhere (
A :
Type) (
P :
A ->
Prop) :
gstore A ->
Prop :=
|
Everywhere:
forall limit m,
(
forall l v,
m l =
Some v ->
P v) ->
everywhere P (
Store limit m).
Hint Constructors everywhere.
Basic properties of everywhere.
Lemma everywhere_read:
forall (
A :
Type) (
P :
A ->
Prop)
limit m l v,
everywhere P (
Store limit m) ->
m l =
Some v ->
P v.
Proof.
introv h ?. dependent destruction h. eauto.
Qed.
Lemma everywhere_extend:
forall (
A :
Type) (
P :
A ->
Prop)
limit m v,
everywhere P (
Store limit m) ->
P v ->
everywhere P (
Store (
S limit) (
extend m limit v)).
Proof.
unfold extend, patch.
introv h1 h2. econstructor. intros ? ?. by_cases. congruence. dependent destruction h1. eauto.
Qed.
Lemma everywhere_write:
forall (
A :
Type) (
P :
A ->
Prop)
limit l m v,
everywhere P (
Store limit m) ->
P v ->
everywhere P (
Store limit (
extend m l v)).
Proof.
unfold extend, patch.
introv h1 h2. econstructor. intros ? ?. by_cases. congruence. dependent destruction h1. eauto.
Qed.