Skip to content

Commit

Permalink
Merge pull request #87 from proux01/sigT_hrel
Browse files Browse the repository at this point in the history
Remove universe constraints
  • Loading branch information
proux01 authored Feb 2, 2024
2 parents 72cbc4f + 9fab8fc commit fb2ecaf
Show file tree
Hide file tree
Showing 4 changed files with 78 additions and 72 deletions.
16 changes: 12 additions & 4 deletions refinements/binnat.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
90 changes: 47 additions & 43 deletions refinements/multipoly.v
Original file line number Diff line number Diff line change
Expand Up @@ -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) :
Expand All @@ -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) :
Expand Down
31 changes: 14 additions & 17 deletions refinements/rational.v
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
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

0 comments on commit fb2ecaf

Please sign in to comment.