From e2683e1e653a1b6872a886f4b99218e2803f7a74 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Wed, 7 Jul 2021 08:55:25 +0200
Subject: use native integers (#96)

---
 src/Array/PArray.v | 477 +++++++++++++++++++----------------------------------
 1 file changed, 171 insertions(+), 306 deletions(-)

(limited to 'src/Array/PArray.v')

diff --git a/src/Array/PArray.v b/src/Array/PArray.v
index 25da052..3c98041 100644
--- a/src/Array/PArray.v
+++ b/src/Array/PArray.v
@@ -13,15 +13,58 @@
 (* Software implementation of arrays, based on finite maps using AVL
    trees *)
 
-
 Declare Scope array_scope.
 
-Require Import Int31.
-Require Export Int63.
+Require Export Int63 Psatz.
 Require FMapAVL.
+Require Import ZArith.
 
 Local Open Scope int63_scope.
 
+Import OrderedType.
+
+Module IntOrderedType <: OrderedType.
+
+  Definition t := int.
+
+  Definition eq x y := (x == y) = true.
+
+  Definition lt x y := (x < y) = true.
+
+  Lemma eq_refl x : eq x x.
+  Proof. unfold eq. rewrite eqb_spec. reflexivity. Qed.
+
+  Lemma eq_sym x y : eq x y -> eq y x.
+  Proof. unfold eq. rewrite !eqb_spec. intros ->. reflexivity. Qed.
+
+  Lemma eq_trans x y z : eq x y -> eq y z -> eq x z.
+  Proof. unfold eq. rewrite !eqb_spec. intros -> ->. reflexivity. Qed.
+
+  Lemma lt_trans x y z : lt x y -> lt y z -> lt x z.
+  Proof. unfold lt; rewrite !ltb_spec; apply Z.lt_trans. Qed.
+
+  Lemma lt_not_eq x y : lt x y -> ~ eq x y.
+  Proof. unfold lt, eq. rewrite ltb_spec, eqb_spec. intros H1 H2. rewrite H2 in H1. lia. Qed.
+
+  Definition compare x y : Compare lt eq x y.
+  Proof.
+    case_eq (x < y); intro e.
+      exact (LT e).
+      case_eq (x == y); intro e2.
+        exact (EQ e2).
+        apply GT. unfold lt.
+        rewrite <- Bool.not_false_iff_true, <- Bool.not_true_iff_false, ltb_spec, eqb_spec in *; intro e3.
+        apply e2, to_Z_inj; lia.
+  Defined.
+
+  Definition eq_dec x y : { eq x y } + { ~ eq x y }.
+  Proof.
+    case_eq (x == y); intro e.
+      left; exact e.
+      right. intro H. rewrite H in e. discriminate.
+  Defined.
+
+End IntOrderedType.
 
 Module Map := FMapAVL.Make(IntOrderedType).
 
@@ -33,12 +76,14 @@ Definition array (A:Type) : Type :=
 Definition make {A:Type} (l:int) (d:A) : array A := (Map.empty A, d, l).
 
 Definition get {A:Type} (t:array A) (i:int) : A :=
-  let (td,_) := t in
-  let (t,d) := td in
-  match Map.find i t with
-    | Some x => x
-    | None => d
-  end.
+  let (td, l) := t in
+  let (t, d) := td in
+  if i < l then
+    match Map.find i t with
+      | Some x => x
+      | None => d
+    end
+  else d.
 
 Definition default {A:Type} (t:array A) : A :=
   let (td,_) := t in let (_,d) := td in d.
@@ -56,340 +101,160 @@ Definition length {A:Type} (t:array A) : int :=
 
 Definition copy {A:Type} (t:array A) : array A := t.
 
-Definition reroot : forall {A:Type}, array A -> array A := @copy.
-
-Definition init {A:Type} (l:int) (f:int -> A) (d:A) : array A :=
-  let r :=
-      if l == 0 then
-        Map.empty A
-      else
-        foldi (fun j m => Map.add j (f j) m) 0 (l-1) (Map.empty A) in
-  (r, d, l).
-
-Definition map {A B:Type} (f:A -> B) (t:array A) : array B :=
-  let (td,l) := t in
-  let (t,d) := td in
-  (Map.map f t, f d, l).
-
 Delimit Scope array_scope with array.
 Notation "t '.[' i ']'" := (get t i) (at level 50) : array_scope.
 Notation "t '.[' i '<-' a ']'" := (set t i a) (at level 50) : array_scope.
 
 Local Open Scope array_scope.
 
-Definition max_array_length := 4194302%int31.
+Definition max_length := max_int.
 
 (** Axioms *)
-Axiom get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t.
-
-Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
-Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
-Axiom default_set : forall A t i (a:A), default (t.[i<-a]) = default t.
-
-
-Axiom get_make : forall A (a:A) size i, (make size a).[i] = a.
-Axiom default_make : forall A (a:A) size, (default (make size a)) = a.
-
-Axiom ltb_length : forall A (t:array A), length t <= max_array_length = true.
-
-Axiom length_make : forall A size (a:A),
-  length (make size a) = if size <= max_array_length then size else max_array_length.
-Axiom length_set : forall A t i (a:A),
-  length (t.[i<-a]) = length t.
-
-Axiom get_copy : forall A (t:array A) i, (copy t).[i] = t.[i].
-Axiom length_copy : forall A (t:array A), length (copy t) = length t.
-
-Axiom get_reroot : forall A (t:array A) i, (reroot t).[i] = t.[i].
-Axiom length_reroot : forall A (t:array A), length (reroot t) = length t.
-
-
-Axiom length_init : forall A f size (def:A),
-  length (init size f def) = if size <= max_array_length then size else max_array_length.
-
-Axiom get_init : forall A f size (def:A) i,
-  (init size f def).[i] = if i < length (init size f def) then f i else def.
-
-Axiom default_init : forall A f size (def:A), default (init size f def) = def.
-
-(* Not true in this implementation (see #71, many thanks to Andres Erbsen) *)
-(*
-Axiom get_ext : forall A (t1 t2:array A),
-  length t1 = length t2 ->
-  (forall i, i < length t1 = true -> t1.[i] = t2.[i]) ->
-  default t1 = default t2 ->
-  t1 = t2.
-*)
-
-(* Definition *)
-Definition to_list {A:Type} (t:array A) :=
-  let len := length t in
-  if 0 == len then nil
-  else foldi_down (fun i l => t.[i] :: l)%list (len - 1) 0 nil.
-
-Definition forallbi {A:Type} (f:int-> A->bool) (t:array A) :=
-  let len := length t in
-  if 0 == len then true
-  else forallb (fun i => f i (t.[i])) 0 (len - 1).
-
-Definition forallb {A:Type} (f: A->bool) (t:array A) :=
-  let len := length t in
-  if 0 == len then true
-  else forallb (fun i => f (t.[i])) 0 (len - 1).
-
-Definition existsbi {A:Type} (f:int->A->bool) (t:array A) :=
-  let len := length t in
-  if 0 == len then false
-  else existsb (fun i => f i (t.[i])) 0 (len - 1).
-
-Definition existsb {A:Type} (f:A->bool) (t:array A) :=
-  let len := length t in
-  if 0 == len then false
-  else existsb (fun i => f (t.[i])) 0 (len - 1).
-
-(* TODO : We should add init as native and add it *)
-Definition mapi {A B:Type} (f:int->A->B) (t:array A) :=
-  let size := length t in
-  let def := f size (default t) in
-  let tb := make size def in
-  if size == 0 then tb
-  else foldi (fun i tb => tb.[i<- f i (t.[i])]) 0 (size - 1) tb.
-
-Definition foldi_left {A B:Type} (f:int -> A -> B -> A) a (t:array B) :=
-  let len := length t in
-  if 0 == len then a
-  else foldi (fun i a => f i a (t.[i])) 0 (len - 1) a.
-
-Definition fold_left {A B:Type} (f: A -> B -> A) a (t:array B) :=
-  let len := length t in
-  if 0 == len then a
-  else foldi (fun i a => f a (t.[i])) 0 (length t - 1) a.
-
-Definition foldi_right {A B:Type} (f:int -> A -> B -> B) (t:array A) b :=
-  let len := length t in
-  if 0 == len then b
-  else foldi_down (fun i b => f i (t.[i]) b) (len - 1) 0 b.
-
-Definition fold_right {A B:Type} (f: A -> B -> B) (t:array A) b :=
-  let len := length t in
-  if 0 == len then b
-  else foldi_down (fun i b => f (t.[i]) b) (len - 1) 0 b.
-
-(* Lemmas *)
-
-Lemma default_copy : forall A (t:array A), default (copy t) = default t.
-Proof.
- intros A t;assert (length t < length t = false).
-  apply Bool.not_true_is_false; apply leb_not_gtb; apply leb_refl.
- rewrite <- (get_outofbound _ (copy t) (length t)), <- (get_outofbound _ t (length t)), get_copy;trivial.
+Require FSets.FMapFacts.
+Module P := FSets.FMapFacts.WProperties_fun IntOrderedType Map.
+
+Lemma get_outofbound : forall A (t:array A) i, (i < length t) = false -> t.[i] = default t.
+intros A t i; unfold get.
+destruct t as ((t, d), l).
+unfold length; intro Hi; rewrite Hi; clear Hi.
+reflexivity.
 Qed.
 
-Lemma reroot_default : forall A (t:array A), default (reroot t) = default t.
-Proof.
- intros A t;assert (length t < length t = false).
-  apply Bool.not_true_is_false; apply leb_not_gtb; apply leb_refl.
- rewrite <- (get_outofbound _ (reroot t) (length t)), <- (get_outofbound _ t (length t)), get_reroot;trivial.
+Lemma get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
+intros A t i a.
+destruct t as ((t, d), l).
+unfold set, get, length.
+intro Hi; generalize Hi.
+rewrite ltb_spec.
+rewrite Z.lt_nge.
+rewrite <- leb_spec.
+rewrite Bool.not_true_iff_false.
+intro Hi'; rewrite Hi'; clear Hi'.
+rewrite Hi; clear Hi.
+rewrite P.F.add_eq_o.
+reflexivity.
+rewrite eqb_spec.
+reflexivity.
 Qed.
 
-Lemma get_set_same_default :
-   forall (A : Type) (t : array A) (i : int) ,
-       (t .[ i <- default t]) .[ i] = default t.
-Proof.
- intros A t i;case_eq (i < (length t));intros.
- rewrite get_set_same;trivial.
- rewrite get_outofbound, default_set;trivial.
- rewrite length_set;trivial.
+Lemma get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
+intros A t i j a Hij.
+destruct t as ((t, d), l).
+unfold set, get, length.
+case (l <= i).
+reflexivity.
+rewrite P.F.add_neq_o.
+reflexivity.
+intro H; apply Hij; clear Hij.
+rewrite eqb_spec in H.
+assumption.
 Qed.
 
-Lemma get_not_default_lt : forall A (t:array A) x,
- t.[x] <> default t -> x < length t = true.
-Proof.
- intros A t x Hd.
- case_eq (x < length t);intros Heq;[trivial | ].
- elim Hd;rewrite get_outofbound;trivial.
+Lemma default_set : forall A t i (a:A), default (t.[i<-a]) = default t.
+intros A t i a.
+destruct t as ((t, d), l).
+unfold default, set.
+case (l <= i); reflexivity.
 Qed.
 
-Lemma foldi_left_Ind :
-     forall A B (P : int -> A -> Prop) (f : int -> A -> B -> A) (t:array B),
-     (forall a i, i < length t = true -> P i a -> P (i+1) (f i a (t.[i]))) ->
-     forall a, P 0 a ->
-     P (length t) (foldi_left f a t).
-Proof.
- intros;unfold foldi_left.
- destruct (reflect_eqb 0 (length t)).
-  rewrite <- e;trivial.
- assert ((length t - 1) + 1 = length t) by ring.
- rewrite <- H1 at 1;apply foldi_Ind;auto.
- assert (W:= leb_max_int (length t));rewrite leb_spec in W.
- rewrite ltb_spec, to_Z_sub_1_diff;auto with zarith.
- intros Hlt;elim (ltb_0 _ Hlt).
- intros;apply H;trivial. rewrite ltb_leb_sub1;auto.
+Lemma get_make : forall A (a:A) size i, (make size a).[i] = a.
+intros A a size i.
+unfold make, get.
+rewrite P.F.empty_o.
+case (i < size); reflexivity.
 Qed.
 
-Lemma fold_left_Ind :
-     forall A B (P : int -> A -> Prop) (f : A -> B -> A) (t:array B),
-     (forall a i, i < length t = true -> P i a -> P (i+1) (f a (t.[i]))) ->
-     forall a, P 0 a ->
-     P (length t) (fold_left f a t).
-Proof.
- intros.
- apply (foldi_left_Ind A B P (fun i => f));trivial.
+Lemma leb_length : forall A (t:array A), length t <= max_length = true.
+intros A t.
+generalize (length t); clear t.
+intro i.
+rewrite leb_spec.
+apply Z.lt_succ_r.
+change (Z.succ (to_Z max_length)) with wB.
+apply to_Z_bounded.
 Qed.
 
-Lemma fold_left_ind :
-     forall A B (P : A -> Prop) (f : A -> B -> A) (t:array B),
-     (forall a i, i < length t = true -> P a -> P (f a (t.[i]))) ->
-     forall a, P a ->
-     P (fold_left f a t).
-Proof.
- intros;apply (fold_left_Ind A B (fun _ => P));trivial.
+Lemma length_make : forall A size (a:A),
+  length (make size a) = if size <= max_length then size else max_length.
+intros A size a.
+unfold length, make.
+replace (size <= max_length) with true.
+reflexivity.
+symmetry.
+rewrite leb_spec.
+apply Z.lt_succ_r.
+change (Z.succ (to_Z max_length)) with wB.
+apply to_Z_bounded.
 Qed.
 
-Lemma foldi_right_Ind :
-     forall A B (P : int -> A -> Prop) (f : int -> B -> A -> A) (t:array B),
-     (forall a i, i < length t = true -> P (i+1) a -> P i (f i (t.[i]) a)) ->
-     forall a, P (length t) a ->
-     P 0 (foldi_right f t a).
-Proof.
- intros;unfold foldi_right.
- destruct (reflect_eqb 0 (length t)).
-  rewrite e;trivial.
- set (P' z a := (*-1 <= z < [|length t|] ->*) P (of_Z (z + 1)) a).
- assert (P' ([|0|] - 1)%Z (foldi_down (fun (i : int) (b : A) => f i (t .[ i]) b) (length t - 1) 0 a)).
- apply foldi_down_ZInd;unfold P'.
- intros Hlt;elim (ltb_0 _ Hlt).
- rewrite to_Z_sub_1_diff;auto.
- ring_simplify ([|length t|] - 1 + 1)%Z;rewrite of_to_Z;trivial.
- intros;ring_simplify ([|i|] - 1 + 1)%Z;rewrite of_to_Z;auto.
- assert (i < length t = true).
-   rewrite ltb_leb_sub1;auto.
- apply H;trivial.
- exact H1.
-Qed.
-
-Lemma fold_right_Ind :
-     forall A B (P : int -> A -> Prop) (f : B -> A -> A) (t:array B),
-     (forall a i, i < length t = true -> P (i+1) a -> P i (f (t.[i]) a)) ->
-     forall a, P (length t) a ->
-     P 0 (fold_right f t a).
-Proof.
- intros;apply (foldi_right_Ind A B P (fun i => f));trivial.
+Lemma length_set : forall A t i (a:A),
+  length (t.[i<-a]) = length t.
+intros A t i a.
+destruct t as ((t, d), l).
+unfold length, set.
+case (l <= i); reflexivity.
 Qed.
 
-Lemma fold_right_ind :
-     forall A B (P : A -> Prop) (f : B -> A -> A) (t:array B),
-     (forall a i, i < length t = true -> P a -> P (f (t.[i]) a)) ->
-     forall a, P a ->
-     P (fold_right f t a).
-Proof.
- intros;apply (fold_right_Ind A B (fun i => P));trivial.
+Lemma get_copy : forall A (t:array A) i, (copy t).[i] = t.[i].
+intros A t i.
+unfold copy; reflexivity.
 Qed.
 
-Lemma forallbi_spec : forall A (f : int -> A -> bool) t,
-  forallbi f t = true <-> forall i, i < length t = true -> f i (t.[i]) = true.
-Proof.
- unfold forallbi;intros A f t.
- destruct (reflect_eqb 0 (length t)).
- split;[intros | trivial].
- elim (ltb_0 i);rewrite e;trivial.
- rewrite forallb_spec;split;intros Hi i;intros;apply Hi.
- apply leb_0. rewrite <- ltb_leb_sub1;auto. rewrite ltb_leb_sub1;auto.
+Lemma length_copy : forall A (t:array A), length (copy t) = length t.
+intros A t.
+unfold copy; reflexivity.
 Qed.
 
-Lemma forallb_spec : forall A (f : A -> bool) t,
-  forallb f t = true <-> forall i, i < length t = true -> f (t.[i]) = true.
-Proof.
- intros A f;apply (forallbi_spec A (fun i => f)).
-Qed.
+(* Not true in this implementation (see #71, many thanks to Andres Erbsen) *)
+(*
+Axiom array_ext : forall A (t1 t2:array A),
+  length t1 = length t2 ->
+  (forall i, i < length t1 = true -> t1.[i] = t2.[i]) ->
+  default t1 = default t2 ->
+  t1 = t2.
+*)
 
-Lemma existsbi_spec : forall A (f : int -> A -> bool) t,
-  existsbi f t = true <-> exists i, i < length t = true /\ f i (t.[i]) = true.
-Proof.
- unfold existsbi;intros A f t.
- destruct (reflect_eqb 0 (length t)).
- split;[discriminate | intros [i [Hi _]];rewrite <- e in Hi;elim (ltb_0 _ Hi)].
- rewrite existsb_spec. repeat setoid_rewrite Bool.andb_true_iff.
- split;intros [i H];decompose [and] H;clear H;exists i;repeat split;trivial.
- rewrite ltb_leb_sub1;auto. apply leb_0. rewrite <- ltb_leb_sub1;auto.
-Qed.
+(* Lemmas *)
 
-Lemma existsb_spec : forall A (f : A -> bool) t,
-  existsb f t = true <-> exists i, i < length t = true /\ f (t.[i]) = true.
-Proof.
- intros A f;apply (existsbi_spec A (fun i => f)).
+Lemma default_copy A (t:array A) : default (copy t) = default t.
+unfold copy; reflexivity.
 Qed.
 
-Local Open Scope list_scope.
-
-Definition to_list_ntr A (t:array A) :=
-  let len := length t in
-  if 0 == len then nil
-  else foldi_ntr _ (fun i l => t.[i] :: l) 0 (len - 1) nil.
-
-Lemma to_list_to_list_ntr : forall A (t:array A),
-   to_list t = to_list_ntr _ t.
-Proof.
- unfold to_list, to_list_ntr; intros A t.
- destruct (reflect_eqb 0 (length t));trivial.
- rewrite foldi_ntr_foldi_down;trivial.
- apply leb_ltb_trans with max_array_length;[ | trivial].
- apply leb_trans with (length t);[ | apply ltb_length].
- rewrite leb_spec, sub_spec.
- rewrite to_Z_1, Zmod_small;try omega.
- generalize (to_Z_bounded (length t)).
- assert (0%Z <> [|length t|]);[ | omega].
-   intros Heq;elim n;apply to_Z_inj;trivial.
+Lemma default_make A (a : A) size : default (make size a) = a.
+unfold default, make; reflexivity.
 Qed.
 
-Lemma fold_left_to_list : forall (A B:Type) (t:array A) (f: B -> A -> B) b,
-   fold_left f b t = List.fold_left f (to_list t) b.
-Proof.
-  intros A B t f;rewrite to_list_to_list_ntr.
-  unfold fold_left, to_list_ntr; destruct (reflect_eqb 0 (length t));[trivial | ].
-  set (P1 := fun i => forall b,
-      foldi (fun (i : int) (a : B) => f a (t .[ i])) i (length t - 1) b =
-      List.fold_left f
-        (foldi_ntr (list A) (fun (i : int) (l : list A) => t .[ i] :: l) i
-           (length t - 1) nil) b).
-  assert (W: P1 0);[ | trivial].
-  apply int_ind_bounded with (max := length t - 1);unfold P1.
-  apply leb_0.
-  intros b;unfold foldi_ntr;rewrite foldi_eq, foldi_cont_eq;trivial.
-  intros i _ Hlt Hrec b.
-  unfold foldi_ntr;rewrite foldi_lt, foldi_cont_lt;trivial;simpl.
-  apply Hrec.
+Lemma get_set_same_default A (t : array A) (i : int) : t.[i <- default t].[i] = default t.
+unfold default, get, set.
+destruct t as ((t, d), l).
+case_eq (i < l).
+intro H; generalize H.
+rewrite ltb_spec.
+rewrite Z.lt_nge.
+rewrite <- leb_spec.
+rewrite Bool.not_true_iff_false.
+intro H'; rewrite H'; clear H'.
+rewrite H; clear H.
+rewrite P.F.add_eq_o.
+reflexivity.
+rewrite eqb_spec.
+reflexivity.
+intro H; generalize H.
+rewrite <- Bool.not_true_iff_false.
+rewrite ltb_spec.
+rewrite <- Z.le_ngt.
+rewrite <- leb_spec.
+intro H'; rewrite H'; clear H'.
+rewrite H.
+reflexivity.
 Qed.
 
-Require Import Bool.
-Local Open Scope bool_scope.
-
-Definition eqb {A:Type} (Aeqb: A->A->bool) (t1 t2:array A) :=
-  (length t1 == length t2) &&
-  Aeqb (default t1) (default t2) &&
-  forallbi (fun i a1 => Aeqb a1 (t2.[i])) t1.
-
-(*
-Lemma reflect_eqb : forall (A:Type) (Aeqb:A->A->bool),
-  (forall a1 a2, reflect (a1 = a2) (Aeqb a1 a2)) ->
-  forall t1 t2, reflect (t1 = t2) (eqb Aeqb t1 t2).
-Proof.
- intros A Aeqb HA t1 t2.
- case_eq (eqb Aeqb t1 t2);unfold eqb;intros H;constructor.
- rewrite !andb_true_iff in H;destruct H as [[H1 H2] H3].
- apply get_ext.
- rewrite (reflect_iff _ _ (reflect_eqb _ _));trivial.
- rewrite forallbi_spec in H3.
- intros i Hlt;rewrite (reflect_iff _ _ (HA _ _));auto.
- rewrite (reflect_iff _ _ (HA _ _));trivial.
- intros Heq;rewrite Heq in H;clear Heq.
- revert H; rewrite Int63Axioms.eqb_refl;simpl.
- case_eq (Aeqb (default t2) (default t2));simpl;intros H0 H1.
- rewrite <- not_true_iff_false, forallbi_spec in H1;apply H1.
- intros i _; rewrite <- (reflect_iff _ _ (HA _ _));trivial.
- rewrite <- not_true_iff_false, <- (reflect_iff _ _ (HA _ _)) in H0;apply H0;trivial.
+Lemma get_not_default_lt A (t:array A) x :
+ t.[x] <> default t -> (x < length t) = true.
+unfold get, default, length.
+destruct t as ((t, d), l).
+case (x < l); tauto.
 Qed.
-*)
-
 
 (* 
    Local Variables:
-- 
cgit