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