Library Aref
This file contains an axiomatisation of adjustable references
Set Implicit Arguments.
Unset Strict Implicit.
Given an internal representation R and an external representation T
and a function f: R -> T for converting internal values to external ones,
we assume a type of adjustable references, aref f, which store values of
of the internal representation type R, but which are observable only up to
the function f, which converts them to the external representation T.
The available operations on adjustable references are:
1. aref_val f v creates an adjustable reference of type aref f holding
the internal value v.
3. aref_getu r upd returns (the external view of) the value of r
and updates it to another internal value with the same external view.
Parameter aref_getu :
forall R A B (f : R -> A -> B) (upd : R -> A -> R * B)
(PF: forall x a, f (fst (upd x a)) = f x)
(PF': forall x a, snd (upd x a) = f x a),
aref f -> A -> B.
4. aref_new r upd creates a new reference cell whose internal value is
upd applied to the internal value of r. One has to prove that any
such upd is a congruence wrt the external views.
Parameter aref_new :
forall R1 T1 (f1 : R1 -> T1) (r: aref f1)
R2 T2 (f2 : R2 -> T2) (upd : forall v, aref_get r = f1 v -> R2)
(PF: forall x pfx y pfy, f2 (upd x pfx) = f2 (upd y pfy)),
aref f2.
Arguments aref_getu [R A B f] upd PF PF' r a.
Arguments aref_new [R1 T1 f1] r [R2 T2 f2] upd PF.
We have four axioms. The first one says that all references are inhabited
by a internal value. The next three characterize the properties of the three
operations on adjustable references.
Axiom aref_inh :
forall R T (f: R -> T) (r : aref f),
exists v, r = aref_val f v.
Axiom aref_get_val :
forall R T (f: R -> T) v, aref_get (aref_val f v) = f v.
Axiom aref_getuE :
forall R A B (f: R -> A -> B) upd PF PF',
aref_getu upd PF PF' = aref_get (f:=f).
Axiom aref_new_val :
forall R1 T1 (f1: R1 -> T1) v R2 T2 (f2: R2 -> T2) upd CONG,
aref_new (aref_val f1 v) upd CONG = aref_val f2 (upd v (aref_get_val f1 v)).
Two lemmas about arefs that follow directly from the previous axioms.
Lemma aref_val_inj :
forall R T (f : R -> T) (x y: R) (EQ: aref_val f x = aref_val f y),
f x = f y.
Proof.
intros; generalize (f_equal (@aref_get _ _ _) EQ); rewrite !aref_get_val; trivial.
Qed.
Lemma aref_get_new :
forall R1 T1 (f1: R1 -> T1) v (r: aref f1) (EQ: r = aref_val f1 v)
R2 T2 (f2: R2 -> T2) upd CONG,
exists PF, aref_get (aref_new r (f2:=f2) upd CONG) = f2 (upd v PF).
Proof.
intros; subst; exists (aref_get_val _ _).
rewrite aref_new_val, (aref_get_val f2); trivial.
Qed.
Finally, we define an operation that simply copies a reference cell.
Program Definition aref_copy R T (f: R -> T) (r: aref f) : aref f :=
aref_new r (fun x _ => x) _.
Solve Obligations using congruence.
Lemma aref_copyE R T (f : R -> T) (r: aref f) : aref_copy r = r.
Proof. destruct (aref_inh r) as [v ->]; apply aref_new_val. Qed.
Directives for extraction
Extract Constant aref "'a" "'b" => "'b ref".
Extraction Implicit aref_val [R T f].
Extraction Implicit aref_getu [R A B f].
Extraction Implicit aref_new [R1 T1 f1 R2 T2 f2].
Extract Inlined Constant aref_val => "ref".
Extract Inlined Constant aref_get => "(fun f r -> f (!v))".
Extract Inlined Constant aref_getu => "(fun r a u -> let (v, fv) = u !r in r := v; fv)".
Extract Inlined Constant aref_new => "(fun r u -> ref (u !r ()))".