# Library Parray

Axiomatisation of persistent arrays

Require Import Vbase Veq MyInt31.
Set Implicit Arguments.
Unset Strict Implicit.

Local Open Scope int31.

Type of arrays
Parameter t : Type -> Type.

Return the length of an array.
Parameter length : forall A, t A -> int31 .

Construct a properly initialized array; array length must be positive.
Parameter unsafe_init :
forall A (length: int31) (POS: 0 <? length)
(f: forall (i : int31) (BND: i <? length), A), t A.

Read the value store at a particular array index (within bounds).
Parameter unsafe_get :
forall A (a: t A) (i: int31) (BND: i <? length a), A.

Update the value store at a particular array index (within bounds).
Parameter unsafe_set :
forall A (a: t A) (i: int31) (v : A) (BND: i <? length a), t A.

Arguments unsafe_init [A] length POS f.
Arguments unsafe_get [A] a i BND.
Arguments unsafe_set [A] a i v BND.

Axiomatization of the length function

Axiom length_pos :
forall A (a: t A), 0 <? length a.

Axiom length_unsafe_init :
forall A n POS f, length (unsafe_init (A:=A) n POS f) = n.

Axiom length_unsafe_set :
forall A (a: t A) x v PF, length (unsafe_set a x v PF) = length a.

Fact ltu_length_unsafe_initD A n POS f i :
i <? (length (unsafe_init (A:=A) n POS f)) -> i <? n.
Proof. by rewrite length_unsafe_init. Qed.

Fact ltu_length_unsafe_setD A (a : t A) x v PF i :
i <? length (unsafe_set a x v PF) -> i <? length a.
Proof. by rewrite length_unsafe_set. Qed.

Axiomatization of reading from initial and updated arrays.

Axiom uginit : forall A n POS f x PF,
unsafe_get (A:=A) (unsafe_init n POS f) x PF
= f x (ltu_length_unsafe_initD PF).
Axiom uguss : forall A a x v PF PF',
unsafe_get (A:=A) (unsafe_set a x v PF) x PF' = v.
Axiom uguso : forall A a x v y PF PF' (NEQ: x <> y),
unsafe_get (A:=A) (unsafe_set a x v PF) y PF'
= unsafe_get a y (ltu_length_unsafe_setD PF').

Two arrays are equal iff they have the same length and store the same values

Axiom eqI : forall A (a b: t A)
(LEQ: length a = length b)
(REQ: forall x POS POS', unsafe_get a x POS = unsafe_get b x POS'),
a = b.

Below, we provide more convenient init, get and set methods that do not require an "inside bounds" precondition.

Definition init A (length : int31) (f: int31 -> A) : t A :=
match 0 <? length as x with
| true => fun pf => unsafe_init length (sym_eq pf) (fun x pf => f x)
| false => fun _ => unsafe_init 1 eq_refl (fun x _ => f x)
end eq_refl.

Definition get A (a: t A) (i: int31) : A :=
match i <? length a as x with
| true => fun pf => unsafe_get a i (eq_sym pf)
| false => fun _ => unsafe_get a 0 (length_pos a)
end eq_refl.

Definition set A (a: t A) (i: int31) (v : A) : t A :=
match i <? length a as x with
| true => fun pf => unsafe_set a i v (eq_sym pf)
| false => fun _ => a
end eq_refl.

Lemma length_init A n (f : int31 -> A) :
length (init n f) = if 0 <? n then n else 1.
Proof.
by unfold init; des_eqrefl; rewrite length_unsafe_init; desf.
Qed.

Lemma length_set A a x (v : A) : length (set a x v) = length a.
Proof.
unfold set; des_eqrefl; try rewrite length_unsafe_set; desf.
Qed.

Lemma unsafe_getE A (a : t A) x PF :
unsafe_get a x PF = get a x.
Proof.
unfold get; des_eqrefl; [f_equal; apply proof_irrelevance|congruence].
Qed.

Lemma unsafe_setE A (a : t A) x v PF :
unsafe_set a x v PF = set a x v.
Proof.
unfold set; des_eqrefl; [f_equal; apply proof_irrelevance|congruence].
Qed.

Lemma ginit : forall A n f x (PF : x <? n), get (A:=A) (init n f) x = f x.
Proof.
ins; unfold init; des_eqrefl; unfold get; des_eqrefl;
rewrite ?length_unsafe_init in *; try congruence;
try by rewrite uginit; f_equal; apply proof_irrelevance.
rewrite uginit; f_equal; unfold int31_ltu in *.
change (phi 0) with 0%Z in *.
destruct (Z.ltb_spec 0 (phi n)); try done.
destruct (Z.ltb_spec (phi x) (phi n)); try done.
pose proof (phi_bounded x).
assert (X: 0%Z = phi x) by omega.
by apply (f_equal phi_inv) in X; rewrite phi_inv_phi in X.
Qed.

Lemma gss : forall A a x (LT: x <? length a) v, get (A:=A) (set a x v) x = v.
Proof.
unfold set; ins; des_eqrefl; simpl;
[unfold get; des_eqrefl; auto using uguss; rewrite length_unsafe_set in *|];
congruence.
Qed.

Lemma gso : forall A a x y (NEQ: x <> y) (LT: y <? length a) v,
get (A:=A) (set a x v) y = get a y.
Proof.
unfold set; ins; des_eqrefl; ins.
unfold get; des_eqrefl; auto using uguso; try rewrite length_unsafe_set in *.
des_eqrefl.
by rewrite uguso; ins; f_equal; apply proof_irrelevance.
exfalso; rewrite length_unsafe_set in *; congruence.
des_eqrefl; try (exfalso; congruence).
Qed.

Lemma gu A (a : t A) x :
get a x = get a (if x <? length a then x else 0).
Proof.
case_eq (x <? length a); ins; unfold get; do 2 des_eqrefl; try congruence.
f_equal; apply proof_irrelevance.
Qed.

Lemma gs :
forall A (a: t A) x v y (LT: y <? length a),
get (set a x v) y = if x == y then v else get a y.
Proof.
intros; desf; clarify; auto using gss, gso.
Qed.

Lemma gs2 A a x (v : A) y :
get (set a x v) y
= if y <? length a then
if x == y then v else get a y
else if x == 0 then v else get a y.
Proof.
rewrite gu, length_set; desf; subst;
auto using gss, gso, length_pos.
rewrite gso; auto using length_pos.
rewrite (gu _ y); desf.
Qed.

A simpler initializer

Definition create A (length: int31) (v: A) := init length (fun _ => v).

Lemma gcreate A n (v: A) x : get (create n v) x = v.
Proof.
by unfold create, init; des_eqrefl; unfold get; des_eqrefl; apply uginit.
Qed.

Lemma length_create A n (v: A) :
length (create n v) = if 0 <? n then n else 1.
Proof. apply length_init. Qed.

Create a copy of the array

Definition copy A (a : t A) : t A :=
unsafe_init (length a) (length_pos a) (unsafe_get a).

Lemma length_copy A (a : t A) : length (copy a) = length a.
Proof. apply length_unsafe_init. Qed.

Lemma gcopy : forall A (a: t A) x,
get (copy a) x = get a x.
Proof.
ins; unfold get, copy; rewrite uginit; try done.
do 2 des_eqrefl; try rewrite uginit;
try (exfalso; rewrite length_unsafe_init in *; congruence);
f_equal; apply proof_irrelevance.
Qed.

Lemma copyE A (a:t A) : copy a = a.
Proof. apply eqI; ins; rewrite ?unsafe_getE; auto using length_copy, gcopy. Qed.

Create a copy of the array, but with double the size (if possible)

Lemma double_helper x :
0 <? x ->
true = (x <? v30) ->
0 <? 2 * x.
Proof.
ins; apply Z.ltb_lt; apply Z.ltb_lt in H;
symmetry in H0; apply Z.ltb_lt in H0.
rewrite spec_mul; change (phi 0) with 0%Z in *.
change (2 ^ Z.of_nat size)%Z with (2 * phi v30)%Z.
rewrite Zmult_mod_distr_l, Zmod_small; omega.
Qed.

Definition double A (a : t A) : t A :=
let n := 2 * length a in
match length a <? v30 as x with
| true => fun pf =>
unsafe_init n (double_helper (length_pos a) pf) (fun i PF => get a i)
| false => fun _ => copy a
end eq_refl.

Lemma length_double A (a : t A) :
length (double a) = if length a <? v30 then 2 * length a else length a.
Proof.
unfold double; des_eqrefl;
[rewrite <- EQ at 1 | rewrite <- EQ]; apply length_unsafe_init.
Qed.

Lemma gdouble A (a : t A) x :
get (double a) x = get a x.
Proof.
unfold double; des_eqrefl; auto using gcopy.
unfold get; do 2 des_eqrefl; simpls; try rewrite uginit;
unfold get; des_eqrefl; try (f_equal; apply proof_irrelevance);
try solve [exfalso; rewrite length_unsafe_init, ?length_pos in *; congruence].
exfalso; rewrite length_unsafe_init in *.
symmetry in EQ; apply Z.ltb_lt in EQ.
symmetry in EQ0; apply Z.ltb_ge in EQ0.
symmetry in EQ1; apply Z.ltb_lt in EQ1.
symmetry in EQ2; apply Z.ltb_lt in EQ2.
revert EQ0; rewrite spec_mul; change (phi 0) with 0%Z in *.
change (2 ^ Z.of_nat size)%Z with (2 * phi v30)%Z.
rewrite Zmult_mod_distr_l, Zmod_small; intros; omega.
Qed.

Extraction

Extract Constant t "'a" => "'a Perarray.t".

Extract Inlined Constant create => "Perarray.create".
Extract Inlined Constant init => "Perarray.init".
Extract Inlined Constant length => "Perarray.length".
Extract Inlined Constant unsafe_get => "Perarray.get".
Extract Inlined Constant unsafe_set => "Perarray.set".