Library ArefNaive

This file defines a simple implementation of adjustable references, thereby ensuring soundness of the adjustable reference axioms.

Require Import Vbase.
Set Implicit Arguments.

Part 1. Adjustable reference axiomatization (same as in Aref.v)

Module Type AREF.

Parameter aref : forall R T, (R -> T) -> Type.
Parameter aref_val : forall R T (f: R -> T), R -> aref f.
Axiom aref_inh : forall R T (f: R -> T) (r: aref f), exists v, r = aref_val f v.

Parameter aref_get : forall R T (f: R -> T), aref f -> T.
Axiom aref_get_val : forall R T (f: R -> T) v, aref_get (aref_val f v) = f v.

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.

Axiom aref_getuE : forall R A B (f : R -> A -> B) upd PF PF',
                     aref_getu upd PF PF' = aref_get (f:=f).

Parameter aref_new :
  forall R1 T1 (f1: R1 -> T1) (r: aref f1)
    R2 T2 (f2 : R2 -> T2) (g: forall v, aref_get r = f1 v -> R2)
    (PF: forall x pfx y pfy, f2 (g x pfx) = f2 (g y pfy)),
    aref f2.

Arguments aref_new [R1 T1 f1] r [R2 T2 f2] g PF.

Axiom aref_new_val :
  forall R1 T1 (f1: R1 -> T1) v R2 T2 (f2: R2 -> T2) g PF,
  aref_new (aref_val f1 v) g PF = aref_val f2 (g v (aref_get_val f1 v)).

End AREF.

Part 2. Adjustable reference implementation

Module ArefImpl : AREF.

Definition aref R T (f : R -> T) := R.
Definition aref_val R T (f: R -> T) (v : R) := v.
Definition aref_get R T (f: R -> T) (r : aref f) := f r.
Definition aref_getu
  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_get f.
Definition aref_new R1 T1 (f1: R1 -> T1) (r: aref f1)
    R2 T2 (f2 : R2 -> T2) (g: forall v, aref_get f1 r = f1 v -> R2)
    (PF: forall x pfx y pfy, f2 (g x pfx) = f2 (g y pfy)) :=
    g r eq_refl.

Arguments aref_new [R1 T1 f1] r [R2 T2 f2] g PF.

Lemma aref_getuE : forall R A B (f : R -> A -> B) upd PF PF',
                     aref_getu f upd PF PF' = aref_get f.
Proof. done. Qed.

Lemma aref_inh : forall R T (f: R -> T) (r: aref f), exists v, r = aref_val f v.
Proof. vauto. Qed.

Lemma aref_get_val : forall R T (f: R -> T) v, aref_get f (aref_val f v) = f v.
Proof. done. Qed.

Lemma aref_new_val :
  forall R1 T1 (f1: R1 -> T1) v R2 T2 (f2: R2 -> T2) g PF,
  aref_new (aref_val f1 v) (f2:=f2) g PF = aref_val f2 (g v (aref_get_val f1 v)).
Proof. intros; unfold aref_new, aref_val; f_equal; apply proof_irrelevance. Qed.

End ArefImpl.