# 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.

Parameter aref : forall R T (f : R -> T), Type.

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.

Parameter aref_val : forall R T (f : R -> T), R -> aref f.

2. aref_get r returns (the external view of) the value of r.

Parameter aref_get : forall R T (f : R -> T), aref f -> T.

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)).

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 ()))".