Skip to content

Commit

Permalink
Now compiles with ssreflect.
Browse files Browse the repository at this point in the history 
Phew...
  • Loading branch information
Bas Spitters committed Sep 15, 2009
1 parent 7758c78 commit 9473954
Show file tree
Hide file tree
Showing 118 changed files with 1,972 additions and 2,398 deletions.
8 changes: 4 additions & 4 deletions CayleyHamilton/CCayleyHamilton.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ Add Ring cpoly_r : (RingClass.r_rt (Ring:=CRing_is_Ring (cpoly_cring CR))).

Section degree_le.

Global Instance degree_le_morph : Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (@degree_le CR).
Global Instance degree_le_morph : Morphisms.Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (@degree_le CR).
Proof. by move=> p q -> x y eqxy; split;[|symmetry in eqxy]; apply degree_le_wd. Qed.

Lemma bigsum_degree_le : forall n (I : finType) (F : I -> cpoly_cring CR),
Expand All @@ -69,7 +69,7 @@ case: (P i)=> Hi; last by apply Hrec.
by apply degree_le_mult; [apply Hi|apply Hrec].
Qed.

Global Instance nth_coeff_morph : Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (@nth_coeff CR).
Global Instance nth_coeff_morph : Morphisms.Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (@nth_coeff CR).
Proof. by move=> p q -> x y eqxy; apply nth_coeff_wd. Qed.

Lemma nth_coeff_bigsum : forall n (I : finType) (F : I -> cpoly_cring CR),
Expand All @@ -82,7 +82,7 @@ have Hplus : forall p q : cpoly_cring CR, nth_coeff n (p[+]q) [=] nth_coeff n p
by apply (big_morph Hplus Hz _ predT).
Qed.

Global Instance monic_morphism : Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (@monic CR).
Global Instance monic_morphism : Morphisms.Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (@monic CR).
Proof. by move=> p q -> x y eqxy; split; [|symmetry in eqxy]; apply monic_wd. Qed.

Lemma monic_bigsum : forall n (I : finType) (F : I -> cpoly_cring CR) (i : I),
Expand Down Expand Up @@ -117,7 +117,7 @@ simpl.
by apply monic_mult.
Qed.

Global Instance cpoly_apply_morph : Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (cpoly_apply CR).
Global Instance cpoly_apply_morph : Morphisms.Morphism (Equivalence.equiv==>Equivalence.equiv==>Equivalence.equiv) (cpoly_apply CR).
Proof. by move=> a b eqab x y eqxy; apply cpoly_apply_wd. Qed.

Lemma apply_bigsum : forall (I : finType) (F : I -> cpoly_cring CR) (x : CR),
Expand Down
12 changes: 6 additions & 6 deletions Liouville/Liouville.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ Lemma Abs_poly_nth_coeff : forall P i, nth_coeff i (AbsPoly P) [=] AbsIR (nth_co
Proof.
intro P.
pattern P; apply Ccpoly_induc; clear P.
intro; rewrite AbsPoly_zero, nth_coeff_zero.
intro; rewrite AbsPoly_zero nth_coeff_zero.
symmetry; apply AbsIRz_isz.
intros P c Hrec n.
rewrite AbsPoly_linear.
Expand Down Expand Up @@ -188,7 +188,7 @@ split.
apply minus_resp_leEq.
apply (leEq_wdl _ (x[+](a[-]x))); [|rational].
apply plus_resp_leEq_lft.
rewrite AbsIR_minus in Hle.
rewrite -> AbsIR_minus in Hle.
apply (leEq_transitive _ _ (AbsIR (a[-]x))); [|assumption].
apply leEq_AbsIR.
apply (leEq_wdl _ (x[-]Two[+]Two)); [|rational].
Expand Down Expand Up @@ -283,7 +283,7 @@ assert ((inject_Z (Zpos q))[^]n [#] Zero).
intro; destruct IHn.
rewrite <- nexp_Sn in H.
destruct (Qmult_integral _ _ H); [discriminate|assumption].
rewrite H0 in H.
rewrite -> H0 in H.
apply (mult_eq_zero _ _ _ X); assumption.
Qed.

Expand All @@ -303,20 +303,20 @@ assert ((zx2qx (qx2zx P)) ! (p#q)%Q[#]Zero).
case (Q_dec ((zx2qx (qx2zx P)) ! (p#q)%Q) Zero); [|tauto].
intro Heq; destruct (ap_imp_neq _ _ _ Hap); revert Heq.
rewrite qx2zx_spec.
rewrite mult_apply, c_apply.
rewrite mult_apply c_apply.
intro Heq.
apply (mult_eq_zero _ (Zlcm_den_poly P:Q_as_CField)).
intro Heq2; injection Heq2.
rewrite Zmult_1_r.
apply Zlcm_den_poly_nz.
assumption.
rewrite qx2zx_deg; fold ZX_deg.
rewrite -> qx2zx_deg; fold ZX_deg.
apply (leEq_wdr _ _ _ _ (Liouville_lemma5 _ _ _ X)); fold ZX_deg.
apply mult_wdr.
apply AbsIR_wd.
apply csf_wd.
rewrite qx2zx_spec.
rewrite mult_apply, c_apply; reflexivity.
rewrite mult_apply c_apply; reflexivity.
Qed.

Lemma Liouville_lemma7 : forall (p : Z_as_CRing) (q : positive), P ! (p#q)%Q [#] Zero ->
Expand Down
22 changes: 11 additions & 11 deletions Liouville/QX_ZX.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ split; intro H.
cut (Zpos Qden = Zgcd Qnum Qden).
intro H0; rewrite H0.
apply Zgcd_is_divisor_lft.
rewrite (Zgcd_div_mult_rht Qnum Qden) at 1.
rewrite {1} (Zgcd_div_mult_rht Qnum Qden).
rewrite H.
apply Zmult_1_l.
intro.
Expand All @@ -158,13 +158,13 @@ split; intro H.
unfold Q_can_den.
destruct q; simpl in *.
case (Z_dec Qnum 0).
intro H0; rewrite H0 in *.
intro H0; rewrite H0.
rewrite Zgcd_zero_lft.
apply Z_div_same_full.
discriminate.
intro Hap.
cut (Zpos Qden = Zgcd Qnum Qden).
intro H0; rewrite H0 at 1.
intro H0; rewrite {1} H0.
apply Z_div_same_full.
intro H1; destruct (Zgcd_zero _ _ H1).
discriminate.
Expand Down Expand Up @@ -202,7 +202,7 @@ intros P Q; pattern P, Q; apply Ccpoly_double_sym_ind; clear P Q.
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.
Expand Down Expand Up @@ -268,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.
Expand All @@ -282,19 +282,19 @@ unfold Q_can_num; simpl.
unfold Q_can_den in Hin.
simpl in Hin.
cut (Zpos qd = Zgcd qn qd).
intro H; rewrite H at 2.
intro H; rewrite {2} H.
rewrite Zmult_comm.
symmetry; apply Zdivides_spec.
apply Zgcd_is_divisor_lft.
rewrite (Zgcd_div_mult_rht qn qd) at 1.
rewrite {1} (Zgcd_div_mult_rht qn qd).
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.

Expand Down Expand Up @@ -331,7 +331,7 @@ intros P c Hrec n.
rewrite zx2qx_linear.
induction n.
reflexivity.
rewrite coeff_Sm_lin, coeff_Sm_lin.
rewrite coeff_Sm_lin coeff_Sm_lin.
apply Hrec.
Qed.

Expand All @@ -344,7 +344,7 @@ set (Hin n).
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.

Expand Down Expand Up @@ -388,7 +388,7 @@ case (RX_dec _ Q_dec P Zero).
intro H.
transitivity (nth_coeff n (Zero:QX)).
apply nth_coeff_wd.
rewrite H at 2.
rewrite {2} H.
apply I.
reflexivity.
intro Hap.
Expand Down
20 changes: 10 additions & 10 deletions Liouville/QX_extract_roots.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ assert (forall x y : Q_as_CRing, {x = y} + {x <> y}).
right; intro H3; injection H3; intros; destruct H2; assumption.
right; intro H3; injection H3; intros; destruct H2; assumption.
destruct (In_dec X (Q_can q) (list_Q (P0 P) (Pn P))).
intro H; rewrite (Q_can_spec q) in H; revert H.
intro H; rewrite -> (Q_can_spec q) in H; revert H.
apply (QX_test_list_spec_none _ _ Hnone _ i).
intro Hval; apply n.
apply QX_root_loc; assumption.
Expand Down Expand Up @@ -152,7 +152,7 @@ clear s.
destruct c.
destruct d.
intro Hq.
rewrite Hq in s.
rewrite -> Hq in s.
assert (H : p [=] r); [rewrite s; unfold cg_minus; unfold QX; ring|].
unfold QX_deg; rewrite (RX_deg_wd _ Q_dec _ _ H); fold QX_deg.
destruct (_X_monic _ a).
Expand All @@ -174,19 +174,19 @@ 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; unfold max.
rewrite QX_deg_mult.
rewrite -> QX_deg_mult.
unfold QX_deg; rewrite RX_deg_minus.
rewrite RX_deg_c_, RX_deg_x_; fold QX_deg.
rewrite RX_deg_c_ RX_deg_x_; fold QX_deg.
simpl; rewrite plus_comm; simpl.
intro H; injection H; symmetry; assumption.
rewrite RX_deg_x_, RX_deg_c_; discriminate.
rewrite RX_deg_x_ RX_deg_c_; discriminate.
apply QX_div_deg0; assumption.
right; left; discriminate.
rewrite QX_deg_mult.
rewrite -> QX_deg_mult.
unfold QX_deg; rewrite RX_deg_minus.
rewrite RX_deg_x_, RX_deg_c_, RX_deg_c_.
rewrite RX_deg_x_ RX_deg_c_ RX_deg_c_.
rewrite plus_comm; discriminate.
rewrite RX_deg_x_, RX_deg_c_; discriminate.
rewrite RX_deg_x_ RX_deg_c_; discriminate.
apply QX_div_deg0; assumption.
right; left; discriminate.
Qed.
Expand Down Expand Up @@ -215,7 +215,7 @@ induction n.
destruct (degree_le_zero _ _ d).
case (Q_dec P ! a Zero); [|tauto].
intro Heq; destruct (ap_imp_neq _ _ _ Hap); clear Hap; revert Heq.
rewrite s, c_apply; intro H; rewrite H; split; [reflexivity|apply I].
rewrite s c_apply; intro H; rewrite H; split; [reflexivity|apply I].
unfold QX_extract_roots_rec.
intros P Hdeg Hap.
case_eq (QX_find_root P).
Expand Down Expand Up @@ -255,7 +255,7 @@ apply IHn.
rewrite Hdeg; apply QX_div_deg.
rewrite <- Hdeg; discriminate.
clear IHn; revert Hval.
rewrite (RX_div_spec _ P y) at 1.
rewrite {1} (RX_div_spec _ P y).
rewrite rh_pres_plus.
rewrite rh_pres_mult.
rewrite rh_pres_minus.
Expand Down
30 changes: 15 additions & 15 deletions Liouville/QX_root_loc.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,21 +47,21 @@ Lemma Sum0_ring_hom : forall R S (phi : RingHom R S) f n,
Proof.
intros.
induction n; [apply rh_pres_zero|].
simpl; rewrite rh_pres_plus, IHn; reflexivity.
simpl; rewrite rh_pres_plus IHn; reflexivity.
Qed.

Lemma Sum_ring_hom : forall R S (phi : RingHom R S) f i j,
phi (Sum i j f) [=] Sum i j (fun i => phi (f i)).
Proof.
intros; unfold Sum, Sum1; simpl.
rewrite rh_pres_minus, rh_pres_plus.
rewrite Sum0_ring_hom, Sum0_ring_hom; reflexivity.
rewrite rh_pres_minus rh_pres_plus.
rewrite Sum0_ring_hom Sum0_ring_hom; reflexivity.
Qed.

Lemma nexp_ring_hom : forall R S (phi : RingHom R S) a n, phi (a[^]n) [=] phi a[^]n.
Proof.
intros; induction n; [apply rh_pres_unit|].
rewrite <- nexp_Sn, <- nexp_Sn; rewrite rh_pres_mult, IHn; reflexivity.
rewrite <- nexp_Sn, <- nexp_Sn; rewrite rh_pres_mult IHn; reflexivity.
Qed.

Lemma Q_Z_nexp : forall (p : Z_as_CRing) (q : positive) i, ((p#q)[^]i[*](q:Q_as_CRing)[^]i [=] p[^]i)%Q.
Expand All @@ -82,7 +82,7 @@ rewrite <- CRings.mult_assoc.
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.
Expand All @@ -106,18 +106,18 @@ assert (degree_le n (zx2qx P)).
rewrite d; [reflexivity|assumption].
rewrite (poly_as_sum _ _ _ H).
rewrite <- mult_distr_sum_lft.
rewrite (Sum_ring_hom _ _ injZ_rh).
rewrite -> (Sum_ring_hom _ _ injZ_rh).
apply Sum_wd'.
apply le_O_n.
intros i H0 Hn.
rewrite nth_coeff_zx2qx.
rewrite rh_pres_mult.
rewrite rh_pres_mult.
rewrite mult_commutes.
rewrite nexp_ring_hom, nexp_ring_hom.
rewrite nexp_ring_hom nexp_ring_hom.
rewrite <- CRings.mult_assoc, <- CRings.mult_assoc.
apply mult_wdr.
rewrite (le_plus_minus _ _ Hn) at 1.
rewrite {1} (le_plus_minus _ _ Hn).
clear H0 Hn.
rewrite <- nexp_plus.
rewrite CRings.mult_assoc.
Expand Down Expand Up @@ -147,7 +147,7 @@ destruct (RX_deg_spec _ Q_dec _ HapP).
split.
intro.
destruct c.
rewrite nth_coeff_c_mult_p in H.
rewrite -> nth_coeff_c_mult_p in H.
apply (mult_eq_zero _ _ _ Hap H).
intros m Hlt.
rewrite nth_coeff_c_mult_p.
Expand Down Expand Up @@ -183,7 +183,7 @@ rewrite <- CRings.mult_assoc.
apply mult_wd.
reflexivity.
rewrite <- minus_Sn_m; [|assumption].
rewrite CRings.mult_commutes; reflexivity.
rewrite -> CRings.mult_commutes; reflexivity.
Qed.

Lemma qx2zx_deg : forall P, QX_deg P = ZX_deg (qx2zx P).
Expand All @@ -208,7 +208,7 @@ Proof.
intros P a Hval.
set (P0 := _C_ (Zlcm_den_poly P:Q_as_CRing)[*]P).
assert (H : P0 ! a [=] Zero).
unfold P0; rewrite mult_apply, c_apply, Hval; ring.
unfold P0; rewrite mult_apply c_apply Hval; ring.
clear Hval; revert H.
rewrite (zx2qx_spec P0); [|apply Zlcm_den_poly_spec].
unfold P0; clear P0.
Expand All @@ -221,7 +221,7 @@ assert ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q [=] Zero).
assert (Q_can_num ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q) [=] Zero).
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.
Expand Down Expand Up @@ -311,7 +311,7 @@ Proof.
intros P a Hval.
set (Q := _C_ (Zlcm_den_poly P:Q_as_CRing)[*]P).
assert (H : Q ! a [=] Zero).
unfold Q; rewrite mult_apply, c_apply, Hval; ring.
unfold Q; rewrite mult_apply c_apply Hval; ring.
clear Hval; revert H.
rewrite (zx2qx_spec Q); [|apply Zlcm_den_poly_spec].
unfold Q; clear Q.
Expand All @@ -324,7 +324,7 @@ assert ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q [=] Zero).
assert (Q_can_num ((q:Q_as_CRing)[^](ZX_deg Q) [*] (zx2qx Q) ! (p # q)%Q) [=] Zero).
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.
Expand Down Expand Up @@ -362,7 +362,7 @@ apply list_Q_spec.
intro; apply Hap; clear Hap.
unfold P0 in H.
cut ((_C_ (Zlcm_den_poly P:Q_as_CRing) [*] P) ! Zero [=] Zero).
rewrite mult_apply, c_apply.
rewrite mult_apply c_apply.
intro H0; apply (Qmult_eq (Zlcm_den_poly P)); [|assumption].
intro H1; destruct (Zlcm_den_poly_nz P).
unfold Qeq in H1; simpl in H1.
Expand Down
Loading

0 comments on commit 9473954

Please sign in to comment.