diff options
Diffstat (limited to 'src/Misc.v')
-rw-r--r-- | src/Misc.v | 1884 |
1 files changed, 1234 insertions, 650 deletions
@@ -10,7 +10,7 @@ (**************************************************************************) -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. @@ -23,6 +23,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 +49,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 +57,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 +76,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 +84,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 +190,1143 @@ 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 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 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. -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 bit_sub1_0 : forall i, bit (i - 1) 0 = negb (bit i 0). 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. +intro i. +cut (b2i (bit (i - 1) 0) = b2i (negb (bit i 0))). +generalize (bit (i - 1) 0) (negb (bit i 0)); intros b1 b2. +destruct b1; destruct b2; simpl; rewrite <- eqb_spec; trivial; discriminate. +replace (b2i (negb (bit i 0))) with (1 - bit i 0); [ | destruct (bit i 0); reflexivity ]. +rewrite <- to_Z_eq. +rewrite sub_spec, to_Z_1. +rewrite 2!bit_0_spec. +rewrite sub_spec, to_Z_1. +case_eq (i == 0). +rewrite eqb_spec; intro Hi; rewrite Hi; reflexivity. +rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0. +generalize (to_Z_bounded i). +intros Hi1 Hi2. +rewrite (Zmod_small _ wB); [ | lia ]. +assert (0 <= to_Z i mod 2 < 2)%Z. +apply Z_mod_lt; lia. +rewrite (Zmod_small _ wB); [ | lia ]. +rewrite 2!Zmod_even. +rewrite Z.even_sub. +case (Z.even (to_Z i)). +reflexivity. +reflexivity. Qed. +Lemma sub1_lsr : forall i, i <> 0 -> (i - 1) >> 1 = if bit i 0 then i >> 1 else i >> 1 - 1. +intro i. +rewrite <- to_Z_eq, to_Z_0; intro Hi0. +assert (Hi : (0 < to_Z i < wB)%Z). +generalize (to_Z_bounded i); lia. +clear Hi0. +rewrite <- to_Z_eq. +rewrite lsr_spec, to_Z_sub_1_0, to_Z_1; [ | lia ]. +case_eq (bit i 0); intro Hibit. +rewrite lsr_spec, to_Z_1. +change (2 ^ 1)%Z with 2%Z. +rewrite to_Z_split. +rewrite Hibit. +rewrite <- Z.add_sub_assoc. +change (to_Z true) with 1%Z. +replace (1 - 1)%Z with 0%Z by ring. +rewrite 2!Z.div_add_l; [ reflexivity | lia | lia ]. +rewrite to_Z_sub_1_0. +rewrite lsr_spec, to_Z_1. +change (2 ^ 1)%Z with 2%Z. +rewrite to_Z_split. +rewrite Hibit. +rewrite <- Z.add_sub_assoc. +change (to_Z false) with 0%Z. +rewrite 2!Z.div_add_l; [ | lia | lia ]. +rewrite <- Z.add_sub_assoc; reflexivity. +rewrite lsr_spec. +change (2 ^ to_Z 1)%Z with 2%Z. +apply Z.div_str_pos. +split; [ lia | ]. +cut (to_Z i <> 1)%Z; [ lia | ]. +change 1%Z with (to_Z 1). +rewrite to_Z_eq. +intro H; rewrite H in Hibit; discriminate. +Qed. -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 pow2_lsr : forall i n, + (to_Z i < 2 ^ Z.of_nat (S n))%Z -> (to_Z (i >> 1) < 2 ^ Z.of_nat n)%Z. Proof. - intros A B f t i H1; rewrite get_outofbound. - apply default_mapi. - rewrite length_mapi; auto. +intros i n Hi. +rewrite lsr_spec. +change (2 ^ to_Z 1)%Z with 2%Z. +apply (Zmult_lt_reg_r _ _ 2); [ lia | ]. +rewrite Zmult_comm. +apply (Z.le_lt_trans _ (to_Z i)). +apply Z.mul_div_le; lia. +rewrite <- two_power_nat_equiv in *. +rewrite two_power_nat_S in Hi. +rewrite Zmult_comm; assumption. Qed. +Lemma pow2_size : forall i, (to_Z i < 2 ^ Z.of_nat size)%Z. +Proof. +intro i. +change (2 ^ Z.of_nat size)%Z with wB. +generalize (to_Z_bounded i); lia. +Qed. -(** Custom fold_left and fold_right *) +Fixpoint iter_int63_aux (n : nat) (i : int) (A : Type) (f : A -> A) : A -> A := + match n with + | O => fun x => x + | S n => + if i == 0 then fun x => x + else let g := iter_int63_aux n (i >> 1) A f in + fun x => if bit i 0 then f (g (g x)) else g (g x) + end. -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 iter_int63 := iter_int63_aux size. +Lemma iter_int63_aux_comm : forall n i A f a, + (to_Z i < 2 ^ Z.of_nat n)%Z -> + iter_int63_aux n i A f (f a) = f (iter_int63_aux n i A f a). +Proof. +intros n i A f; revert i; induction n. +intros i a Hi. +assert (i = 0). +rewrite <- to_Z_eq, to_Z_0. +generalize (to_Z_bounded i); lia. +reflexivity. +intros i a Hi; simpl. +case (i == 0); [ reflexivity | ]. +rewrite IHn; [ | apply pow2_lsr; assumption]. +rewrite IHn; [ | apply pow2_lsr; assumption]. +case (bit i 0); reflexivity. +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 iter_int63_comm : forall i A f a, + iter_int63 i A f (f a) = f (iter_int63 i A f a). +Proof. +intros i A f a. +unfold iter_int63. +apply iter_int63_aux_comm. +apply pow2_size. +Qed. +Lemma iter_int63_aux_S : forall n i A f a, + (0 < to_Z i < 2 ^ Z.of_nat n)%Z -> + iter_int63_aux n i A f a = f (iter_int63_aux n (i - 1) A f a). +Proof. +intros n i A f; revert i; induction n; intros i a Hi. +{ + lia. +} +simpl. +replace (i == 0) with false. +{ + rewrite bit_sub1_0, sub1_lsr. + { + case_eq (bit i 0); simpl. + { + intros _. + case_eq (i == 1). + { + rewrite eqb_spec; intro H; rewrite H in *; clear i H. + case n; reflexivity. + } + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. + replace (i - 1 == 0) with false. + { + reflexivity. + } + symmetry. + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia. + } + intro Hibit. + case_eq (i == 1). + { + rewrite eqb_spec; intro H; rewrite H in *; clear i H; discriminate. + } + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. + replace (i - 1 == 0) with false. + { + case_eq (i == 2). + { + rewrite eqb_spec; intro H; rewrite H in *; clear i H. + destruct n; [ lia | ]. + case n; reflexivity. + } + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq. + change (to_Z 2) with 2%Z; intro Hi2. + rewrite (IHn (i >> 1)). + { + rewrite (IHn (i >> 1)). + { + f_equal. + apply iter_int63_aux_comm. + replace (i >> 1 - 1) with ((i - 1) >> 1). + { + apply pow2_lsr. + rewrite to_Z_sub_1_0; lia. + } + rewrite sub1_lsr, Hibit; [ reflexivity | ]. + rewrite <- to_Z_eq, to_Z_0; lia. + } + split. + { + rewrite lsr_spec, to_Z_1. + change (2 ^ 1)%Z with 2%Z. + apply Z.div_str_pos; lia. + } + apply pow2_lsr; lia. + } + split. + { + rewrite lsr_spec, to_Z_1. + change (2 ^ 1)%Z with 2%Z. + apply Z.div_str_pos; lia. + } + apply pow2_lsr; lia. + } + symmetry. + rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia. + } + rewrite <- to_Z_eq, to_Z_0; lia. +} +symmetry. +rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0; lia. +Qed. -(** Some properties about afold_left *) +Lemma iter_int63_S : forall i A f a, 0 < i = true -> iter_int63 i A f a = f (iter_int63 (i - 1) A f a). +Proof. +intros i A f a. +rewrite ltb_spec, to_Z_0; intro Hi. +unfold iter_int63. +apply iter_int63_aux_S. +split; [ lia | ]. +apply pow2_size. +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. +Definition foldi + {A : Type} + (f : int -> A -> A) + (from to : int) + (a : A) + : A := + if to <= from then + a + else + let (_,r) := iter_int63 (to - from) _ (fun (jy: (int * A)%type) => + let (j,y) := jy in (j + 1, f j y) + ) (from, a) in r. + +Lemma foldi_ge : forall A f from to (a:A), + to <= from = true -> foldi f from to a = a. 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. + intros A f from to a; unfold foldi. + intro H; rewrite H; reflexivity. 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 Hfromto. +pose proof (to_Z_bounded from) as Hfrom. +pose proof (to_Z_bounded to) as Hto. +unfold foldi. +rewrite leb_negb_gtb. +rewrite Hfromto; simpl. +rewrite ltb_spec in Hfromto. +case_eq (to <= from + 1). +rewrite leb_spec, to_Z_add_1_wB; [ | lia ]. +intro Htofrom. +assert (H : to = from + 1). +rewrite <- to_Z_eq. +rewrite to_Z_add_1_wB; lia. +rewrite H; clear H. +replace (from + 1 - from) with 1 by ring. +rewrite iter_int63_S; [ | reflexivity ]. +change (1 - 1) with 0. +reflexivity. +replace (to - (from + 1)) with (to - from - 1) by ring. +rewrite iter_int63_S. +rewrite (iter_int63_comm _ _ + (fun jy : int * A => let (j, y) := jy in (j + 1, f j y)) + (from, a)). +reflexivity. +rewrite ltb_spec, to_Z_0, sub_spec, Zmod_small; lia. +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 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 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 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 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 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. -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). +(** Lemmas about to_list *) + +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. + +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. + +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. + +(** 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 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. + +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 A B P default OP F t; - apply (afoldi_left_Ind P default (fun _ => OP)); trivial. + intros; unfold amap; apply default_amapi. Qed. +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 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 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 get_amap : forall {A B} (f:A -> B) t i, + i < length t = true -> (amap f t).[i] = f (t.[i]). 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; unfold amap; apply get_amapi; assumption. Qed. +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 f t i H1; rewrite get_outofbound. + apply default_amapi. + rewrite length_amapi; auto. +Qed. -Lemma afold_left_spec : forall A B (f:B -> A) args op e, +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 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 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 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 +1351,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. @@ -815,26 +1389,26 @@ Section List2. | In2_hd : forall l, In j l -> In2 i j (i::l) | In2_tl : forall k l, In2 i j l -> In2 i j (k::l). - Local Hint Constructors In2. + Local Hint Constructors In2 : smtcoq_in2. Lemma In2_app : forall i j l m, In2 i j (l ++ m) <-> In2 i j l \/ (In i l /\ In j m) \/ In2 i j m. Proof. - intros i j; induction l as [ |t l IHl]; simpl; intro m; split; auto. - intros [H|[[H _]|H]]; auto. + intros i j; induction l as [ |t l IHl]; simpl; intro m; split; auto with smtcoq_in2. + intros [H|[[H _]|H]]; auto with smtcoq_in2. inversion H. elim H. intro H; inversion H; clear H. - subst i l0; rewrite in_app_iff in H1; destruct H1 as [H1|H1]; auto. - subst k l0; rewrite IHl in H1; destruct H1 as [H1|[[H1 H2]|H1]]; auto. + subst i l0; rewrite in_app_iff in H1; destruct H1 as [H1|H1]; auto with smtcoq_in2. + subst k l0; rewrite IHl in H1; destruct H1 as [H1|[[H1 H2]|H1]]; auto with smtcoq_in2. intros [H|[[[H|H] H1]|H]]. inversion H; clear H. - subst i l0; constructor 1; rewrite in_app_iff; auto. - subst k l0; constructor 2; rewrite IHl; left; auto. - subst t; constructor 1; rewrite in_app_iff; auto. - constructor 2; rewrite IHl; right; left; auto. - constructor 2; rewrite IHl; right; right; auto. + subst i l0; constructor 1; rewrite in_app_iff; auto with smtcoq_in2. + subst k l0; constructor 2; rewrite IHl; left; auto with smtcoq_in2. + subst t; constructor 1; rewrite in_app_iff; auto with smtcoq_in2. + constructor 2; rewrite IHl; right; left; auto with smtcoq_in2. + constructor 2; rewrite IHl; right; right; auto with smtcoq_in2. Qed. @@ -848,17 +1422,17 @@ Section List2. Lemma In2_rev_aux : forall i j l acc, In2 i j (rev_aux acc l) <-> In2 i j acc \/ (In i l /\ In j acc) \/ In2 j i l. Proof. - intros i j; induction l as [ |t q IHq]; simpl; intro acc; split; auto. - intros [H|[[H _]|H]]; auto. + intros i j; induction l as [ |t q IHq]; simpl; intro acc; split; auto with smtcoq_in2. + intros [H|[[H _]|H]]; auto with smtcoq_in2. elim H. inversion H. - rewrite IHq; clear IHq; intros [H|[[H1 H2]|H]]; auto. - inversion H; auto. - inversion H2; auto; clear H2; subst t; right; right; auto. - intros [H|[[[H1|H1] H2]|H]]; rewrite IHq; clear IHq; auto. - subst t; auto. - right; left; split; auto; constructor 2; auto. - inversion H; clear H; auto; subst j l; right; left; split; auto; constructor 1; auto. + rewrite IHq; clear IHq; intros [H|[[H1 H2]|H]]; auto with smtcoq_in2. + inversion H; auto with smtcoq_in2. + inversion H2; auto with smtcoq_in2; clear H2; subst t; right; right; auto with smtcoq_in2. + intros [H|[[[H1|H1] H2]|H]]; rewrite IHq; clear IHq; auto with smtcoq_in2. + subst t; auto with smtcoq_in2. + right; left; split; auto with smtcoq_in2; constructor 2; auto with smtcoq_in2. + inversion H; clear H; auto with smtcoq_in2; subst j l; right; left; split; auto with smtcoq_in2; constructor 1; auto with smtcoq_in2. Qed. @@ -867,7 +1441,7 @@ Section List2. Lemma In2_rev : forall i j l, In2 i j (rev l) <-> In2 j i l. Proof. - intros i j l; unfold rev; rewrite In2_rev_aux; split; auto; intros [H|[[_ H]|H]]; auto; inversion H. + intros i j l; unfold rev; rewrite In2_rev_aux; split; auto with smtcoq_in2; intros [H|[[_ H]|H]]; auto with smtcoq_in2; inversion H. Qed. @@ -877,15 +1451,15 @@ Section List2. intros [H1 H2]; generalize H1 H2; clear H1 H2; induction l as [ |t q IHq]. intro H1; inversion H1. intros H1 H2; inversion H1; clear H1. - subst t; inversion H2; auto; elim H; auto. + subst t; inversion H2; auto with smtcoq_in2; elim H; auto with smtcoq_in2. inversion H2; clear H2. - subst t; auto. - destruct (IHq H0 H1) as [H2|H2]; auto. + subst t; auto with smtcoq_in2. + destruct (IHq H0 H1) as [H2|H2]; auto with smtcoq_in2. intros [H1|H1]; induction H1 as [H1|t q H1 [IH1 IH2]]. - split; [constructor 1|constructor 2]; auto. - split; constructor 2; auto. - split; [constructor 2|constructor 1]; auto. - split; constructor 2; auto. + split; [constructor 1|constructor 2]; auto with smtcoq_in2. + split; constructor 2; auto with smtcoq_in2. + split; [constructor 2|constructor 1]; auto with smtcoq_in2. + split; constructor 2; auto with smtcoq_in2. Qed. End List2. @@ -944,32 +1518,32 @@ Section Distinct. distinct_aux acc' q end. - Local Hint Constructors In2. + Local Hint Constructors In2 : smtcoq_in2. Lemma distinct_aux_spec : forall l acc, distinct_aux acc l = true <-> acc = true /\ (forall i j, In2 i j l -> eq i j = false). Proof. induction l as [ |t q IHq]; simpl. intro acc; split. - intro H; split; auto; intros i j H1; inversion H1. - intros [H _]; auto. + intro H; split; auto with smtcoq_in2; intros i j H1; inversion H1. + intros [H _]; auto with smtcoq_in2. intro acc; rewrite (IHq (distinct_aux2 acc t q)), distinct_aux2_spec; split. - intros [[H1 H2] H3]; split; auto; intros i j H; inversion H; auto. - intros [H1 H2]; repeat split; auto. + intros [[H1 H2] H3]; split; auto with smtcoq_in2; intros i j H; inversion H; auto with smtcoq_in2. + intros [H1 H2]; repeat split; auto with smtcoq_in2. Qed. Lemma distinct_aux_spec_neg : forall l acc, distinct_aux acc l = false <-> acc = false \/ (exists i j, In2 i j l /\ eq i j = true). Proof. induction l as [ |t q IHq]; simpl. - intro acc; split; auto; intros [H|[i [j [H _]]]]; auto; inversion H. + intro acc; split; auto with smtcoq_in2; intros [H|[i [j [H _]]]]; auto with smtcoq_in2; inversion H. intro acc; rewrite (IHq (distinct_aux2 acc t q)), distinct_aux2_spec_neg; split. - intros [[H|[i [H1 H2]]]|[i [j [H1 H2]]]]; auto. - right; exists t; exists i; auto. - right; exists i; exists j; auto. - intros [H|[i [j [H1 H2]]]]; auto; inversion H1; clear H1. - subst i l; left; right; exists j; auto. - subst k l; right; exists i; exists j; auto. + intros [[H|[i [H1 H2]]]|[i [j [H1 H2]]]]; auto with smtcoq_in2. + right; exists t; exists i; auto with smtcoq_in2. + right; exists i; exists j; auto with smtcoq_in2. + intros [H|[i [j [H1 H2]]]]; auto with smtcoq_in2; inversion H1; clear H1. + subst i l; left; right; exists j; auto with smtcoq_in2. + subst k l; right; exists i; exists j; auto with smtcoq_in2. Qed. Definition distinct := distinct_aux true. @@ -977,61 +1551,80 @@ Section Distinct. Lemma distinct_spec : forall l, distinct l = true <-> (forall i j, In2 i j l -> eq i j = false). Proof. - unfold distinct; intro l; rewrite distinct_aux_spec; split; auto; intros [_ H]; auto. + unfold distinct; intro l; rewrite distinct_aux_spec; split; auto with smtcoq_in2; intros [_ H]; auto with smtcoq_in2. Qed. Lemma distinct_false_spec : forall l, distinct l = false <-> (exists i j, In2 i j l /\ eq i j = true). Proof. - unfold distinct; intro l; rewrite distinct_aux_spec_neg; split; auto; intros [H|H]; auto; discriminate. + unfold distinct; intro l; rewrite distinct_aux_spec_neg; split; auto with smtcoq_in2; intros [H|H]; auto with smtcoq_in2; discriminate. Qed. 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 +1644,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. @@ -1092,6 +1653,29 @@ Lemma is_true_iff e : e = true <-> is_true e. Proof. now unfold is_true. Qed. +(* Register constants for OCaml access *) +Register distinct as SMTCoq.Misc.distinct. + +Register Int63.eqb as num.int63.eqb. +Register PArray.array as array.array.type. +Register PArray.make as array.array.make. +Register PArray.set as array.array.set. +Register Coq.Init.Datatypes.is_true as core.is_true.is_true. +Register Coq.PArith.BinPosDef.Pos.eqb as num.pos.eqb. +Register Coq.NArith.BinNat.N.of_nat as num.N.of_nat. +Register Coq.ZArith.BinInt.Z.ltb as num.Z.ltb. +Register Coq.ZArith.BinInt.Z.leb as num.Z.leb. +Register Coq.ZArith.BinInt.Z.gtb as num.Z.gtb. +Register Coq.ZArith.BinInt.Z.geb as num.Z.geb. +Register Coq.ZArith.BinInt.Z.eqb as num.Z.eqb. +Register Coq.Init.Datatypes.implb as core.bool.implb. +Register Coq.Bool.Bool.eqb as core.bool.eqb. +Register Coq.Bool.Bool.ifb as core.bool.ifb. +Register Coq.Bool.Bool.reflect as core.bool.reflect. +Register Coq.Init.Datatypes.length as core.list.length. +Register Coq.micromega.ZMicromega.ZArithProof as micromega.ZMicromega.ZArithProof. + + (* Local Variables: coq-load-path: ((rec "." "SMTCoq")) |