Skip to content

Adapt to https://github.com/rocq-prover/rocq/pull/20707 #101

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Jun 27, 2025
Merged

Adapt to https://github.com/rocq-prover/rocq/pull/20707 #101

Show file tree
Hide file tree
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 @@ -1226,7 +1226,7 @@
rewrite separable_poly.unlock.
apply/coprimepP => q /(irredp_XsubCP irreducible_example) [//| eqq].
have size_deriv_example : size poly_example^`() = 5%N.
rewrite !derivCE addr0 alg_polyC -scaler_nat addr0.
rewrite !derivCE ?mul0rn ?addr0 alg_polyC -scaler_nat.
by rewrite size_addl ?size_scale ?size_opp ?size_polyXn ?size_polyC.
rewrite gtNdvdp -?size_poly_eq0 ?size_deriv_example//.
by rewrite (eqp_size eqq) ?size_poly_example.
Expand Down Expand Up @@ -1263,7 +1263,7 @@
Qed.

Lemma deriv_poly_example : poly_example^`() = 5%:R *: 'X^4 - 4%:R%:P.
Proof. by rewrite /poly_example !derivE addr0 alg_polyC scaler_nat ?addr0. Qed.
Proof. by rewrite /poly_example !derivE ?mul0rn?addr0 alg_polyC scaler_nat. Qed.

Lemma deriv_poly_example_neq0 : poly_example^`() != 0.
Proof.
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//.

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.
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
2 changes: 1 addition & 1 deletion theories/xmathcomp/map_gal.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_fingroup all_algebra.

Check warning on line 2 in theories/xmathcomp/map_gal.v

View workflow job for this annotation

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

Notations "\pi ( _ )" defined at level 2 and "\pi"

Check warning on line 2 in theories/xmathcomp/map_gal.v

View workflow job for this annotation

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

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
From mathcomp Require Import all_solvable all_field.
From Abel Require Import various char0.

Expand Down Expand Up @@ -556,7 +556,7 @@
Lemma gal_kAEndf (K E : {subfield L}) : (K <= E)%VS ->
(gal E @* kAEndf K)%g = (gal E @* kAEnd K E)%g :> {set _}.
Proof.
move=> KE; rewrite kAEnd_split morphimIG ?ker_gal ?kAEndSl// (setIidPr _)//=.
move=> KE; rewrite (kAEnd_split K) morphimIG ?ker_gal ?kAEndSl ?(setIidPr _)//=.
by rewrite (subset_trans (morphim_sub _ _))//= morphimS// subfield_closed.
Qed.

Expand Down
2 changes: 1 addition & 1 deletion theories/xmathcomp/various.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_fingroup all_algebra all_solvable.

Check warning on line 2 in theories/xmathcomp/various.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.20) 

Library File mathcomp.ssreflect.all_ssreflect is deprecated

Check warning on line 2 in theories/xmathcomp/various.v

View workflow job for this annotation

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

Notations "\pi ( _ )" defined at level 2 and "\pi"

Check warning on line 2 in theories/xmathcomp/various.v

View workflow job for this annotation

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

Notations "[ seq _ | _ <- _ ]" defined at level 0 with arguments
From mathcomp Require Import all_field.

Set Implicit Arguments.
Expand Down Expand Up @@ -161,7 +161,7 @@
Lemma extnprod_mulgA : associative extnprod_mulg.
Proof. by move=> x y z; apply/ffunP => i; rewrite !ffunE mulgA. Qed.

HB.instance Definition _ := isMulGroup.Build gTn

Check warning on line 164 in theories/xmathcomp/various.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.20) 

HB: no new instance is generated
extnprod_mulgA extnprod_mul1g extnprod_mulVg.

End ExternalNDirProd.
Expand Down Expand Up @@ -1100,7 +1100,7 @@
apply/permP => i; rewrite permE/= /gsf/=; apply: (canLR fK).
by rewrite !permE/= -f0 -[y]gK !(can_eq fK) -!fun_if.
have phic : phi c = perm (addrI 1%R).
apply/permP => i; rewrite permE /gsf/=; apply: (canLR fK).
apply/permP => i; rewrite [LHS]permE /gsf/=; apply: (canLR fK).
by rewrite !permE /f /Zpm -permM addrC expgDzmod.
rewrite -(injmSK phi_inj)//= morphim_gen/= ?subsetT//= -/phi.
rewrite phiT /morphim !setTI/= -/phi imsetU1 imset_set1/= phixy phic.
Expand Down
Loading