Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Adapt to https://github.com/math-comp/math-comp/pull/1352 #98

Merged
merged 1 commit into from
Mar 3, 2025
Merged

Adapt to https://github.com/math-comp/math-comp/pull/1352 #98

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions theories/abel.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -903,12 +903,12 @@
Proof.
have := p_irr; rewrite /irreducible_poly => -[+ _].
by apply: contraTneq => ->; rewrite size_poly0.
Qed.

Check warning on line 906 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

p_neq0 is declared opaque (Qed) but this is not fully respected

Let ratr_p' : map_poly ratr p %= \prod_(x <- rp') ('X - x%:P).
Proof.
by have := poly_numfield_eqp p_neq0; rewrite (eq_map_poly (fmorph_eq_rat _)).
Qed.

Check warning on line 911 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

ratr_p' is declared opaque (Qed) but this is not fully respected

Let rp'_uniq : uniq rp'.
Proof.
Expand All @@ -918,7 +918,7 @@
rewrite size_poly_eq1; have [//|dN1 /(_ isT)] := boolP (d %= 1).
move=> /eqp_dvdl-> /dvdp_leq; rewrite -size_poly_eq0 polyorder.size_deriv.
by case: (size p) sp_gt1 => [|[|n]]//= _; rewrite ltnn; apply.
Qed.

Check warning on line 921 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

rp'_uniq is declared opaque (Qed) but this is not fully respected

Let d := (size p).-1.
Hypothesis d_prime : prime d.
Expand All @@ -927,13 +927,13 @@
Let rp := [seq x <- rp' | iota x \isn't Num.real]
++ [seq x <- rp' | iota x \is Num.real].

Let rp_perm : perm_eq rp rp'. Proof. by rewrite perm_catC perm_filterC. Qed.

Check warning on line 930 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

rp_perm is declared opaque (Qed) but this is not fully respected
Let rp_uniq : uniq rp. Proof. by rewrite (perm_uniq rp_perm). Qed.

Check warning on line 931 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

rp_uniq is declared opaque (Qed) but this is not fully respected
Let ratr_p : map_poly ratr p %= \prod_(x <- rp) ('X - x%:P).
Proof.
rewrite (eqp_trans ratr_p')// eqp_monic ?monic_prod_XsubC//.
exact/eqP/esym/perm_big.
Qed.

Check warning on line 936 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

ratr_p is declared opaque (Qed) but this is not fully respected

Lemma nth_rp_real i : (iota rp`_i \is Num.real) = (i > 1)%N.
Proof.
Expand All @@ -947,16 +947,16 @@

Let K := <<1 & rp'>>%AS.
Let K_eq : K = <<1 & rp>>%AS :> {vspace _}.
Proof. exact/esym/eq_adjoin/perm_mem. Qed.

Check warning on line 950 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

K_eq is declared opaque (Qed) but this is not fully respected inside

Let K_split_p : splittingFieldFor 1%AS (map_poly ratr p) K.
Proof. by exists rp => //; rewrite ratr_p eqpxx. Qed.

Check warning on line 953 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

K_split_p is declared opaque (Qed) but this is not fully respected

Let p_sep : separable_poly p.
Proof.
rewrite -(separable_map (char0_ratr charL)).
by rewrite (eqp_separable ratr_p) separable_prod_XsubC.
Qed.

Check warning on line 959 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.1.0-coq-8.18) 

p_sep is declared opaque (Qed) but this is not fully respected

Let d_gt0 : (d > 0)%N.
Proof. by rewrite prime_gt0. Qed.
Expand Down Expand Up @@ -1323,11 +1323,11 @@
have p1 : Num.sg pR.[1%:~R] = - 1 by rewrite pRE !pesimp -lock rmorphN1.
have p2 : Num.sg pR.[2%:~R] = 1 by rewrite pRE !pesimp -lock rmorph1.
have simp := (pN2, pN1, p1, p2, mulN1r, mulrN1).
have [||x0 /andP[_ x0N1] rx0] := @ivt_sign _ pR (- 2%:R) (- 1); rewrite ?simp//.

Check warning on line 1326 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19) 

Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
by rewrite -subr_ge0 opprK addKr ler01.
have [||x1 /andP[x10 x11] rx1] := @ivt_sign _ pR (-1) 1; rewrite ?simp//.
by rewrite -subr_ge0 opprK addr_ge0 ?ler01.
(have [||x1 /andP[x10 x11] rx1] := @ivt_sign _ pR (-1) 1; rewrite ?simp) => [|//|].

Check warning on line 1328 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19) 

Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
by rewrite -subr_ge0 opprK addr_ge0 ?ler01. (* add a by above and Remove this line when requiring mathcomp >= 2.4.0 *)
have [||x2 /andP[/= x21 _] rx2] := @ivt_sign _ pR 1 2%:R; rewrite ?simp//.

Check warning on line 1330 in theories/abel.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.2.0-coq-8.19) 

Notation ivt_sign is deprecated since mathcomp-real-closed 1.1.0.
by rewrite -subr_ge0 addrK ler01.
have: sorted <%R [:: x0; x1; x2] by rewrite /= (lt_trans x0N1) ?(lt_trans x11).
rewrite lt_sorted_uniq_le => /andP[uniqx012 _].
Expand Down
Loading