Skip to content

Commit

Permalink
Get rid of remaining uses of legacy_rational.
Browse files Browse the repository at this point in the history
  • Loading branch information
@Eelis
Eelis committed Oct 23, 2009
1 parent f570380 commit 4a5d974
Show file tree
Hide file tree
Showing 8 changed files with 69 additions and 48 deletions.
21 changes: 11 additions & 10 deletions algebra/Bernstein.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,7 @@ Section Bernstein.
Opaque cpoly_cring.

Variable R : CRing.
Add Ring R : (CRing_Ring R).
Add Ring cpolycring_th : (CRing_Ring (cpoly_cring R)).
(** [Bernstein n i] is the ith element of the n dimensional Bernstein basis *)

Expand Down Expand Up @@ -117,12 +118,13 @@ Proof.
do 2 rewrite -> mult_distr_sum0_lft.
rewrite -> Sumx_to_Sum in IHn; auto with *.
setoid_replace (Sum0 (S (S n)) (part_tot_nat_fun (cpoly_cring R) (S n) A))
with (Sum0 (S (S n)) (part_tot_nat_fun (cpoly_cring R) (S n) A)[-]Zero);[|legacy_rational].
with (Sum0 (S (S n)) (part_tot_nat_fun (cpoly_cring R) (S n) A)[-]Zero);[|unfold cg_minus;ring].
change (Sum0 (S (S n)) (part_tot_nat_fun (cpoly_cring R) (S n) A)[-]Zero)
with (Sum 0 (S n) (part_tot_nat_fun (cpoly_cring R) (S n) A)).
set (C:=(fun i : nat => match i with | 0 => (Zero : cpoly_cring R)
| S i' => part_tot_nat_fun (cpoly_cring R) (S n) A i' end)).
setoid_replace (Sum0 (S (S n)) C) with (Sum0 (S (S n)) C[-]Zero);[|legacy_rational].
setoid_replace (Sum0 (S (S n)) C) with (Sum0 (S (S n)) C[-]Zero).
2: unfold cg_minus; ring.
change (Sum0 (S (S n)) C[-]Zero) with (Sum 0 (S n) C).
rewrite -> Sum_last.
rewrite -> IHn.
Expand All @@ -131,7 +133,7 @@ Proof.
change (C 0) with (Zero:cpoly_cring R).
rewrite <- (Sum_shift _ (part_tot_nat_fun (cpoly_cring R) (S n) A)).
rewrite -> IHn.
legacy_rational.
unfold cg_minus. ring.
reflexivity.
unfold part_tot_nat_fun.
destruct (le_lt_dec (S n) (S n)).
Expand All @@ -150,15 +152,14 @@ Proof.
intros l l0.
simpl (Bernstein l).
replace l0 with (le_O_n n) by apply le_irrelevent.
legacy_rational.
unfold cg_minus. ring.
destruct (le_lt_dec (S n) i).
elimtype False; omega.
destruct (le_lt_dec (S n) (S i)); simpl (Bernstein (lt_n_Sm_le (S i) (S n) Hi));
destruct (le_lt_eq_dec (S i) (S n) (lt_n_Sm_le (S i) (S n) Hi)).
elimtype False; omega.
replace (lt_n_Sm_le i n (lt_n_Sm_le (S i) (S n) Hi)) with (lt_n_Sm_le i n l) by apply le_irrelevent.
simpl.
legacy_rational.
simpl. unfold cg_minus. ring.
replace (le_S_n i n (lt_n_Sm_le (S i) (S n) Hi)) with (lt_n_Sm_le i n l) by apply le_irrelevent.
replace l1 with l0 by apply le_irrelevent.
reflexivity.
Expand All @@ -169,10 +170,10 @@ Lemma RaiseDegreeA : forall n i (H:i<=n), (nring (S n))[*]_X_[*]Bernstein H[=](n
Proof.
induction n.
intros [|i] H; [|elimtype False; omega].
repeat split; legacy_rational.
repeat split; ring.
intros i H.
change (nring (S (S n)):cpoly_cring R) with (nring (S n)[+]One:cpoly_cring R).
stepl (nring (S n)[*]_X_[*]Bernstein H[+]_X_[*]Bernstein H). 2:legacy_rational.
stepl (nring (S n)[*]_X_[*]Bernstein H[+]_X_[*]Bernstein H). 2: ring.
destruct i as [|i].
simpl (Bernstein H) at 1.
rstepl ((One[-]_X_)[*](nring (S n)[*]_X_[*]Bernstein (le_O_n n))[+] _X_[*]Bernstein H).
Expand Down Expand Up @@ -210,7 +211,7 @@ Lemma RaiseDegreeB : forall n i (H:i<=n), (nring (S n))[*](One[-]_X_)[*]Bernstei
Proof.
induction n.
intros [|i] H; [|elimtype False; omega].
repeat split; legacy_rational.
repeat split; ring.
intros i H.
change (nring (S (S n)):cpoly_cring R) with (nring (S n)[+]One:cpoly_cring R).
set (X0:=(One[-](@cpoly_var R))) in *.
Expand Down Expand Up @@ -269,7 +270,7 @@ Proof.
stepl ((nring (S n))[*](One[-]_X_)[*]Bernstein H[+](nring (S n))[*]_X_[*]Bernstein H).
rewrite -> RaiseDegreeA, RaiseDegreeB.
reflexivity.
legacy_rational.
unfold cg_minus. ring.
Qed.

Opaque Bernstein.
Expand Down
4 changes: 3 additions & 1 deletion algebra/CPoly_ApZero.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,8 @@ Variable f : cpoly_cring R.
Variable n : nat.
Hypothesis degree_f : degree_le n f.

Add Ring cpolycring_th : (cpoly_ring_th R).

(* begin hide *)
Notation RX := (cpoly_cring R).
(* end hide *)
Expand All @@ -85,7 +87,7 @@ Proof.
apply eq_symmetric_unfolded.
cut (_C_ (a[*]g''[+]s) [=] _C_ a[*]_C_ g''[+]_C_ s). intro.
astepl ((_X_[-]_C_ a) [*] (_X_[*]g'[+]_C_ g'') [+] (_C_ a[*]_C_ g''[+]_C_ s)).
legacy_rational. (* Does not recognize polyring *)
unfold cg_minus. ring.
Step_final (_C_ (a[*]g'') [+]_C_ s).
Qed.
Load "Opaque_algebra".
Expand Down
11 changes: 6 additions & 5 deletions algebra/CPoly_Degree.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,8 @@ Section Degree_props.

Variable R : CRing.

Add Ring R: (CRing_Ring R).

(* begin hide *)
Notation RX := (cpoly_cring R).
(* end hide *)
Expand Down Expand Up @@ -468,11 +470,10 @@ Proof.
unfold degree_le in |- *. intros.
exists (nth_coeff 1 p). exists (nth_coeff 0 p).
apply all_nth_coeff_eq_imp. intros.
elim i; intros.
simpl in |- *. legacy_rational.
elim n; intros.
simpl in |- *. algebra.
simpl in |- *. apply H. auto with arith.
elim i; intros. simpl in |- *. ring.
elim n; intros.
simpl in |- *. algebra.
simpl in |- *. apply H. auto with arith.
Qed.

Lemma degree_le_cpoly_linear : forall (p : cpoly R) c n,
Expand Down
32 changes: 18 additions & 14 deletions algebra/CPoly_Euclid.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,9 @@ Unset Strict Implicit.
Section poly_eucl.
Variable CR : CRing.

Add Ring CR: (CRing_Ring CR).
Add Ring cpolycring_th : (CRing_Ring (cpoly_cring CR)).

Lemma degree_poly_div : forall (m n : nat) (f g : cpoly CR),
let f1 := (_C_ (nth_coeff n g) [*] f [-] _C_ (nth_coeff (S m) f) [*] ((_X_ [^] ((S m) - n)) [*] g)) in
S m >= n -> degree_le (S m) f -> degree_le n g -> degree_le m f1.
Expand All @@ -36,10 +39,11 @@ Proof.
rewrite -> (Sum_term _ _ _ (S m - n)); [ | omega | omega | intros ].
rewrite -> nth_coeff_nexp_eq.
destruct Hp.
replace (S m - (S m - n)) with n by omega; legacy_rational.
replace (S m - (S m - n)) with n by omega.
unfold cg_minus. ring.
rewrite -> (dg (S m0 - (S m - n))); [ | omega].
rewrite -> df; [ legacy_rational | omega].
rewrite -> nth_coeff_nexp_neq; [ legacy_rational | assumption].
rewrite -> df; [ unfold cg_minus; ring | omega].
rewrite nth_coeff_nexp_neq. ring. assumption.
Qed.

Theorem cpoly_div1 : forall (m n : nat) (f g : cpoly_cring CR),
Expand All @@ -52,7 +56,7 @@ Proof.
generalize (m - n) at 1 as p; intro p; revert m n; induction p; intros.
exists ((Zero : cpoly_cring CR),f).
rewrite <- H.
simpl (nth_coeff (S n) g[^]0); rewrite <- c_one; legacy_rational.
simpl (nth_coeff (S n) g[^]0). rewrite <- c_one. ring.
replace n with m by omega; assumption.
set (f1 := (_C_ (nth_coeff (S n) g) [*] f [-] _C_ (nth_coeff m f) [*] ((_X_ [^] (m - (S n))) [*] g))).
destruct (IHp (m - 1) n) with (f := f1) (g := g); [ omega | | assumption | omega | ].
Expand All @@ -67,7 +71,7 @@ Proof.
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; legacy_rational.
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 [=] Zero).
Expand All @@ -90,14 +94,14 @@ Proof.
cut (a [=] Zero); [ 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.
rewrite -> (nth_coeff_wd _ _ _ Zero); [ simpl; legacy_rational | ].
rewrite -> aeqz; legacy_rational.
rewrite -> (nth_coeff_wd _ _ _ Zero); [ simpl; ring | ].
rewrite -> aeqz; ring.
rewrite -> H3.
rewrite -> (nth_coeff_wd _ _ _ _ H2).
destruct H1 as [d s0].
destruct H0 as [H0 H1].
destruct m; [ rewrite -> (nth_coeff_wd _ _ _ _ (s0 H1)); reflexivity | apply (d m H1); apply le_n ].
apply (IHn (S m) _ (Zero [+X*] b) (c [-] _C_ s [*] b)); [ | | | rewrite <- H2, cpoly_lin, <- c_zero; legacy_rational ].
apply (IHn (S m) _ (Zero [+X*] b) (c [-] _C_ s [*] b)); [ | | | rewrite <- H2, cpoly_lin, <- c_zero; unfold cg_minus; ring ].
unfold degree_le; intros; rewrite <- (coeff_Sm_lin _ _ s).
apply H; apply lt_n_S; apply H3.
split; [ rewrite -> coeff_Sm_lin; destruct H0; apply H0 | unfold degree_le; intros ].
Expand All @@ -113,7 +117,7 @@ Proof.
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 (linear_eq_linear_ _ _ _ _ _ s0) as [H4 H5].
rewrite <- H2, -> H5. legacy_rational.
rewrite <- H2, -> H5. unfold cg_minus. ring.
Qed.

Lemma cpoly_div : forall (f g : cpoly_cring CR) (n : nat), monic n g ->
Expand All @@ -125,10 +129,10 @@ Proof.
exists (f,Zero).
intros; destruct y; simpl (snd (s0, s1)) in *; simpl (fst (s0, s1)) in *.
rename H1 into X. destruct X; destruct d; split; [ | symmetry; apply (s3 H0) ].
rewrite -> s2, (s3 H0), s, <- c_one; legacy_rational.
rewrite -> s2, (s3 H0), s, <- c_one; ring.
simpl (fst (f, Zero : cpoly_cring CR)); simpl (snd (f, Zero : cpoly_cring CR)).
replace (cpoly_zero CR) with (Zero : cpoly_cring CR) by (simpl;reflexivity).
split; [ rewrite -> s, <- c_one; legacy_rational | ].
split; [ rewrite -> s, <- c_one; ring | ].
split; [ | reflexivity ].
unfold degree_le; intros; apply nth_coeff_zero.
destruct (@cpoly_div1 (max (lth_of_poly f) n) n f g); [ | destruct H; assumption | apply le_max_r | ].
Expand All @@ -151,9 +155,9 @@ Proof.
apply (@cpoly_div2 (lth_of_poly (q [-] q1)) (S n) (q [-] q1) g (r1 [-] r)); [ apply poly_degree_lth | split; assumption | | ].
destruct d; destruct d0; split.
intros; apply degree_le_minus; [ apply d0 | apply d ]; assumption.
intro; rewrite -> (s1 H1) ,(s2 H1); legacy_rational.
assert (r1[=]q1[*]g[+]r1[-]q1[*]g); [ legacy_rational | ].
rewrite -> H1, <- s0; legacy_rational.
intro; rewrite -> (s1 H1) ,(s2 H1); unfold cg_minus; ring.
assert (r1[=]q1[*]g[+]r1[-]q1[*]g); [ unfold cg_minus; ring | ].
rewrite -> H1, <- s0; unfold cg_minus; ring.
split; [ assumption | ].
rewrite -> H1 in s0; apply (cg_cancel_lft _ _ _ _ s0).
Qed.
Expand Down
9 changes: 5 additions & 4 deletions algebra/CPolynomials.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2549,7 +2549,7 @@ Proof.
induction p.
intros q.
change (_D_(Zero[*]q)[=]Zero[*]q[+]Zero[*]_D_ q).
stepl (_D_(Zero:RX)). 2:legacy_rational.
stepl (_D_(Zero:RX)). 2: by destruct q.
rewrite -> diff_zero.
ring.
intros q.
Expand Down Expand Up @@ -2627,9 +2627,10 @@ Proof.
apply (cpoly_double_ind0 R).
intros p.
change (cpoly_map_csf(p[+]Zero)[=]cpoly_map_csf p[+]Zero).
stepr (cpoly_map_csf p). 2:legacy_rational.
stepr (cpoly_map_csf p). 2: ring.
apply csf_wd.
legacy_rational. (* ring cannot find the ring structure *)
cut (forall p: cpoly_cring R, csg_op p Zero [=] p). done.
intros. ring.
reflexivity.
intros p q c d H.
split.
Expand Down Expand Up @@ -2689,7 +2690,7 @@ Proof.
change ((cpoly_map_csf (cpoly_mult_cs R q p))[=](cpoly_mult_cs S (cpoly_map_csf q) (cpoly_map_csf p))).
repeat setoid_rewrite <- cpoly_mult_fast_equiv.
change (cpoly_map_csf (q[*]p)[=]cpoly_map_csf q[*]cpoly_map_csf p).
stepr (cpoly_map_csf p[*]cpoly_map_csf q). 2:legacy_rational.
stepr (cpoly_map_csf p[*]cpoly_map_csf q). 2: ring.
rewrite <- H.
apply csf_wd;ring.
Qed.
Expand Down
6 changes: 4 additions & 2 deletions algebra/Cauchy_COF.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -520,6 +520,8 @@ Defined.

End Ring_Structure.

Add Ring R_CRing: (CRing_Ring R_CRing).

Section Field_Structure.

(**
Expand Down Expand Up @@ -626,8 +628,8 @@ Proof.
apply R_integral_domain.
apply R_integral_domain; auto.
apply minus_ap_zero; apply ap_symmetric_unfolded; auto.
stepl (y[*]R_recip y y_[*]x[-]x[*]R_recip x x_[*]y). 2: legacy_rational.
stepr (One[*]x[-]One[*]y). 2:legacy_rational.
stepl (y[*]R_recip y y_[*]x[-]x[*]R_recip x x_[*]y). 2: unfold cg_minus; ring.
stepr (One[*]x[-]One[*]y). 2: unfold cg_minus; ring.
apply cg_minus_wd; apply mult_wdl; apply R_recip_inverse.
Qed.

Expand Down
26 changes: 17 additions & 9 deletions fta/KneserLemma.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -377,15 +377,23 @@ Proof.
apply nexp_resp_pos; apply pos_three.
Qed.

Lemma Kneser_2a : forall (R : CRing) (m n i : nat) (f : nat -> R), 1 <= i ->
Sum m n f [=] f m[+]f i[+] (Sum (S m) (pred i) f[+]Sum (S i) n f).
Proof.
intros.
astepl (f m[+]Sum (S m) n0 f).
astepl (f m[+] (Sum (S m) i f[+]Sum (S i) n0 f)).
astepl (f m[+] (Sum (S m) (pred i) f[+]f i[+]Sum (S i) n0 f)).
rational.
Qed.
Section with_CRing. (* We need a context so we can declare the ring structure. *)

Variable R: CRing.

Add Ring R: (CRing_Ring R).

Lemma Kneser_2a : forall (m n i : nat) (f : nat -> R), 1 <= i ->
Sum m n f [=] f m[+]f i[+] (Sum (S m) (pred i) f[+]Sum (S i) n f).
Proof.
intros.
astepl (f m[+]Sum (S m) n0 f).
astepl (f m[+] (Sum (S m) i f[+]Sum (S i) n0 f)).
astepl (f m[+] (Sum (S m) (pred i) f[+]f i[+]Sum (S i) n0 f)).
ring.
Qed.

End with_CRing.

Lemma Kneser_2b : forall (k : nat) (z : CC), 1 <= k ->
let p_ := fun i => b i[*]z[^]i in
Expand Down
8 changes: 5 additions & 3 deletions reals/OddPolyRootIR.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,8 @@ Section Flip_Poly.

Variable R : CRing.

Add Ring R: (CRing_Ring R).

(* begin hide *)
Let RX := (cpoly R).
(* end hide *)
Expand All @@ -150,7 +152,7 @@ Proof.
change ( [--]c[+]x[*] (cpoly_inv _ (flip q)) ! x [=] [--] (c[+][--]x[*]q ! ( [--]x))) in |- *.
astepl ( [--]c[+]x[*][--] (flip q) ! x).
astepl ( [--]c[+]x[*][--][--]q ! ( [--]x)).
legacy_rational.
ring.
Qed.

Lemma flip_coefficient : forall (p : RX) i,
Expand All @@ -159,11 +161,11 @@ Proof.
intro p. elim p.
simpl in |- *. algebra.
intros c q. intros.
elim i. simpl in |- *. legacy_rational.
elim i. simpl in |- *. ring.
intros. simpl in |- *.
astepl ( [--] (nth_coeff n (flip q))).
astepl ( [--] ( [--] ( [--]One[^]n) [*]nth_coeff n q)).
simpl in |- *. legacy_rational.
simpl in |- *. ring.
Qed.

Hint Resolve flip_coefficient: algebra.
Expand Down

0 comments on commit 4a5d974

Please sign in to comment.