diff options
Diffstat (limited to 'src/Misc.v')
| -rw-r--r-- | src/Misc.v | 118 |
1 files changed, 59 insertions, 59 deletions
@@ -10,7 +10,7 @@ (**************************************************************************) -Require Import Bool List PArray Int63 ZArith. +Require Import Bool List PArray Int63 ZArith Psatz. Local Open Scope int63_scope. Local Open Scope array_scope. @@ -30,12 +30,12 @@ Proof. rewrite <- leb_spec in H; rewrite H; discriminate. intros H1 _; apply to_Z_inj; rewrite add_spec, to_Z_1 in H. assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB). - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. destruct H2 as [H2|H2]. rewrite Zmod_small in H. - omega. + lia. split. - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. assumption. rewrite H2, Z_mod_same_full in H; elim H; destruct (to_Z_bounded i) as [H3 _]; assumption. Qed. @@ -48,14 +48,14 @@ Proof. rewrite <- ltb_spec in H; rewrite H; discriminate. intros H1 _; apply to_Z_inj. rewrite add_spec in H1. rewrite to_Z_1 in H1. assert (H2: (([|j|] + 1)%Z < wB)%Z \/ ([|j|] + 1)%Z = wB). - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. destruct H2 as [H2|H2]. rewrite Zmod_small in H1. - omega. + lia. split. - pose (H3 := to_Z_bounded j); omega. + pose (H3 := to_Z_bounded j); lia. assumption. - rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. omega. + rewrite H2, Z_mod_same_full in H1; elimtype False. destruct (to_Z_bounded i) as [H3 _]. lia. Qed. @@ -74,19 +74,19 @@ Proof. min (fun a0 : A => a0))). apply foldi_down_cont_ZInd;intros;red. assert (H20: (z+1 < [|min|]+1)%Z). - omega. + 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;omega. + 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;omega). + 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 omega. auto. + 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). omega. + intro H22; assert (H21: ([|max|] < [|min|])%Z). lia. rewrite <- ltb_spec in H21. intros;rewrite foldi_down_cont_lt;auto. Qed. @@ -120,26 +120,26 @@ Lemma to_list_In : forall {A} (t: array A) i, i < length t = true -> In (t.[i]) (to_list t). 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; omega. + 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; omega. - intro H2; elimtype False; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded (length t - 1)); omega. + 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; omega. + 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; omega. + 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; omega. + unfold is_true in H2; rewrite ltb_spec, to_Z_0 in H2; pose (H3 := to_Z_bounded i); elimtype False; lia. Qed. Lemma In_to_list : forall {A} (t: array A) x, @@ -151,11 +151,11 @@ Proof. 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)); omega. + 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; omega. + 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. Qed. @@ -190,17 +190,17 @@ Proof. 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; omega. + 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); omega. - rewrite ltb_spec; rewrite leb_spec, (to_Z_sub_1 _ _ Hi) in H1; omega. + 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; omega. - rewrite ltb_spec, to_Z_sub_1_diff; auto; destruct (to_Z_bounded (length t)) as [_ H]; change [|max_int|] with (wB-1)%Z; omega. + 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. Qed. @@ -268,7 +268,7 @@ Proof. 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)); omega. + 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. @@ -321,7 +321,7 @@ Lemma afold_left_spec : forall A B (f:B -> A) args op e, 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;omega. + intros;apply to_Z_inj;rewrite to_Z_1;lia. rewrite H1; change (1 - 1) with 0; rewrite (foldi_eq _ _ 0 0); auto. Qed. @@ -347,7 +347,7 @@ Proof. 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;omega. + intros HH;assert (W:= to_Z_bounded (length V1));rewrite Zmod_small;lia. Qed. @@ -379,10 +379,10 @@ Proof. 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; [omega| ]. intro H13. assert (H14: [|length t|] = 0%Z) by (rewrite H13; auto). omega. + 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; [omega| ]. 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; [omega| ]. intro H7. assert (H8: [|length t|] = 0%Z) by (rewrite H7; auto). omega. + 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. @@ -412,7 +412,7 @@ 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). omega. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto. + 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. @@ -425,7 +425,7 @@ 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). omega. rewrite Heq in H3. unfold afold_right in H3. rewrite H10, Heq in H3. apply H3; auto. + 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. @@ -440,11 +440,11 @@ Lemma afold_right_spec : forall A B (f:B -> A) args op e, 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. omega. + 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. omega. + 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. Qed. @@ -459,7 +459,7 @@ 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); omega. + 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. Qed. @@ -490,7 +490,7 @@ 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; omega. + 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. Qed. @@ -505,7 +505,7 @@ 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); omega. + 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. Qed. @@ -536,7 +536,7 @@ 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; omega. + 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. Qed. @@ -566,15 +566,15 @@ Proof. 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; omega. + 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); omega. - intro H; split; auto; intros i H1 H2; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; omega. + 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. @@ -586,7 +586,7 @@ 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; omega. + 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. @@ -594,9 +594,9 @@ Proof. 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); omega. - rewrite leb_spec, (to_Z_add_1 _ _ H); rewrite ltb_spec in H; omega. - intros [i [H1 [H2 _]]]; elimtype False; rewrite leb_spec in H1; rewrite ltb_spec in H2; omega. + 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. @@ -614,7 +614,7 @@ Proof. 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; [omega| ]; 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. @@ -626,19 +626,19 @@ 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; omega. + 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; omega. + 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); omega. + 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; omega. + 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. @@ -946,14 +946,14 @@ Lemma existsb_false_spec : forall f from to, forall i, ((from <= i) = true /\ (i <= to) = true) -> f 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; omega. + 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 omega; rewrite leb_spec in H2; auto. + 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); omega. - apply H; omega. + 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. Qed. @@ -964,8 +964,8 @@ 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. omega. - intros H i [_ Hi]. apply H. rewrite ltb_spec. rewrite leb_spec in Hi. rewrite to_Z_sub_1_diff in Hi; auto; omega. + 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. Qed. @@ -976,8 +976,8 @@ 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; omega. - intros H1 i [_ H2]; apply H1; rewrite ltb_spec; rewrite leb_spec in H2; rewrite to_Z_sub_1_diff in H2; [omega| ]; intro H3; rewrite H3 in H; discriminate. + 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. Qed. |