Skip to content
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

Jump to bottom

Remove universe constraints #87

Merged
merged 1 commit into from
Feb 2, 2024
Merged

Remove universe constraints #87

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
16 changes: 12 additions & 4 deletions refinements/binnat.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,8 +2,8 @@
(c) Copyright INRIA and University of Gothenburg, see LICENSE *)
Require Import ZArith Lia.

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp.

Check warning on line 5 in refinements/binnat.v

View workflow job for this annotation

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

Hiding binding of key N to N_scope

Check warning on line 5 in refinements/binnat.v

View workflow job for this annotation

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

Hiding binding of key N to N_scope
From mathcomp Require Import path choice fintype tuple finset ssralg ssrnum bigop ssrint.

Check warning on line 6 in refinements/binnat.v

View workflow job for this annotation

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

Hiding binding of key Z to Z_scope

Check warning on line 6 in refinements/binnat.v

View workflow job for this annotation

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

Hiding binding of key Z to Z_scope

From CoqEAL Require Import hrel param refinements pos.

Expand Down Expand Up @@ -292,16 +292,24 @@
by rewrite divn_small ?addn0 // ?to_natE.
Qed.

(* chunk of proof extracted from below to avoid tc
generating spurious universe constraints *)
Lemma Rnat_div_subproof
x x' (rx : refines Rnat x x') y y' (ry : refines Rnat y y') :
refines (prod_R Rnat Rnat) (edivn x y) (N.div_eucl x' y').
Proof. tc. Qed.

#[export] Instance Rnat_div : refines (Rnat ==> Rnat ==> Rnat) divn div_op.
Proof.
by apply refines_abstr2; rewrite /divn /div_op /div_N /N.div=> x x' rx y y' ry; tc.
apply refines_abstr2; rewrite /divn /div_op /div_N /N.div=> x x' rx y y' ry.
exact: (refines_apply (refines_fst_R _ _) (Rnat_div_subproof _ _)).
Qed.

#[export] Instance Rnat_mod : refines (Rnat ==> Rnat ==> Rnat) modn mod_op.
Proof.
apply refines_abstr2; rewrite /mod_op /mod_N /N.modulo=> x x' rx y y' ry.
rewrite modn_def.
exact: refines_apply.
apply refines_abstr2; rewrite /mod_op /mod_N /N.modulo=> x x' rx y y' ry.
rewrite modn_def.
exact: (refines_apply (refines_snd_R _ _) (Rnat_div_subproof _ _)).
Qed.

#[export] Instance Rnat_exp : refines (Rnat ==> Rnat ==> Rnat) expn exp_op.
Expand Down
90 changes: 47 additions & 43 deletions refinements/multipoly.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@
Local Open Scope ring_scope.

(** BEGIN FIXME this is redundant with PR CoqEAL/CoqEAL#3 *)
Arguments refines A%type B%type R%rel _ _. (* Fix a scope issue with refines *)

Check warning on line 32 in refinements/multipoly.v

View workflow job for this annotation

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

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 32 in refinements/multipoly.v

View workflow job for this annotation

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

The '%' scope delimiter in 'Arguments' commands is deprecated, use

#[export] Hint Resolve list_R_nil_R : core.
(** END FIXME this is redundant with PR CoqEAL/CoqEAL#3 *)
Expand Down Expand Up @@ -1850,11 +1850,13 @@
move=> h' t' i i' ref_i Hyp.
eapply inv_list_R; last exact: Hyp; try done.
move=> H a c sa sc Heq Heqs [H1 H2] [H3 H4].
eapply IHt.
- refines_apply1; first refines_apply1; first refines_apply1.
{ rewrite !refinesE -H1 -H3; by case: Heq. }
{ rewrite -H1 -H3; by refines_apply1. }
- rewrite -H2 -H4; exact: Heqs.
apply: IHt; last first.
rewrite -H2 -H4; exact: Heqs.
rewrite -H1 -H3; case: Heq => [h1 _ <- h2 h2' rh2] /=.
apply: refines_apply ref_i.
apply: refines_apply.
apply: refines_apply.
by rewrite refinesE.
Qed.

#[export] Instance refine_filter A' B (rAB : A' -> B -> Type) :
Expand All @@ -1878,44 +1880,46 @@
list_R (prod_R Rseqmultinom rAC))
(@list_of_mpoly A n) list_of_mpoly_eff.
Proof.
eapply refines_trans; [|by apply refine_list_of_mpoly_eff|].
{ apply (composable_imply _ _ (R2 := list_R (prod_R eq rAC))).
rewrite composableE=> l.
elim: l => [|h t IH].
{ case=> [|h' t']; [by move=>_; apply list_R_nil_R|].
move=> H; inversion H as [x X]; inversion X as [X0 X1].
by inversion X0 as [H' Hx|H' Hx]; rewrite -Hx in X1; inversion X1. }
case=> [|h' t'].
{ move=> H; inversion H as [x X]; inversion X as [X0 X1].
by inversion X1 as [Hx H'|Hx H']; rewrite -Hx in X0; inversion X0. }
specialize (IH t'); move=> H.
case: H => l'' X.
case: X => X0 X1.
move: X0 X1; case: l'' => [|h'' t''] X0 X1; [by inversion X0|].
inversion X0 as [|X X' ref_X Y Y' ref_Y].
inversion X1 as [|Z Z' ref_Z T T' ref_T].
inversion ref_X as [x x' ref_x x0 x0' ref_x0'].
inversion ref_Z as [u u' ref_u v v' ref_v].
apply list_R_cons_R.
{ apply/prod_RI; split; simpl.
suff->: u' = x' by [].
rewrite -[u']/(u',v').1 H10 -[x']/(x', x0').1 H8.
symmetry.
by eapply refinesP; refines_apply1.
suff->: x0 = v by [].
rewrite -[x0]/(x, x0).2 H7.
rewrite -[v]/(u, v).2 H9.
by eapply refinesP; refines_apply1. }
by apply IH; exists t''; split. }
rewrite /list_of_mpoly_eff.
apply refines_abstr => p p' rp.
eapply refines_apply;
[|eapply refines_apply; [apply refine_M_hrel_elements|exact rp]].
eapply refines_apply; [by apply refine_filter|].
eapply refines_abstr => mc mc' rmc.
rewrite refinesE; f_equal.
rewrite refinesE in rmc; inversion rmc as [a a' ref_a b b' ref_b].
apply refinesP; tc.
have: refines (M_hrel ==> list_R (prod_R eq rAC))
(@list_of_mpoly_eff _ _ (@eq_of_instance_0 A)) list_of_mpoly_eff.
{ rewrite /list_of_mpoly_eff.
apply refines_abstr => p p' rp.
eapply refines_apply;
[|eapply refines_apply; [apply refine_M_hrel_elements|exact rp]].
eapply refines_apply; [by apply refine_filter|].
eapply refines_abstr => mc mc' rmc.
rewrite refinesE; f_equal.
rewrite refinesE in rmc; inversion rmc as [a a' ref_a b b' ref_b].
apply refinesP; tc. }
apply: refines_trans (refine_list_of_mpoly_eff _).
apply: (composable_imply _ _ (R2 := list_R (prod_R eq rAC))).
rewrite composableE => l.
elim: l => [|h t IH].
{ case=> [|h' t']; [by move=>_; apply list_R_nil_R|].
move=> H; inversion H as [x X]; inversion X as [X0 X1].
by inversion X0 as [H' Hx|H' Hx]; rewrite -Hx in X1; inversion X1. }
case=> [|h' t'].
{ move=> H; inversion H as [x X]; inversion X as [X0 X1].
by inversion X1 as [Hx H'|Hx H']; rewrite -Hx in X0; inversion X0. }
specialize (IH t'); move=> H.
case: H => l'' X.
case: X => X0 X1.
move: X0 X1; case: l'' => [|h'' t''] X0 X1; [by inversion X0|].
inversion X0 as [|X X' ref_X Y Y' ref_Y].
inversion X1 as [|Z Z' ref_Z T T' ref_T].
inversion ref_X as [x x' ref_x x0 x0' ref_x0'].
inversion ref_Z as [u u' ref_u v v' ref_v].
apply: list_R_cons_R; last first.
by apply IH; exists t''; split.
apply/prod_RI; split; simpl.
suff->: u' = x' by [].
rewrite -[u']/(u',v').1 H10 -[x']/(x', x0').1 H8.
symmetry.
by rewrite -H9 -H10 /=.
suff->: x0 = v by [].
rewrite -[x0]/(x, x0).2 H7.
rewrite -[v]/(u, v).2 H9.
by rewrite -H7 -H8 /=.
Qed.

#[export] Instance ReffmpolyC_mp0_eff (n : nat) :
Expand Down
31 changes: 14 additions & 17 deletions refinements/rational.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,35 +206,32 @@ Qed.

Instance Rrat_eq : refines (Rrat ==> Rrat ==> bool_R) eqtype.eq_op eq_op.
Proof.
apply refines_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
have -> : (x == y) = ((na, pos_of da_gt0) == (nb, pos_of db_gt0))%C.
rewrite /eq_op /eqQ /cast /cast_pos_int /pos_to_int /=; simpC.
rewrite [x]RratE [y]RratE /= GRing.eqr_div; last 2 first.
- by rewrite gt_eqF // ltr0z.
- by rewrite gt_eqF // ltr0z.
by rewrite -!rmorphM /= eqr_int !natz.
apply: refines_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
rewrite /eq_op /eqQ /cast /cast_pos_int /pos_to_int /=; simpC.
rewrite [x]RratE [y]RratE /= GRing.eqr_div; last 2 first.
- by rewrite gt_eqF // ltr0z.
- by rewrite gt_eqF // ltr0z.
rewrite -!rmorphM /= eqr_int !natz.
rewrite refinesE; exact: bool_Rxx.
Qed.

Instance Rrat_leq : refines (Rrat ==> Rrat ==> bool_R) Num.le leq_op.
Proof.
apply refines_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
have -> : (x <= y)%R = ((na, pos_of da_gt0) <= (nb, pos_of db_gt0))%C.
rewrite /leq_op /leqQ /cast /cast_pos_int /pos_to_int /=; simpC.
rewrite [x]RratE [y]RratE /= !natz.
rewrite ler_pdivrMr ?ltr0z // mulrAC ler_pdivlMr ?ltr0z //.
by rewrite -!rmorphM /= ler_int.
rewrite /leq_op /leqQ /cast /cast_pos_int /pos_to_int /=; simpC.
rewrite [x]RratE [y]RratE /= !natz.
rewrite ler_pdivrMr ?ltr0z // mulrAC ler_pdivlMr ?ltr0z //.
rewrite -!rmorphM /= ler_int.
rewrite refinesE; exact: bool_Rxx.
Qed.

Instance Rrat_lt : refines (Rrat ==> Rrat ==> bool_R) Num.lt lt_op.
Proof.
apply refines_abstr2 => x [na [da da_gt0]] rx y [nb [db db_gt0]] ry.
have -> : (x < y) = ((na, pos_of da_gt0) < (nb, pos_of db_gt0))%C.
rewrite /leq_op /leqQ /cast /cast_pos_int /pos_to_int /=.
rewrite [x]RratE [y]RratE /= /lt_op /ltQ /cast /= !natz.
rewrite ltr_pdivrMr ?ltr0z // mulrAC ltr_pdivlMr ?ltr0z //.
by rewrite -!rmorphM /= ltr_int.
rewrite /leq_op /leqQ /cast /cast_pos_int /pos_to_int /=.
rewrite [x]RratE [y]RratE /= /lt_op /ltQ /cast /= !natz.
rewrite ltr_pdivrMr ?ltr0z // mulrAC ltr_pdivlMr ?ltr0z //.
rewrite -!rmorphM /= ltr_int.
rewrite refinesE; exact: bool_Rxx.
Qed.

Expand Down
13 changes: 5 additions & 8 deletions refinements/seqpoly.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -568,10 +568,12 @@ Proof. rewrite -['X]expr1; exact: RseqpolyC_scaleXn. Qed.
refines (rN ==> RseqpolyC ==> prod_R RseqpolyC RseqpolyC)
(splitp (R:=R)) split_op.
Proof.
eapply refines_trans; tc.
have: refines (rN ==> list_R rAC ==> prod_R (list_R rAC) (list_R rAC))
split_op split_op.
rewrite refinesE; do ?move=> ?*.
eapply (split_seqpoly_R (N_R:=rN))=> // *.
exact: refinesP.
exact: refines_trans Rseqpoly_split.
Qed.

#[export] Instance RseqpolyC_splitn n rn p sp :
Expand All @@ -586,13 +588,8 @@ Definition eq_prod_seqpoly (x y : (seqpoly C * seqpoly C)) :=
refines (prod_R RseqpolyC RseqpolyC ==> prod_R RseqpolyC RseqpolyC ==> bool_R)
eqtype.eq_op eq_prod_seqpoly.
Proof.
rewrite refinesE=> x x' hx y y' hy.
rewrite /eqtype.eq_op /eq_prod_seqpoly /=.
have -> : (x.1 == y.1) = (x'.1 == y'.1)%C.
apply: refines_eq.
have -> : (x.2 == y.2) = (x'.2 == y'.2)%C.
apply: refines_eq.
exact: bool_Rxx.
rewrite refinesE => _ _ [x1 x'1 hx1 x2 x'2 hx2] _ _ [y1 y'1 hy1 y2 y'2 hy2].
by apply: andb_R => /=; apply: refinesP.
Qed.

#[export] Instance RseqpolyC_lead_coef :
Expand Down
Loading