diff --git a/src/FCF/Array.v b/src/FCF/Array.v index 946f892..89a7a52 100644 --- a/src/FCF/Array.v +++ b/src/FCF/Array.v @@ -667,7 +667,7 @@ Theorem arrayLookup_allNats_eq : rewrite app_length in H. rewrite fst_split_app_eq in H. simpl in *. - rewrite plus_comm in H. + rewrite Nat.add_comm in H. simpl in *. eapply app_inj_tail in H. intuition. diff --git a/src/FCF/Asymptotic.v b/src/FCF/Asymptotic.v index 9763ffa..cc46682 100644 --- a/src/FCF/Asymptotic.v +++ b/src/FCF/Asymptotic.v @@ -34,29 +34,29 @@ Theorem polynomial_nz_equiv : intuition. lia. rewrite H. - rewrite plus_assoc. - eapply plus_le_compat; intuition. + rewrite Nat.add_assoc. + eapply Nat.add_le_mono; intuition. simpl. destruct (eq_nat_dec x 0). subst. simpl. - repeat rewrite mult_1_r. - rewrite <- plus_0_l at 1. - eapply plus_le_compat; intuition. + repeat rewrite Nat.mul_1_r. + rewrite <- Nat.add_0_l at 1. + eapply Nat.add_le_mono; intuition. - rewrite <- plus_0_l at 1. - rewrite <- plus_0_r at 1. + rewrite <- Nat.add_0_l at 1. + rewrite <- Nat.add_0_r at 1. - eapply plus_le_compat; intuition. - eapply plus_le_compat; intuition. - eapply mult_le_compat; intuition. + eapply Nat.add_le_mono; intuition. + eapply Nat.add_le_mono; intuition. + eapply Nat.mul_le_mono; intuition. destruct (eq_nat_dec n 0); subst. rewrite expnat_0; lia. - rewrite <- mult_1_l at 1. - eapply mult_le_compat; intuition. + rewrite <- Nat.mul_1_l at 1. + eapply Nat.mul_le_mono; intuition. lia. Qed. @@ -84,19 +84,19 @@ Theorem polynomial_plus : exists (x4 + x1). intuition. - eapply le_trans. - eapply plus_le_compat. + eapply Nat.le_trans. + eapply Nat.add_le_mono. eapply H6; trivial. eapply H7; trivial. - rewrite mult_plus_distr_r. - repeat rewrite plus_assoc. - eapply plus_le_compat; trivial. - rewrite plus_comm. - rewrite plus_assoc. - eapply plus_le_compat; trivial. - rewrite plus_comm. - eapply plus_le_compat; - eapply mult_le_compat; intuition. + rewrite Nat.mul_add_distr_r. + repeat rewrite Nat.add_assoc. + eapply Nat.add_le_mono; trivial. + rewrite Nat.add_comm. + rewrite Nat.add_assoc. + eapply Nat.add_le_mono; trivial. + rewrite Nat.add_comm. + eapply Nat.add_le_mono; + eapply Nat.mul_le_mono; intuition. eapply expnat_exp_le; intuition. eapply expnat_exp_le; intuition. @@ -145,77 +145,77 @@ Theorem polynomial_mult : exists (3 * (x3 * x0 * x4 * x1)). exists (x4 * x1). intros n. - eapply le_trans. - eapply mult_le_compat. + eapply Nat.le_trans. + eapply Nat.mul_le_mono. eapply H6; intuition. eapply H7; intuition. - repeat rewrite mult_plus_distr_l. - repeat rewrite mult_plus_distr_r. + repeat rewrite Nat.mul_add_distr_l. + repeat rewrite Nat.mul_add_distr_r. - rewrite plus_assoc. - eapply plus_le_compat; trivial. + rewrite Nat.add_assoc. + eapply Nat.add_le_mono; trivial. rewrite expnat_plus. simpl. - rewrite plus_0_r. - repeat rewrite mult_plus_distr_r. - rewrite plus_assoc. - eapply plus_le_compat. - eapply plus_le_compat. - rewrite (mult_comm (expnat n x)). - repeat rewrite mult_assoc. - eapply mult_le_compat. 2: reflexivity. - rewrite mult_comm. - rewrite mult_assoc. - eapply mult_le_compat. 2: reflexivity. - rewrite <- mult_1_r at 1. - rewrite <- mult_1_r at 1. - eapply mult_le_compat. 2: auto with zarith. - eapply mult_le_compat. 2: auto with zarith. - rewrite mult_comm. + rewrite Nat.add_0_r. + repeat rewrite Nat.mul_add_distr_r. + rewrite Nat.add_assoc. + eapply Nat.add_le_mono. + eapply Nat.add_le_mono. + rewrite (Nat.mul_comm (expnat n x)). + repeat rewrite Nat.mul_assoc. + eapply Nat.mul_le_mono. 2: reflexivity. + rewrite Nat.mul_comm. + rewrite Nat.mul_assoc. + eapply Nat.mul_le_mono. 2: reflexivity. + rewrite <- Nat.mul_1_r at 1. + rewrite <- Nat.mul_1_r at 1. + eapply Nat.mul_le_mono. 2: auto with zarith. + eapply Nat.mul_le_mono. 2: auto with zarith. + rewrite Nat.mul_comm. reflexivity. destruct (eq_nat_dec n 0); subst. repeat rewrite expnat_0. simpl. - repeat rewrite mult_0_r. + repeat rewrite Nat.mul_0_r. reflexivity. trivial. trivial. - rewrite (mult_comm (expnat n x)). - repeat rewrite mult_assoc. - eapply mult_le_compat; trivial. - rewrite <- mult_1_r at 1. - eapply mult_le_compat; trivial. - rewrite <- mult_1_r at 1. - eapply mult_le_compat; trivial. - rewrite mult_comm. - eapply mult_le_compat; trivial. - rewrite <- mult_1_l at 1. - eapply mult_le_compat; trivial. + rewrite (Nat.mul_comm (expnat n x)). + repeat rewrite Nat.mul_assoc. + eapply Nat.mul_le_mono; trivial. + rewrite <- Nat.mul_1_r at 1. + eapply Nat.mul_le_mono; trivial. + rewrite <- Nat.mul_1_r at 1. + eapply Nat.mul_le_mono; trivial. + rewrite Nat.mul_comm. + eapply Nat.mul_le_mono; trivial. + rewrite <- Nat.mul_1_l at 1. + eapply Nat.mul_le_mono; trivial. eapply expnat_ge_1. lia. destruct (eq_nat_dec n 0); subst. repeat rewrite expnat_0. simpl. - repeat rewrite mult_0_r. + repeat rewrite Nat.mul_0_r. intuition. trivial. trivial. - rewrite (mult_comm (expnat n x)). - repeat rewrite mult_assoc. - rewrite <- mult_1_r at 1. - eapply mult_le_compat; trivial. - rewrite <- mult_assoc. - rewrite (mult_comm (expnat n x2)). - rewrite mult_assoc. - eapply mult_le_compat; trivial. - eapply mult_le_compat; trivial. - rewrite <- mult_1_r at 1. - eapply mult_le_compat; trivial. - rewrite <- mult_1_r at 1. - eapply mult_le_compat; trivial. + rewrite (Nat.mul_comm (expnat n x)). + repeat rewrite Nat.mul_assoc. + rewrite <- Nat.mul_1_r at 1. + eapply Nat.mul_le_mono; trivial. + rewrite <- Nat.mul_assoc. + rewrite (Nat.mul_comm (expnat n x2)). + rewrite Nat.mul_assoc. + eapply Nat.mul_le_mono; trivial. + eapply Nat.mul_le_mono; trivial. + rewrite <- Nat.mul_1_r at 1. + eapply Nat.mul_le_mono; trivial. + rewrite <- Nat.mul_1_r at 1. + eapply Nat.mul_le_mono; trivial. eapply expnat_ge_1. lia. Qed. @@ -303,8 +303,8 @@ Lemma negligible_plus : rewrite H8 in H3. eapply H2. - eapply le_lt_trans. - eapply Max.le_max_r. + eapply Nat.le_lt_trans. + eapply Nat.le_max_r. eauto. rewrite H7. @@ -321,8 +321,8 @@ Lemma negligible_plus : rewrite H8 in H3. eapply H1. - eapply le_lt_trans. - eapply Max.le_max_l. + eapply Nat.le_lt_trans. + eapply Nat.le_max_l. eauto. rewrite H7. @@ -349,7 +349,7 @@ Theorem double_log_plus_3_le_h : induction y; intuition; simpl in *. lia. - rewrite plus_0_r in *. + rewrite Nat.add_0_r in *. assert (S (y + S y + 3) = (y + y + 3) + 2). @@ -367,14 +367,14 @@ Theorem double_log_plus_3_le_h : lia. lia. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H2. } simpl. lia. - assert ( y + y + 3 <= div2 x). + assert ( y + y + 3 <= Nat.div2 x). eapply IHy. symmetry. @@ -382,12 +382,12 @@ Theorem double_log_plus_3_le_h : trivial. lia. - assert (2 <= div2 x). - assert (2 = div2 4). + assert (2 <= Nat.div2 x). + assert (2 = Nat.div2 4). trivial. rewrite H3. eapply div2_le_mono. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply Nat.log2_le_lin. destruct (eq_nat_dec 0 x); subst. @@ -397,8 +397,8 @@ Theorem double_log_plus_3_le_h : } lia. - eapply le_trans. - eapply plus_le_compat. + eapply Nat.le_trans. + eapply Nat.add_le_mono. eapply H2. eapply H3. @@ -415,14 +415,14 @@ Theorem S_log_square_lt_h : induction y; intuition; simpl in *. lia. - assert (y = Nat.log2 (div2 x)). + assert (y = Nat.log2 (Nat.div2 x)). symmetry. eapply log2_div2. trivial. - rewrite (mult_comm _ (S (S y))). + rewrite (Nat.mul_comm _ (S (S y))). simpl. - rewrite (mult_comm _ (S y)) in IHy. + rewrite (Nat.mul_comm _ (S y)) in IHy. simpl in *. assert ( S (S (y + S (S (y + (y + (y + y * y)))))) = @@ -451,23 +451,23 @@ Theorem S_log_square_lt_h : lia. lia. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H3. } simpl. lia. - assert ( S (y + (y + y * y)) <= div2 x). + assert ( S (y + (y + y * y)) <= Nat.div2 x). eapply IHy. trivial. lia. - assert (2 * y + 3 <= div2 x). + assert (2 * y + 3 <= Nat.div2 x). eapply double_log_plus_3_le_h; trivial. lia. - eapply le_trans. - eapply plus_le_compat. + eapply Nat.le_trans. + eapply Nat.add_le_mono. eapply H2. eapply H3. @@ -482,7 +482,7 @@ Theorem S_log_square_lt : intuition. eapply S_log_square_lt_h; trivial. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply Nat.log2_le_mono. eapply H. @@ -499,7 +499,7 @@ Theorem log_square_lt : assert (Nat.log2 x < S (Nat.log2 x)). lia. - eapply lt_le_trans. + eapply Nat.lt_le_trans. eapply mult_lt_compat. eapply H0. @@ -518,7 +518,7 @@ Theorem poly_lt_exp_ge_6 : specialize (Nat.log2_spec_alt); intuition. destruct (H1 x). - eapply lt_le_trans. + eapply Nat.lt_le_trans. 2:{ eapply H. } @@ -528,7 +528,7 @@ Theorem poly_lt_exp_ge_6 : (* This case split probably isn't necessary *) destruct (eq_nat_dec x0 0). rewrite e in H3. - rewrite plus_0_r in *. + rewrite Nat.add_0_r in *. rewrite H3. rewrite <- Nat.pow_mul_r. @@ -541,13 +541,13 @@ Theorem poly_lt_exp_ge_6 : lia. rewrite <- H3. trivial. - eapply le_lt_trans. - eapply mult_le_compat. - eapply le_refl. + eapply Nat.le_lt_trans. + eapply Nat.mul_le_mono. + eapply Nat.le_refl. eapply H4. eapply log_square_lt. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H0. } @@ -558,7 +558,7 @@ Theorem poly_lt_exp_ge_6 : destruct (eq_nat_dec c 0). rewrite e. simpl. - eapply le_lt_trans. + eapply Nat.le_lt_trans. assert (1 <= expnat 2 0). trivial. eapply H4. @@ -571,7 +571,7 @@ Theorem poly_lt_exp_ge_6 : lia. eapply Nat.log2_spec. lia. - eapply lt_le_trans. + eapply Nat.lt_le_trans. eapply H4. rewrite <- Nat.pow_mul_r. @@ -580,20 +580,20 @@ Theorem poly_lt_exp_ge_6 : assert (c <= S (Nat.log2 x)). eapply (@Nat.pow_le_mono_r_iff 2). lia. - eapply le_trans. + eapply Nat.le_trans. eapply H. - eapply lt_le_weak. + eapply Nat.lt_le_incl. eapply Nat.log2_spec. lia. - eapply le_trans. - eapply mult_le_compat. - eapply le_refl. + eapply Nat.le_trans. + eapply Nat.mul_le_mono. + eapply Nat.le_refl. eapply H6. eapply S_log_square_lt. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H0. } @@ -612,21 +612,21 @@ Theorem poly_lt_exp : exists (expnat 2 (max c 6)). intuition. eapply poly_lt_exp_ge_6. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H. } eapply Nat.pow_le_mono_r. lia. - eapply Max.le_max_l. + eapply Nat.le_max_l. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H. } eapply Nat.pow_le_mono_r. lia. - eapply Max.le_max_r. + eapply Nat.le_max_r. Qed. Theorem negligible_exp_den : @@ -682,7 +682,7 @@ Theorem negligible_const_mult : rewrite <- ratMult_num_den. eapply eqRat_terms. symmetry. - eapply mult_1_r. + eapply Nat.mul_1_r. unfold natToPosnat, posnatToNat, posnatMult. rewrite expnat_plus. trivial. @@ -703,10 +703,10 @@ Theorem negligible_const_mult : eapply rat_le_1. destruct d. unfold natToPosnat, posnatToNat, posnatMult. - rewrite mult_comm. - eapply mult_le_compat. + rewrite Nat.mul_comm. + eapply Nat.mul_le_mono. - eapply le_trans. + eapply Nat.le_trans. eapply le_expnat_2. eapply expnat_base_le. lia. @@ -761,7 +761,7 @@ Theorem negligible_exp : rewrite <- ratMult_num_den. eapply eqRat_terms; trivial. unfold posnatToNat, natToPosnat, posnatMult. - eapply mult_1_l. + eapply Nat.mul_1_l. Qed. @@ -776,9 +776,9 @@ Theorem negligible_const_num : intuition. rewrite <- ratMult_num_den. eapply eqRat_terms. - eapply mult_1_r. + eapply Nat.mul_1_r. unfold natToPosnat, posnatToNat, posnatMult. - eapply mult_1_l. + eapply Nat.mul_1_l. Qed. Theorem negligible_poly_num : @@ -793,7 +793,7 @@ Theorem negligible_poly_num : intuition. eapply leRat_terms. eapply H. - eapply le_refl. + eapply Nat.le_refl. eapply negligible_eq. eapply negligible_plus. @@ -812,7 +812,7 @@ Theorem negligible_poly_num : assert (posnatToNat (pos expnat 2 n) = posnatToNat (posnatMult (pos 1) (pos expnat 2 n))). unfold natToPosnat, posnatToNat, posnatMult. symmetry. - eapply mult_1_l. + eapply Nat.mul_1_l. eapply H0. eapply eqRat_refl. Qed. diff --git a/src/FCF/Blist.v b/src/FCF/Blist.v index 82f38b2..468454d 100644 --- a/src/FCF/Blist.v +++ b/src/FCF/Blist.v @@ -111,7 +111,7 @@ Theorem shiftOut_None_inv : forall n ls, n > length ls. induction n; destruct ls; intuition; simpl in *; try discriminate. - apply gt_n_S. + apply ->Nat.succ_lt_mono. eapply IHn. case_eq (shiftOut ls n); intuition; trivial. rewrite H0 in H. @@ -308,7 +308,7 @@ Lemma getAllBvectors_length : forall n, induction n; intuition; simpl in *. rewrite app_length. repeat rewrite map_length. - rewrite plus_0_r. + rewrite Nat.add_0_r. f_equal; eauto. Qed. @@ -318,12 +318,8 @@ Lemma getAllBvectors_length_nz : forall n, induction n; intuition; simpl in *. rewrite app_length. repeat rewrite map_length. - rewrite <- plus_0_r. - eapply gt_trans. - eapply plus_gt_compat_l. - apply IHn. - repeat rewrite plus_0_r. - apply IHn. + apply Nat.lt_le_trans with (1 := IHn). + now apply Nat.le_add_r. Qed. Theorem in_getAllBvectors : forall (n : nat)(v : Bvector n), @@ -600,7 +596,7 @@ Lemma getAllBlists_app_In_length : forall n ls, subst; rewrite app_length; simpl; - rewrite plus_comm; simpl; + rewrite Nat.add_comm; simpl; f_equal; eapply IHn; eauto. Qed. @@ -699,7 +695,7 @@ Theorem getAllBlists_length : forall n, induction n; intuition; simpl in *. rewrite app_length. repeat rewrite map_length. - rewrite plus_0_r. + rewrite Nat.add_0_r. rewrite <- IHn. trivial. Qed. diff --git a/src/FCF/CompFold.v b/src/FCF/CompFold.v index d819b63..2f27392 100644 --- a/src/FCF/CompFold.v +++ b/src/FCF/CompFold.v @@ -1050,7 +1050,7 @@ Lemma list_pred_allNatsLt : econstructor. rewrite app_length. - rewrite plus_comm. + rewrite Nat.add_comm. simpl. eapply list_pred_rev. @@ -1064,7 +1064,7 @@ Lemma list_pred_allNatsLt : intuition. rewrite app_nth2. - rewrite minus_diag. + rewrite Nat.sub_diag. simpl. trivial. intuition. @@ -1554,7 +1554,7 @@ Lemma lookupIndex_lt_length : destruct (eqd a0 a); subst. lia. - eapply lt_n_S. + apply ->Nat.succ_lt_mono. eapply IHls. trivial. @@ -1574,7 +1574,7 @@ Lemma fold_add_init_nat_h : init1 + fold_left (fun acc a => acc + (f a))%nat ls init2)%nat. induction ls; intuition; simpl in *. - rewrite <- plus_assoc. + rewrite <- Nat.add_assoc. eapply IHls. Qed. @@ -1585,7 +1585,7 @@ Lemma fold_add_init_nat : init + fold_left (fun acc a => acc + (f a))%nat ls O)%nat. intuition. - rewrite <- (plus_0_r init) at 1. + rewrite <- (Nat.add_0_r init) at 1. rewrite fold_add_init_nat_h. trivial. Qed. @@ -1626,7 +1626,7 @@ Lemma fold_add_nat_Permutation : f_equal. eauto. - rewrite plus_comm. + rewrite Nat.add_comm. trivial. Qed. @@ -1687,13 +1687,13 @@ Lemma fold_add_nat_filter_partition : destruct (P a); simpl; repeat rewrite (fold_add_init_nat _ _ (f a)). rewrite IHls. - repeat rewrite plus_assoc. + repeat rewrite Nat.add_assoc. trivial. rewrite IHls. - repeat rewrite plus_assoc. + repeat rewrite Nat.add_assoc. f_equal. - rewrite plus_comm. + rewrite Nat.add_comm. trivial. Qed. @@ -1721,7 +1721,8 @@ Lemma fold_left_add_removePresent : simpl. repeat rewrite (@fold_add_init_nat _ _ _ (f a)). - rewrite <- minus_plus_simpl_l_reverse. + rewrite Nat.sub_add_distr, Nat.add_sub_swap, Nat.sub_diag, Nat.add_0_l + by (exact (Nat.le_refl _)). f_equal. eapply fold_add_nat_Permutation. eapply intersect_comm_Permutation; intuition. @@ -1743,8 +1744,8 @@ Lemma fold_left_add_removePresent : eapply intersect_comm_Permutation; intuition. rewrite (@fold_add_nat_filter_partition _ (fun a => if (in_dec eqd a u) then true else false) _ ls). - rewrite <- plus_0_r at 1. - eapply plus_le_compat; intuition. + rewrite <- Nat.add_0_r at 1. + eapply Nat.add_le_mono; intuition. trivial. trivial. @@ -2003,7 +2004,7 @@ Lemma nth_lt_length : destruct i; subst. lia. - eapply lt_n_S. + apply ->Nat.succ_lt_mono. eauto. Qed. @@ -2187,7 +2188,7 @@ Theorem list_pred_app_both_if : eapply list_pred_app in H0. rewrite H in H0. rewrite ?firstn_app, ?skipn_app, ?firstn_ge_all, - ?minus_diag, ?firstn_O, ?app_nil_r in * by lia. + ?Nat.sub_diag, ?firstn_O, ?app_nil_r in * by lia. firstorder. Qed. diff --git a/src/FCF/DistSem.v b/src/FCF/DistSem.v index 59e0d38..3228595 100644 --- a/src/FCF/DistSem.v +++ b/src/FCF/DistSem.v @@ -363,7 +363,7 @@ Lemma evalDist_lossless : forall (A : Set)(c : Comp A), rewrite sumList_body_const. rewrite getAllBvectors_length. rewrite <- ratMult_num_den. - rewrite mult_1_l. + rewrite Nat.mul_1_l. eapply num_dem_same_rat1. rewrite posnatMult_1_r. @@ -515,7 +515,7 @@ Lemma evalDist_sum_le_1 : forall (A : Set)(c : Comp A), rewrite sumList_body_const. rewrite getAllBvectors_length. rewrite <- ratMult_num_den. - rewrite mult_1_l. + rewrite Nat.mul_1_l. eapply eqRat_impl_leRat. eapply num_dem_same_rat1. diff --git a/src/FCF/EqDec.v b/src/FCF/EqDec.v index f8cbf03..94e2ca8 100644 --- a/src/FCF/EqDec.v +++ b/src/FCF/EqDec.v @@ -254,12 +254,12 @@ refine {| eqb := (fun x y => (leb x y) && (leb y x)) |}. intuition. apply andb_true_iff in H. intuition. -eapply le_antisym; +eapply Nat.le_antisymm; eapply leb_iff; eauto. apply andb_true_iff. intuition; -eapply leb_iff; subst; eapply le_refl. +eapply leb_iff; subst; eapply Nat.le_refl. Qed. diff --git a/src/FCF/Fold.v b/src/FCF/Fold.v index cfa254e..0a7246b 100644 --- a/src/FCF/Fold.v +++ b/src/FCF/Fold.v @@ -1228,9 +1228,9 @@ Lemma fold_left_max_ge_init : forall (ls : list nat)(n : nat), fold_left max ls n >= n. induction ls; intuition; simpl in *. - eapply le_trans. - eapply Max.max_lub_l. - eapply le_refl. + eapply Nat.le_trans. + eapply Nat.max_lub_l. + eapply Nat.le_refl. eapply IHls. Qed. @@ -1244,9 +1244,9 @@ Lemma maxList_correct_h : forall (ls : list nat)(n init : nat), simpl in *. intuition; subst. - eapply le_trans. - eapply Max.max_lub_r. - eapply le_refl. + eapply Nat.le_trans. + eapply Nat.max_lub_r. + eapply Nat.le_refl. eapply fold_left_max_ge_init. Qed. @@ -2164,7 +2164,7 @@ Lemma sumList_rel_factor_constant : forall (p1 p2 : posnat) (A : Type)(rel : A - unfold posnatMult, natToPosnat, posnatToNat. destruct p1. destruct p2. - apply mult_comm. + apply Nat.mul_comm. trivial. Qed. @@ -3435,7 +3435,7 @@ Lemma allNatsLt_length : induction n; intuition; simpl in *. rewrite app_length. rewrite IHn. - rewrite plus_comm. + rewrite Nat.add_comm. trivial. Qed. @@ -3551,7 +3551,7 @@ Lemma nth_allNatsLt_lt : assert (k = n). lia. rewrite H0. - rewrite minus_diag. + rewrite Nat.sub_diag. simpl. trivial. rewrite allNatsLt_length. @@ -3943,7 +3943,7 @@ Theorem nth_skipn_eq : nth x (skipn y ls) def = nth (x + y) ls def. induction y; intuition; simpl in *. - rewrite plus_0_r. + rewrite Nat.add_0_r. trivial. destruct ls. @@ -3951,9 +3951,9 @@ Theorem nth_skipn_eq : rewrite nth_nil. trivial. - rewrite plus_comm. + rewrite Nat.add_comm. simpl. - rewrite plus_comm. + rewrite Nat.add_comm. eapply IHy. @@ -4630,9 +4630,8 @@ Theorem nth_option_Some_lt : discriminate. destruct i. lia. - eapply lt_n_S. + apply ->Nat.succ_lt_mono. eauto. - Qed. Theorem nth_option_app_None : @@ -4888,7 +4887,7 @@ Lemma forNats_In : intuition; subst. lia. - eapply lt_trans. + eapply Nat.lt_trans. eapply IHn. trivial. lia. diff --git a/src/FCF/GroupTheory.v b/src/FCF/GroupTheory.v index 6e04beb..0924710 100644 --- a/src/FCF/GroupTheory.v +++ b/src/FCF/GroupTheory.v @@ -81,16 +81,16 @@ Section GroupProperties. ((x^n1)^n2) = (x^(n1 * n2)). induction n2; intuition; simpl in *. - rewrite mult_0_r. + rewrite Nat.mul_0_r. trivial. - rewrite mult_comm. + rewrite Nat.mul_comm. simpl. rewrite groupExp_plus. f_equal. rewrite IHn2. - rewrite mult_comm. + rewrite Nat.mul_comm. trivial. Qed. @@ -127,7 +127,7 @@ Section FiniteCyclicGroupProperties. g^(c1 * order + v) = g^v. induction c1; intuition; simpl in *. - rewrite <- plus_assoc. + rewrite <- Nat.add_assoc. rewrite (groupExp_plus order). rewrite groupOrder; trivial. rewrite groupIdent; trivial. diff --git a/src/FCF/HasDups.v b/src/FCF/HasDups.v index fb2ae1b..9d5886a 100644 --- a/src/FCF/HasDups.v +++ b/src/FCF/HasDups.v @@ -170,7 +170,7 @@ Section DupProb. eapply leRat_trans. 2:{ eapply leRat_terms. - eapply le_n_Sn. + eapply Nat.le_succ_diag_r. reflexivity. } @@ -185,7 +185,7 @@ Section DupProb. eapply leRat_terms; lia. eapply leRat_terms; intuition. simpl. - eapply mult_le_compat; intuition. + eapply Nat.mul_le_mono; intuition. eapply leRat_trans. 2:{ diff --git a/src/FCF/Limit.v b/src/FCF/Limit.v index bc53444..81dcd4a 100644 --- a/src/FCF/Limit.v +++ b/src/FCF/Limit.v @@ -66,7 +66,7 @@ Section Limit. Variable plus_0_eq : forall (a1 a2 : A), eq a2 zero -> eq a1 (plus a1 a2). - Variable plus_le_compat : forall a1 a2 a3 a4, + Variable add_le_mono : forall a1 a2 a3 a4, le a1 a2 -> le a3 a4 -> le (plus a1 a3) (plus a2 a4). @@ -171,15 +171,15 @@ Section Limit. eapply le_trans. eapply (triangle_inequality _ _ x1). eapply le_trans. - eapply plus_le_compat. + eapply add_le_mono. eapply le_trans. eapply le_eq. eapply distance_comm. eapply H1. - eapply Max.max_lub_l; eauto. + eapply Nat.max_lub_l; eauto. trivial. eapply H2. - eapply Max.max_lub_r; eauto. + eapply Nat.max_lub_r; eauto. trivial. eapply le_eq. eapply half_plus. @@ -252,12 +252,12 @@ Theorem rat_inf_limit_2_trans : forall f1 f2 f3, eapply leRat_trans. eapply ratDistance_le_trans. eapply H3. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eapply H5. trivial. eapply H8. eapply H4. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eapply H5. eauto. trivial. @@ -288,24 +288,24 @@ Lemma rat_inf_limit_squeeze : forall (f1 f2 f: nat -> Rat -> Prop) c (v : Rat), eapply leRat_trans. eapply ratDistance_le_max. eapply H1. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. eapply H9. eapply H10. eapply H2. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. eapply H9. eapply H11. - eapply maxRat_leRat_same; eauto using Max.max_lub_l, Max.max_lub_r. + eapply maxRat_leRat_same; eauto using Nat.max_lub_l, Nat.max_lub_r. Qed. Lemma rat_inf_limit_div_2 : forall (f : nat -> Rat -> Prop)(v : Rat), rat_inf_limit f v -> - rat_inf_limit (fun n => (f (div2 n))) v. + rat_inf_limit (fun n => (f (Nat.div2 n))) v. unfold rat_inf_limit, inf_limit. intuition. @@ -313,7 +313,7 @@ Lemma rat_inf_limit_div_2 : forall (f : nat -> Rat -> Prop)(v : Rat), econstructor. intuition. - specialize (H1 (div2 n')). + specialize (H1 (Nat.div2 n')). eapply H1. eapply div2_ge; eauto. @@ -335,7 +335,7 @@ Lemma rat_inf_limit_sum : forall (f1 f2 : nat -> Rat -> Prop) v1 v2, edestruct (H2 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. - exists (Max.max x x0). + exists (Nat.max x x0). intuition. unfold ratAdd_rel in *. destruct (H n'). @@ -347,10 +347,10 @@ Lemma rat_inf_limit_sum : forall (f1 f2 : nat -> Rat -> Prop) v1 v2, rewrite H5. rewrite ratHalf_add. intuition. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eauto. trivial. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. trivial. Qed. @@ -375,7 +375,7 @@ Lemma rat_inf_limit_difference : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, edestruct (H2 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. - exists (Max.max x x0). + exists (Nat.max x x0). intuition. unfold ratSubtract_rel in *. destruct (H n'). @@ -392,7 +392,7 @@ Lemma rat_inf_limit_difference : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, rewrite H4. rewrite ratHalf_add. intuition. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. trivial. } @@ -406,7 +406,7 @@ Lemma rat_inf_limit_difference : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, rewrite H5. rewrite <- ratAdd_0_l. intuition. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eauto. trivial. @@ -434,7 +434,7 @@ Lemma rat_inf_limit_difference : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, eapply ratSubtract_0_inv. trivial. - exists (Max.max x x0). + exists (Nat.max x x0). intuition. destruct (H n'). destruct (H0 n'). @@ -444,7 +444,7 @@ Lemma rat_inf_limit_difference : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, eapply leRat_trans. eapply ratDistance_le_sum. eapply H5. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eauto. trivial. eapply leRat_trans. @@ -460,7 +460,7 @@ Lemma rat_inf_limit_difference : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, eapply leRat_trans. rewrite ratDistance_comm. eapply H4. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. trivial. eapply minRat_le_r. @@ -476,12 +476,12 @@ Lemma rat_inf_limit_difference : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, trivial. eapply H4. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. trivial. eapply H5. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eauto. trivial. @@ -540,13 +540,13 @@ Lemma rat_inf_limit_product : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, eapply ratMult_leRat_compat. eapply ratDistance_le_sum. eapply H6; [idtac | eapply H10]. - eapply le_trans. + eapply Nat.le_trans. eapply (maxList_correct (x :: x0 :: x1 :: nil)). simpl. intuition. trivial. eapply H4; [idtac | eapply H9]. - eapply le_trans. + eapply Nat.le_trans. eapply (maxList_correct (x :: x0 :: x1 :: nil)). simpl. intuition. @@ -555,7 +555,7 @@ Lemma rat_inf_limit_product : forall (f1 f2 : nat -> Rat -> Prop) c1 c2, eapply (ratAdd_any_leRat_l 1). eapply leRat_refl. eapply H5; [idtac | eapply H10]. - eapply le_trans. + eapply Nat.le_trans. eapply (maxList_correct (x :: x0 :: x1 :: nil)). simpl. intuition. @@ -651,7 +651,7 @@ Lemma rat_inf_limit_trans : forall (f1 f2 : nat -> Rat -> Prop) a, edestruct (H0 (ratHalf epsilon)). eapply ratHalf_ne_0. intuition. - exists (Max.max x x0). + exists (Nat.max x x0). intuition. destruct (H1 n'). eapply leRat_trans. @@ -660,10 +660,10 @@ Lemma rat_inf_limit_trans : forall (f1 f2 : nat -> Rat -> Prop) a, rewrite H4. rewrite ratHalf_add. intuition. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eauto. eauto. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. trivial. trivial. @@ -895,7 +895,7 @@ Lemma rat_inf_limit_exp_0 : forall (f : nat -> Rat -> Prop) a, eapply half_distance_1_le; trivial. trivial. - exists (Max.max x x0). + exists (Nat.max x x0). intuition. unfold expRat_rel in *. destruct (H1 n'). @@ -906,14 +906,14 @@ Lemma rat_inf_limit_exp_0 : forall (f : nat -> Rat -> Prop) a, eapply expRat_leRat_compat. eapply ratDistance_le_sum. eapply H3. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eauto. trivial. eapply expRat_le'. eauto. eapply half_distance_1_le; trivial. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eauto. Qed. @@ -1066,13 +1066,13 @@ Lemma rat_inf_limit_mono : forall (f : nat -> Rat -> Prop) (g : nat -> nat)(v : econstructor. intuition. eapply (H3 (g n')). - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H0. eapply H5. } rewrite <- H4. - eapply le_refl. + eapply Nat.le_refl. trivial. Qed. diff --git a/src/FCF/Lognat.v b/src/FCF/Lognat.v index 957e9ad..eb9cf80 100644 --- a/src/FCF/Lognat.v +++ b/src/FCF/Lognat.v @@ -430,7 +430,7 @@ Lemma lognat_prod_sum_gen_h : forall (a' a b: nat)(pf1 : (a <> 0))(pf2 : (b <> 0 rewrite <- (lognat_prod_sum H0) in H. assert (lognat pf3 = S (lognat H1)). generalize pf3. - rewrite mult_assoc_reverse. + rewrite <-Nat.mul_assoc. intros. rewrite (lognat_prod_sum _ pf0). trivial. @@ -449,7 +449,7 @@ Lemma lognat_prod_sum_gen_h : forall (a' a b: nat)(pf1 : (a <> 0))(pf2 : (b <> 0 assert (2 * x <> 0). lia. assert (x * b <> 0). destruct x; destruct b; simpl; congruence. - assert (2 * x * b <> 0). rewrite mult_assoc_reverse. lia. +assert (2 * x * b <> 0). rewrite <-Nat.mul_assoc. lia. subst. rewrite (lognat_odd _ H1) in H. rewrite <- (lognat_prod_sum n) in H. @@ -462,12 +462,12 @@ Lemma lognat_prod_sum_gen_h : forall (a' a b: nat)(pf1 : (a <> 0))(pf2 : (b <> 0 assert (S (2 * x) * b = b + 2 * x * b). intuition. rewrite H4. intros. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply (lognat_monotonic H3). intuition. } generalize H3. - rewrite mult_assoc_reverse. + rewrite <-Nat.mul_assoc. intros. rewrite <- (lognat_prod_sum H2). lia. diff --git a/src/FCF/OracleHybrid.v b/src/FCF/OracleHybrid.v index f39b6f7..fc2e638 100644 --- a/src/FCF/OracleHybrid.v +++ b/src/FCF/OracleHybrid.v @@ -489,8 +489,8 @@ Section OracleMapHybrid. econstructor. intuition. econstructor. - rewrite mult_1_r. - rewrite plus_0_r. + rewrite Nat.mul_1_r. + rewrite Nat.add_0_r. eapply max_queries. eauto. Qed. @@ -627,7 +627,7 @@ Section OracleMapHybrid. fcf_inline_first. fcf_simp. - rewrite plus_0_r in H6. + rewrite Nat.add_0_r in H6. destruct (ge_dec i (length l)). rewrite skipn_ge_nil; trivial. unfold oracleMap. diff --git a/src/FCF/Rat.v b/src/FCF/Rat.v index 8f59fef..b76b1bc 100644 --- a/src/FCF/Rat.v +++ b/src/FCF/Rat.v @@ -75,18 +75,18 @@ Ltac rattac_one := (* rules that solve goals *) | [|- posnatMult ?x1 ?x2 = posnatMult ?x2 ?x1] => apply posnatMult_comm | [|- posnatToNat (posnatMult ?x1 ?x2) = posnatToNat (posnatMult ?x2 ?x1)] => rewrite posnatMult_comm; trivial - | [|- ?x1 * ?x2 = ?x2 * ?x1 ] => apply mult_comm + | [|- ?x1 * ?x2 = ?x2 * ?x1 ] => apply Nat.mul_comm | [|- (mult (?x1 + ?x2) _) = (mult (?x2 + ?x1) _ )] => f_equal | [|- ?x1 * ?x2 * _ = ?x2 * ?x1 * _ ] => f_equal | [ |- posnatToNat ?p > 0 ] => destruct p; unfold posnatToNat; lia (* inversion on hypotheses *) | [H1 : ?n * ?x = ?n0 * ?x1, H2: ?n1 * ?x1 = ?n * ?x0 |- ?n1 * ?x = ?n0 * ?x0 ] => eapply (@mult_same_l x1)(* ; - [idtac | rewrite mult_assoc ; - rewrite (mult_comm x1 n1); + [idtac | rewrite Nat.mul_assoc ; + rewrite (Nat.mul_comm x1 n1); rewrite H2; - rewrite <- mult_assoc ; - rewrite (mult_comm x x0) ; - repeat rewrite mult_assoc; + rewrite <- Nat.mul_assoc ; + rewrite (Nat.mul_comm x x0) ; + repeat rewrite Nat.mul_assoc; f_equal] *) | [H : ?x = ?n * (posnatToNat ?p) |- ?x = (posnatToNat ?p) * ?n ] => rewrite H | [H : RatIntro _ _ = RatIntro _ _ |- _ ] => inversion H; clear H; subst @@ -117,7 +117,7 @@ Ltac rattac_one := end. Ltac rattac := intuition idtac; unfold ratCD in *; - repeat (rattac_one; subst); repeat rewrite mult_1_r; repeat rewrite plus_0_r; trivial; try congruence; try lia. + repeat (rattac_one; subst); repeat rewrite Nat.mul_1_r; repeat rewrite Nat.add_0_r; trivial; try congruence; try lia. Lemma ratCD_comm : forall r1 r2 n1 n2 d n1' n2' d', ratCD r1 r2 = (n1, n2, d) -> @@ -229,18 +229,18 @@ Theorem leRat_trans : forall r1 r2 r3, rattac. eapply (@mult_le_compat_r_iff x1); trivial. - rewrite <- mult_assoc. - rewrite (mult_comm x). - rewrite mult_assoc. - eapply le_trans. - eapply mult_le_compat. + rewrite <- Nat.mul_assoc. + rewrite (Nat.mul_comm x). + rewrite Nat.mul_assoc. + eapply Nat.le_trans. + eapply Nat.mul_le_mono. eapply l. eauto. - repeat rewrite <- mult_assoc. - repeat rewrite (mult_comm x0). - repeat rewrite mult_assoc. - eapply mult_le_compat; eauto. + repeat rewrite <- Nat.mul_assoc. + repeat rewrite (Nat.mul_comm x0). + repeat rewrite Nat.mul_assoc. + eapply Nat.mul_le_mono; eauto. Qed. Theorem eqRat_impl_leRat : forall r1 r2, @@ -336,7 +336,7 @@ Theorem ratAdd_0_r : forall r, rattac; inversion H; subst; - rewrite mult_1_r; + rewrite Nat.mul_1_r; trivial. Qed. @@ -363,13 +363,13 @@ Theorem ratAdd_assoc : forall r1 r2 r3, Local Open Scope nat_scope. Ltac arithNormalize_step := - repeat rewrite mult_succ_r in *; - repeat rewrite mult_plus_distr_r in *; - repeat rewrite mult_plus_distr_l in *; - repeat rewrite mult_minus_distr_r in *; - repeat rewrite mult_minus_distr_l in *; - repeat rewrite plus_assoc in *; - repeat rewrite mult_assoc in *. + repeat rewrite Nat.mul_succ_r in *; + repeat rewrite Nat.mul_add_distr_r in *; + repeat rewrite Nat.mul_add_distr_l in *; + repeat rewrite Nat.mul_sub_distr_r in *; + repeat rewrite Nat.mul_sub_distr_l in *; + repeat rewrite Nat.add_assoc in *; + repeat rewrite Nat.mul_assoc in *. Ltac arithNormalize := repeat arithNormalize_step. @@ -380,12 +380,12 @@ Theorem ratAdd_assoc : forall r1 r2 r3, | [|- _ + (?x1 * ?x2 * ?x3) = _ + (?x1 * ?x3 * ?x2) ] => f_equal | [|- _ + (?x1 * ?x2 * ?x3 * ?x4 * ?x5 * ?x6) = _ + (?x1 * ?x3 * ?x2 * ?x4 * ?x5 * ?x6) ] => f_equal | [|- _ * ?x1 = _ * ?x1] => f_equal - | [|- _ * ?x = _ ] => rewrite mult_comm; repeat rewrite mult_assoc; arithSimplify - | [|- _ + ?x = _ ] => rewrite plus_comm; repeat rewrite plus_assoc; arithSimplify - | [|- _ * ?x1 <= _ * ?x1] => apply mult_le_compat; auto - | [|- _ * ?x1 <= _ * ?x1] => apply plus_le_compat; auto - | [|- _ * ?x <= _ ] => rewrite mult_comm; repeat rewrite mult_assoc; arithSimplify - | [|- _ + ?x <= _ ] => rewrite plus_comm; repeat rewrite plus_assoc; arithSimplify + | [|- _ * ?x = _ ] => rewrite Nat.mul_comm; repeat rewrite Nat.mul_assoc; arithSimplify + | [|- _ + ?x = _ ] => rewrite Nat.add_comm; repeat rewrite Nat.add_assoc; arithSimplify + | [|- _ * ?x1 <= _ * ?x1] => apply Nat.mul_le_mono; auto + | [|- _ * ?x1 <= _ * ?x1] => apply Nat.add_le_mono; auto + | [|- _ * ?x <= _ ] => rewrite Nat.mul_comm; repeat rewrite Nat.mul_assoc; arithSimplify + | [|- _ + ?x <= _ ] => rewrite Nat.add_comm; repeat rewrite Nat.add_assoc; arithSimplify end. @@ -417,13 +417,13 @@ Lemma ratAdd_eqRat_compat_l : forall r1 r2 r3, arithNormalize. f_equal. f_equal. - rewrite mult_comm. - rewrite (mult_comm _ x1). - repeat rewrite mult_assoc. + rewrite Nat.mul_comm. + rewrite (Nat.mul_comm _ x1). + repeat rewrite Nat.mul_assoc. f_equal. - rewrite mult_comm. + rewrite Nat.mul_comm. rewrite e. - apply mult_comm. + apply Nat.mul_comm. do 3 arithSimplify. Qed. @@ -448,19 +448,19 @@ Lemma ratAdd_leRat_compat_l : forall r1 r2 r3, unfold leRat, bleRat in *. rattac. arithNormalize. - apply plus_le_compat. + apply Nat.add_le_mono. - apply mult_le_compat; trivial. - repeat rewrite <- mult_assoc. - repeat rewrite (mult_comm x0). - repeat rewrite mult_assoc. - apply mult_le_compat; trivial. + apply Nat.mul_le_mono; trivial. + repeat rewrite <- Nat.mul_assoc. + repeat rewrite (Nat.mul_comm x0). + repeat rewrite Nat.mul_assoc. + apply Nat.mul_le_mono; trivial. - apply mult_le_compat; trivial. - rewrite <- mult_assoc. - rewrite (mult_comm x1). - rewrite mult_assoc. - apply mult_le_compat; trivial. + apply Nat.mul_le_mono; trivial. + rewrite <- Nat.mul_assoc. + rewrite (Nat.mul_comm x1). + rewrite Nat.mul_assoc. + apply Nat.mul_le_mono; trivial. Qed. Theorem ratAdd_leRat_compat : forall r1 r2 r3 r4, @@ -512,14 +512,14 @@ Theorem ratMult_eqRat_compat : forall (r1 r2 r3 r4 : Rat), rattac. - repeat rewrite mult_assoc. - rewrite <- (mult_assoc n1). - rewrite (mult_comm n). - rewrite mult_assoc. - rewrite <- mult_assoc. + repeat rewrite Nat.mul_assoc. + rewrite <- (Nat.mul_assoc n1). + rewrite (Nat.mul_comm n). + rewrite Nat.mul_assoc. + rewrite <- Nat.mul_assoc. rewrite e. rewrite e0. - rewrite mult_assoc. + rewrite Nat.mul_assoc. do 3 arithSimplify. Qed. @@ -547,27 +547,27 @@ Theorem ratAdd_0 : forall r1 r2, intuition. rattac. - rewrite mult_0_l in e. + rewrite Nat.mul_0_l in e. unfold posnatToNat in *. simpl in *. destruct p1. destruct p0. - rewrite mult_1_r in e. - apply plus_is_O in e. + rewrite Nat.mul_1_r in e. + apply Nat.eq_add_0 in e. destruct e as [H0 e]. - eapply mult_is_O in H0. + eapply Nat.eq_mul_0 in H0. lia. rattac. - rewrite mult_0_l in e. + rewrite Nat.mul_0_l in e. unfold posnatToNat in *. simpl in *. destruct p1. destruct p0. - rewrite mult_1_r in e. - apply plus_is_O in e. + rewrite Nat.mul_1_r in e. + apply Nat.eq_add_0 in e. destruct e as [e H1]. - eapply mult_is_O in H1. + eapply Nat.eq_mul_0 in H1. lia. rewrite (ratAdd_0_r 0). @@ -621,7 +621,7 @@ Lemma ratMult_1_l : forall r, rattac. inversion H; clear H; subst. - repeat rewrite mult_1_l in *. + repeat rewrite Nat.mul_1_l in *. trivial. Qed. @@ -631,11 +631,11 @@ Theorem ratMult_0 : forall r1 r2, intuition. rattac. - rewrite mult_0_l in e. + rewrite Nat.mul_0_l in e. unfold posnatToNat in *. simpl in *. - rewrite mult_1_r in e. - apply mult_is_O in e. + rewrite Nat.mul_1_r in e. + apply Nat.eq_mul_0 in e. intuition; subst. left. apply rat_num_0. @@ -672,7 +672,7 @@ Theorem leRat_num : forall n1 n2 d, leRat (RatIntro n1 d) (RatIntro n2 d). rattac. - eapply mult_le_compat; eauto. + eapply Nat.mul_le_mono; eauto. Qed. @@ -733,7 +733,7 @@ Theorem ratIdentityIndiscernables : forall r1 r2, rewrite H0 in H2. rattac. inversion e; clear e; subst. - apply mult_is_O in H2; intuition. + apply Nat.eq_mul_0 in H2; intuition. unfold posnatMult in *. inversion H5; clear H5; subst. assert ((RatIntro n4 (exist (fun n : nat => n > 0) x0 g0)) <= (RatIntro n3 (exist (fun n : nat => n > 0) x g))). @@ -751,7 +751,7 @@ Theorem ratIdentityIndiscernables : forall r1 r2, unfold posnatMult in *. simpl in *. inversion H5; clear H5; subst. - apply mult_is_O in e. intuition. + apply Nat.eq_mul_0 in e. intuition. symmetry. eapply nat_minus_eq; trivial. @@ -784,7 +784,7 @@ Lemma ratDistance_comm_2 : forall r1 r2 r3 r4, apply minus_eq_compat. arithSimplify. - rewrite (mult_comm _ x). + rewrite (Nat.mul_comm _ x). arithNormalize. arithSimplify. unfold minRat, maxRat in *. @@ -836,12 +836,12 @@ Lemma ratSubtract_partition : forall r1 r2 r3, unfold ratSubtract in *. rattac. arithNormalize. - rewrite <- NPeano.Nat.add_sub_swap. + rewrite <- Nat.add_sub_swap. eapply minus_eq_compat. rewrite minus_add_assoc. - rewrite plus_comm. + rewrite Nat.add_comm. rewrite <- minus_add_assoc. - rewrite <- plus_0_r at 1. + rewrite <- Nat.add_0_r at 1. apply plus_eq_compat. do 4 arithSimplify. symmetry. @@ -849,9 +849,9 @@ Lemma ratSubtract_partition : forall r1 r2 r3, do 4 arithSimplify. apply le_eq. do 5 arithSimplify. - do 4 (apply mult_le_compat; trivial). + do 4 (apply Nat.mul_le_mono; trivial). do 4 arithSimplify. - do 4 (apply mult_le_compat; trivial). + do 4 (apply Nat.mul_le_mono; trivial). Qed. @@ -862,13 +862,13 @@ Lemma ratAdd_any_leRat_l : forall r1 r2 r3, rattac. arithNormalize. assert (n * x * x0 <= n0 * x0 * x1)%nat. - rewrite (mult_comm (n0 * x0) x1). - rewrite mult_assoc. - apply mult_le_compat; trivial. - rewrite (mult_comm x1). + rewrite (Nat.mul_comm (n0 * x0) x1). + rewrite Nat.mul_assoc. + apply Nat.mul_le_mono; trivial. + rewrite (Nat.mul_comm x1). trivial. - rewrite <- plus_0_r at 1. - apply plus_le_compat; eauto. + rewrite <- Nat.add_0_r at 1. + apply Nat.add_le_mono; eauto. apply le_0_n. Qed. @@ -927,14 +927,14 @@ Lemma ratSubtract_leRat_r : forall r1 r2 r3, inversion H3; clear H3; subst. arithNormalize. assert (n * x3 * x3 * x1 <= n0 * x3 * x3 * x2)%nat. - rewrite <- mult_comm. - rewrite <- (mult_comm x2). - repeat rewrite mult_assoc. - eapply mult_le_compat; trivial. - eapply mult_le_compat; trivial. - rewrite mult_comm. + rewrite <- Nat.mul_comm. + rewrite <- (Nat.mul_comm x2). + repeat rewrite Nat.mul_assoc. + eapply Nat.mul_le_mono; trivial. + eapply Nat.mul_le_mono; trivial. + rewrite Nat.mul_comm. rewrite l. - rewrite mult_comm. + rewrite Nat.mul_comm. trivial. assert (n3 * x1 * x3 * x2 = n3 * x2 * x3 * x1)%nat. do 3 arithSimplify. @@ -954,14 +954,14 @@ Lemma ratSubtract_leRat_l: arithNormalize. assert (n * x3 * x1 * x3 <= n0 * x3 * x2 * x3)%nat. - apply mult_le_compat; trivial. - rewrite <- (mult_comm x1). - rewrite <- (mult_comm x2). - repeat rewrite mult_assoc. - apply mult_le_compat; trivial. - rewrite mult_comm. + apply Nat.mul_le_mono; trivial. + rewrite <- (Nat.mul_comm x1). + rewrite <- (Nat.mul_comm x2). + repeat rewrite Nat.mul_assoc. + apply Nat.mul_le_mono; trivial. + rewrite Nat.mul_comm. rewrite l. - rewrite mult_comm. + rewrite Nat.mul_comm. trivial. assert (n3 * x2 * x1 * x3 = n3 * x1 * x2 * x3)%nat. @@ -1116,10 +1116,10 @@ Theorem ratSubtract_le : forall r1 r2 d, arithNormalize. apply minus_le. - rewrite <- (mult_assoc n). - rewrite (mult_comm x0). - rewrite mult_assoc. - apply mult_le_compat; trivial. + rewrite <- (Nat.mul_assoc n). + rewrite (Nat.mul_comm x0). + rewrite Nat.mul_assoc. + apply Nat.mul_le_mono; trivial. Qed. @@ -1161,21 +1161,21 @@ Lemma ratSubtract_eqRat_compat : forall r1 r2 r3 r4, arithNormalize. apply minus_eq_compat. arithSimplify. - rewrite <- (mult_assoc n1). - rewrite (mult_comm x2). - rewrite mult_assoc. + rewrite <- (Nat.mul_assoc n1). + rewrite (Nat.mul_comm x2). + rewrite Nat.mul_assoc. arithSimplify. trivial. - rewrite <- (mult_assoc (n2 * x1)). - rewrite (mult_comm x). - rewrite mult_assoc. + rewrite <- (Nat.mul_assoc (n2 * x1)). + rewrite (Nat.mul_comm x). + rewrite Nat.mul_assoc. arithSimplify. - rewrite <- (mult_assoc n2). - rewrite (mult_comm x1 x0). - rewrite mult_assoc. + rewrite <- (Nat.mul_assoc n2). + rewrite (Nat.mul_comm x1 x0). + rewrite Nat.mul_assoc. arithSimplify. - rewrite mult_comm. + rewrite Nat.mul_comm. trivial. Qed. @@ -1274,12 +1274,12 @@ Lemma ratSubtract_add_same_r : forall r1 r2 r3, unfold ratSubtract. rattac. arithNormalize. - rewrite (plus_comm (n2 * x0 * x1 * x0 * x1 * x)). - rewrite NPeano.Nat.sub_add_distr. + rewrite (Nat.add_comm (n2 * x0 * x1 * x0 * x1 * x)). + rewrite Nat.sub_add_distr. apply minus_eq_compat. - rewrite <- NPeano.Nat.add_sub_assoc. + rewrite <- Nat.add_sub_assoc. rewrite minus_diag_eq. - rewrite plus_0_r. + rewrite Nat.add_0_r. do 5 arithSimplify. do 5 arithSimplify. eapply le_eq. @@ -1295,12 +1295,12 @@ Lemma ratSubtract_add_same_l : forall r1 r2 r3, unfold ratSubtract. rattac. arithNormalize. - rewrite NPeano.Nat.sub_add_distr. + rewrite Nat.sub_add_distr. apply minus_eq_compat. - rewrite plus_comm. - rewrite <- NPeano.Nat.add_sub_assoc. + rewrite Nat.add_comm. + rewrite <- Nat.add_sub_assoc. rewrite minus_diag_eq. - rewrite plus_0_r. + rewrite Nat.add_0_r. do 5 arithSimplify. do 5 arithSimplify. eapply le_eq. @@ -1328,11 +1328,11 @@ Lemma ratSubtract_ratAdd_assoc: forall r1 r2 r3, f_equal. do 5 arithSimplify. do 5 arithSimplify. - do 3 (eapply mult_le_compat; trivial). - repeat rewrite <- mult_assoc. - repeat rewrite (mult_comm x). - repeat rewrite mult_assoc. - apply mult_le_compat; trivial. + do 3 (eapply Nat.mul_le_mono; trivial). + repeat rewrite <- Nat.mul_assoc. + repeat rewrite (Nat.mul_comm x). + repeat rewrite Nat.mul_assoc. + apply Nat.mul_le_mono; trivial. Qed. Lemma ratAdd_add_same_r : forall r1 r2 r3, @@ -1537,7 +1537,7 @@ Theorem ratS_num : forall n, rattac. unfold natToPosnat in *. inversion H0; clear H0; subst. - repeat rewrite mult_1_r. + repeat rewrite Nat.mul_1_r. inversion H; clear H; subst. trivial. Qed. @@ -1776,8 +1776,8 @@ Lemma ratMult_3_ratAdd : forall r, inversion H0; clear H0; subst. simpl. arithNormalize. - repeat rewrite mult_0_r. - repeat rewrite plus_0_r. + repeat rewrite Nat.mul_0_r. + repeat rewrite Nat.add_0_r. trivial. Qed. @@ -1787,13 +1787,13 @@ Lemma ratMult_small_le : forall r1 r2, rattac. inversion H0; clear H0; subst. - rewrite mult_1_r in l. - rewrite mult_1_l in l. - rewrite mult_assoc. - rewrite <- (mult_assoc n2). - rewrite (mult_comm n). - rewrite mult_assoc. - apply mult_le_compat; + rewrite Nat.mul_1_r in l. + rewrite Nat.mul_1_l in l. + rewrite Nat.mul_assoc. + rewrite <- (Nat.mul_assoc n2). + rewrite (Nat.mul_comm n). + rewrite Nat.mul_assoc. + apply Nat.mul_le_mono; auto. Qed. @@ -1974,7 +1974,7 @@ Lemma posnatMult_1_r : forall p, destruct p2. unfold posnatToNat. inversion Heqp2; subst. - apply mult_1_r. + apply Nat.mul_1_r. Qed. @@ -2041,24 +2041,24 @@ Lemma ratMult_same_r_inv : forall r1 r2 r3, eapply n2. clear n2. arithNormalize. - rewrite <- (mult_assoc n) in e. - rewrite (mult_comm n0) in e. + rewrite <- (Nat.mul_assoc n) in e. + rewrite (Nat.mul_comm n0) in e. arithNormalize. - rewrite <- mult_assoc in e. - rewrite <- (mult_assoc n1) in e. - rewrite <- (mult_comm x1) in e. - rewrite (mult_assoc n1) in e. - rewrite <- (mult_assoc (n1 * x1)) in e. + rewrite <- Nat.mul_assoc in e. + rewrite <- (Nat.mul_assoc n1) in e. + rewrite <- (Nat.mul_comm x1) in e. + rewrite (Nat.mul_assoc n1) in e. + rewrite <- (Nat.mul_assoc (n1 * x1)) in e. eapply mult_same_r. 2:{ eapply e. } - rewrite mult_0_r in H0. - rewrite plus_0_l in H0. + rewrite Nat.mul_0_r in H0. + rewrite Nat.add_0_l in H0. destruct (eq_nat_dec n0 0). intuition. assert (~n0 * x0 = O)%nat. intros H1. - eapply mult_is_O in H1. + eapply Nat.eq_mul_0 in H1. intuition. remember (n0 * x0)%nat as a. lia. @@ -2070,8 +2070,8 @@ Lemma rat_le_1 : forall n (d : posnat), rattac. inversion H1; clear H1; subst. - rewrite mult_1_r. - rewrite mult_1_l. + rewrite Nat.mul_1_r. + rewrite Nat.mul_1_l. trivial. Qed. @@ -2090,13 +2090,13 @@ Lemma ratMult_2 : forall r, rattac. inversion H; clear H; subst. arithNormalize. - rewrite mult_0_r. - rewrite plus_0_r. + rewrite Nat.mul_0_r. + rewrite Nat.add_0_r. f_equal. f_equal. - rewrite <- mult_assoc. - rewrite <- mult_assoc. - rewrite mult_comm. + rewrite <- Nat.mul_assoc. + rewrite <- Nat.mul_assoc. + rewrite Nat.mul_comm. simpl. trivial. Qed. @@ -2129,7 +2129,7 @@ Lemma ratInverse_prod_1 : forall r, eapply num_dem_same_rat1. unfold posnatMult, natToPosnat, posnatToNat. destruct p. - apply mult_comm. + apply Nat.mul_comm. Qed. Fixpoint expRat r n := @@ -2150,16 +2150,16 @@ Lemma ratInverse_nz : forall (r : Rat), destruct p. destruct p0. inversion H0; clear H0; subst. - rewrite mult_1_r in e. - rewrite mult_1_r in e. + rewrite Nat.mul_1_r in e. + rewrite Nat.mul_1_r in e. lia. unfold posnatToNat, natToPosnat in *. destruct p. destruct p0. inversion H0; clear H0; subst. - rewrite mult_1_r in e. - rewrite mult_0_l in e. + rewrite Nat.mul_1_r in e. + rewrite Nat.mul_0_l in e. lia. Qed. @@ -2208,7 +2208,7 @@ Lemma ratInverse_leRat : forall r1 r2, eapply rat_num_0. destruct n. exfalso. - rewrite mult_0_l in l. + rewrite Nat.mul_0_l in l. simpl in *. remember (n0 * x1)%nat as a. nia. @@ -2228,17 +2228,17 @@ Lemma ratAdd_not_leRat : forall r1 r2, unfold posnatMult, natToPosnat, posnatToNat in *. destruct p1. destruct p0. - rewrite mult_plus_distr_r in l. - rewrite <- mult_assoc in l. - rewrite (mult_comm x) in l. + rewrite Nat.mul_add_distr_r in l. + rewrite <- Nat.mul_assoc in l. + rewrite (Nat.mul_comm x) in l. assert ((n1 * x0 * x0) = O)%nat. remember (n0 * (x0 * x))%nat as a. remember (n1 * x0 * x0)%nat as b. lia. - apply mult_is_O in H1; + apply Nat.eq_mul_0 in H1; intuition; subst. - apply mult_is_O in H2; + apply Nat.eq_mul_0 in H2; intuition; subst. apply rat_num_0. @@ -2305,7 +2305,7 @@ Lemma ratSubtract_ratAdd_distr : forall r1 r2 r3, unfold ratSubtract, ratAdd. rattac. arithNormalize. - rewrite NPeano.Nat.sub_add_distr. + rewrite Nat.sub_add_distr. f_equal. f_equal. do 5 arithSimplify. @@ -2326,17 +2326,17 @@ Lemma ratSubtract_ratAdd_assoc_1 : forall r1 r2 r3, do 5 arithSimplify. do 5 arithSimplify. unfold natToPosnat, posnatToNat in *. - eapply mult_le_compat; trivial. - eapply mult_le_compat; trivial. - eapply mult_le_compat; trivial. + eapply Nat.mul_le_mono; trivial. + eapply Nat.mul_le_mono; trivial. + eapply Nat.mul_le_mono; trivial. - rewrite <- (mult_assoc). - rewrite (mult_comm x). - rewrite mult_assoc. - rewrite <- (mult_assoc n3). - rewrite (mult_comm x). - rewrite mult_assoc. - eapply mult_le_compat; trivial. + rewrite <- (Nat.mul_assoc). + rewrite (Nat.mul_comm x). + rewrite Nat.mul_assoc. + rewrite <- (Nat.mul_assoc n3). + rewrite (Nat.mul_comm x). + rewrite Nat.mul_assoc. + eapply Nat.mul_le_mono; trivial. Qed. @@ -2369,14 +2369,14 @@ Lemma eqRat_ratMult_same_r : forall r1 r2 r3, eapply n2. eapply (@mult_same_l (n * x0)). eapply mult_gt_0. - rewrite mult_1_r in n3. - rewrite mult_0_l in n3. + rewrite Nat.mul_1_r in n3. + rewrite Nat.mul_0_l in n3. lia. trivial. - rewrite (mult_comm). - rewrite mult_assoc. - rewrite <- (mult_assoc n0). - rewrite (mult_comm x). + rewrite (Nat.mul_comm). + rewrite Nat.mul_assoc. + rewrite <- (Nat.mul_assoc n0). + rewrite (Nat.mul_comm x). arithNormalize. rewrite e. do 3 arithSimplify. @@ -2518,7 +2518,7 @@ Lemma ratMult_eq_rat1 : forall n1 n2 (nz1 : nz n1)(nz2 : nz n2), rewrite <- ratMult_num_den. eapply num_dem_same_rat1. unfold posnatMult, natToPosnat, posnatToNat. - eapply mult_comm. + eapply Nat.mul_comm. Qed. @@ -2565,7 +2565,7 @@ Lemma leRat_terms : forall n1 n2 (d1 d2 : posnat), RatIntro n1 d1 <= RatIntro n2 d2. rattac. - eapply mult_le_compat; trivial. + eapply Nat.mul_le_mono; trivial. Qed. @@ -2623,7 +2623,7 @@ Lemma expRat_le_half_exists : forall r, eapply expRat_leRat_compat. eapply leRat_terms. eapply l. - eapply le_refl. + eapply Nat.le_refl. rewrite expRat_terms. @@ -2632,7 +2632,7 @@ Lemma expRat_le_half_exists : forall r, lia. simpl. destruct (eq_nat_dec x O); subst. - rewrite mult_0_l. + rewrite Nat.mul_0_l. rewrite rat_num_0. eapply rat0_le_all. @@ -2658,21 +2658,21 @@ Lemma expRat_le_half_exists : forall r, assert (posnatToNat (pos (2 * (x * expnat x x))) <= posnatToNat (pos (expnat (S x) x + x * expnat (S x) x)))%nat. unfold natToPosnat, posnatToNat. - rewrite mult_assoc. - rewrite (mult_comm 2 x). - rewrite <- mult_assoc. - rewrite <- (plus_0_l (x * (2 * expnat x x))). - eapply plus_le_compat. + rewrite Nat.mul_assoc. + rewrite (Nat.mul_comm 2 x). + rewrite <- Nat.mul_assoc. + rewrite <- (Nat.add_0_l (x * (2 * expnat x x))). + eapply Nat.add_le_mono. intuition. - eapply mult_le_compat. + eapply Nat.mul_le_mono. intuition. eapply expnat_base_S_same. lia. eapply leRat_trans. eapply leRat_terms. - rewrite <- (mult_1_l (x * expnat x x)). - eapply le_refl. + rewrite <- (Nat.mul_1_l (x * expnat x x)). + eapply Nat.le_refl. unfold natToPosnat, posnatToNat. eapply H2. assert (nz (x * expnat x x)). @@ -2740,7 +2740,7 @@ Lemma expRat_half_le_exp_exists : forall d, 2:{ eapply leRat_terms. eapply H0. - eapply le_refl. + eapply Nat.le_refl. } erewrite expnat_1. eapply leRat_terms. @@ -2892,11 +2892,11 @@ Theorem le_ratHalf_0 : forall r, destruct p. unfold natToPosnat in *. unfold posnatToNat in *. - rewrite mult_1_r in *. - rewrite (mult_comm x) in l. - rewrite mult_assoc in *. + rewrite Nat.mul_1_r in *. + rewrite (Nat.mul_comm x) in l. + rewrite Nat.mul_assoc in *. assert (n * 2 <= n)%nat. - eapply mult_le_compat_r_iff; eauto. + lia. lia. Qed. @@ -2908,7 +2908,7 @@ Lemma ratSubtract_0_r : forall r, arithNormalize. inversion H; clear H; subst. simpl. - rewrite <- minus_n_O. + rewrite Nat.sub_0_r. do 2 arithSimplify. Qed. @@ -2935,8 +2935,8 @@ Lemma ratSubtract_0_inv : forall r1 r2, intuition. unfold ratSubtract in *. rattac. - rewrite mult_0_l in e. - apply mult_is_O in e. + rewrite Nat.mul_0_l in e. + apply Nat.eq_mul_0 in e. lia. Qed. @@ -3323,12 +3323,12 @@ Lemma ratSubtract_half : forall x, rattac. arithNormalize. inversion H; clear H; subst. - rewrite <- (mult_assoc (n * x * 2)). - rewrite (mult_comm (n * x)). - repeat rewrite mult_assoc. + rewrite <- (Nat.mul_assoc (n * x * 2)). + rewrite (Nat.mul_comm (n * x)). + repeat rewrite Nat.mul_assoc. simpl. - rewrite (plus_0_r). - repeat rewrite mult_plus_distr_r. + rewrite (Nat.add_0_r). + repeat rewrite Nat.mul_add_distr_r. remember (n * x * x * 2)%nat as a. lia. Qed. @@ -3456,13 +3456,12 @@ Lemma leRat_0_eq : intuition. rattac. - symmetry. - eapply le_n_0_eq. + eapply Nat.le_0_r. unfold natToPosnat, posnatToNat in *. - rewrite mult_1_r in l. + rewrite Nat.mul_1_r in l. rewrite l. destruct p. - rewrite mult_0_l. + rewrite Nat.mul_0_l. intuition. Qed. @@ -3476,8 +3475,8 @@ Lemma rat_le_1_if : unfold leRat, bleRat, ratCD, rat1 in *. unfold natToPosnat, posnatToNat in *. destruct d. - rewrite mult_1_r in H. - rewrite mult_1_l in H. + rewrite Nat.mul_1_r in H. + rewrite Nat.mul_1_l in H. destruct (le_gt_dec n x). lia. discriminate. @@ -3504,7 +3503,7 @@ Theorem ratFraction_le_1 : unfold posnatMult, natToPosnat, posnatToNat. destruct p. - rewrite mult_comm. + rewrite Nat.mul_comm. intuition. Qed. diff --git a/src/FCF/RepeatCore.v b/src/FCF/RepeatCore.v index c737624..08f6c94 100644 --- a/src/FCF/RepeatCore.v +++ b/src/FCF/RepeatCore.v @@ -80,7 +80,7 @@ Section DistSingle_impl_Mult. unfold computeHybrid. unfold minus. fold minus. - rewrite <- minus_n_O. + rewrite Nat.sub_0_r. unfold forNats. fold forNats. unfold compMap. @@ -348,7 +348,7 @@ Section DistSingle_impl_Mult. fold compMap. comp_simp. inline_first. - rewrite <- minus_n_O. + rewrite Nat.sub_0_r. comp_skip. comp_simp. simpl. @@ -366,7 +366,7 @@ Section DistSingle_impl_Mult. comp_skip. inline_first. - rewrite minus_diag. + rewrite Nat.sub_diag. unfold forNats. unfold compMap. comp_simp. diff --git a/src/FCF/RndGrpElem.v b/src/FCF/RndGrpElem.v index dfa6ed7..52bea17 100644 --- a/src/FCF/RndGrpElem.v +++ b/src/FCF/RndGrpElem.v @@ -83,7 +83,7 @@ Section RndGrpElem. (fun z => (modNat (z + (modNatAddInverse (groupLog g y) order) + (groupLog g x))) order) (fun z => (modNat (z + (groupLog g y) + (modNatAddInverse (groupLog g x) order)) order))); intuition. - rewrite <- plus_assoc. + rewrite <- Nat.add_assoc. rewrite <- modNat_plus. assert ((x0 + groupLog g y + modNatAddInverse (groupLog g x) order + (modNatAddInverse (groupLog g y) order + groupLog g x)) = @@ -94,15 +94,15 @@ Section RndGrpElem. rewrite H0. rewrite modNat_plus. rewrite modNatAddInverse_correct. - rewrite plus_0_l. + rewrite Nat.add_0_l. rewrite modNat_plus. rewrite modNatAddInverse_correct. - rewrite plus_0_l. + rewrite Nat.add_0_l. eapply modNat_eq. eapply RndNat_support_lt. trivial. - rewrite <- plus_assoc. + rewrite <- Nat.add_assoc. rewrite <- modNat_plus. assert ((x0 + modNatAddInverse (groupLog g y) order + groupLog g x + (groupLog g y + modNatAddInverse (groupLog g x) order)) = @@ -112,10 +112,10 @@ Section RndGrpElem. rewrite H0. rewrite modNat_plus. rewrite modNatAddInverse_correct. - rewrite plus_0_l. + rewrite Nat.add_0_l. rewrite modNat_plus. rewrite modNatAddInverse_correct. - rewrite plus_0_l. + rewrite Nat.add_0_l. eapply modNat_eq. eapply RndNat_support_lt. trivial. @@ -136,7 +136,7 @@ Section RndGrpElem. rewrite groupExp_mod. rewrite modNat_plus. rewrite modNatAddInverse_correct_gen. - rewrite plus_0_l. + rewrite Nat.add_0_l. rewrite <- groupExp_mod. rewrite group_cyclic. destruct (EqDec_dec GroupElement_EqDec x x). diff --git a/src/FCF/RndInList.v b/src/FCF/RndInList.v index 0be8898..f6334b2 100644 --- a/src/FCF/RndInList.v +++ b/src/FCF/RndInList.v @@ -25,23 +25,23 @@ Theorem qam_count_gen : (* Bind case *) repeat simp_in_support. destruct x. - rewrite mult_plus_distr_r. + rewrite Nat.mul_add_distr_r. pose proof H4. eapply (IHqueries_at_most _ count) in H4. eapply (H1 _ _ S count) in H5. rewrite H5. - rewrite plus_comm. - rewrite <- (plus_assoc). - rewrite (plus_comm (q2 * n)). - rewrite plus_assoc. - eapply plus_le_compat. + rewrite Nat.add_comm. + rewrite <- (Nat.add_assoc). + rewrite (Nat.add_comm (q2 * n)). + rewrite Nat.add_assoc. + eapply Nat.add_le_mono. eauto. - eapply le_refl. + eapply Nat.le_refl. intuition. intuition. (* query case *) - rewrite plus_0_r. + rewrite Nat.add_0_r. eapply H; eauto. (* ret case *) @@ -62,7 +62,7 @@ Theorem qam_count_gen : (s, s0) (q2 * n) ). - eapply le_trans. + eapply Nat.le_trans. eapply IHqueries_at_most. intuition. simpl. @@ -74,16 +74,16 @@ Theorem qam_count_gen : eauto. eauto. simpl. - rewrite mult_assoc. + rewrite Nat.mul_assoc. intuition. (* trans case *) - eapply le_trans. + eapply Nat.le_trans. eapply IHqueries_at_most. eauto. eauto. - eapply plus_le_compat; intuition. - eapply mult_le_compat; intuition. + eapply Nat.add_le_mono; intuition. + eapply Nat.mul_le_mono; intuition. Unshelve. repeat econstructor. @@ -214,15 +214,15 @@ Theorem oc_eventProb : intuition. eapply ratMult_leRat_compat; intuition. eapply H2. - eapply plus_le_compat; intuition. + eapply Nat.add_le_mono; intuition. - eapply le_trans. + eapply Nat.le_trans. eapply (qam_count_gen _ _ _ _ _ i). intuition. eapply H5. eauto. eauto. - rewrite mult_comm. + rewrite Nat.mul_comm. reflexivity. rewrite H6. @@ -240,10 +240,10 @@ Theorem oc_eventProb : 1, 3: reflexivity. intuition. eapply H2. - rewrite mult_plus_distr_l. - rewrite plus_comm. - repeat rewrite <- plus_assoc. - eapply plus_le_compat; intuition. + rewrite Nat.mul_add_distr_l. + rewrite Nat.add_comm. + repeat rewrite <- Nat.add_assoc. + eapply Nat.add_le_mono; intuition. rewrite H1; intuition. rewrite <- ratMult_1_l. @@ -370,7 +370,7 @@ Theorem oc_eventProb : repeat simp_in_support. destruct x. simpl in *. - rewrite mult_comm. + rewrite Nat.mul_comm. eapply qam_count_gen. eapply H0. intuition. @@ -384,10 +384,10 @@ Theorem oc_eventProb : rewrite <- ratMult_num_den. eapply eqRat_terms; intuition. eapply H2. - eapply plus_le_compat. 2: reflexivity. - rewrite <- mult_assoc. - eapply mult_le_compat. reflexivity. - rewrite mult_comm. + eapply Nat.add_le_mono. 2: reflexivity. + rewrite <- Nat.mul_assoc. + eapply Nat.mul_le_mono. reflexivity. + rewrite Nat.mul_comm. reflexivity. rewrite IHqueries_at_most. @@ -424,8 +424,8 @@ Theorem oc_eventProb_0_1 : eapply oc_eventProb; intuition. eauto. rewrite H4. - rewrite mult_1_l. - rewrite plus_0_r. + rewrite Nat.mul_1_l. + rewrite Nat.add_0_r. intuition. Qed. @@ -446,7 +446,7 @@ Theorem qam_count : count b <= q. intuition. - eapply le_trans. + eapply Nat.le_trans. eapply qam_count_gen; eauto. lia. @@ -889,6 +889,4 @@ Section RndInAdaptive. eapply leRat_terms; intuition. Qed. - - End RndInAdaptive. diff --git a/src/FCF/RndListElem.v b/src/FCF/RndListElem.v index 57c2e98..983f989 100644 --- a/src/FCF/RndListElem.v +++ b/src/FCF/RndListElem.v @@ -76,7 +76,7 @@ Theorem firstIndexOf_in_lt : destruct (eqd a0 a); subst. lia. - eapply lt_n_S. + apply ->Nat.succ_lt_mono. eauto. Qed. diff --git a/src/FCF/RndListPred.v b/src/FCF/RndListPred.v index 8ef7bf0..29b4e90 100644 --- a/src/FCF/RndListPred.v +++ b/src/FCF/RndListPred.v @@ -327,7 +327,7 @@ Section DupList. reflexivity. eapply ratMult_leRat_compat. eapply leRat_terms. - eapply mult_le_compat. + eapply Nat.mul_le_mono. trivial. lia. trivial. diff --git a/src/FCF/RndPerm.v b/src/FCF/RndPerm.v index 19e4447..7b0cb03 100644 --- a/src/FCF/RndPerm.v +++ b/src/FCF/RndPerm.v @@ -334,7 +334,7 @@ Theorem allNats_nth_pred : rewrite app_length. simpl. - rewrite plus_comm. + rewrite Nat.add_comm. simpl. eapply list_pred_app_both. diff --git a/src/FCF/SemEquiv.v b/src/FCF/SemEquiv.v index 9acdf8b..78401c0 100644 --- a/src/FCF/SemEquiv.v +++ b/src/FCF/SemEquiv.v @@ -645,13 +645,13 @@ Lemma low_tree_approx_same_inv_h : forall n (A : Set)(eqd : eq_dec A)(c : Comp A rewrite <- ratAdd_den_same. rewrite H8. rewrite <- ratMult_num_den. - rewrite mult_1_r. + rewrite Nat.mul_1_r. unfold posnatMult. unfold natToPosnat. rewrite <- H5. eapply eqRat_terms; trivial. unfold natToPosnat, posnatToNat. - rewrite mult_comm. + rewrite Nat.mul_comm. simpl. trivial. Qed. @@ -913,10 +913,10 @@ Lemma low_tree_approx_same_h : forall n (A : Set)(eqd : eq_dec A)(c : Comp A)(t repeat rewrite <- ratMult_num_den. rewrite <- ratAdd_den_same. eapply eqRat_terms. - repeat rewrite mult_1_r. + repeat rewrite Nat.mul_1_r. trivial. unfold posnatMult, natToPosnat, posnatToNat. - rewrite mult_comm. + rewrite Nat.mul_comm. simpl. trivial. Qed. @@ -1415,7 +1415,7 @@ Lemma lowDistApprox_le_1 : forall (A : Set)(c : Comp A) a n r, rewrite H2. eapply rat_le_1. - eapply le_trans. + eapply Nat.le_trans. eapply pred_count_le_length. eapply H. @@ -1604,7 +1604,7 @@ Lemma lowDistApprox_bind_evalDist_limit : forall (A B :Set)(c1 : Comp B)(c2 : B intuition. eapply H12. - eapply le_trans. + eapply Nat.le_trans. eapply maxList_correct; eauto. eauto. trivial. @@ -1663,7 +1663,7 @@ Lemma lowDistApprox_bind_evalDist_limit : forall (A B :Set)(c1 : Comp B)(c2 : B intuition. simpl in *. eapply H12. - eapply le_trans. + eapply Nat.le_trans. eapply maxList_correct; eauto. eauto. trivial. @@ -1739,11 +1739,11 @@ Lemma lowDistApprox_bind_evalDist_limit : forall (A B :Set)(c1 : Comp B)(c2 : B eapply ratDistance_ratMult_le. eapply H5. - eapply Max.max_lub_l. + eapply Nat.max_lub_l. eapply H1. trivial. eapply H4. - eapply Max.max_lub_r. + eapply Nat.max_lub_r. eapply H1. trivial. trivial. @@ -1770,7 +1770,7 @@ Lemma lowDistApprox_bind_evalDist_limit : forall (A B :Set)(c1 : Comp B)(c2 : B rewrite ratMult_1_l. eapply leRat_refl. unfold posnatMult, natToPosnat, posnatToNat. - rewrite mult_comm. + rewrite Nat.mul_comm. trivial. Qed. @@ -2259,17 +2259,17 @@ Lemma datMap_depth_better' : forall (B : Set)(tb1 tb2 : DistApproxTree B), eauto. eauto. destruct (le_dec (datDepth tb1) (datDepth tb2)). - rewrite Max.max_r in H3; eauto. + rewrite Nat.max_r in H3; eauto. lia. - rewrite Max.max_l in H3; lia. + rewrite Nat.max_l in H3; lia. eauto. eapply IHdat_better2. eauto. eauto. destruct (le_dec (datDepth tb1) (datDepth tb2)). - rewrite Max.max_r in H3; lia. - rewrite Max.max_l in H3; lia. + rewrite Nat.max_r in H3; lia. + rewrite Nat.max_l in H3; lia. eauto. Qed. @@ -2281,14 +2281,14 @@ Lemma datCorrect_datDepth : forall (A : Set)(c : Comp A) n t, induction 1; intuition; simpl in *. destruct (le_dec (datDepth t1) (datDepth t2)). - rewrite Max.max_r; eauto. + rewrite Nat.max_r; eauto. lia. - rewrite Max.max_l; lia. + rewrite Nat.max_l; lia. Qed. Lemma dat_better_bind_div2 : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) n t1 t2, dat_correct_bind c1 c2 n t1 -> - dat_correct_bind2 c1 c2 (div2 n) t2 -> + dat_correct_bind2 c1 c2 (Nat.div2 n) t2 -> dat_better t1 t2. intuition. @@ -2306,11 +2306,11 @@ Lemma dat_better_bind_div2 : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) n simpl. eauto. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply div2_ge_double. } - eapply plus_le_compat. + eapply Nat.add_le_mono. auto. eapply datCorrect_datDepth. eauto. @@ -2323,7 +2323,7 @@ Qed. Lemma lowDistApprox_bind_le_div2 : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) a n r1 r2, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b)) -> - lowDistApprox_bind c1 c2 a (div2 n) r1 -> + lowDistApprox_bind c1 c2 a (Nat.div2 n) r1 -> lowDistApprox (Bind c1 c2) a n r2 -> r1 <= r2. @@ -2410,7 +2410,7 @@ Qed. Lemma lowDistApprox_bind_div2_left_total : forall (A B : Set)(c1 : Comp B)(c2 : B -> Comp A) a, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b)) -> - left_total (fun n => lowDistApprox_bind c1 c2 a (div2 n)). + left_total (fun n => lowDistApprox_bind c1 c2 a (Nat.div2 n)). intuition. unfold left_total. @@ -2518,7 +2518,7 @@ Theorem lowDistApprox_Rnd: forall n2 n1 (a : Bvector n1) r, induction n2; intuition; simpl in *. - rewrite plus_0_r in *. + rewrite Nat.add_0_r in *. unfold lowDistApprox in *. destruct H. destruct H. @@ -2721,7 +2721,7 @@ Theorem lowDistApprox_Rnd: forall n2 n1 (a : Bvector n1) r, rewrite <- ratMult_num_den. eapply eqRat_trans. eapply eqRat_terms. - eapply mult_comm. + eapply Nat.mul_comm. eapply posnatMult_1_r. rewrite rat_remove_common_factor. @@ -2853,7 +2853,7 @@ Qed. Lemma lowDistApprox_repeat_sqrt_div2_left_total : forall (A : Set)(c : Comp A)(P : A -> bool) a, well_formed_comp c -> - left_total (fun n => (lowDistApprox_repeat c P a (Nat.sqrt (div2 n)))). + left_total (fun n => (lowDistApprox_repeat c P a (Nat.sqrt (Nat.div2 n)))). unfold left_total. intuition. @@ -3996,7 +3996,7 @@ Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistAppro inversion H1; clear H1; subst. inversion H; clear H; subst. simpl in *. - rewrite mult_0_r in *. + rewrite Nat.mul_0_r in *. simpl in *. assert (depth0 >= (max (datDepth t2_1) (datDepth t2_2))). lia. @@ -4007,8 +4007,8 @@ Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistAppro lia. eauto. eauto. - rewrite mult_0_r; simpl. - eapply Max.max_lub_l. + rewrite Nat.mul_0_r; simpl. + eapply Nat.max_lub_l. eauto. trivial. trivial. @@ -4020,8 +4020,8 @@ Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistAppro lia. eauto. trivial. - rewrite mult_0_r; simpl. - eapply Max.max_lub_r. + rewrite Nat.mul_0_r; simpl. + eapply Nat.max_lub_r. eauto. trivial. trivial. @@ -4041,7 +4041,7 @@ Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistAppro congruence. lia. - rewrite mult_comm in H3. + rewrite Nat.mul_comm in H3. simpl in *. eapply IHn2. @@ -4052,15 +4052,15 @@ Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistAppro remember (n2 * n1)%nat as x. lia. - eapply le_trans. + eapply Nat.le_trans. 2:{ eapply H3. } - rewrite plus_0_r. - rewrite plus_comm. - eapply plus_le_compat. + rewrite Nat.add_0_r. + rewrite Nat.add_comm. + eapply Nat.add_le_mono. eauto. - rewrite mult_comm. + rewrite Nat.mul_comm. trivial. trivial. trivial. @@ -4076,11 +4076,11 @@ Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistAppro trivial. eauto. trivial. - eapply le_trans. - eapply plus_le_compat. - eapply le_refl. - eapply (Max.max_lub_l (datDepth t2_1) (datDepth t2_2)). - eapply le_refl. + eapply Nat.le_trans. + eapply Nat.add_le_mono. + eapply Nat.le_refl. + eapply (Nat.max_lub_l (datDepth t2_1) (datDepth t2_2)). + eapply Nat.le_refl. lia. trivial. trivial. @@ -4091,11 +4091,11 @@ Lemma datRepeat_depth_better: forall (n2 : nat) (A : Set) (t2 t1 t1' : DistAppro trivial. eauto. trivial. - eapply le_trans. - eapply plus_le_compat. - eapply le_refl. - eapply (Max.max_lub_r (datDepth t2_1) (datDepth t2_2)). - eapply le_refl. + eapply Nat.le_trans. + eapply Nat.add_le_mono. + eapply Nat.le_refl. + eapply (Nat.max_lub_r (datDepth t2_1) (datDepth t2_2)). + eapply Nat.le_refl. lia. trivial. trivial. @@ -4105,7 +4105,7 @@ Qed. Lemma dat_better_repeat_sqrt : forall (A : Set) (c : Comp A)(P : A -> bool)(n : nat) (t1 t2 : DistApproxTree A), (exists a, In a (filter P (getSupport c))) -> dat_correct_repeat c P n t1 -> - dat_correct_repeat2 c P (Nat.sqrt (div2 n)) t2 -> + dat_correct_repeat2 c P (Nat.sqrt (Nat.div2 n)) t2 -> well_formed_comp c -> dat_better t1 t2. @@ -4129,11 +4129,11 @@ Lemma dat_better_repeat_sqrt : forall (A : Set) (c : Comp A)(P : A -> bool)(n : eapply sqrt_le_lin_gen. eapply div2_le. - eapply le_trans. - eapply plus_le_compat. + eapply Nat.le_trans. + eapply Nat.add_le_mono. eapply Nat.sqrt_spec. lia. - eapply le_trans. + eapply Nat.le_trans. eapply datCorrect_datDepth. eauto. eapply Nat.sqrt_le_lin. @@ -4162,7 +4162,7 @@ Lemma lowDistApprox_repeat_sqrt_le : forall n (A : Set)(c : Comp A)(P : A -> boo well_formed_comp c -> (exists a, In a (filter P (getSupport c))) -> lowDistApprox (Repeat c P) a n v1 -> - lowDistApprox_repeat c P a (Nat.sqrt (div2 n)) v2 -> + lowDistApprox_repeat c P a (Nat.sqrt (Nat.div2 n)) v2 -> n > 1 -> v2 <= v1. @@ -4197,9 +4197,9 @@ Lemma lowDistApprox_repeat_sqrt_le : forall n (A : Set)(c : Comp A)(P : A -> boo lia. simpl. - eapply lt_le_trans. + eapply Nat.lt_le_trans. econstructor. - eapply le_trans. + eapply Nat.le_trans. rewrite <- Nat.sqrt_1. eauto. eapply Nat.sqrt_le_mono. @@ -5094,7 +5094,7 @@ Lemma lowDistApprox_limit_repeat : forall (A : Set)(c : Comp A)(P : A -> bool) a rat_inf_limit (lowDistApprox (Repeat c P) a) (evalDist (Repeat c P) a). intuition. - eapply (@rat_inf_limit_squeeze (fun n => (lowDistApprox_repeat c P a (Nat.sqrt (div2 n)))) (fun n => eqRat (evalDist (Repeat c P) a))). + eapply (@rat_inf_limit_squeeze (fun n => (lowDistApprox_repeat c P a (Nat.sqrt (Nat.div2 n)))) (fun n => eqRat (evalDist (Repeat c P) a))). eapply rat_inf_limit_mono. eapply lowDistApprox_repeat_limit; trivial. @@ -5106,7 +5106,7 @@ Lemma lowDistApprox_limit_repeat : forall (A : Set)(c : Comp A)(P : A -> bool) a intuition. exists (2 * (y * y))%nat. - rewrite div2_double. + rewrite Nat.div2_double. rewrite Nat.sqrt_square. trivial. @@ -5155,7 +5155,7 @@ Theorem evalDet_evalDist_equiv : forall (A : Set)(c : Comp A), eapply lowDistApprox_Ret_inv. eauto. eapply rat0_le_all. - eapply (@rat_inf_limit_squeeze (fun n => lowDistApprox_bind c1 c2 a (div2 n)) (lowDistApprox_bind c1 c2 a)); intuition. + eapply (@rat_inf_limit_squeeze (fun n => lowDistApprox_bind c1 c2 a (Nat.div2 n)) (lowDistApprox_bind c1 c2 a)); intuition. eapply rat_inf_limit_div_2. eapply lowDistApprox_bind_evalDist_limit; eauto. eapply lowDistApprox_bind_evalDist_limit; eauto. diff --git a/src/FCF/StdNat.v b/src/FCF/StdNat.v index 9d715e0..7ad8c24 100644 --- a/src/FCF/StdNat.v +++ b/src/FCF/StdNat.v @@ -7,8 +7,6 @@ Set Implicit Arguments. Require Export Arith. Require Export micromega.Lia. -Require Export Arith.Div2. -Require Export Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.NArith.BinNat. Local Ltac Tauto.intuition_solver ::= auto with crelations arith. @@ -27,7 +25,7 @@ Lemma mult_same_r : forall n1 n2 n3, f_equal. eapply IHn1; eauto. - eapply plus_reg_l. eauto. + eapply Nat.add_cancel_l. eauto. Qed. Lemma mult_same_l : forall n3 n1 n2, @@ -37,8 +35,8 @@ Lemma mult_same_l : forall n3 n1 n2, intuition. eapply mult_same_r; eauto. - rewrite mult_comm. - rewrite (mult_comm n2 n3). + rewrite Nat.mul_comm. + rewrite (Nat.mul_comm n2 n3). trivial. Qed. @@ -128,7 +126,7 @@ Lemma posnatMult_comm : forall p1 p2, unfold posnatMult. destruct p1; destruct p2. econstructor. - apply mult_comm. + apply Nat.mul_comm. Qed. Coercion posnatToNat : posnat >-> nat. @@ -172,7 +170,7 @@ Theorem expnat_pos : forall x n, Qed. Lemma div2_le : forall n, - le (div2 n) n. + le (Nat.div2 n) n. intuition. @@ -182,17 +180,17 @@ Lemma div2_le : forall n, Qed. Lemma div2_ge_double : forall n, - n >= (div2 n) + (div2 n). + n >= (Nat.div2 n) + (Nat.div2 n). intuition. - destruct (Even.even_odd_dec n). + destruct (Nat.Even_Odd_dec n). - rewrite (even_double n) at 1. - unfold double. + rewrite (Nat.Even_double n) at 1. + unfold Nat.double. lia. trivial. - rewrite (odd_double n) at 1. - unfold double. + rewrite (Nat.Odd_double n) at 1. + unfold Nat.double. lia. trivial. Qed. @@ -318,10 +316,10 @@ Lemma modNatAddInverse_correct_gen : forall x y p, rewrite <- H. rewrite modNat_plus. rewrite minus_add_assoc. - rewrite (plus_comm). + rewrite (Nat.add_comm). rewrite <- minus_add_assoc. - rewrite minus_diag. - rewrite plus_0_r. + rewrite Nat.sub_diag. + rewrite Nat.add_0_r. apply modNat_arg_eq. trivial. @@ -386,7 +384,7 @@ Lemma modNat_divides : forall x p, destruct (modNat_correct x p). rewrite H in H0. econstructor. - rewrite plus_0_r in H0. + rewrite Nat.add_0_r in H0. eauto. Qed. @@ -406,7 +404,7 @@ Lemma modNatAddInverse_sum_0 : forall x y p, rewrite modNat_plus in H. unfold modNatAddInverse in *. rewrite minus_add_assoc in H; intuition. - rewrite plus_comm in H. + rewrite Nat.add_comm in H. apply modNat_divides in H. destruct H. @@ -432,7 +430,7 @@ Lemma modNatAddInverse_sum_0 : forall x y p, destruct x0. simpl in H. - rewrite plus_0_r in H. + rewrite Nat.add_0_r in H. lia. assert (p > 0). @@ -455,10 +453,10 @@ Lemma modNat_correct_if : forall x y z (p : posnat), apply IHx in H0. rewrite H0. - rewrite plus_comm. + rewrite Nat.add_comm. rewrite modNat_plus. rewrite modNat_arg_eq. - rewrite plus_0_l. + rewrite Nat.add_0_l. trivial. Qed. @@ -468,7 +466,7 @@ Lemma modNat_mult : forall x (p : posnat), induction x; intuition; simpl in *. rewrite modNat_plus. rewrite modNat_arg_eq. - rewrite plus_0_l. + rewrite Nat.add_0_l. eauto. Qed. @@ -508,7 +506,7 @@ Lemma modNat_add_same_l : forall x y z p, rewrite modNat_plus in H5. rewrite modNat_mult in H5. - rewrite plus_0_l in H5. + rewrite Nat.add_0_l in H5. auto. Qed. @@ -519,9 +517,9 @@ Lemma modNat_add_same_r : forall x y z p, intuition. eapply (modNat_add_same_l x y z). - rewrite plus_comm. + rewrite Nat.add_comm. rewrite H. - rewrite plus_comm. + rewrite Nat.add_comm. trivial. Qed. @@ -530,30 +528,30 @@ Lemma expnat_base_S : forall n k, induction n; intuition. simpl in *. - eapply le_trans. + eapply Nat.le_trans. 2:{ - eapply plus_le_compat. + eapply Nat.add_le_mono. eapply IHn. - eapply mult_le_compat. - eapply le_refl. + eapply Nat.mul_le_mono. + eapply Nat.le_refl. eapply IHn. } - rewrite mult_plus_distr_l. - repeat rewrite mult_assoc. - repeat rewrite plus_assoc. - eapply plus_le_compat. - rewrite plus_comm. - eapply plus_le_compat. - rewrite <- (plus_0_r (expnat k n)) at 1. - eapply plus_le_compat. + rewrite Nat.mul_add_distr_l. + repeat rewrite Nat.mul_assoc. + repeat rewrite Nat.add_assoc. + eapply Nat.add_le_mono. + rewrite Nat.add_comm. + eapply Nat.add_le_mono. + rewrite <- (Nat.add_0_r (expnat k n)) at 1. + eapply Nat.add_le_mono. lia. intuition. intuition. - rewrite (mult_comm k n). - rewrite <- (mult_assoc n). + rewrite (Nat.mul_comm k n). + rewrite <- (Nat.mul_assoc n). destruct n; simpl; intuition. Qed. @@ -563,8 +561,8 @@ Lemma expnat_base_S_same : forall n, intuition. simpl in *. - rewrite plus_0_r. - eapply le_trans. + rewrite Nat.add_0_r. + eapply Nat.le_trans. 2:{ eapply expnat_base_S. } @@ -578,81 +576,49 @@ Lemma sqrt_le_lin_gen : forall a b, Nat.sqrt a <= b)%nat. intuition. - eapply le_trans. + eapply Nat.le_trans. eapply Nat.sqrt_le_lin. trivial. Qed. Lemma div2_le_mono : forall n1 n2, (n1 <= n2 -> - div2 n1 <= div2 n2)%nat. - - induction n1; intuition. - destruct n2. - lia. - destruct (Even.even_odd_dec n1). - destruct (Even.even_odd_dec n2). - repeat rewrite <- even_div2; trivial. - eapply IHn1. - lia. - - rewrite <- even_div2; trivial. - rewrite <- odd_div2; trivial. - econstructor. - eapply IHn1. - lia. - - destruct (Even.even_odd_dec n2). - destruct (lt_dec n1 n2). - assert (n1 <= (S n2))%nat. - lia. - destruct n2. - lia. - rewrite <- odd_div2; trivial. - rewrite <- even_div2. - rewrite <- odd_div2. - eapply le_n_S. - eapply IHn1. - lia. - inversion e. - trivial. - trivial. - assert (n1 = n2). - lia. - subst. - exfalso. - eapply Even.not_even_and_odd; eauto. - - rewrite <- odd_div2; trivial. - rewrite <- odd_div2; trivial. - eapply le_n_S. - eapply IHn1. - lia. + Nat.div2 n1 <= Nat.div2 n2)%nat. + assert (I : 0 < 2) by now apply Nat.lt_0_succ. + intros n1 n2; + destruct (Nat.Even_Odd_dec n1) as [[k1 ->] | [k1 ->]]; + destruct (Nat.Even_Odd_dec n2) as [[k2 ->] | [k2 ->]]; intros H. + - now rewrite 2!Nat.div2_double; apply Nat.mul_le_mono_pos_l with (1 := I). + - rewrite Nat.div2_double, Nat.add_1_r, Nat.div2_succ_double. + apply Nat.mul_le_mono_pos_l with (1 := I). lia. + - rewrite Nat.div2_double, Nat.add_1_r, Nat.div2_succ_double. + apply Nat.mul_le_mono_pos_l with (1 := I). lia. + - rewrite 2!Nat.add_1_r, 2!Nat.div2_succ_double. lia. Qed. Lemma div2_ge : forall n n', n >= n' -> forall x, (n' = 2 * x)%nat -> - div2 n >= x. + Nat.div2 n >= x. induction 1; intuition; subst; simpl in *. - specialize (div2_double x); intuition; simpl in *. + specialize (Nat.div2_double x); intuition; simpl in *. rewrite H. lia. destruct m. lia. - destruct (Even.even_odd_dec m). - rewrite even_div2. - assert (div2 (S m) >= x). + destruct (Nat.Even_Odd_dec m). + rewrite Nat.Even_div2. + assert (Nat.div2 (S m) >= x). eapply IHle. trivial. lia. trivial. - rewrite odd_div2. + rewrite Nat.Odd_div2. eapply IHle. trivial. @@ -685,11 +651,11 @@ Lemma le_expnat_2 : forall n, (n <= expnat 2 n)%nat. induction n; intuition; simpl in *. - rewrite plus_0_r. + rewrite Nat.add_0_r. assert (S n = 1 + n)%nat. lia. rewrite H. - eapply plus_le_compat. + eapply Nat.add_le_mono. eapply expnat_2_ge_1. trivial. @@ -699,7 +665,7 @@ Lemma expnat_1 : forall k, expnat 1%nat k = 1%nat. induction k; intuition; simpl in *. - rewrite plus_0_r. + rewrite Nat.add_0_r. trivial. Qed. @@ -711,8 +677,7 @@ Theorem expnat_base_le : expnat n2 k. induction k; intuition; simpl in *. - eapply mult_le_compat; intuition. - + eapply Nat.mul_le_mono; intuition. Qed. Theorem expnat_double_le : @@ -722,12 +687,12 @@ Theorem expnat_double_le : induction k; intuition; simpl in *. lia. - rewrite plus_0_r. - rewrite <- mult_plus_distr_l. - eapply mult_le_compat. + rewrite Nat.add_0_r. + rewrite <- Nat.mul_add_distr_l. + eapply Nat.mul_le_mono. trivial. - rewrite <- plus_0_r at 1. - rewrite <- plus_assoc. + rewrite <- Nat.add_0_r at 1. + rewrite <- Nat.add_assoc. eapply IHk. trivial. Qed. @@ -751,7 +716,7 @@ Theorem nat_half_plus : destruct H0. intuition. destruct x1. - rewrite plus_0_r in H3. + rewrite Nat.add_0_r in H3. exists x0. exists 1. subst. @@ -768,7 +733,7 @@ Qed. Theorem log2_div2 : forall x y, S y = Nat.log2 x -> - Nat.log2 (div2 x) = y. + Nat.log2 (Nat.div2 x) = y. intuition. specialize (Nat.log2_double); intuition. @@ -781,16 +746,16 @@ Theorem log2_div2 : intuition. subst. destruct x1. - rewrite plus_0_r in *. - rewrite div2_double. + rewrite Nat.add_0_r in *. + rewrite Nat.div2_double. rewrite H0 in H. lia. lia. destruct x1. - rewrite plus_comm. - rewrite div2_double_plus_one. + rewrite Nat.add_comm. + rewrite Nat.add_1_l, Nat.div2_succ_double. rewrite Nat.log2_succ_double in H. lia. @@ -820,7 +785,7 @@ Theorem expnat_plus : induction k1; simpl in *; intuition. rewrite IHk1. - rewrite mult_assoc. + rewrite Nat.mul_assoc. trivial. Qed. @@ -831,8 +796,8 @@ Theorem expnat_ge_1 : 1 <= expnat n k. induction k; intuition; simpl in *. - rewrite <- mult_1_r at 1. - eapply mult_le_compat. + rewrite <- Nat.mul_1_r at 1. + eapply Nat.mul_le_mono. lia. eauto. Qed. @@ -845,14 +810,14 @@ Theorem expnat_exp_le : expnat n n2 <= expnat n n4. induction n2; destruct n4; simpl in *; intuition; try lia. - rewrite <- mult_1_l at 1. - eapply mult_le_compat. + rewrite <- Nat.mul_1_l at 1. + eapply Nat.mul_le_mono. lia. eapply expnat_ge_1; trivial. destruct (eq_nat_dec n 0); subst. simpl; intuition. - eapply mult_le_compat; intuition. + eapply Nat.mul_le_mono; intuition. eapply IHn2. lia. lia. @@ -866,15 +831,13 @@ Lemma mult_lt_compat : a * c < b * d. intuition. - eapply le_lt_trans. - eapply mult_le_compat. + eapply Nat.le_lt_trans. + eapply Nat.mul_le_mono. assert (a <= b). lia. eapply H1. - eapply le_refl. - eapply mult_lt_compat_l. - trivial. - lia. + eapply Nat.le_refl. + apply Nat.mul_lt_mono_pos_l; lia. Qed. Theorem orb_same_eq_if : diff --git a/src/FCF/examples/Commit.v b/src/FCF/examples/Commit.v index 7885a9c..6d7facd 100644 --- a/src/FCF/examples/Commit.v +++ b/src/FCF/examples/Commit.v @@ -14,15 +14,15 @@ Theorem modNat_mult_eq : destruct (modNat_correct b c). rewrite H. clear H; - rewrite mult_plus_distr_l. + rewrite Nat.mul_add_distr_l. rewrite modNat_plus. - rewrite mult_assoc. + rewrite Nat.mul_assoc. rewrite modNat_mult. - rewrite plus_0_l. + rewrite Nat.add_0_l. symmetry. rewrite modNat_plus. rewrite modNat_mult. - rewrite plus_0_l. + rewrite Nat.add_0_l. rewrite (@modNat_eq _ (modNat b c)). trivial. eapply modNat_lt. @@ -127,26 +127,26 @@ Section Pedersen. eapply (comp_spec_iso (fun z => modNat (x * z) order) (fun z => modNat (z * multInverseModOrder x) order)). intuition. - rewrite (mult_comm x0). + rewrite (Nat.mul_comm x0). rewrite <- modNat_mult_eq. - rewrite mult_assoc. - rewrite mult_comm. + rewrite Nat.mul_assoc. + rewrite Nat.mul_comm. rewrite modNat_mult_eq. rewrite multInverseCorrect. - rewrite mult_1_r. + rewrite Nat.mul_1_r. eapply modNat_eq. eapply RndNat_support_lt. trivial. intuition. - rewrite mult_comm. + rewrite Nat.mul_comm. rewrite <- modNat_mult_eq. - rewrite mult_assoc. - rewrite mult_comm. + rewrite Nat.mul_assoc. + rewrite Nat.mul_comm. rewrite modNat_mult_eq. - rewrite (mult_comm _ x). + rewrite (Nat.mul_comm _ x). rewrite multInverseCorrect. - rewrite mult_1_r. + rewrite Nat.mul_1_r. eapply modNat_eq. eapply RndNat_support_lt. trivial. @@ -343,23 +343,23 @@ Section Pedersen. intuition. unfold modNatAddInverse. - rewrite mult_minus_distr_l. + rewrite Nat.mul_sub_distr_l. rewrite modNat_mult_eq. remember (modNat b c) as z. eapply (modNat_add_same_r (modNat (a * z) c)). rewrite Nat.sub_add. rewrite modNat_arg_eq. - rewrite plus_comm. + rewrite Nat.add_comm. rewrite <- modNat_plus. - rewrite plus_comm. + rewrite Nat.add_comm. rewrite Nat.sub_add. symmetry. apply modNat_mult. - eapply mult_le_compat; intuition. + eapply Nat.mul_le_mono; intuition. subst. - eapply lt_le_weak. + eapply Nat.lt_le_incl. apply modNat_lt. - eapply lt_le_weak. + eapply Nat.lt_le_incl. apply modNat_lt. Qed. @@ -369,11 +369,11 @@ Section Pedersen. modNat (a * c) d = modNat (b * c) d. intuition. - rewrite mult_comm. + rewrite Nat.mul_comm. rewrite modNat_mult_eq. rewrite H0. rewrite <- modNat_mult_eq. - rewrite mult_comm. + rewrite Nat.mul_comm. intuition. Qed. @@ -426,45 +426,45 @@ Section Pedersen. eapply (modNat_eq_compat_gen order) in H4. repeat rewrite <- modNat_plus in H4. - rewrite <- (plus_comm (x * n2)) in H4. - rewrite <- (plus_assoc _ n1) in H4. - rewrite (plus_comm (x * n2)) in H4. + rewrite <- (Nat.add_comm (x * n2)) in H4. + rewrite <- (Nat.add_assoc _ n1) in H4. + rewrite (Nat.add_comm (x * n2)) in H4. symmetry in H4. rewrite modNat_plus in H4. rewrite modNatAddInverse_correct in H4. - rewrite plus_0_l in H4. + rewrite Nat.add_0_l in H4. symmetry in H4. - rewrite (plus_comm) in H4. - rewrite plus_assoc in H4. + rewrite (Nat.add_comm) in H4. + rewrite Nat.add_assoc in H4. eapply (plus_add_same_r_if (modNatAddInverse (x * n0) order)) in H4. eapply (modNat_eq_compat_gen order) in H4. rewrite <- modNat_plus in H4. - rewrite <- plus_assoc in H4. - rewrite plus_comm in H4. + rewrite <- Nat.add_assoc in H4. + rewrite Nat.add_comm in H4. rewrite modNat_plus in H4. rewrite modNatAddInverse_correct in H4. - rewrite plus_0_l in H4. + rewrite Nat.add_0_l in H4. rewrite <- modNat_plus in H4. symmetry in H4. - rewrite (plus_comm (x * n2)) in H4. + rewrite (Nat.add_comm (x * n2)) in H4. rewrite modNat_plus in H4. rewrite modNatAddInverse_mult in H4. rewrite <- modNat_plus in H4. - rewrite <- mult_plus_distr_l in H4. + rewrite <- Nat.mul_add_distr_l in H4. apply (modNat_mult_same_r _ _ (multInverseModOrder (n2 + modNatAddInverse n0 order)))in H4. - rewrite <- mult_assoc in H4. + rewrite <- Nat.mul_assoc in H4. rewrite modNat_mult_eq in H4. - rewrite (plus_comm n2) in H4. + rewrite (Nat.add_comm n2) in H4. rewrite multInverseCorrect in H4. - rewrite mult_1_r in H4. + rewrite Nat.mul_1_r in H4. rewrite modNat_eq in H4. rewrite H4. clear H4. - rewrite (plus_comm (modNatAddInverse n1 order)). - rewrite (plus_comm n2). + rewrite (Nat.add_comm (modNatAddInverse n1 order)). + rewrite (Nat.add_comm n2). trivial. eapply RndNat_support_lt; intuition. diff --git a/src/FCF/examples/ElGamal.v b/src/FCF/examples/ElGamal.v index 9af33b3..d267119 100644 --- a/src/FCF/examples/ElGamal.v +++ b/src/FCF/examples/ElGamal.v @@ -56,7 +56,7 @@ Section ElGamal. repeat simp_in_support. rewrite <- associativity. repeat rewrite groupExp_mult. - rewrite mult_comm. + rewrite Nat.mul_comm. rewrite left_inverse. apply left_identity. Qed. diff --git a/src/FCF/examples/PRF_DRBG.v b/src/FCF/examples/PRF_DRBG.v index df228e1..28c95be 100644 --- a/src/FCF/examples/PRF_DRBG.v +++ b/src/FCF/examples/PRF_DRBG.v @@ -711,14 +711,14 @@ Section PRF_DRBG. (* The rest is just arithmetic. *) simpl. - rewrite mult_1_r. + rewrite Nat.mul_1_r. replace (S (length ls + length ls * S (length ls))) with (S (length ls) + length ls * S (length ls))%nat. rewrite ratAdd_num. eapply ratAdd_leRat_compat. eapply leRat_terms; lia. eapply leRat_terms. - eapply mult_le_compat; lia. + eapply Nat.mul_le_mono; lia. trivial. lia. Qed. @@ -733,7 +733,7 @@ Section PRF_DRBG. simpl. rewrite forNats_length. - rewrite mult_1_r. + rewrite Nat.mul_1_r. reflexivity. Qed. diff --git a/src/FCF/examples/PRF_Encryption_IND_CPA.v b/src/FCF/examples/PRF_Encryption_IND_CPA.v index 580b653..dd849c2 100644 --- a/src/FCF/examples/PRF_Encryption_IND_CPA.v +++ b/src/FCF/examples/PRF_Encryption_IND_CPA.v @@ -1546,7 +1546,7 @@ Section PRF_Encryption_concrete. intuition. simpl. - repeat rewrite plus_0_r. + repeat rewrite Nat.add_0_r. (* lia can't handle the functions -- remove them *) assert (A1_cost (eta + eta + (x + (eta + (eta + eta)))) = @@ -1777,8 +1777,8 @@ Section PRF_Encryption. econstructor. econstructor. eapply H8. - eapply le_refl. - eapply le_refl. + eapply Nat.le_refl. + eapply Nat.le_refl. intuition. eapply PRFE_Encrypt_OC_qam. intuition.