From 5521ddd4fe73f2756130f91856cab81cfad517bb Mon Sep 17 00:00:00 2001 From: Valentin Blot <24938579+vblot@users.noreply.github.com> Date: Mon, 8 Jan 2018 16:34:12 +0100 Subject: [PATCH] Removed the ssreflect dependency and fixed some "Admitted" --- liouville/CPoly_Euclid.v | 22 +++++++--------- liouville/QX_ZX.v | 49 ++++++++++++++++++------------------ liouville/QX_extract_roots.v | 19 +++++++------- liouville/QX_root_loc.v | 9 +++---- liouville/Q_can.v | 17 ++++++------- liouville/RX_deg.v | 15 ++++++----- liouville/Zlcm.v | 21 ++++++++-------- 7 files changed, 71 insertions(+), 81 deletions(-) diff --git a/liouville/CPoly_Euclid.v b/liouville/CPoly_Euclid.v index e2757259..df01d89d 100644 --- a/liouville/CPoly_Euclid.v +++ b/liouville/CPoly_Euclid.v @@ -52,8 +52,7 @@ Theorem cpoly_div1 : forall (m n : nat) (f g : cpoly_cring CR), let (q,r):=qr in f [*] _C_ ((nth_coeff (S n) g) [^] (m - n)) [=] q [*] g [+] r & let (q,r):=qr in degree_le n r}. Proof. -Admitted. (* - intros m n; set (H := refl_equal (m - n)); revert H. + intros m n; generalize (refl_equal (m - n)). generalize (m - n) at 1 as p; intro p; revert m n; induction p; intros. exists (([0] : cpoly_cring CR),f). rewrite <- H. @@ -72,28 +71,26 @@ Admitted. (* replace (m - 1 - n) with (m - S n) by omega. rewrite <- nexp_Sn. generalize (nth_coeff (S n) g) (nth_coeff m f) (m - S n). - intros. rewrite c_mult c_mult. unfold cg_minus. ring. + intros. rewrite c_mult, c_mult. unfold cg_minus. ring. Qed. -*) Definition degree_lt_pair (p q : cpoly_cring CR) := (forall n : nat, degree_le (S n) q -> degree_le n p) and (degree_le O q -> p [=] [0]). Lemma cpoly_div2 : forall (n m : nat) (a b c : cpoly_cring CR), degree_le n a -> monic m b -> degree_lt_pair c b -> a [*] b [=] c -> a [=] [0]. Proof. -Admitted. (* induction n. intros m a b c H X H1 H2; destruct (degree_le_zero _ _ H) as [x s]. - move: H1. rewrite -> s; destruct X as [H0 H1]; rewrite -> c_zero. rewrite -> s in H2. intro. apply cpoly_const_eq. + revert H1. rewrite -> s; destruct X as [H0 H1]; rewrite -> c_zero. rewrite -> s in H2. intro. apply cpoly_const_eq. destruct m. - set (tmp := nth_coeff_wd _ 0 _ _ H2); destruct H3 as [d s0]. - move: tmp. rewrite -> nth_coeff_c_mult_p, H0, mult_one, (nth_coeff_wd _ _ _ _ (s0 H1)). intro tmp; apply tmp. - set (tmp := nth_coeff_wd _ (S m) _ _ H2); destruct H3 as [d s0]. - move: tmp. rewrite -> nth_coeff_c_mult_p, H0, mult_one, (d m H1 (S m)). apply. apply le_n. + generalize (nth_coeff_wd _ 0 _ _ H2); destruct H3 as [d s0]. + rewrite -> nth_coeff_c_mult_p, H0, mult_one, (nth_coeff_wd _ _ _ _ (s0 H1)). intro tmp; apply tmp. + generalize (nth_coeff_wd _ (S m) _ _ H2); destruct H3 as [d s0]. + rewrite -> nth_coeff_c_mult_p, H0, mult_one, (d m H1 (S m)). intro; assumption. apply le_n. intros. induction a as [ | a s ] using cpoly_induc; [ reflexivity | ]. apply _linear_eq_zero. - move: H2. rewrite -> cpoly_lin, ring_distl_unfolded. intro H2. + revert H2. rewrite -> cpoly_lin, ring_distl_unfolded. intro H2. cut (a [=] [0]); [ intro aeqz; split; [ | apply aeqz ] | ]. assert (s [=] nth_coeff m (_C_ s[*]b[+]_X_[*]a[*]b)). destruct H0; rewrite -> nth_coeff_plus, nth_coeff_c_mult_p, H0. @@ -118,11 +115,10 @@ Admitted. (* destruct m; [ destruct H0; apply (nth_coeff_wd _ _ _ _ (s0 H1)) | ]. apply (d n0); [ | apply H4 ]. apply (degree_le_mon _ _ n0); [ apply le_S; apply le_n | apply (degree_le_cpoly_linear _ _ _ _ H3) ]. - destruct (degree_le_zero _ _ H3) as [x s0]. move: s0. rewrite -> cpoly_C_. intro s0. + destruct (degree_le_zero _ _ H3) as [x s0]. revert s0. rewrite -> cpoly_C_. intro s0. destruct (linear_eq_linear_ _ _ _ _ _ s0) as [H4 H5]. rewrite <- H2, -> H5. unfold cg_minus. ring. Qed. -*) Lemma cpoly_div : forall (f g : cpoly_cring CR) (n : nat), monic n g -> ex_unq (fun (qr : ProdCSetoid (cpoly_cring CR) (cpoly_cring CR)) => f[=](fst qr)[*]g[+](snd qr) and degree_lt_pair (snd qr) g). diff --git a/liouville/QX_ZX.v b/liouville/QX_ZX.v index 31d5871e..e828b03f 100644 --- a/liouville/QX_ZX.v +++ b/liouville/QX_ZX.v @@ -23,7 +23,6 @@ Require Import CoRN.model.rings.Qring. Require Import Zring. Require Import Qordfield. Require Import CRing_Homomorphisms. -Require Import ssreflect. Require Import RingClass CRingClass. Require Import Zlcm Q_can RX_deg. @@ -146,16 +145,16 @@ Proof. cut (Zpos Qden = Zgcd Qnum Qden). intro H0; rewrite H0. apply Zgcd_is_divisor_lft. - rewrite {1} (Zgcd_div_mult_rht Qnum Qden). - intro. - destruct (Zgcd_zero _ _ H0). - rewrite H1 in H. - rewrite H2 in H. - rewrite Zgcd_zero_rht in H. - rewrite Zdiv_0_r in H. - discriminate. - rewrite H. - apply Zmult_1_l. + rewrite (Zgcd_div_mult_rht Qnum Qden) at 1. + rewrite H. + apply Zmult_1_l. + intro. + destruct (Zgcd_zero _ _ H0). + rewrite H1 in H. + rewrite H2 in H. + rewrite Zgcd_zero_rht in H. + rewrite Zdiv_0_r in H. + discriminate. unfold Q_can_den. destruct q; simpl in *. case (Z_dec Qnum 0). @@ -165,7 +164,7 @@ Proof. discriminate. intro Hap. cut (Zpos Qden = Zgcd Qnum Qden). - intro H0; rewrite {1} H0. + intro H0; rewrite H0 at 1. apply Z_div_same_full. intro H1; destruct (Zgcd_zero _ _ H1). discriminate. @@ -197,13 +196,13 @@ Proof. destruct (zero_eq_linear_ _ _ _ Heq). split. rewrite (Q_can_num_spec _ [0]). - assumption. - reflexivity. + reflexivity. + assumption. change ([0] [=] Q_can_num_poly P). symmetry; apply Hrec; symmetry; assumption. intros P Q c d Hrec Heq. destruct (linear_eq_linear_ _ _ _ _ _ Heq). - rewrite Q_can_num_poly_linear Q_can_num_poly_linear. + rewrite Q_can_num_poly_linear, Q_can_num_poly_linear. apply _linear_eq_linear. split. apply Q_can_num_spec; assumption. @@ -245,9 +244,9 @@ Proof. unfold Q_can_num; simpl; unfold Qeq; simpl. rewrite Zmult_1_r. intro H; rewrite (Zgcd_div_mult_lft qn qd). - intro H0; destruct (Zgcd_zero _ _ H0); discriminate. - rewrite H. - apply Zmult_0_l. + rewrite H. + apply Zmult_0_l. + intro H0; destruct (Zgcd_zero _ _ H0); discriminate. reflexivity. Qed. @@ -269,7 +268,7 @@ Lemma injZ_strext : fun_strext (inject_Z : Z_as_CRing -> Q_as_CRing). Proof. intros x y. unfold inject_Z; simpl; unfold Qap, Qeq, ap_Z; simpl. - rewrite Zmult_1_r Zmult_1_r; tauto. + rewrite Zmult_1_r, Zmult_1_r; tauto. Qed. Lemma injZ_spec : forall q : Q_as_CRing, in_Z q -> q [=] (Q_can_num q). Proof. @@ -283,19 +282,19 @@ Proof. unfold Q_can_den in Hin. simpl in Hin. cut (Zpos qd = Zgcd qn qd). - intro H; rewrite {2} H. + intro H; rewrite H at 2. rewrite Zmult_comm. symmetry; apply Zdivides_spec. apply Zgcd_is_divisor_lft. - rewrite {1} (Zgcd_div_mult_rht qn qd). - intro H; destruct (Zgcd_zero _ _ H); discriminate. - rewrite Hin; rewrite Zmult_1_l; reflexivity. + rewrite (Zgcd_div_mult_rht qn qd) at 1. + rewrite Hin; rewrite Zmult_1_l; reflexivity. + intro H; destruct (Zgcd_zero _ _ H); discriminate. Qed. Lemma injZ_spec2 : forall p : Z_as_CRing, p = Q_can_num p. Proof. intro p. unfold Q_can_num, inject_Z; simpl. - rewrite Zgcd_one_rht Zdiv_1_r; reflexivity. + rewrite Zgcd_one_rht, Zdiv_1_r; reflexivity. Qed. Definition injZ_fun := Build_CSetoid_fun _ _ _ injZ_strext. @@ -345,7 +344,7 @@ Proof. rewrite -> nth_coeff_zx2qx. rewrite -> (injZ_spec _ i). unfold inject_Z; simpl; unfold Qeq; simpl. - rewrite Zmult_1_r Zmult_1_r. + rewrite Zmult_1_r, Zmult_1_r. symmetry; apply nth_coeff_Q_can_num_poly_spec. Qed. diff --git a/liouville/QX_extract_roots.v b/liouville/QX_extract_roots.v index 1c6b630a..18cafa6a 100644 --- a/liouville/QX_extract_roots.v +++ b/liouville/QX_extract_roots.v @@ -23,7 +23,6 @@ Require Import CRing_Homomorphisms. Require Import CoRN.model.ordfields.Qordfield. Require Import CauchySeq. Require Import Q_in_CReals. -Require Import ssreflect. Require Import CPoly_Euclid RingClass CRingClass. Require Import Q_can nat_Q_lists RX_deg RX_div QX_root_loc. @@ -169,21 +168,21 @@ Proof. revert Heq. unfold QX_deg; rewrite (RX_deg_wd _ Q_dec _ _ (RX_div_spec _ p a)). rewrite RX_deg_sum. - rewrite RX_deg_c_. + rewrite max_comm. rewrite -> QX_deg_mult. unfold QX_deg; rewrite RX_deg_minus. - rewrite RX_deg_x_ RX_deg_c_; discriminate. - rewrite RX_deg_x_ RX_deg_c_. - rewrite plus_comm; discriminate. + rewrite RX_deg_c_, RX_deg_x_, RX_deg_c_; fold QX_deg. + simpl; rewrite plus_comm; simpl. + intro H; injection H; symmetry; assumption. + rewrite RX_deg_x_, RX_deg_c_; discriminate. apply QX_div_deg0; assumption. right; left; discriminate. - rewrite max_comm. + rewrite RX_deg_c_. rewrite -> QX_deg_mult. unfold QX_deg; rewrite RX_deg_minus. - rewrite RX_deg_x_ RX_deg_c_; discriminate. - rewrite RX_deg_c_ RX_deg_x_ RX_deg_c_; fold QX_deg. - simpl; rewrite plus_comm; simpl. - intro H; injection H; symmetry; assumption. + rewrite RX_deg_x_, RX_deg_c_. + rewrite plus_comm; discriminate. + rewrite RX_deg_x_, RX_deg_c_; discriminate. apply QX_div_deg0; assumption. right; left; discriminate. Qed. diff --git a/liouville/QX_root_loc.v b/liouville/QX_root_loc.v index 75e4c924..7c7aa4eb 100644 --- a/liouville/QX_root_loc.v +++ b/liouville/QX_root_loc.v @@ -23,7 +23,6 @@ Require Import CRing_Homomorphisms. Require Import Qring. Require Import Zring. Require Import Qordfield. -Require Import ssreflect. Require Import RingClass CRingClass. Require Import Zlcm Q_can nat_Q_lists RX_deg QX_ZX. @@ -83,7 +82,7 @@ Proof. apply (mult_wdr _ (inject_Z ((p:Z_as_CRing)[^]i)) ((q:Q_as_CRing)[*](p # q)%Q) p). simpl; unfold Qeq; simpl. case p. - rewrite Zmult_0_l Zmult_0_l; reflexivity. + rewrite Zmult_0_l, Zmult_0_l; reflexivity. intro r; rewrite Zmult_1_r; rewrite Zmult_comm; reflexivity. intro r; rewrite Zmult_1_r; rewrite Zmult_comm; reflexivity. Qed. @@ -118,7 +117,7 @@ Proof. rewrite -> nexp_ring_hom, nexp_ring_hom. rewrite <- CRings.mult_assoc, <- CRings.mult_assoc. apply mult_wdr. - rewrite {1} (le_plus_minus _ _ Hn). + rewrite (le_plus_minus _ _ Hn) at 1. clear H0 Hn. rewrite <- nexp_plus. rewrite -> CRings.mult_assoc. @@ -222,7 +221,7 @@ Proof. assert (Q_can_num ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q) [=] [0]). rewrite (Q_can_num_spec _ _ H). unfold Q_can_num; simpl. - rewrite Zgcd_one_rht Zdiv_0_l; reflexivity. + rewrite Zgcd_one_rht, Zdiv_0_l; reflexivity. clear Hval H; revert H0. rewrite (Q_can_num_spec _ _ (Q_Z_poly_apply _ _ _)). rewrite <- injZ_spec2. @@ -325,7 +324,7 @@ Proof. assert (Q_can_num ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q) [=] [0]). rewrite (Q_can_num_spec _ _ H). unfold Q_can_num; simpl. - rewrite Zgcd_one_rht Zdiv_0_l; reflexivity. + rewrite Zgcd_one_rht, Zdiv_0_l; reflexivity. clear Hval H; revert H0. rewrite (Q_can_num_spec _ _ (Q_Z_poly_apply _ _ _)). rewrite <- injZ_spec2. diff --git a/liouville/Q_can.v b/liouville/Q_can.v index a236f641..117e54a6 100644 --- a/liouville/Q_can.v +++ b/liouville/Q_can.v @@ -20,7 +20,6 @@ CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) Require Import CRings Qring Zring. -Require Import ssreflect. Require Import Zlcm. Section Q_can. @@ -44,11 +43,11 @@ Proof. rewrite -> (Zmult_comm (Zgcd q'n q'd) (q'n / Zgcd q'n q'd)). rewrite <- Zgcd_div_mult_lft, <- Zgcd_div_mult_lft; try (intro H; destruct (Zgcd_zero _ _ H); discriminate). - rewrite Zmult_comm (Zmult_comm _ q'n). + rewrite Zmult_comm, (Zmult_comm _ q'n). rewrite <- (Zabs_Zsgn qn) at 1; rewrite <- (Zabs_Zsgn q'n) at 2. - rewrite (Zmult_comm (Zabs qn)) (Zmult_comm (Zabs q'n)). + rewrite (Zmult_comm (Zabs qn)), (Zmult_comm (Zabs q'n)). rewrite <- Zmult_assoc, <- Zmult_assoc. - rewrite Zgcd_lin Zgcd_lin. + rewrite Zgcd_lin, Zgcd_lin. rewrite Heq. rewrite (Zmult_comm qn q'n). cut (Zsgn qn = Zsgn q'n). @@ -73,12 +72,12 @@ Proof. rewrite (Zmult_comm (Zgcd q'n q'd) (q'd / Zgcd q'n q'd)). rewrite <- Zgcd_div_mult_rht, <- Zgcd_div_mult_rht; try (intro H; destruct (Zgcd_zero _ _ H); discriminate). - rewrite Zmult_comm (Zmult_comm _ q'd). + rewrite Zmult_comm, (Zmult_comm _ q'd). rewrite <- (Zabs_Zsgn qd) at 1; rewrite <- (Zabs_Zsgn q'd) at 2. - rewrite (Zmult_comm (Zabs qd)) (Zmult_comm (Zabs q'd)). + rewrite (Zmult_comm (Zabs qd)), (Zmult_comm (Zabs q'd)). rewrite <- Zmult_assoc, <- Zmult_assoc. - rewrite Zgcd_lin Zgcd_lin. - rewrite (Zmult_comm qd q'n) (Zmult_comm q'd qn). + rewrite Zgcd_lin, Zgcd_lin. + rewrite (Zmult_comm qd q'n), (Zmult_comm q'd qn). rewrite Heq. rewrite (Zmult_comm qd q'd). reflexivity. @@ -93,7 +92,7 @@ Proof. assert (0 < Zgcd qn qd)%Z. apply Zgcd_pos; right; discriminate. assert (Zgcd qn qd <= qd)%Z. - by apply Zgcd_le_rht. + apply Zgcd_le_rht; apply Zgt_pos_0. apply Z.div_str_pos. split; assumption. Qed. diff --git a/liouville/RX_deg.v b/liouville/RX_deg.v index d0923b62..861c03e9 100644 --- a/liouville/RX_deg.v +++ b/liouville/RX_deg.v @@ -19,7 +19,6 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) Require Import CPoly_Degree RingClass CRingClass. -Require Import ssreflect. Section RX_deg. @@ -151,7 +150,7 @@ Lemma RX_deg_inv : forall p, RX_deg p = RX_deg ([--]p). Proof. intro p. case (RX_dec p [0]). - intro H; rewrite (RX_deg_wd _ _ H) RX_deg_zero. + intro H; rewrite (RX_deg_wd _ _ H), RX_deg_zero. rewrite <- RX_deg_zero; apply RX_deg_wd; rewrite -> H; unfold RX; ring. intro Hp. apply (degree_inj p). @@ -177,7 +176,7 @@ Proof. set (RX_deg_spec _ Hp). set (RX_deg_spec _ Hq). case (le_lt_dec (RX_deg p) (RX_deg q)); intro. - rewrite max_r; [assumption|]. + rewrite max_r; [|assumption]. inversion l. destruct (Hneq H0). apply (degree_inj (p[+]q)). @@ -185,19 +184,19 @@ Proof. case (RX_dec (p[+]q) [0]); [|tauto]. intro; destruct Hneq. rewrite (RX_deg_wd p ([--]q)). - apply cg_inv_unique'; assumption. - symmetry; apply RX_deg_inv. + symmetry; apply RX_deg_inv. + apply cg_inv_unique'; assumption. apply (degree_plus_rht _ _ _ m); [| |apply le_n]. apply (degree_le_mon _ _ (RX_deg p)); [assumption|apply d]. rewrite H; apply RX_deg_spec; assumption. - rewrite max_l; [apply lt_le_weak; assumption|]. + rewrite max_l; [|apply lt_le_weak; assumption]. apply (degree_inj (p[+]q)). apply RX_deg_spec. case (RX_dec (p[+]q) [0]); [|tauto]. intro; destruct Hneq. rewrite (RX_deg_wd p ([--]q)). - apply cg_inv_unique'; assumption. - symmetry; apply RX_deg_inv. + symmetry; apply RX_deg_inv. + apply cg_inv_unique'; assumption. apply (degree_wd _ _ _ _ (cag_commutes _ _ _)). apply (degree_plus_rht _ _ _ (RX_deg q)); [| |assumption]. apply degree_imp_degree_le. diff --git a/liouville/Zlcm.v b/liouville/Zlcm.v index 9e2d4e34..2ec61e3f 100644 --- a/liouville/Zlcm.v +++ b/liouville/Zlcm.v @@ -19,7 +19,6 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE PROOF OR THE USE OR OTHER DEALINGS IN THE PROOF. *) Require Import CRings Zring. -Require Import ssreflect. Section Zgcd_lin. @@ -34,11 +33,11 @@ Lemma Zgcd_lin : forall a b c, (Zabs c * Zgcd a b = Zgcd (c * a) (c * b))%Z. Proof. intros a b c. case (Z_eq_dec a 0). - intro H; rewrite H; rewrite Zmult_0_r Zgcd_zero_lft Zgcd_zero_lft; apply Zabs_mult_compat. + intro H; rewrite H; rewrite Zmult_0_r, Zgcd_zero_lft, Zgcd_zero_lft; apply Zabs_mult_compat. intro Ha; case (Z_eq_dec b 0). - intro H; rewrite H; rewrite Zmult_0_r Zgcd_zero_rht Zgcd_zero_rht; apply Zabs_mult_compat. + intro H; rewrite H; rewrite Zmult_0_r, Zgcd_zero_rht, Zgcd_zero_rht; apply Zabs_mult_compat. intro Hb; case (Z_eq_dec c 0). - intro H; rewrite H; rewrite Zmult_0_l Zmult_0_l Zmult_0_l Zgcd_zero_lft; reflexivity. + intro H; rewrite H; rewrite Zmult_0_l, Zmult_0_l, Zmult_0_l, Zgcd_zero_lft; reflexivity. intro Hc; apply Zdivides_antisymm. rewrite <- (Zmult_0_r (Zabs c)). apply Zmult_pos_mon_lt_lft. @@ -71,14 +70,14 @@ Proof. assert ((p:Z) = Zabs p). reflexivity. rewrite H0; clear H0. - rewrite Zabs_mult_compat Zabs_mult_compat. + rewrite Zabs_mult_compat, Zabs_mult_compat. rewrite <- Zgcd_abs. apply H. clear c Hc; intro c. rewrite (Zgcd_lin_comb a b). rewrite Zmult_plus_distr_r. simpl (Zabs c). - rewrite Zmult_assoc Zmult_assoc. + rewrite Zmult_assoc, Zmult_assoc. rewrite (Zmult_comm c (Zgcd_coeff_a a b)). rewrite (Zmult_comm c (Zgcd_coeff_b a b)). rewrite <- Zmult_assoc, <- Zmult_assoc. @@ -104,7 +103,7 @@ Proof. intro H; rewrite -> (Zgcd_div_mult_rht a b) at 1; [|assumption]. simpl. rewrite Zmult_assoc. - rewrite Z_div_mult_full; [assumption|]. + rewrite Z_div_mult_full; [|assumption]. apply Zdivides_mult_rht. Qed. @@ -120,7 +119,7 @@ Proof. simpl. rewrite Zmult_comm. rewrite Zmult_assoc. - rewrite Z_div_mult_full; [assumption|]. + rewrite Z_div_mult_full; [|assumption]. apply Zdivides_mult_rht. Qed. @@ -188,11 +187,11 @@ Proof. rewrite -> (Zgcd_div_mult_lft p q) at 1; [|assumption]. rewrite (Zmult_comm (p / Zgcd p q)). rewrite <- Zmult_assoc. - rewrite Zdiv_mult_cancel_lft; [assumption|]. + rewrite Zdiv_mult_cancel_lft; [|assumption]. intro Heq. - rewrite (Zgcd_div_mult_lft p q); [assumption|]. + rewrite (Zgcd_div_mult_lft p q); [|assumption]. rewrite <- Zmult_assoc, (Zmult_comm _ q), Zmult_assoc. - rewrite Heq Zmult_0_l; reflexivity. + rewrite Heq, Zmult_0_l; reflexivity. Qed. Fixpoint Zlcm_gen (l : list Z_as_CRing) : Z_as_CRing :=