Merge remote-tracking branch 'remotes/origin/coq-8.11' into coq-8.12

1 files changed, 937 insertions, 609 deletions

diff --git a/src/Misc.v b/src/Misc.v
index 520c41c..e558ce3 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -10,10 +10,12 @@
 (**************************************************************************)
 
 
-Require Import Bool List PArray Int63 ZArith Psatz.
+Require Import Bool List PArray Int63 Ring63 ZArith Psatz.
 Local Open Scope int63_scope.
 Local Open Scope array_scope.
 
+Global Notation "[| x |]" := (φ x).
+
 
 (** Lemmas about Bool *)
 
@@ -23,6 +25,23 @@ Proof. intros [ | ]; reflexivity. Qed.
 
 (** Lemmas about Int63 *)
 
+Lemma reflect_eqb : forall i j, reflect (i = j)%Z (i == j).
+Proof.
+ intros; apply iff_reflect.
+ symmetry;apply eqb_spec.
+Qed.
+
+Lemma to_Z_eq : forall x y, [|x|] = [|y|] <-> x = y.
+Proof.
+ split;intros;subst;trivial.
+ apply to_Z_inj;trivial.
+Qed.
+
+Lemma max_int_wB : [|max_int|] = (wB - 1)%Z.
+Proof.
+ reflexivity.
+Qed.
+
 Lemma le_eq : forall i j,
   (j <= i) = true -> (j + 1 <= i) = false -> i = j.
 Proof.
@@ -32,7 +51,7 @@ Proof.
   assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB).
   pose (H3 := to_Z_bounded j); lia.
   destruct H2 as [H2|H2].
-  rewrite Zmod_small in H.
+  rewrite Z.mod_small in H.
   lia.
   split.
   pose (H3 := to_Z_bounded j); lia.
@@ -40,6 +59,15 @@ Proof.
   rewrite H2, Z_mod_same_full in H; elim H; destruct (to_Z_bounded i) as [H3 _]; assumption.
 Qed.
 
+Lemma leb_0 : forall x, 0 <= x = true.
+Proof.
+ intros x;rewrite leb_spec;destruct (to_Z_bounded x);trivial.
+Qed.
+
+Lemma leb_refl : forall n, n <= n = true.
+Proof.
+ intros n;rewrite leb_spec;apply Z.le_refl.
+Qed.
 
 Lemma lt_eq : forall i j,
   (i < j + 1) = true -> (i < j) = false -> i = j.
@@ -50,7 +78,7 @@ Proof.
   assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB).
   pose (H3 := to_Z_bounded j); lia.
   destruct H2 as [H2|H2].
-  rewrite Zmod_small in H1.
+  rewrite Z.mod_small in H1.
   lia.
   split.
   pose (H3 := to_Z_bounded j); lia.
@@ -58,6 +86,100 @@ Proof.
   rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. lia.
 Qed.
 
+Lemma not_0_ltb : forall x, x <> 0 <-> 0 < x = true.
+Proof.
+ intros x;rewrite ltb_spec, to_Z_0;assert (W:=to_Z_bounded x);split.
+ intros Hd;assert ([|x|] <> 0)%Z;[ | omega].
+   intros Heq;elim Hd;apply to_Z_inj;trivial.
+ intros Hlt Heq;elimtype False.
+ assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | omega].
+Qed.
+
+Lemma ltb_0 : forall x, ~ (x < 0 = true).
+Proof.
+ intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);omega.
+Qed.
+
+Lemma not_ltb_refl : forall i, ~(i < i = true).
+Proof.
+ intros;rewrite ltb_spec;omega.
+Qed.
+
+Lemma ltb_trans : forall x y z, x < y = true ->  y < z = true -> x < z = true.
+Proof.
+ intros x y z;rewrite !ltb_spec;apply Z.lt_trans.
+Qed.
+
+Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y)).
+Proof.
+ intros.
+ apply eq_true_iff_eq.
+ rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;omega.
+Qed.
+
+Lemma leb_ltb_trans : forall x y z, x <= y = true ->  y < z = true -> x < z = true.
+Proof.
+ intros x y z;rewrite leb_spec, !ltb_spec;apply Z.le_lt_trans.
+Qed.
+
+Lemma to_Z_add_1 : forall x y, x < y = true -> [|x+1|] = ([|x|] + 1)%Z.
+Proof.
+  intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
+   rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;omega.
+Qed.
+
+Lemma to_Z_add_1_wB : forall x, ([|x|] < wB - 1)%Z -> [|x + 1|] = ([|x|] + 1)%Z.
+Proof.
+  intros; assert (Bx := to_Z_bounded x); rewrite add_spec, to_Z_1, Z.mod_small; lia.
+Qed.
+
+Lemma leb_not_gtb : forall n m, m <= n = true -> ~(n < m = true).
+Proof.
+ intros n m; rewrite ltb_spec, leb_spec;omega.
+Qed.
+
+Lemma leb_negb_gtb : forall x y, x <= y = negb (y < x).
+Proof.
+ intros x y;apply Bool.eq_true_iff_eq;split;intros.
+ apply Bool.eq_true_not_negb;apply leb_not_gtb;trivial.
+ rewrite Bool.negb_true_iff, <- Bool.not_true_iff_false in H.
+ rewrite leb_spec; rewrite ltb_spec in H;omega.
+Qed.
+
+Lemma ltb_negb_geb : forall x y, x < y = negb (y <= x).
+Proof.
+ intros;rewrite leb_negb_gtb, Bool.negb_involutive;trivial.
+Qed.
+
+Lemma to_Z_sub_gt : forall x y, y <= x = true -> [|x - y|] = ([|x|] - [|y|])%Z.
+Proof.
+ intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
+   rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;omega.
+Qed.
+
+Lemma to_Z_sub_1 : forall x y, y < x = true -> ([| x - 1|] = [|x|] - 1)%Z.
+Proof.
+ intros;apply to_Z_sub_gt.
+ generalize (leb_ltb_trans _ _ _ (leb_0 y) H).
+ rewrite ltb_spec, leb_spec, to_Z_0, to_Z_1;auto with zarith.
+Qed.
+
+Lemma to_Z_sub_1_diff : forall x, x <> 0 -> ([| x - 1|] = [|x|] - 1)%Z.
+Proof.
+  intros x;rewrite not_0_ltb;apply to_Z_sub_1.
+Qed.
+
+Lemma to_Z_sub_1_0 : forall x, (0 < [|x|])%Z -> [|x - 1|] = ([|x|] - 1)%Z.
+Proof.
+ intros; apply (to_Z_sub_1 _ 0); rewrite ltb_spec; assumption.
+Qed.
+
+Lemma ltb_leb_sub1 : forall x i,  x <> 0 -> (i < x = true <-> i <= x - 1 = true).
+Proof.
+ intros x i Hdiff.
+ rewrite ltb_spec, leb_spec, to_Z_sub_1_diff;trivial.
+ split;auto with zarith.
+Qed.
 
 Lemma minus_1_lt i : (i == 0) = false -> i - 1 < i = true.
 Proof.
@@ -70,689 +192,908 @@ Proof.
     clear -H H1. change [|0|] with 0%Z. lia.
 Qed.
 
+Lemma lsr0_l i: 0 >> i = 0.
+Proof.
+ apply to_Z_inj.
+ generalize (lsr_spec 0 i).
+ rewrite to_Z_0, Zdiv_0_l; auto.
+Qed.
 
-Lemma foldi_down_ZInd2 :
-   forall A (P: Z -> A -> Prop) (f:int -> A -> A) max min a,
-   (max < min = true -> P ([|min|])%Z a) ->
-   (P ([|max|]+1)%Z a) ->
-   (forall i a, min <= i = true -> i <= max = true -> P ([|i|]+1)%Z a -> P [|i|] (f i a)) ->
-   P [|min|] (foldi_down f max min a).
-Proof.
- unfold foldi_down;intros A P f max min a Hlt;intros.
- set (P' z cont :=
-       if Zlt_bool z ([|min|]+1)%Z then cont = (fun a0 : A => a0)
-       else forall a, P z a -> P [|min|] (cont a)).
- assert (H1: P' ([|max|]+1)%Z (foldi_down_cont (fun (i : int) (cont : A -> A) (a0 : A) => cont (f i a0)) max
-                       min (fun a0 : A => a0))).
- apply foldi_down_cont_ZInd;intros;red.
- assert (H20: (z+1 < [|min|]+1)%Z).
- lia.
- rewrite Zlt_is_lt_bool in H20; rewrite H20;trivial.
- case_eq (Zlt_bool ([|i|]+1) ([|min|]+1));intros.
-  rewrite <- Zlt_is_lt_bool in H4;rewrite leb_spec in H1;elimtype False;lia.
- clear H4;revert H3;unfold P'.
- case_eq (Zlt_bool ([|i|] - 1 + 1) ([|min|]+1));intros;auto.
-  rewrite <- Zlt_is_lt_bool in H3; assert ([|i|] = [|min|]) by (rewrite leb_spec in H1;lia).
-  rewrite H4, <- H6. apply H0;trivial.
-  apply H4. replace ([|i|] - 1 + 1)%Z with [|i|] by lia. auto.
- revert H1;unfold P'.
- case_eq (Zlt_bool ([|max|]+1)%Z ([|min|]+1)%Z);auto.
- rewrite <- Zlt_is_lt_bool.
- intro H22; assert (H21: ([|max|] < [|min|])%Z). lia.
- rewrite <- ltb_spec in H21. intros;rewrite foldi_down_cont_lt;auto.
-Qed.
-
-
-Lemma foldi_down_Ind2 : forall A (P : int -> A -> Prop) f max min a,
-  (max < max_int = true) ->
-  (max < min = true -> P min a) ->
-  P (max+1) a ->
-  (forall i a, min <= i = true -> i <= max = true ->
-    P (i+1) a -> P i (f i a)) ->
-  P min (foldi_down f max min a).
-Proof.
-  intros A P f max min a H H0 H1 H2.
-  set (P' z a := (0 <= z < wB)%Z -> P (of_Z z) a).
-  assert (W:= to_Z_add_1 _ _ H).
-  assert (P' ([|min|])%Z (foldi_down f max min a)).
-  apply foldi_down_ZInd2;unfold P';intros.
-  rewrite of_to_Z;auto.
-  rewrite <- W, of_to_Z;auto.
-  rewrite of_to_Z. apply H2; trivial.
-  assert (i < max_int = true).
-  apply leb_ltb_trans with max; trivial.
-  rewrite <- (to_Z_add_1 _ _ H7) in H5. rewrite of_to_Z in H5. apply H5. apply to_Z_bounded.
-  unfold P' in H3; rewrite of_to_Z in H3;apply H3;apply to_Z_bounded.
-Qed.
-
-
-(** Lemmas about PArray.to_list *)
+Lemma lxor_lsr i1 i2 i: (i1 lxor i2) >> i = (i1 >> i) lxor (i2 >> i).
+Proof.
+ apply bit_ext; intros n.
+ rewrite lxor_spec, !bit_lsr, lxor_spec.
+ case (_ <= _); auto.
+Qed.
 
-Lemma to_list_In : forall {A} (t: array A) i,
-  i < length t = true -> In (t.[i]) (to_list t).
+Lemma bit_or_split i : i = (i>>1)<<1 lor bit i 0.
 Proof.
-  intros A t i H; unfold to_list; case_eq (0 == length t); intro Heq.
-  unfold is_true in H; rewrite ltb_spec in H; rewrite eqb_spec in Heq; rewrite <- Heq in H; rewrite to_Z_0 in H; pose (H1 := to_Z_bounded i); elimtype False; lia.
-  pose (P := fun j a => i < j = true \/ In (t .[ i]) a).
-  pose (H1:= foldi_down_Ind2 _ P); unfold P in H1.
-  assert (H2: i < 0 = true \/ In (t .[ i]) (foldi_down (fun (i0 : int) (l : list A) => t .[ i0] :: l) (length t - 1) 0 nil)).
-  apply H1.
-  rewrite ltb_spec; erewrite to_Z_sub_1; try eassumption.
-  pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; lia.
-  intro H2; elimtype False; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded (length t - 1)); lia.
-  left; unfold is_true; rewrite ltb_spec; rewrite (to_Z_add_1 _ max_int).
-  erewrite to_Z_sub_1; try eassumption.
-  unfold is_true in H; rewrite ltb_spec in H; lia.
-  rewrite ltb_spec; erewrite to_Z_sub_1; try eassumption.
-  pose (H2 := to_Z_bounded (length t)); change [|max_int|] with (wB-1)%Z; lia.
-  intros j a H2 H3 [H4|H4].
-  case_eq (i < j); intro Heq2.
-  left; reflexivity.
-  right; rewrite (lt_eq _ _ H4 Heq2); constructor; reflexivity.
-  right; constructor 2; assumption.
-  destruct H2 as [H2|H2]; try assumption.
-  unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; lia.
+ apply bit_ext.
+ intros n; rewrite lor_spec.
+ rewrite bit_lsl, bit_lsr, bit_b2i.
+ case (to_Z_bounded n); intros Hi _.
+ case (Zle_lt_or_eq _ _ Hi).
+ 2: replace 0%Z with [|0|]; auto; rewrite to_Z_eq.
+ 2: intros H; rewrite <-H.
+ 2: replace (0 < 1) with true; auto.
+ intros H; clear Hi.
+ case_eq (n == 0).
+ rewrite eqb_spec; intros H1; generalize H; rewrite H1; discriminate.
+ intros _; rewrite orb_false_r.
+ case_eq (n < 1).
+ rewrite ltb_spec, to_Z_1; intros HH; contradict HH; auto with zarith.
+ intros _.
+ generalize (@bit_M i n); case (_ <= _).
+ intros H1; rewrite H1; auto.
+ intros _.
+ case (to_Z_bounded n); intros H1n H2n.
+ assert (F1: [|n - 1|] = ([|n|] - 1)%Z).
+ rewrite sub_spec, Zmod_small; rewrite to_Z_1; auto with zarith.
+ generalize (add_le_r 1 (n - 1)); case (_ <= _); rewrite F1, to_Z_1; intros HH.
+ replace (1 + (n -1)) with n. change (bit i n = bit i n). reflexivity.
+ apply to_Z_inj; rewrite add_spec, F1, Zmod_small; rewrite to_Z_1;
+  auto with zarith.
+ rewrite bit_M; auto; rewrite leb_spec.
+ replace [|n|] with wB; try discriminate; auto with zarith.
 Qed.
 
-Lemma to_list_In_eq : forall {A} (t: array A) i x,
-  i < length t = true -> x = t.[i] -> In x (to_list t).
+Lemma lsr_is_even_eq : forall i j,
+  i >> 1 = j >> 1 ->
+  is_even i = is_even j ->
+  i = j.
 Proof.
-  intros A t i x Hi ->. now apply to_list_In.
+ intros;apply bit_ext.
+ intros n;destruct (reflect_eqb n 0).
+ rewrite <- (negb_involutive (bit i n)), <- (negb_involutive (bit j n)).
+ rewrite e, <- !is_even_bit, H0;trivial.
+ assert (W1 : [|n|] <> 0%Z) by (intros Heq;apply n0;apply to_Z_inj;trivial).
+ assert (W2 := to_Z_bounded n);clear n0.
+ assert (W3 : [|n-1|] = ([|n|] - 1)%Z).
+   rewrite sub_spec, to_Z_1, Zmod_small;trivial;omega.
+ assert (H1 : n = (n-1)+1).
+   apply to_Z_inj;rewrite add_spec, W3.
+   rewrite Zmod_small;rewrite to_Z_1; omega.
+ case_eq ((n-1) < digits); intro l.
+  rewrite ltb_spec in l.
+  rewrite H1, <- !bit_half, H; trivial; rewrite ltb_spec; trivial.
+ assert ((digits <= n) = true).
+  rewrite <- Bool.not_true_iff_false, ltb_spec in l; rewrite leb_spec;omega.
+ rewrite !bit_M;trivial.
 Qed.
 
-Lemma In_to_list : forall {A} (t: array A) x,
-  In x (to_list t) -> exists i, i < length t = true /\ x = t.[i].
+Lemma lsr1_bit : forall i k, bit i k >> 1 = 0.
 Proof.
-  intros A t x; unfold to_list; case_eq (0 == length t); intro Heq.
-  intro H; inversion H.
-  rewrite eqb_false_spec in Heq.
-  pose (P (_:int) l := In x l ->
-   exists i : int, (i < length t) = true /\ x = t .[ i]).
-  pose (H1 := foldi_down_Ind2 _ P (fun (i : int) (l : list A) => t .[ i] :: l) (length t - 1) 0); unfold P in H1; apply H1.
-  rewrite ltb_spec, to_Z_sub_1_diff; auto; change [|max_int|] with (wB-1)%Z; pose (H2 := to_Z_bounded (length t)); lia.
-  intros _ H; inversion H.
-  intro H; inversion H.
-  simpl; intros i a _ H2 IH [H3|H3].
-  exists i; split; auto; rewrite ltb_spec; rewrite leb_spec, to_Z_sub_1_diff in H2; auto; lia.
-  destruct (IH H3) as [j [H4 H5]]; exists j; auto.
+ intros;destruct (bit i k);trivial.
 Qed.
 
+Lemma is_even_or i j : is_even (i lor j) = is_even i && is_even j.
+Proof.
+ rewrite !is_even_bit, lor_spec; case bit; auto.
+Qed.
 
-(** Lemmas about PArray.mapi *)
+Lemma is_even_xor i j : is_even (i lxor j) = negb (xorb (is_even i) (is_even j)).
+Proof.
+ rewrite !is_even_bit, lxor_spec; do 2 case bit; auto.
+Qed.
 
-Lemma length_mapi : forall {A B} (f:int -> A -> B) t,
-  length (mapi f t) = length t.
+Lemma bit_xor_split: forall i : int, i = (i >> 1) << 1 lxor bit i 0.
 Proof.
-  unfold mapi; intros A B f t; case_eq (length t == 0).
-  rewrite Int63Properties.eqb_spec; intro Heq; rewrite Heq, length_make; auto.
-  rewrite eqb_false_spec; intro Heq; apply foldi_ind.
-  rewrite length_make, ltb_length; auto.
-  intros i a _ H1 H2; rewrite length_set; auto.
+ intros.
+ rewrite bit_or_split at 1.
+ apply lsr_is_even_eq.
+ rewrite lxor_lsr, lor_lsr, lsr1_bit, lxor0_r, lor0_r;trivial.
+ rewrite is_even_or, is_even_xor.
+ rewrite is_even_lsl_1;trivial.
+ rewrite (xorb_true_l (is_even (bit i 0))), negb_involutive;trivial.
 Qed.
 
+Lemma lxor_nilpotent: forall i, i lxor i = 0.
+Proof.
+ intros;apply bit_ext;intros.
+ rewrite lxor_spec, xorb_nilpotent, bit_0;trivial.
+Qed.
 
-Lemma default_mapi : forall {A B} (f:int -> A -> B) t,
-  default (mapi f t) = f (length t) (default t).
+Lemma int_ind : forall (P : int -> Prop),
+  P 0 ->
+  (forall i, (i < max_int) = true -> P i -> P (i + 1)) ->
+  forall i, P i.
 Proof.
-  unfold mapi; intros A B f t; case (length t == 0).
-  rewrite default_make; auto.
-  apply foldi_ind.
-  rewrite default_make; auto.
-  intros; rewrite default_set; auto.
+ intros P HP0 Hrec i.
+ assert (Bi := to_Z_bounded i).
+ destruct Bi as [ Bi0 Bi ].
+ rewrite <- of_to_Z.
+ rewrite Z2Nat.inj_lt in Bi; [ | exact Bi0 | lia ]; clear Bi0.
+ rewrite <- (Z2Nat.id (to_Z i)); [ | apply to_Z_bounded ].
+ revert Bi.
+ induction (Z.to_nat (to_Z i)); clear i.
+ intro; apply HP0.
+ rewrite Nat2Z.inj_lt.
+ rewrite Z2Nat.id; [ | generalize wB_pos; clear IHn; lia ].
+ rewrite Nat2Z.inj_succ.
+ rewrite <- Z.add_1_r.
+ rewrite <- (Nat2Z.id n) in IHn at 1.
+ rewrite <- Z2Nat.inj_lt in IHn; [ | clear IHn; lia | clear IHn; generalize wB_pos; lia ].
+ generalize (Z.of_nat n) IHn (Nat2Z.is_nonneg n); clear n IHn; intros z IHz Hz1 Hz2.
+ replace (of_Z (z + 1)) with (of_Z z + 1).
+ apply Hrec.
+ apply ltb_spec.
+ rewrite of_Z_spec, Z.mod_small, max_int_wB; lia.
+ apply IHz; lia.
+ apply to_Z_inj.
+ rewrite of_Z_spec, Z.mod_small by lia.
+ rewrite to_Z_add_1_wB, of_Z_spec.
+ rewrite Z.mod_small; lia.
+ rewrite of_Z_spec, Z.mod_small; lia.
 Qed.
 
-Lemma get_mapi : forall {A B} (f:int -> A -> B) t i,
-  i < length t = true -> (mapi f t).[i] = f i (t.[i]).
+Lemma int_ind_bounded : forall (P : int -> Prop) min max,
+  min <= max = true ->
+  P min ->
+  (forall i, min <= i = true -> i < max = true -> P i -> P (i + 1)) ->
+  P max.
 Proof.
-  intros A B f t i Hi; generalize (length_mapi f t); unfold mapi; case_eq (length t == 0).
-  rewrite Int63Properties.eqb_spec; intro Heq; rewrite Heq in Hi; eelim ltb_0; eassumption.
-  rewrite eqb_false_spec; intro Heq; pose (Hi':=Hi); replace (length t) with ((length t - 1) + 1) in Hi'.
-  generalize Hi'; apply (foldi_Ind _ (fun j a => (i < j) = true -> length a = length t -> a.[i] = f i (t.[i]))).
-  rewrite ltb_spec, (to_Z_sub_1 _ i); auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; lia.
-  intros H _; eelim ltb_0; eassumption.
-  intros H; eelim ltb_0; eassumption.
-  intros j a _ H1 IH H2 H3; rewrite length_set in H3; case_eq (j == i).
-  rewrite Int63Properties.eqb_spec; intro Heq2; subst i; rewrite get_set_same; auto; rewrite H3; auto.
-  rewrite eqb_false_spec; intro Heq2; rewrite get_set_other; auto; apply IH; auto; rewrite ltb_spec; rewrite ltb_spec, (to_Z_add_1 _ (length t)) in H2.
-  assert (H4: [|i|] <> [|j|]) by (intro H4; apply Heq2, to_Z_inj; auto); lia.
-  rewrite ltb_spec; rewrite leb_spec, (to_Z_sub_1 _ _ Hi) in H1; lia.
-  apply to_Z_inj; rewrite (to_Z_add_1 _ max_int).
-  rewrite to_Z_sub_1_diff; auto; lia.
-  rewrite ltb_spec, to_Z_sub_1_diff; auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; lia.
+ intros P min max Hle Hmin Hrec.
+ rewrite leb_spec in Hle.
+ assert (Bmin := to_Z_bounded min);assert (Bmax := to_Z_bounded max).
+ replace max with (min + (max - min)) by ring.
+ generalize (leb_refl (max - min)).
+ pattern (max - min) at 1 3.
+ apply int_ind.
+ intros _; replace (min + 0) with min by ring; exact Hmin.
+ intros i Hi1 IH; revert Hi1.
+ rewrite ltb_spec, leb_spec.
+ assert (Bi := to_Z_bounded i).
+ rewrite max_int_wB; intro Hi1.
+ replace (min + (i + 1)) with (min + i + 1) by ring.
+ rewrite to_Z_add_1_wB, sub_spec, Z.mod_small by lia.
+ intro Hi2; apply Hrec.
+ rewrite leb_spec, add_spec, Z.mod_small; lia.
+ rewrite ltb_spec, add_spec, Z.mod_small; lia.
+ apply IH.
+ rewrite leb_spec, sub_spec, Z.mod_small; lia.
 Qed.
 
+Definition foldi {A : Type} (f : int -> A -> A) (from to : int) (a : A) : A :=
+  let fix foldi_rec (n : nat) (a : A) : A :=
+    match n with
+      | O => a
+      | S m => foldi_rec m (f (to - of_Z (Z.of_nat n)) a)
+    end in
+  foldi_rec (Z.to_nat (to_Z to) - Z.to_nat (to_Z from))%nat a.
 
-Lemma get_mapi_outofbound : forall {A B} (f:int -> A -> B) t i,
-  i < length t = false -> (mapi f t).[i] = f (length t) (default t).
+Lemma foldi_ge : forall A f from to (a:A),
+  to <= from = true -> foldi f from to a = a.
 Proof.
-  intros A B f t i H1; rewrite get_outofbound.
-  apply default_mapi.
-  rewrite length_mapi; auto.
+ intros A f from to a; unfold foldi.
+ assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to).
+ rewrite leb_spec, Z2Nat.inj_le by lia; intro Hle.
+ replace (_ - _)%nat with O by lia; tauto.
+Qed.
+
+Lemma foldi_lt_l : forall A f from to (a:A),
+  from < to = true -> foldi f from to a = foldi f (from + 1) to (f from a).
+Proof.
+ intros A f from to a; rewrite ltb_spec; intro Hlt; unfold foldi.
+ assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to).
+ rewrite <- Nat.sub_succ.
+ rewrite Nat.sub_succ_l by (rewrite Nat.le_succ_l, <- Z2Nat.inj_lt; lia); f_equal.
+ rewrite to_Z_add_1_wB, Z.add_1_r, Z2Nat.inj_succ by lia; reflexivity.
+ f_equal.
+ rewrite <- Nat.sub_succ_l by (rewrite Nat.le_succ_l, <- Z2Nat.inj_lt; lia).
+ rewrite Nat.sub_succ, <- Z2Nat.inj_sub, Z2Nat.id by lia.
+ apply to_Z_inj; rewrite sub_spec, of_Z_spec, <- 2!sub_spec; f_equal; ring.
+Qed.
+
+Lemma foldi_lt_r : forall A f from to (a:A),
+  from < to = true -> foldi f from to a = f (to - 1) (foldi f from (to - 1) a).
+Proof.
+ intros A f from to a; rewrite ltb_spec; intro Hlt.
+ assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to).
+ replace from with (max_int - (max_int - from)) by ring.
+ revert a; pattern (max_int - from).
+ apply (int_ind_bounded _ (max_int - (to - 1))).
+ rewrite leb_spec, sub_spec, to_Z_sub_1_0, sub_spec, max_int_wB, 2!Z.mod_small by lia; lia.
+ intro a; replace (max_int - (max_int - (to - 1))) with (to - 1) by ring.
+ rewrite foldi_lt_l by (rewrite ltb_spec, to_Z_sub_1_0; lia).
+ ring_simplify (to - 1 + 1).
+ rewrite 2!foldi_ge by (rewrite leb_spec; lia); reflexivity.
+ intro i; rewrite leb_spec, ltb_spec, sub_spec, to_Z_sub_1_0, sub_spec, max_int_wB, 2!Z.mod_small by lia.
+ intros Hi1 Hi2 IH a.
+ rewrite foldi_lt_l by (rewrite ltb_spec, sub_spec, to_Z_add_1_wB, max_int_wB, Z.mod_small by lia; lia).
+ rewrite (foldi_lt_l _ _ (max_int - (i + 1))) by (rewrite ltb_spec, sub_spec, to_Z_add_1_wB, to_Z_sub_1_0, max_int_wB, Z.mod_small by lia; lia).
+ replace (max_int - (i + 1) + 1) with (max_int - i) by ring.
+ apply IH.
+Qed.
+
+Lemma foldi_ind : forall A (P : int -> A -> Prop) f from to a,
+  from <= to = true -> P from a ->
+  (forall i a, from <= i = true -> i < to = true -> P i a -> P (i + 1) (f i a)) ->
+  P to (foldi f from to a).
+Proof.
+  intros A P f from to a Hle Hfrom IH.
+  assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to).
+  pattern to; apply (int_ind_bounded _ from).
+  exact Hle.
+  rewrite foldi_ge by (rewrite leb_spec; lia).
+  exact Hfrom.
+  intro i; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, ltb_spec; intros Hi1 Hi2; rewrite (foldi_lt_r _ _ _ (i + 1)) by (rewrite ltb_spec, to_Z_add_1_wB; lia).
+  ring_simplify (i + 1 - 1); apply IH; [ rewrite leb_spec; exact Hi1 | rewrite ltb_spec; exact Hi2 ].
+Qed.
+
+Lemma foldi_ind2 : forall A B (P : int -> A -> B -> Prop) f1 f2 from to a1 a2,
+  from <= to = true -> P from a1 a2 ->
+  (forall i a1 a2, from <= i = true -> i < to = true -> P i a1 a2 -> P (i + 1) (f1 i a1) (f2 i a2)) ->
+  P to (foldi f1 from to a1) (foldi f2 from to a2).
+Proof.
+  intros A B P f1 f2 from to a1 a2 Hle Hfrom IH.
+  assert (Bfrom := to_Z_bounded from); assert (Bto := to_Z_bounded to).
+  pattern to; apply (int_ind_bounded _ from).
+  exact Hle.
+  rewrite 2!foldi_ge by (rewrite leb_spec; lia).
+  exact Hfrom.
+  intro i; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, ltb_spec; intros Hi1 Hi2; rewrite 2!(foldi_lt_r _ _ _ (i + 1)) by (rewrite ltb_spec, to_Z_add_1_wB; lia).
+  ring_simplify (i + 1 - 1); apply IH; [ rewrite leb_spec; exact Hi1 | rewrite ltb_spec; exact Hi2 ].
 Qed.
 
+Lemma foldi_eq_compat : forall A (f1 f2:int -> A -> A) min max a,
+  (forall i a, min <= i = true -> i < max = true -> f1 i a = f2 i a) ->
+  foldi f1 min max a = foldi f2 min max a.
+Proof.
+ intros A f1 f2 min max a Hf.
+ assert (Bmin := to_Z_bounded min); assert (Bmax := to_Z_bounded max).
+ case (Z.lt_ge_cases [|min|] [|max|]); [ intro Hlt | intro Hle ].
+ apply (foldi_ind2 _ _ (fun _ a b => a = b)); [ rewrite leb_spec; lia | reflexivity | ].
+ intros i a1 a2 Hi1 Hi2 Heq; rewrite Heq; apply Hf; assumption.
+ rewrite 2!foldi_ge by (rewrite leb_spec; lia); reflexivity.
+Qed.
 
-(** Custom fold_left and fold_right *)
+(** Lemmas about to_list *)
 
-Definition afold_left A B default (OP : A -> A -> A) (F : B -> A) (V : array B) :=
-  let n := PArray.length V in
-  if n == 0 then default
-  else foldi (fun i a => OP a (F (V.[i]))) 1 (n-1) (F (V.[0])).
+Definition to_list {A : Type} (t : array A) :=
+  List.rev (foldi (fun i l => t.[i] :: l)%list 0 (length t) nil).
 
+Lemma foldi_to_list : forall A B (f : A -> B -> A) a e,
+ foldi (fun i x => f x (a.[i])) 0 (length a) e = fold_left f (to_list a) e.
+Proof.
+  intros A B f a e; unfold to_list.
+  rewrite <- fold_left_rev_right, rev_involutive.
+  apply (foldi_ind2 _ _ (fun _ a b => a = fold_right (fun y x => f x y) e b)).
+  apply leb_0.
+  reflexivity.
+  intros i x l _ Hi IH.
+  simpl; f_equal; exact IH.
+Qed.
 
-Definition afold_right A B default (OP : A -> A -> A) (F : B -> A) (V : array B) :=
-  let n := PArray.length V in
-  if n == 0 then default else
-    if n <= 1 then F (V.[0])
-    else foldi_down (fun i b => OP (F (V.[i])) b) (n-2) 0 (F (V.[n-1])).
+Lemma to_list_In : forall {A} (t: array A) i,
+  i < length t = true -> In (t.[i]) (to_list t).
+  intros A t i; assert (Bt := to_Z_bounded (length t)); assert (Bi := to_Z_bounded i); rewrite ltb_spec; unfold to_list.
+  rewrite <- in_rev.
+  apply foldi_ind.
+  rewrite leb_spec, to_Z_0; lia.
+  rewrite to_Z_0; lia.
+  intros j l _; assert (Bj := to_Z_bounded j).
+  rewrite ltb_spec; intros Hj IH.
+  rewrite to_Z_add_1_wB by lia; intro Hij.
+  case (reflect_eqb j i); [ intro Heq; rewrite Heq; clear Heq | rewrite <- to_Z_eq; intro Hneq ].
+  apply in_eq.
+  apply in_cons.
+  apply IH.
+  lia.
+Qed.
 
+Lemma to_list_In_eq : forall {A} (t: array A) i x,
+  i < length t = true -> x = t.[i] -> In x (to_list t).
+Proof.
+  intros A t i x Hi ->. now apply to_list_In.
+Qed.
 
-(** Some properties about afold_left *)
+Lemma In_to_list : forall {A} (t: array A) x,
+  In x (to_list t) -> exists i, i < length t = true /\ x = t.[i].
+Proof.
+  intros A t x; assert (Bt := to_Z_bounded (length t)); unfold to_list.
+  rewrite <- in_rev.
+  set (a := foldi _ _ _ _); pattern (length t) at 0, a; subst a; apply foldi_ind.
+  rewrite leb_spec, to_Z_0; lia.
+  intro H; elim (in_nil H).
+  intros i a _; assert (Bi := to_Z_bounded i); rewrite ltb_spec; intros Hi IH.
+  intro Hin; case (in_inv Hin); clear Hin; [ | exact IH ].
+  intro H; rewrite <- H; clear H.
+  exists i.
+  split; [ rewrite ltb_spec; lia | reflexivity ].
+Qed.
 
-Lemma afold_left_eq :
-  forall A B OP def (F1 F2 : A -> B) V1 V2,
-    length V1 = length V2 ->
-    (forall i, i < length V1 = true -> F1 (V1.[i]) = F2 (V2.[i])) ->
-    afold_left _ _ def OP F1 V1 = afold_left _ _ def OP F2 V2.
+(** Lemmas about amapi/amap *)
+
+Definition amapi {A B:Type} (f:int->A->B) (t:array A) :=
+  let l := length t in
+  foldi (fun i tb => tb.[i <- f i (t.[i])]) 0 l (make l (f l (default t))).
+
+Definition amap {A B:Type} (f:A->B) := amapi (fun _ => f).
+
+Lemma length_amapi : forall {A B} (f:int -> A -> B) t,
+  length (amapi f t) = length t.
 Proof.
-  unfold afold_left;intros. rewrite <- H.
-  destruct (Int63Properties.reflect_eqb (length V1) 0);trivial.
-  rewrite (H0 0); [ |  unfold is_true;rewrite <- not_0_ltb;trivial].
-  apply foldi_eq_compat;intros;rewrite H0;trivial.
-  unfold is_true;rewrite ltb_leb_sub1;trivial.
+  unfold amapi; intros A B f t.
+  assert (Bt := to_Z_bounded (length t)).
+  apply (foldi_ind _ (fun _ a => length a = length t)).
+  apply leb_0.
+  rewrite length_make, leb_length by reflexivity; reflexivity.
+  intros i a _; assert (Bi := to_Z_bounded i).
+  rewrite ltb_spec; intros Hi IH.
+  rewrite length_set; exact IH.
 Qed.
 
+Lemma length_amap : forall {A B} (f:A -> B) t,
+  length (amap f t) = length t.
+Proof.
+  intros; unfold amap; apply length_amapi.
+Qed.
 
-Definition afoldi_left {A B:Type} default (OP : int -> A -> A -> A) (F : B -> A) (V : array B) :=
-  let n := PArray.length V in
-    if n == 0 then default
-      else foldi (fun i a => OP i a (F (V.[i]))) 1 (n-1) (F (V.[0])).
+Lemma default_amapi : forall {A B} (f:int -> A -> B) t,
+  default (amapi f t) = f (length t) (default t).
+Proof.
+  unfold amapi; intros A B f t.
+  assert (Bt := to_Z_bounded (length t)).
+  apply (foldi_ind _ (fun i a => default a = f (length t) (default t))).
+  apply leb_0.
+  rewrite default_make by reflexivity; reflexivity.
+  intros i a _; assert (Bi := to_Z_bounded i).
+  rewrite ltb_spec; intros Hi IH.
+  rewrite default_set; exact IH.
+Qed.
 
+Lemma default_amap : forall {A B} (f:A -> B) t,
+  default (amap f t) = f (default t).
+Proof.
+  intros; unfold amap; apply default_amapi.
+Qed.
 
-Lemma afoldi_left_Ind :
-  forall {A B: Type} (P : int -> A -> Prop) default (OP : int -> A -> A -> A) (F : B -> A) (t:array B),
-    if length t == 0 then
-      True
-    else
-      (forall a i, i < length t = true -> P i a -> P (i+1) (OP i a (F (t.[i])))) ->
-      P 1 (F (t.[0])) ->
-      P (length t) (afoldi_left default OP F t).
+Lemma get_amapi : forall {A B} (f:int -> A -> B) t i,
+  i < length t = true -> (amapi f t).[i] = f i (t.[i]).
 Proof.
-  intros A B P default OP F t; case_eq (length t == 0).
-  intros; exact I.
-  intros Heq H1 H2; unfold afoldi_left; rewrite Heq;
-    assert (H: (length t - 1) + 1 = length t) by ring.
-  rewrite <- H 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.
-  intro H3; rewrite H3 in Heq; discriminate.
-  intro Hlt; assert (H3: length t - 1 = 0).
-  rewrite ltb_spec, to_Z_1 in Hlt; apply to_Z_inj; rewrite to_Z_0; pose (H3 := to_Z_bounded (length t - 1)); lia.
-  rewrite H3; assumption.
-  intros i a H3 H4; apply H1; trivial.
-  rewrite ltb_leb_sub1; auto.
-  intro H5; rewrite H5 in Heq; discriminate.
+  intros A B f t.
+  assert (Bt := to_Z_bounded (length t)).
+  intro i; assert (Bi := to_Z_bounded i).
+  rewrite ltb_spec; intro Hi.
+  generalize (length_amapi f t); unfold amapi; revert Hi.
+  set (a := foldi _ _ _ _); pattern (length t) at 1, a; subst a; apply foldi_ind.
+  rewrite leb_spec, to_Z_0; lia.
+  rewrite to_Z_0; lia.
+  intros j a _; assert (Bj := to_Z_bounded j).
+  rewrite ltb_spec; intros Hj IH.
+  rewrite to_Z_add_1_wB by lia; intro Hij.
+  rewrite length_set; case (reflect_eqb j i); [ intro Heq; rewrite Heq | intro Hneq ]; intro Hlength.
+  rewrite get_set_same by (rewrite Hlength, ltb_spec; lia); reflexivity.
+  rewrite get_set_other by exact Hneq.
+  apply IH; [ rewrite <- to_Z_eq in Hneq; lia | exact Hlength ].
 Qed.
 
+Lemma get_amap : forall {A B} (f:A -> B) t i,
+  i < length t = true -> (amap f t).[i] = f (t.[i]).
+Proof.
+  intros; unfold amap; apply get_amapi; assumption.
+Qed.
 
-Lemma afold_left_Ind :
-  forall A B (P : int -> A -> Prop) default (OP : A -> A -> A) (F : B -> A) (t:array B),
-    if length t == 0 then
-      True
-    else
-      (forall a i, i < length t = true -> P i a -> P (i+1) (OP a (F (t.[i])))) ->
-      P 1 (F (t.[0])) ->
-      P (length t) (afold_left A B default OP F t).
+Lemma get_amapi_outofbound : forall {A B} (f:int -> A -> B) t i,
+  i < length t = false -> (amapi f t).[i] = f (length t) (default t).
 Proof.
-  intros A B P default OP F t;
-    apply (afoldi_left_Ind P default (fun _ => OP)); trivial.
+  intros A B f t i H1; rewrite get_outofbound.
+  apply default_amapi.
+  rewrite length_amapi; auto.
 Qed.
 
+Lemma get_amap_outofbound : forall {A B} (f:A -> B) t i,
+  i < length t = false -> (amap f t).[i] = f (default t).
+Proof.
+  intros; unfold amap; apply get_amapi_outofbound; assumption.
+Qed.
 
-Lemma afold_left_ind :
-  forall A B (P : A -> Prop) default (OP : A -> A -> A) (F : B -> A) (t:array B),
-    (forall a i, i < length t = true -> P a -> P (OP a (F (t.[i])))) ->
-    P default -> P (F (t.[0])) ->
-    P (afold_left _ _ default OP F t).
+Lemma to_list_amap : forall A B (f : A -> B) t, to_list (amap f t) = List.map f (to_list t).
 Proof.
-  intros A B P default OP F t H1 H2 H4.
-  pose (H3 := afold_left_Ind A B (fun _ => P) default OP F t).
-  case_eq (length t == 0); intro Heq.
-  unfold afold_left; rewrite Heq; assumption.
-  rewrite Heq in H3; apply H3; trivial.
+  intros A B f t.
+  assert (Bt := to_Z_bounded (length t)).
+  unfold to_list; rewrite length_amap.
+  rewrite map_rev; f_equal.
+  apply (foldi_ind2 _ _ (fun i a b  => a = map f b)).
+  apply leb_0.
+  reflexivity.
+  intros i a1 a2 _; assert (Bi := to_Z_bounded i).
+  rewrite ltb_spec; intros Hi IH.
+  simpl; f_equal.
+  apply get_amap.
+  rewrite ltb_spec; lia.
+  apply IH.
 Qed.
 
+(** Some properties about afold_left *)
+
+Definition afold_left A default (OP : A -> A -> A) (V : array A) :=
+  if length V == 0 then default
+  else foldi (fun i a => OP a (V.[i])) 1 (length V) (V.[0]).
 
-Lemma afold_left_spec : forall A B (f:B -> A) args op e,
+Lemma afold_left_spec : forall A args op (e : A),
   (forall a, op e a = a) ->
-  afold_left _ _ e op f args =
-  fold_left (fun a v  => op a (f v)) e args.
+  afold_left _ e op args =
+  foldi (fun i a => op a (args.[i])) 0 (length args) e.
   Proof.
-    unfold afold_left, fold_left;intros A B f args op neu H10.
+    unfold afold_left;intros A args op neu H10.
     destruct (reflect_eqb (length args) 0) as [e|n].
-    rewrite e, eqb_refl;trivial.
-    apply not_eq_sym in n;rewrite (eqb_false_complete _ _ n).
-    case_eq (0 < (length args - 1));intros H.
-    rewrite foldi_lt with (from := 0);trivial.
-    rewrite H10; auto.
-    assert (H0: (0 <> [|length args|])%Z).
-    intros Heq;apply n;apply to_Z_inj;trivial.
-    assert (H1: length args = 1).
-    generalize (to_Z_bounded (length args)).
-    rewrite <- not_true_iff_false, ltb_spec, to_Z_0, to_Z_sub_1_diff in H;auto.
-    intros;apply to_Z_inj;rewrite to_Z_1;lia.
-    rewrite H1; change (1 - 1) with 0; rewrite (foldi_eq _ _ 0 0); auto.
+    rewrite e, foldi_ge by reflexivity;trivial.
+    rewrite (foldi_lt_l _ _ 0) by (apply not_0_ltb; assumption).
+    f_equal; rewrite H10; reflexivity.
   Qed.
 
+Lemma afold_left_eq :
+  forall A OP (def : A) V1 V2,
+    length V1 = length V2 ->
+    (forall i, i < length V1 = true -> V1.[i] = V2.[i]) ->
+    afold_left _ def OP V1 = afold_left _ def OP V2.
+Proof.
+  intros A OP def V1 V2 Heqlength HeqV.
+  assert (BV1 := to_Z_bounded (length V1)).
+  unfold afold_left.
+  rewrite <- Heqlength.
+  case (reflect_eqb (length V1) 0).
+  reflexivity.
+  rewrite <- to_Z_eq, to_Z_0; intro Hneq.
+  rewrite <- HeqV by (rewrite ltb_spec, to_Z_0; lia).
+  apply (foldi_ind2 _ _ (fun i a b => a = b)).
+  rewrite leb_spec, to_Z_1; lia.
+  reflexivity.
+  intros i a1 a2; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, to_Z_1; intro Hi1.
+  rewrite ltb_spec by lia; intros Hi2 IH.
+  f_equal;[ exact IH | apply HeqV; rewrite ltb_spec; lia ].
+Qed.
+
+Lemma afold_left_ind : forall A OP def V (P : int -> A -> Prop),
+  (length V = 0 -> P 0 def) ->
+  (0 < length V = true -> P 1 (V.[0])) ->
+  (forall a i, 0 < i = true -> i < length V = true -> P i a -> P (i + 1) (OP a (V.[i]))) ->
+  P (length V) (afold_left A def OP V).
+Proof.
+  intros A OP def V P HP0 HP1 HPOP.
+  assert (BV := to_Z_bounded (length V)).
+  unfold afold_left.
+  case (reflect_eqb (length V) 0); [ intro Heq; rewrite Heq; tauto | intro Hneq ].
+  rewrite <- to_Z_eq, to_Z_0 in Hneq.
+  apply foldi_ind.
+  rewrite leb_spec, to_Z_1; lia.
+  apply HP1; rewrite ltb_spec, to_Z_0; lia.
+  intros i a; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, to_Z_1, ltb_spec; intros Hi1 Hi2 IH.
+  apply HPOP; [ rewrite ltb_spec, to_Z_0; lia | rewrite ltb_spec; lia | exact IH ].
+Qed.
 
 (** Some properties about afold_right *)
 
-Lemma afold_right_eq :
-  forall A B OP def (F1 F2 : A -> B) V1 V2,
-    length V1 = length V2 ->
-    (forall i, i < length V1 = true -> F1 (V1.[i]) = F2 (V2.[i])) ->
-    afold_right _ _ def OP F1 V1 = afold_right _ _ def OP F2 V2.
-Proof.
-  unfold afold_right;intros.
-  rewrite <- H.
-  destruct (Int63Properties.reflect_eqb (length V1) 0);trivial.
-  destruct (reflect_leb (length V1) 1);intros.
-  apply H0;unfold is_true;rewrite ltb_leb_sub1;trivial. apply leb_0.
-  assert (length V1 - 1 < length V1 = true).
-  rewrite ltb_leb_sub1;auto using leb_refl.
-  rewrite (H0 (length V1 - 1));trivial.
-  apply foldi_down_eq_compat;intros;rewrite H0;trivial.
-  unfold is_true;rewrite ltb_leb_sub1;[ | trivial].
-  apply ltb_leb_sub1;trivial.
-  revert n0 H3;rewrite ltb_spec, leb_spec, to_Z_1, sub_spec.
-  change [|2|] with 2%Z.
-  intros HH;assert (W:= to_Z_bounded (length V1));rewrite Zmod_small;lia.
-Qed.
-
-
-Definition afoldi_right {A B:Type} default (OP : int -> A -> A -> A) (F : B -> A) (V : array B) :=
-  let n := PArray.length V in
-    if n == 0 then default
-      else if n <= 1 then F (V .[ 0])
-        else foldi_down (fun i a => OP i (F (V.[i])) a) (n-2) 0 (F (V.[n-1])).
-
-
-Lemma afoldi_right_Ind :
-  forall {A B: Type} (P : int -> A -> Prop) default (OP : int -> A -> A -> A) (F : B -> A) (t:array B),
-    if length t <= 1 then
-      True
-    else
-      (forall a i, i < length t - 1 = true -> P (i+1) a -> P i (OP i (F (t.[i])) a)) ->
-      P ((length t)-1) (F (t.[(length t)-1])) ->
-      P 0 (afoldi_right default OP F t).
-Proof.
-  intros A B P default OP F t; case_eq (length t <= 1).
-  intros; exact I.
-  intros Heq H1 H2; unfold afoldi_right. replace (length t == 0) with false.
-  rewrite Heq.
-  set (P' z a := P (of_Z (z + 1)) a).
-  change (P' ([|0|] - 1)%Z (foldi_down (fun (i : int) (a : A) => OP i (F (t .[ i])) a) (length t - 2) 0 (F (t .[ length t - 1])))).
-  apply foldi_down_ZInd;unfold P'.
-  intros Hlt;elim (ltb_0 _ Hlt).
-  replace (length t - 2) with (length t - 1 - 1) by ring.
-  rewrite to_Z_sub_1_diff.
-  ring_simplify ([|length t - 1|] - 1 + 1)%Z;rewrite of_to_Z;trivial.
-  assert (H10: (1 < length t) = true) by (rewrite ltb_negb_geb, Heq; auto).
-  intro H11. rewrite ltb_spec in H10. assert (H12: [|length t - 1|] = 0%Z) by (rewrite H11; auto). change [|1|] with (1%Z) in H10. rewrite to_Z_sub_1_diff in H12; [lia| ]. intro H13. assert (H14: [|length t|] = 0%Z) by (rewrite H13; auto). lia.
-  intros;ring_simplify ([|i|] - 1 + 1)%Z;rewrite of_to_Z;auto.
-  assert (i < length t - 1 = true).
-    rewrite ltb_spec. rewrite leb_spec in H0. replace (length t - 2) with (length t - 1 - 1) in H0 by ring. rewrite to_Z_sub_1_diff in H0; [lia| ]. intro H4. assert (H5: [|length t - 1|] = 0%Z) by (rewrite H4; auto). assert (H6: 1 < length t = true) by (rewrite ltb_negb_geb, Heq; auto). rewrite ltb_spec in H6. change ([|1|]) with (1%Z) in H6. rewrite to_Z_sub_1_diff in H5; [lia| ]. intro H7. assert (H8: [|length t|] = 0%Z) by (rewrite H7; auto). lia.
-  apply H1; [trivial| ].
-  rewrite <-(to_Z_add_1 _ _ H4), of_to_Z in H3;auto.
-  symmetry. rewrite eqb_false_spec. intro H. rewrite H in Heq. discriminate.
-Qed.
-
-
-Lemma afold_right_Ind :
-  forall A B (P : int -> A -> Prop) default (OP : A -> A -> A) (F : B -> A) (t:array B),
-    if length t <= 1 then
-      True
-    else
-      (forall a i, i < length t - 1 = true -> P (i+1) a -> P i (OP (F (t.[i])) a)) ->
-      P ((length t)-1) (F (t.[(length t)-1])) ->
-      P 0 (afold_right A B default OP F t).
-Proof.
-  intros A B P default OP F t;
-    apply (afoldi_right_Ind P default (fun _ => OP) F).
-Qed.
-
-
-Lemma afold_right_ind :
-  forall A B (P : A -> Prop) default (OP : A -> A -> A) (F : B -> A) (t:array B),
-    (forall a i, i < length t - 1 = true -> P a -> P (OP (F (t.[i])) a)) ->
-    P default -> P (F (t.[length t - 1])) ->
-    P (afold_right _ _ default OP F t).
-Proof.
-  intros A B P default OP F t H1 H2 H4.
-  pose (H3 := afold_right_Ind A B (fun _ => P) default OP F t).
-  unfold afold_right. case_eq (length t == 0); auto. intro H10. assert (H := H10). rewrite eqb_false_spec in H. case_eq (length t <= 1); intro Heq.
-  replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). lia. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto.
-Qed.
-
-
-Lemma afold_right_ind_nonempty :
-  forall A B (P : A -> Prop) default (OP : A -> A -> A) (F : B -> A) (t:array B),
-    (forall a i, i < length t - 1 = true -> P a -> P (OP (F (t.[i])) a)) ->
-    0 < length t = true -> P (F (t.[length t - 1])) ->
-    P (afold_right _ _ default OP F t).
-Proof.
-  intros A B P default OP F t H1 H2 H4.
-  pose (H3 := afold_right_Ind A B (fun _ => P) default OP F t).
-  unfold afold_right. assert (H10 : length t == 0 = false) by (rewrite eqb_false_spec; intro H; rewrite H in H2; discriminate). rewrite H10. assert (H := H10). rewrite eqb_false_spec in H. case_eq (length t <= 1); intro Heq.
-  replace 0 with (length t - 1); auto. apply to_Z_inj. rewrite to_Z_sub_1_diff; auto. rewrite leb_spec in Heq. assert (H5 := leb_0 (length t)). rewrite leb_spec in H5. change [|0|] with 0%Z in *. change [|1|] with 1%Z in Heq. assert (H6 : [|length t|] <> 0%Z) by (intro H6; elim H; apply to_Z_inj; auto). lia. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto.
-Qed.
-
-
-Lemma afold_right_spec : forall A B (f:B -> A) args op e,
+Definition afold_right A default (OP : A -> A -> A) (V : array A) :=
+  if length V == 0 then default
+  else foldi (fun i => OP (V.[length V - 1 - i])) 1 (length V) (V.[length V - 1]).
+
+Lemma afold_right_spec : forall A args op (e : A),
   (forall a, op a e = a) ->
-  afold_right _ _ e op f args =
-  fold_right (fun v a => op (f v) a) args e.
+  afold_right _ e op args =
+  foldi (fun i a => op (args.[length args - 1 - i]) a) 0 (length args) e.
   Proof.
-    unfold afold_right, fold_right;intros A B f args op neu H10.
+    unfold afold_right;intros A args op neu H10.
+    assert (Bargs := to_Z_bounded (length args)).
     destruct (reflect_eqb (length args) 0) as [e|n].
-    rewrite e, eqb_refl;trivial.
-    apply not_eq_sym in n;rewrite (eqb_false_complete _ _ n).
-    case_eq (length args <= 1); intro Heq.
-    assert (H11: length args = 1).
-    apply to_Z_inj. rewrite leb_spec in Heq. assert (H11: 0%Z <> [|length args|]) by (intro H; elim n; apply to_Z_inj; auto). change [|1|] with (1%Z) in *. assert (H12 := leb_0 (length args)). rewrite leb_spec in H12. change [|0|] with 0%Z in H12. lia.
-    rewrite H11, foldi_down_eq; auto.
-    assert (H11: 1 < length args = true) by (rewrite ltb_negb_geb, Heq; auto). replace (foldi_down (fun (i : int) (b : A) => op (f (args .[ i])) b) (length args - 1) 0 neu) with (foldi_down (fun (i : int) (b : A) => op (f (args .[ i])) b) (length args - 1 - 1) 0 (op (f (args .[ length args - 1])) neu)).
-    replace (length args - 1 - 1) with (length args - 2) by ring. rewrite H10. auto.
-    symmetry. apply foldi_down_gt. rewrite ltb_spec. change [|0|] with 0%Z. rewrite to_Z_sub_1_diff; auto. rewrite ltb_spec in H11. change [|1|] with 1%Z in H11. lia.
+    rewrite e, foldi_ge by reflexivity;trivial.
+    change 1 with (0 + 1) at 2.
+    replace (length args - 1) with (length args - 1 - 0) at 1 by ring.
+    rewrite <- (H10 (args.[length args - 1 - 0])).
+    rewrite <- (foldi_lt_l _ (fun i => op (args.[length args - 1 - i]))) by (apply not_0_ltb; assumption).
+    apply foldi_eq_compat; intros; reflexivity.
   Qed.
 
+Lemma afold_right_eq :
+  forall A OP (def : A) V1 V2,
+    length V1 = length V2 ->
+    (forall i, i < length V1 = true -> V1.[i] = V2.[i]) ->
+    afold_right _ def OP V1 = afold_right _ def OP V2.
+Proof.
+  intros A OP def V1 V2 Heqlength HeqV.
+  assert (BV1 := to_Z_bounded (length V1)).
+  unfold afold_right.
+  rewrite <- Heqlength.
+  case (reflect_eqb (length V1) 0); [ reflexivity | intro Hneq ].
+  rewrite <- to_Z_eq, to_Z_0 in Hneq.
+  rewrite <- HeqV by (rewrite ltb_spec, to_Z_sub_1_0; lia).
+  apply (foldi_ind2 _ _ (fun i a b => a = b)).
+  rewrite leb_spec, to_Z_1; lia.
+  reflexivity.
+  intros i a1 a2; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, to_Z_1; intro Hi1.
+  rewrite ltb_spec by lia; intros Hi2 IH.
+  f_equal;[ apply HeqV; rewrite ltb_spec, sub_spec, to_Z_sub_1_0, Z.mod_small; lia | exact IH ].
+Qed.
+
+Lemma afold_right_ind : forall A OP def V (P : int -> A -> Prop),
+  (length V = 0 -> P 0 def) ->
+  (0 < length V = true -> P (length V - 1) (V.[length V - 1])) ->
+  (forall a i, 0 < i = true -> i < length V = true -> P i a -> P (i - 1) (OP (V.[i - 1]) a)) ->
+  P 0 (afold_right A def OP V).
+Proof.
+  intros A OP def V P HP0 HP1 HPOP.
+  assert (BV := to_Z_bounded (length V)).
+  unfold afold_right.
+  case (reflect_eqb (length V) 0); [ intro Heq; apply HP0; exact Heq | intro Hneq ].
+  rewrite <- to_Z_eq, to_Z_0 in Hneq.
+  replace 0 with (length V - length V) at 1 by ring.
+  apply (foldi_ind _ (fun i a => P (length V - i) a)).
+  rewrite leb_spec, to_Z_1; lia.
+  apply HP1; rewrite ltb_spec, to_Z_0; lia.
+  intros i a; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, to_Z_1, ltb_spec; intros Hi1 Hi2 IH.
+  replace (length V - (i + 1)) with (length V - i - 1) by ring.
+  replace (length V - 1 - i) with (length V - i - 1) by ring.
+  apply HPOP; [ rewrite ltb_spec, to_Z_0, sub_spec, Z.mod_small; lia | rewrite ltb_spec, sub_spec, Z.mod_small; lia | exact IH ].
+Qed.
 
 (** Application to our uses of afold_left and afold_right *)
 (* Case andb *)
 
-Lemma afold_left_andb_false : forall A i a f,
+Lemma afold_left_andb_false : forall i a,
   i < length a = true ->
-  f (a .[ i]) = false ->
-  afold_left bool A true andb f a = false.
+  a .[ i] = false ->
+  afold_left bool true andb a = false.
 Proof.
-  intros A i a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => (i < j) = true -> f (a .[ i]) = false -> t = false)).
-  intros b j H1 H2 H3 H4; case_eq (i == j).
-  rewrite Int63Properties.eqb_spec; intro; subst i; rewrite H4, andb_false_r; auto.
-  rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); lia.
-  intro H; eelim ltb_0; eassumption.
+  intros i a; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i).
+  rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
+  apply leb_0.
+  rewrite ltb_spec, to_Z_0; lia.
+  intros j b _; assert (Bj := to_Z_bounded j).
+  rewrite 2!ltb_spec; intros Hj IH.
+  rewrite ltb_spec, to_Z_add_1_wB by lia; intro Hij.
+  case (reflect_eqb i j).
+  intros Heq Hai; rewrite <- Heq, Hai; apply andb_false_r.
+  rewrite <- to_Z_eq; intros Hneq Hai.
+  rewrite IH; [ apply andb_false_l | lia | exact Hai ].
 Qed.
 
-
-Lemma afold_left_andb_false_inv : forall A a f,
-  afold_left bool A true andb f a = false ->
-  exists i, (i < length a = true) /\ (f (a .[ i]) = false).
+Lemma afold_left_andb_false_inv : forall a,
+  afold_left bool true andb a = false ->
+  exists i, (i < length a = true) /\ (a .[ i] = false).
 Proof.
-  intros A a f; rewrite afold_left_spec; auto; apply fold_left_ind; try discriminate.
-  intros b i H1; case b; simpl.
-  intros _ H2; exists i; auto.
-  intros H2 _; destruct (H2 (refl_equal false)) as [j [H3 H4]]; exists j; auto.
+  intro a; assert (Ba := to_Z_bounded (length a)).
+  rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
+  apply leb_0.
+  discriminate.
+  intros i b _; assert (Bi := to_Z_bounded i).
+  rewrite ltb_spec; intros Hj IH.
+  destruct b.
+  rewrite andb_true_l; intro H; exists i; rewrite H.
+  split; [ rewrite ltb_spec, to_Z_add_1_wB; lia | reflexivity ].
+  generalize (IH eq_refl); clear IH; intros [ j [ Hji Haj ] ] _.
+  rewrite ltb_spec in Hji; exists j.
+  split; [ rewrite ltb_spec, to_Z_add_1_wB; lia | exact Haj ].
 Qed.
 
-
-Lemma afold_left_andb_true : forall A a f,
-  (forall i, i < length a = true -> f (a.[i]) = true) ->
-  afold_left bool A true andb f a = true.
+Lemma afold_left_andb_true : forall a,
+  (forall i, i < length a = true -> a.[i] = true) ->
+  afold_left bool true andb a = true.
 Proof.
-  intros A a f H; rewrite afold_left_spec; auto; apply fold_left_ind; trivial; intros b j H1 H2; rewrite H2; simpl; rewrite H; trivial.
+  intros a H.
+  rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
+  apply leb_0.
+  reflexivity.
+  intros b j _ H1 H2; rewrite H2; simpl; rewrite H; trivial.
 Qed.
 
-
-Lemma afold_left_andb_true_inv : forall A a f,
-  afold_left bool A true andb f a = true ->
-  forall i, i < length a = true -> f (a.[i]) = true.
+Lemma afold_left_andb_true_inv : forall a,
+  afold_left bool true andb a = true ->
+  forall i, i < length a = true -> a.[i] = true.
 Proof.
-  intros A a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => t = true -> forall i, (i < j) = true -> f (a .[ i]) = true)).
-  intros b i H1; case b; simpl; try discriminate; intros H2 H3 j Hj; case_eq (j == i); intro Heq.
-  rewrite Int63Properties.eqb_spec in Heq; subst j; auto.
-  apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; lia.
-  intros _ i H; eelim ltb_0; eassumption.
+  intros a H i; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i).
+  revert H; rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
+  apply leb_0.
+  rewrite ltb_spec, to_Z_0; lia.
+  intros j b _; assert (Bj := to_Z_bounded j).
+  rewrite 2!ltb_spec; intros Hj IH.
+  rewrite ltb_spec, to_Z_add_1_wB by lia.
+  rewrite andb_true_iff.
+  case (reflect_eqb i j).
+  intro Heq; rewrite <- Heq; tauto.
+  rewrite <- to_Z_eq; intros Hneq [ Hb Haj ] Hij.
+  apply IH; [ exact Hb | lia ].
 Qed.
 
-
-Lemma afold_left_and p a :
-  afold_left bool int true andb p a =
+Lemma afold_left_and A (p : A -> bool) a :
+  afold_left bool true andb (amap p a) =
   List.forallb p (to_list a).
 Proof.
-  rewrite afold_left_spec; auto.
-  rewrite fold_left_to_list.
-  assert (H:forall l acc, List.fold_left (fun (a0 : bool) (v : int) => a0 && p v) l acc =
-  acc && List.forallb p l).
-  {
-    clear a. induction l; simpl.
-    - intros; now rewrite andb_true_r.
-    - intro acc. rewrite IHl. now rewrite andb_assoc.
-  }
-  now apply H.
+  rewrite afold_left_spec, foldi_to_list, to_list_amap by exact andb_true_l.
+  rewrite <- andb_true_r.
+  generalize true.
+  induction (to_list a) as [ | x l ]; clear a; intro b.
+  reflexivity.
+  simpl; rewrite IHl.
+  rewrite (andb_comm b (p x)), (andb_comm (p x) (forallb p l)); apply andb_assoc.
 Qed.
 
-
 (* Case orb *)
 
-Lemma afold_left_orb_true : forall A i a f,
+Lemma afold_left_orb_true : forall i a,
   i < length a = true ->
-  f (a .[ i]) = true ->
-  afold_left bool A false orb f a = true.
+  a .[ i] = true ->
+  afold_left bool false orb a = true.
 Proof.
-  intros A i a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => (i < j) = true -> f (a .[ i]) = true -> t = true)).
-  intros b j H1 H2 H3 H4; case_eq (i == j).
-  rewrite Int63Properties.eqb_spec; intro; subst i; rewrite H4, orb_true_r; auto.
-  rewrite eqb_false_spec; intro Heq; rewrite H2; auto; rewrite ltb_spec; rewrite ltb_spec in H3; rewrite (to_Z_add_1 _ (length a)) in H3; auto; assert (H5: [|i|] <> [|j|]) by (intro H5; apply Heq, to_Z_inj; auto); lia.
-  intro H; eelim ltb_0; eassumption.
+  intros i a; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i).
+  rewrite afold_left_spec by apply orb_false_l; apply foldi_ind.
+  apply leb_0.
+  rewrite ltb_spec, to_Z_0; lia.
+  intros j b _; assert (Bj := to_Z_bounded j).
+  rewrite 2!ltb_spec; intros Hj IH.
+  rewrite ltb_spec, to_Z_add_1_wB by lia; intro Hij.
+  case (reflect_eqb i j).
+  intros Heq Hai; rewrite <- Heq, Hai; apply orb_true_r.
+  rewrite <- to_Z_eq; intros Hneq Hai.
+  rewrite IH; [ apply orb_true_l | lia | exact Hai ].
 Qed.
 
-
-Lemma afold_left_orb_true_inv : forall A a f,
-  afold_left bool A false orb f a = true ->
-  exists i, (i < length a = true) /\ (f (a .[ i]) = true).
+Lemma afold_left_orb_true_inv : forall a,
+  afold_left bool false orb a = true ->
+  exists i, i < length a = true /\ a .[ i] = true.
 Proof.
-  intros A a f; rewrite afold_left_spec; auto; apply fold_left_ind; try discriminate.
-  intros b i H1; case b; simpl.
-  intros H2 _; destruct (H2 (refl_equal true)) as [j [H3 H4]]; exists j; auto.
-  intros _ H2; exists i; auto.
+  intro a; assert (Ba := to_Z_bounded (length a)).
+  rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
+  apply leb_0.
+  discriminate.
+  intros i b _; assert (Bi := to_Z_bounded i).
+  rewrite ltb_spec; intros Hj IH.
+  destruct b.
+  generalize (IH eq_refl); clear IH; intros [ j [ Hji Haj ] ] _.
+  rewrite ltb_spec in Hji; exists j.
+  split; [ rewrite ltb_spec, to_Z_add_1_wB; lia | exact Haj ].
+  rewrite orb_false_l; intro H; exists i; rewrite H.
+  split; [ rewrite ltb_spec, to_Z_add_1_wB; lia | reflexivity ].
 Qed.
 
-
-Lemma afold_left_orb_false : forall A a f,
-  (forall i, i < length a = true -> f (a.[i]) = false) ->
-  afold_left bool A false orb f a = false.
+Lemma afold_left_orb_false : forall a,
+  (forall i, i < length a = true -> a.[i] = false) ->
+  afold_left bool false orb a = false.
 Proof.
-  intros A a f H; rewrite afold_left_spec; auto; apply fold_left_ind; trivial; intros b j H1 H2; rewrite H2; simpl; rewrite H; trivial.
+  intros a H.
+  rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
+  apply leb_0.
+  reflexivity.
+  intros b j _ H1 H2; rewrite H2; simpl; rewrite H; trivial.
 Qed.
 
-
-Lemma afold_left_orb_false_inv : forall A a f,
-  afold_left bool A false orb f a = false ->
-  forall i, i < length a = true -> f (a.[i]) = false.
+Lemma afold_left_orb_false_inv : forall a,
+  afold_left bool false orb a = false ->
+  forall i, i < length a = true -> a.[i] = false.
 Proof.
-  intros A a f; rewrite afold_left_spec; auto; apply (fold_left_Ind _ _ (fun j t => t = false -> forall i, (i < j) = true -> f (a .[ i]) = false)).
-  intros b i H1; case b; simpl; try discriminate; intros H2 H3 j Hj; case_eq (j == i); intro Heq.
-  rewrite Int63Properties.eqb_spec in Heq; subst j; auto.
-  apply H2; auto; rewrite eqb_false_spec in Heq; rewrite ltb_spec; rewrite ltb_spec in Hj; assert (H4: [|j|] <> [|i|]) by (intro H; apply Heq, to_Z_inj; auto); rewrite (to_Z_add_1 _ (length a)) in Hj; auto; lia.
-  intros _ i H; eelim ltb_0; eassumption.
+  intros a H i; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i).
+  revert H; rewrite afold_left_spec by apply andb_true_l; apply foldi_ind.
+  apply leb_0.
+  rewrite ltb_spec, to_Z_0; lia.
+  intros j b _; assert (Bj := to_Z_bounded j).
+  rewrite 2!ltb_spec; intros Hj IH.
+  rewrite ltb_spec, to_Z_add_1_wB by lia.
+  rewrite orb_false_iff.
+  case (reflect_eqb i j).
+  intro Heq; rewrite <- Heq; tauto.
+  rewrite <- to_Z_eq; intros Hneq [ Hb Haj ] Hij.
+  apply IH; [ exact Hb | lia ].
 Qed.
 
-
-Lemma afold_left_or p a :
-  afold_left bool int false orb p a =
+Lemma afold_left_or A (p : A -> bool) a :
+  afold_left bool false orb (amap p a) =
   List.existsb p (to_list a).
 Proof.
-  rewrite afold_left_spec; auto.
-  rewrite fold_left_to_list.
-  assert (H:forall l acc, List.fold_left (fun (a0 : bool) (v : int) => a0 || p v) l acc =
-  acc || List.existsb p l).
-  {
-    clear a. induction l; simpl.
-    - intros; now rewrite orb_false_r.
-    - intro acc. rewrite IHl. now rewrite orb_assoc.
-  }
-  now apply H.
+  rewrite afold_left_spec, foldi_to_list, to_list_amap by exact andb_true_l.
+  rewrite <- orb_false_r.
+  generalize false.
+  induction (to_list a) as [ | x l ]; clear a; intro b.
+  reflexivity.
+  simpl; rewrite IHl.
+  rewrite (orb_comm b (p x)), (orb_comm (p x) (existsb p l)); apply orb_assoc.
 Qed.
 
-
 (* Case implb *)
 
-Lemma afold_right_implb_false : forall A a f,
+Lemma afold_right_implb_false : forall a,
   0 < length a = true /\
-  (forall i, i < length a - 1 = true -> f (a .[ i]) = true) /\
-  f (a.[length a - 1]) = false ->
-  afold_right bool A true implb f a = false.
+  (forall i, i < length a - 1 = true -> a .[ i] = true) /\
+  a.[length a - 1] = false ->
+  afold_right bool true implb a = false.
 Proof.
-  intros A a f; intros [H1 [H2 H3]]; apply afold_right_ind_nonempty; auto; intros b i H4 H5; rewrite H5, H2; auto.
+  intros a; intros [H1 [H2 H3]].
+  pattern 0; apply afold_right_ind.
+  intro H; rewrite H in H1; discriminate.
+  intros _; exact H3.
+  intros b i H4 H5 H6; rewrite H6; clear H6.
+  rewrite H2; [ reflexivity | ].
+  assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i).
+  revert H1 H4 H5; rewrite 4!ltb_spec, to_Z_0; intros H1 H4 H5.
+  rewrite 2!to_Z_sub_1_0; lia.
 Qed.
 
-
-Lemma afold_right_implb_false_inv : forall A a f,
-  afold_right bool A true implb f a = false ->
+Lemma afold_right_implb_false_inv : forall a,
+  afold_right bool true implb a = false ->
   0 < length a = true /\
-  (forall i, i < length a - 1 = true -> f (a .[ i]) = true) /\
-  f (a.[length a - 1]) = false.
-Proof.
-  intros A a f; case_eq (length a == 0); intro Heq1.
-  unfold afold_right; rewrite Heq1; discriminate.
-  intro H; split.
-  rewrite eqb_false_spec in Heq1; rewrite <- not_0_ltb; auto.
-  generalize H; clear H; case_eq (length a <= 1); intro Heq2.
-  unfold afold_right; rewrite Heq1, Heq2; intro H; replace (length a - 1) with 0.
-  split; auto; intros i Hi; elim (ltb_0 i); auto.
-  rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; assert ([|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; lia.
-  pose (P j k := k = false -> (forall i : int, (j <= i) = true -> (i < length a - 1) = true -> f (a .[ i]) = true) /\ f (a .[ length a - 1]) = false); assert (H: P 0 (afold_right bool A true implb f a)).
-  generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P.
-  intros b i H1 H2 H3; case_eq b; intro Heq3.
-  rewrite Heq3 in H3; generalize H3; case (f (a .[ i])); discriminate.
-  destruct (H2 Heq3) as [H4 H5]; split; auto; intros j H6 H7; case_eq (i == j); intro Heq4.
-  rewrite eqb_spec in Heq4; subst j b; generalize H3; case (f (a .[ i])); auto; discriminate.
-  apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq4; assert ([|i|] <> [|j|]) by (intro H; apply Heq4, to_Z_inj; auto); lia.
-  intro H; split; auto; intros i H1 H2; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; lia.
-  unfold P in H; intro H1; destruct (H H1) as [H2 H3]; split; auto; intro i; apply H2, leb_0.
-Qed.
-
-
-Lemma afold_right_implb_true_aux : forall A a f,
-  (exists i, i < length a - 1 = true /\ f (a.[i]) = false) ->
-  afold_right bool A true implb f a = true.
-Proof.
-  intros A a f; case_eq (length a == 0); intro Heq1.
-  intros _; unfold afold_right; rewrite Heq1; auto.
-  case_eq (length a <= 1); intro Heq2.
-  intros [i [Hi _]]; elim (ltb_0 i); replace 0 with (length a - 1); auto; rewrite eqb_false_spec in Heq1; apply to_Z_inj; rewrite to_Z_sub_1_diff; auto; assert (H1: [|length a|] <> 0%Z) by (intro H; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; generalize (leb_0 (length a)); rewrite leb_spec; change [|0|] with 0%Z; change [|1|] with 1%Z in Heq2; lia.
-  pose (P j k := (exists i : int, (j <= i) = true /\ (i < length a - 1) = true /\ f (a .[ i]) = false) -> k = true); assert (H: P 0 (afold_right bool A true implb f a)).
-  generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P.
-  intros b i H1 H2 [j [H3 [H4 H5]]]; case_eq (i == j); intro Heq3.
-  rewrite eqb_spec in Heq3; subst i; rewrite H5; case b; auto.
-  rewrite H2.
-  case (f (a .[ i])); auto.
-  exists j; repeat split; auto; assert (H: i < j = true).
-  rewrite ltb_spec; rewrite leb_spec in H3; rewrite eqb_false_spec in Heq3; assert (H: [|i|] <> [|j|]) by (intro H; apply Heq3, to_Z_inj; auto); lia.
-  rewrite leb_spec, (to_Z_add_1 _ _ H); rewrite ltb_spec in H; lia.
-  intros [i [H1 [H2 _]]]; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; lia.
-  unfold P in H; intros [i Hi]; apply H; exists i; split; auto; apply leb_0.
-Qed.
-
-
-Lemma afold_right_implb_true : forall A a f,
-  length a = 0 \/ (exists i, i < length a - 1 = true /\ f (a.[i]) = false) \/
-  (forall i, i < length a = true -> f (a.[i]) = true) ->
-  afold_right bool A true implb f a = true.
-Proof.
-  intros A a f; case_eq (length a == 0).
-  intros H _; unfold afold_right; rewrite H; auto.
-  intros Heq [H1|[H1|H1]].
-  rewrite H1 in Heq; discriminate.
+  (forall i, i < length a - 1 = true -> a .[ i] = true) /\
+  a.[length a - 1] = false.
+Proof.
+  intros a H; assert (Ba := to_Z_bounded (length a)); split; [ | split ].
+  revert H; unfold afold_right.
+  case (reflect_eqb (length a) 0).
+  intro Heq; rewrite Heq; discriminate.
+  rewrite <- to_Z_eq, to_Z_0; intros Hlength _.
+  rewrite ltb_spec, to_Z_0; lia.
+  intro i; generalize (leb_0 i); revert H i; apply afold_right_ind.
+  discriminate.
+  intros _ _ i; rewrite leb_spec, ltb_spec; lia.
+  intros b j; assert (Bj := to_Z_bounded j).
+  rewrite 2!ltb_spec, to_Z_0; intros Hj1 Hj2 IH.
+  unfold implb; case_eq (a.[j - 1]); [ | discriminate ]; intros Ha H; subst b; intro i.
+  case (reflect_eqb i (j - 1)).
+  intro Heq; subst i; intros; exact Ha.
+  rewrite <- to_Z_eq, to_Z_sub_1_0 by lia; intro Hneq.
+  rewrite leb_spec, to_Z_sub_1_0 by lia; intro Hji.
+  apply IH; [ reflexivity | rewrite leb_spec; lia ].
+  revert H; unfold afold_right.
+  case (reflect_eqb (length a) 0).
+  discriminate.
+  rewrite <- to_Z_eq, to_Z_0; intro Hlength.
+  apply (foldi_ind _ (fun i b => b = false -> a.[length a - 1] = false)).
+  rewrite leb_spec, to_Z_1; lia.
+  tauto.
+  intros i b; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, to_Z_1; intro Hi1.
+  rewrite ltb_spec; intros Hi2 IH.
+  unfold implb at 1; case (a.[length a - 1 - i]); [ exact IH | discriminate ].
+Qed.
+
+Lemma afold_right_implb_true_aux : forall a,
+  (exists i, i < length a - 1 = true /\ a.[i] = false) ->
+  afold_right bool true implb a = true.
+Proof.
+  intros a [ i [ Hi Hai ] ].
+  assert (Bi := to_Z_bounded i).
+  generalize (leb_0 i); apply afold_right_ind.
+  reflexivity.
+  intros _; revert Hi; rewrite ltb_spec, leb_spec; lia.
+  intros b j.
+  assert (Bj := to_Z_bounded j).
+  rewrite ltb_spec, to_Z_0; intro Hj1.
+  rewrite ltb_spec; intro Hj2.
+  rewrite leb_spec; intro IH.
+  rewrite leb_spec, to_Z_sub_1_0 by lia; intro Hji.
+  case (reflect_eqb i (j - 1)).
+  intro Heq; rewrite Heq in Hai; rewrite Hai; reflexivity.
+  rewrite <- to_Z_eq, to_Z_sub_1_0 by lia; intro Hneq.
+  rewrite IH by lia; case (a.[j - 1]); reflexivity.
+Qed.
+
+Lemma afold_right_implb_true : forall a,
+  length a = 0 \/ (exists i, i < length a - 1 = true /\ a.[i] = false) \/
+  (forall i, i < length a = true -> a.[i] = true) ->
+  afold_right bool true implb a = true.
+Proof.
+  intro a; assert (Ba := to_Z_bounded (length a)); case (reflect_eqb (length a) 0).
+  intros H _; unfold afold_right; rewrite H; reflexivity.
+  intro Hneq.
+  intros [H1|[H1|H1]].
+  elim (Hneq H1).
   apply afold_right_implb_true_aux; auto.
-  apply afold_right_ind_nonempty.
-  intros b i H2 H3; subst b; case (f (a .[ i])); auto.
-  apply not_0_ltb; intro H; rewrite H in Heq; discriminate.
-  apply H1; rewrite ltb_spec, to_Z_sub_1_diff; [lia| ]; intro H; rewrite H in Heq; discriminate.
-Qed.
-
-
-Lemma afold_right_implb_true_inv : forall A a f,
-  afold_right bool A true implb f a = true ->
-  length a = 0 \/ (exists i, i < length a - 1 = true /\ f (a.[i]) = false) \/
-  (forall i, i < length a = true -> f (a.[i]) = true).
-Proof.
-  intros A a f; case_eq (length a == 0); intro Heq1.
-  intros _; left; rewrite eqb_spec in Heq1; auto.
-  case_eq (length a <= 1); intro Heq2.
-  unfold afold_right; rewrite Heq1, Heq2; intro H; right; right; intros i Hi; replace i with 0; auto; apply to_Z_inj; rewrite ltb_spec in Hi; rewrite eqb_false_spec in Heq1; assert (H1: [|length a|] <> 0%Z) by (intro H1; apply Heq1, to_Z_inj; auto); rewrite leb_spec in Heq2; change [|1|] with 1%Z in Heq2; generalize (leb_0 (length a)) (leb_0 i); rewrite !leb_spec; change [|0|] with 0%Z;  lia.
-  pose (P j k := k = true -> (exists i : int, (j <= i) = true /\ (i < length a - 1) = true /\ f (a .[ i]) = false) \/ (forall i : int, (j <= i) = true -> (i < length a) = true -> f (a .[ i]) = true)); assert (H: P 0 (afold_right bool A true implb f a)).
-  generalize (afold_right_Ind _ _ P true implb f a); rewrite Heq2; intro IH; apply IH; clear IH; unfold P.
-  intros b i H1 H2 H3; case_eq b; intro Heq3.
-  destruct (H2 Heq3) as [[j [H4 [H5 H6]]]|H4].
-  left; exists j; repeat split; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1) in H4; lia.
-  case_eq (f (a.[i])); intro Heq4.
-  right; intros j H5 H6; case_eq (i == j); intro Heq5.
-  rewrite eqb_spec in Heq5; subst j; auto.
-  apply H4; auto; rewrite leb_spec in *; rewrite (to_Z_add_1 _ _ H1); rewrite eqb_false_spec in Heq5; assert ([|i|] <> [|j|]) by (intro H; apply Heq5, to_Z_inj; auto); lia.
-  left; exists i; repeat split; auto; apply leb_refl.
-  rewrite Heq3 in H3; case_eq (f (a .[ i])); intro Heq4; rewrite Heq4 in H3; try discriminate; left; exists i; repeat split; auto; apply leb_refl.
-  intros H1; right; intros i H2 H3; replace i with (length a - 1); auto; apply to_Z_inj; rewrite leb_spec in H2; rewrite (to_Z_sub_1 _ _ H3) in *; rewrite ltb_spec in H3; lia.
-  unfold P in H; intro H1; right; destruct (H H1) as [[i [_ H2]]|H2].
-  left; exists i; auto.
-  right; intro i; apply H2, leb_0.
+  assert (Heq : length a == 0 = false) by (rewrite <- not_true_iff_false, eqb_spec; exact Hneq).
+  unfold afold_right; rewrite Heq.
+  revert Hneq; rewrite <- to_Z_eq, to_Z_0; intro Hneq.
+  apply (foldi_ind _ (fun i a => a = true)).
+  rewrite leb_spec, to_Z_1; lia.
+  apply H1; rewrite ltb_spec, to_Z_sub_1_0; lia.
+  intros i b; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, to_Z_1; intro Hi1.
+  rewrite ltb_spec; intros Hi2 IH.
+  rewrite IH; case (a.[length a - 1 - i]); reflexivity.
 Qed.
 
+Lemma afold_right_implb_true_inv : forall a,
+  afold_right bool true implb a = true ->
+  length a = 0 \/ (exists i, i < length a - 1 = true /\ a.[i] = false) \/
+  (forall i, i < length a = true -> a.[i] = true).
+Proof.
+  intros a H; cut (length a = 0
+    \/ (exists i, 0 <= i = true /\ i < length a - 1 = true /\ a.[i] = false)
+    \/ (forall i, 0 <= i = true -> i < length a = true -> a.[i] = true)).
+  clear H; intro H; destruct H as [ H | H ].
+  left; tauto.
+  destruct H as [ H | H ].
+  destruct H as [ i [ Hi1 Hi2 ] ].
+  right; left; exists i; tauto.
+  right; right; intro i; apply H; apply leb_0.
+  assert (Ba := to_Z_bounded (length a)).
+  revert H; apply afold_right_ind.
+  left; tauto.
+  rewrite ltb_spec, to_Z_0; intro Hlength.
+  intro Ha; right; right.
+  intro i; assert (Bi := to_Z_bounded i).
+  rewrite leb_spec, to_Z_sub_1_0 by lia; intro Hi1.
+  rewrite ltb_spec; intro Hi2.
+  replace i with (length a - 1) by (rewrite <- to_Z_eq, to_Z_sub_1_0; lia); exact Ha.
+  intros b i; assert (Bi := to_Z_bounded i).
+  rewrite ltb_spec, to_Z_0; intro Hi1.
+  rewrite ltb_spec; intros Hi2 IH.
+  case_eq (a.[i - 1]); unfold implb.
+  intros Ha Hb; destruct (IH Hb) as [ Heq | H ]; clear IH.
+  rewrite Heq in Hi2; lia.
+  destruct H as [ [ j [ Hij Hj ] ] | H ].
+  right; left; exists j.
+  split; [ | exact Hj ].
+  revert Hij; rewrite 2!leb_spec, to_Z_sub_1_0; lia.
+  right; right; intro j.
+  rewrite leb_spec, sub_spec, to_Z_1, Z.mod_small by lia; intro Hij.
+  rewrite ltb_spec; intro Hj.
+  case (reflect_eqb j (i - 1)).
+  intro Heq; rewrite Heq; exact Ha.
+  rewrite <- to_Z_eq, to_Z_sub_1_0 by lia; intro Hneq.
+  apply H; [ rewrite leb_spec; lia | rewrite ltb_spec; lia ].
+  intros Ha _; right; left; exists (i - 1).
+  split; [ rewrite leb_spec; lia | ].
+  split; [ rewrite ltb_spec, 2!to_Z_sub_1_0; lia | exact Ha ].
+Qed.
 
 (* Other cases *)
 
-Lemma afold_left_length_2 : forall A B default OP F t,
+Lemma afold_left_length_2 : forall A default OP t,
   (length t == 2) = true ->
-  afold_left A B default OP F t = OP (F (t.[0])) (F (t.[1])).
+  afold_left A default OP t = OP (t.[0]) (t.[1]).
 Proof.
-  intros A B default OP F t H; unfold afold_left; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; simpl; change (2-1) with 1; rewrite foldi_eq; trivial.
+  intros A default OP t H; unfold afold_left; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; reflexivity.
 Qed.
 
 
-Lemma afold_right_length_2 : forall A B default OP F t,
+Lemma afold_right_length_2 : forall A default OP t,
   (length t == 2) = true ->
-  afold_right A B default OP F t = OP (F (t.[0])) (F (t.[1])).
+  afold_right A default OP t = OP (t.[0]) (t.[1]).
 Proof.
-  intros A B default OP F t H; unfold afold_right; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; simpl; change (2<=1) with false; simpl; change (2-2) with 0; rewrite foldi_down_eq; trivial.
+  intros A default OP t H; unfold afold_right; rewrite eqb_spec in H; rewrite H; change (2 == 0) with false; reflexivity.
 Qed.
 
 
 Ltac tac_left :=
-  intros t f H H1 H2; rewrite afold_left_length_2;
+  intros t H H1 H2; rewrite afold_left_length_2;
     [rewrite H1, H2| ]; trivial.
 
 
 Ltac tac_right :=
-  try (intros t f H H1 H2; rewrite afold_right_length_2;
+  try (intros t H H1 H2; rewrite afold_right_length_2;
     [rewrite H1, H2| ]; trivial);
-  try (intros t f H H1; rewrite afold_right_length_2;
+  try (intros t H H1; rewrite afold_right_length_2;
     [rewrite H1| ]; trivial);
   try (rewrite implb_true_r; trivial).
 
 
-Lemma afold_left_xorb_false1 : forall t f,
+Lemma afold_left_xorb_false1 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = false -> f (t .[ 1]) = false ->
-  afold_left bool int false xorb f t = false.
+  t .[ 0] = false -> t .[ 1] = false ->
+  afold_left bool false xorb t = false.
 Proof. tac_left. Qed.
 
 
-Lemma afold_left_xorb_false2 : forall t f,
+Lemma afold_left_xorb_false2 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = true -> f (t .[ 1]) = true ->
-  afold_left bool int false xorb f t = false.
+  t .[ 0] = true -> t .[ 1] = true ->
+  afold_left bool false xorb t = false.
 Proof. tac_left. Qed.
 
 
-Lemma afold_left_xorb_true1 : forall t f,
+Lemma afold_left_xorb_true1 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = false -> f (t .[ 1]) = true ->
-  afold_left bool int false xorb f t = true.
+  t .[ 0] = false -> t .[ 1] = true ->
+  afold_left bool false xorb t = true.
 Proof. tac_left. Qed.
 
 
-Lemma afold_left_xorb_true2 : forall t f,
+Lemma afold_left_xorb_true2 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = true -> f (t .[ 1]) = false ->
-  afold_left bool int false xorb f t = true.
+  t .[ 0] = true -> t .[ 1] = false ->
+  afold_left bool false xorb t = true.
 Proof. tac_left. Qed.
 
 
@@ -777,31 +1118,31 @@ Proof. tac_left. Qed.
 (* Proof. tac_right. Qed. *)
 
 
-Lemma afold_left_eqb_false1 : forall t f,
+Lemma afold_left_eqb_false1 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = false -> f (t .[ 1]) = true ->
-  afold_left bool int true eqb f t = false.
+  t .[ 0] = false -> t .[ 1] = true ->
+  afold_left bool true eqb t = false.
 Proof. tac_left. Qed.
 
 
-Lemma afold_left_eqb_false2 : forall t f,
+Lemma afold_left_eqb_false2 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = true -> f (t .[ 1]) = false ->
-  afold_left bool int true eqb f t = false.
+  t .[ 0] = true -> t .[ 1] = false ->
+  afold_left bool true eqb t = false.
 Proof. tac_left. Qed.
 
 
-Lemma afold_left_eqb_true1 : forall t f,
+Lemma afold_left_eqb_true1 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = true -> f (t .[ 1]) = true ->
-  afold_left bool int true eqb f t = true.
+  t .[ 0] = true -> t .[ 1] = true ->
+  afold_left bool true eqb t = true.
 Proof. tac_left. Qed.
 
 
-Lemma afold_left_eqb_true2 : forall t f,
+Lemma afold_left_eqb_true2 : forall t,
   (PArray.length t == 2) = true ->
-  f (t .[ 0]) = false -> f (t .[ 1]) = false ->
-  afold_left bool int true eqb f t = true.
+  t .[ 0] = false -> t .[ 1] = false ->
+  afold_left bool true eqb t = true.
 Proof. tac_left. Qed.
 
 
@@ -990,48 +1331,67 @@ End Distinct.
 
 Arguments distinct [A] eq l.
 
+(** Specification of aexistsbi and aforallbi *)
 
-(** Specification of existsb *)
+Definition aexistsbi {A:Type} (f:int->A->bool) (t:array A) :=
+  afold_left _ false orb (amapi f t).
 
-Lemma existsb_false_spec : forall f from to,
-  existsb f from to = false <->
-  forall i, ((from <= i) = true /\ (i <= to) = true) -> f i = false.
+Lemma aexistsbi_false_spec : forall A (f : int -> A -> bool) t,
+  aexistsbi f t = false <->
+  forall i, i < length t = true -> f i (t.[i]) = false.
 Proof.
-  unfold existsb;intros; setoid_rewrite leb_spec; apply foldi_cont_ZInd.
-  intros z Hz; split; auto; intros _ i [H1 H2]; assert (H3 := Z.le_trans _ _ _ H1 H2); elimtype False; lia.
-  intros i cont H1 H2 H3; case_eq (f i); intro Heq.
-  split; try discriminate; intro H; rewrite <- Heq; apply H; split; try lia; rewrite leb_spec in H2; auto.
-  rewrite H3; split; intros H j [Hj1 Hj2].
-  case_eq (i == j); intro Heq2.
-  rewrite eqb_spec in Heq2; subst j; auto.
-  apply H; split; auto; rewrite eqb_false_spec in Heq2; assert ([|i|] <> [|j|]) by (intro; apply Heq2, to_Z_inj; auto); lia.
-  apply H; lia.
+  intros A f t; unfold aexistsbi.
+  split.
+  intro H; generalize (afold_left_orb_false_inv _ H); clear H.
+  rewrite length_amapi; intros H i Hi.
+  rewrite <- get_amapi by exact Hi.
+  apply H; exact Hi.
+  intro H; apply afold_left_orb_false.
+  intro i; rewrite length_amapi; intro Hi; rewrite get_amapi by exact Hi; apply H; exact Hi.
 Qed.
 
-
-Lemma array_existsbi_false_spec : forall A (f : int -> A -> bool) t,
-  existsbi f t = false <->
-  forall i, i < length t = true -> f i (t.[i]) = false.
+Lemma aexistsbi_spec : forall A (f : int -> A -> bool) t,
+  aexistsbi 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; auto. intros _ i Hi. elim (ltb_0 i). rewrite e. auto.
-  rewrite existsb_false_spec. split.
-  intros H i Hi. apply H. split; [apply leb_0| ]. rewrite leb_spec. rewrite (to_Z_sub_1 _ _ Hi). rewrite ltb_spec in Hi. lia.
-  intros H i [_ Hi]. apply H. rewrite ltb_spec. rewrite leb_spec in Hi. rewrite to_Z_sub_1_diff in Hi; auto; lia.
+  intros A f t; unfold aexistsbi.
+  split.
+  intro H; generalize (afold_left_orb_true_inv _ H); clear H.
+  intros [ i [ Hi Hf ] ]; exists i.
+  rewrite length_amapi in Hi; rewrite get_amapi in Hf by exact Hi.
+  split; [ exact Hi | exact Hf ].
+  intros [ i [ Hi Hf ] ].
+  apply (afold_left_orb_true i); [ rewrite length_amapi; exact Hi | rewrite get_amapi by exact Hi; exact Hf ].
 Qed.
 
+Definition aforallbi {A:Type} (f:int->A->bool) (t:array A) :=
+  afold_left _ true andb (amapi f t).
 
-Lemma array_existsb_false_spec : forall A (f : A -> bool) t,
-  PArray.existsb f t = false <->
-  forall i, i < length t = true -> f (t.[i]) = false.
+Lemma aforallbi_false_spec : forall A (f : int -> A -> bool) t,
+  aforallbi f t = false <-> exists i, i < length t = true /\ f i (t.[i]) = false.
 Proof.
-  intros A f t; unfold PArray.existsb; case_eq (0 == length t).
-  rewrite eqb_spec; intro H; split; auto; intros _ i Hi; elim (ltb_0 i); rewrite H; auto.
-  intro H; rewrite existsb_false_spec; split.
-  intros H1 i Hi; apply H1; split; [apply leb_0| ]; rewrite leb_spec, (to_Z_sub_1 _ _ Hi); rewrite ltb_spec in Hi; lia.
-  intros H1 i [_ H2]; apply H1; rewrite ltb_spec; rewrite leb_spec in H2; rewrite to_Z_sub_1_diff in H2; [lia| ]; intro H3; rewrite H3 in H; discriminate.
+  intros A f t; unfold aforallbi.
+  split.
+  intro H; generalize (afold_left_andb_false_inv _ H); clear H.
+  intros [ i [ Hi Hf ] ]; exists i.
+  rewrite length_amapi in Hi; rewrite get_amapi in Hf by exact Hi.
+  split; [ exact Hi | exact Hf ].
+  intros [ i [ Hi Hf ] ].
+  apply (afold_left_andb_false i); [ rewrite length_amapi; exact Hi | rewrite get_amapi by exact Hi; exact Hf ].
 Qed.
 
+Lemma aforallbi_spec : forall A (f : int -> A -> bool) t,
+  aforallbi f t = true <->
+  forall i, i < length t = true -> f i (t.[i]) = true.
+Proof.
+  intros A f t; unfold aforallbi.
+  split.
+  intro H; generalize (afold_left_andb_true_inv _ H); clear H.
+  rewrite length_amapi; intros H i Hi.
+  rewrite <- get_amapi by exact Hi.
+  apply H; exact Hi.
+  intro H; apply afold_left_andb_true.
+  intro i; rewrite length_amapi; intro Hi; rewrite get_amapi by exact Hi; apply H; exact Hi.
+Qed.
 
 (** Forall of two lists at the same time *)
 
@@ -1051,38 +1411,6 @@ End Forall2.
 Arguments forallb2 {A B} f l1 l2.
 
 
-(* Compatibility between native-coq and Coq 8.5 *)
-
-Definition Nat_eqb :=
-  fix eqb (n m : nat) {struct n} : bool :=
-    match n with
-    | O => match m with
-           | O => true
-           | S _ => false
-           end
-    | S n' => match m with
-              | O => false
-              | S m' => eqb n' m'
-              end
-    end.
-
-Definition List_map_ext_in
-  : forall (A B : Type) (f g : A -> B) (l : list A),
-    (forall a : A, In a l -> f a = g a) -> List.map f l = List.map g l :=
-  fun (A B : Type) (f g : A -> B) (l : list A) =>
-    list_ind
-      (fun l0 : list A =>
-         (forall a : A, In a l0 -> f a = g a) -> List.map f l0 = List.map g l0)
-      (fun _ : forall a : A, False -> f a = g a => eq_refl)
-      (fun (a : A) (l0 : list A)
-           (IHl : (forall a0 : A, In a0 l0 -> f a0 = g a0) -> List.map f l0 = List.map g l0)
-           (H : forall a0 : A, a = a0 \/ In a0 l0 -> f a0 = g a0) =>
-         eq_ind_r (fun b : B => b :: List.map f l0 = g a :: List.map g l0)
-                  (eq_ind_r (fun l1 : list B => g a :: l1 = g a :: List.map g l0) eq_refl
-                            (IHl (fun (a0 : A) (H0 : In a0 l0) => H a0 (or_intror H0))))
-                  (H a (or_introl eq_refl))) l.
-
-
 (* Misc lemmas *)
 
 Lemma neg_eq_true_eq_false b : b = false <-> b <> true.