Remove universe constraints

coq-community · Jan 24, 2024 · 9fab8fc · 9fab8fc
1 parent aa50f63
commit 9fab8fc
Show file tree

Hide file tree

Showing 4 changed files with 78 additions and 72 deletions.
diff --git a/refinements/binnat.v b/refinements/binnat.v
@@ -292,16 +292,24 @@ Proof.
   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.

diff --git a/refinements/multipoly.v b/refinements/multipoly.v
@@ -1850,11 +1850,13 @@ elim=> [|h t IHt]; case=> //=.
 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) :
@@ -1878,44 +1880,46 @@ Qed.
     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) :

diff --git a/refinements/rational.v b/refinements/rational.v
@@ -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.
 

diff --git a/refinements/seqpoly.v b/refinements/seqpoly.v
@@ -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 :
@@ -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 :