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

Import order in multipoly.v #93

Merged
merged 1 commit into from
Aug 6, 2024
Merged

Import order in multipoly.v #93

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
18 changes: 9 additions & 9 deletions refinements/multipoly.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(** Authors: Erik Martin-Dorel and Pierre Roux, 2016-2017 *)
Require Import ZArith NArith FMaps FMapAVL.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
From mathcomp Require Import choice finfun tuple fintype ssralg bigop.
From mathcomp Require Import choice finfun tuple fintype order ssralg bigop.
From CoqEAL Require Import hrel.
From CoqEAL Require Import refinements.
From CoqEAL Require Import param binord binnat.
Expand Down 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-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 @@ -653,20 +653,20 @@
case: (boolP (m1 == m2)) => /= [E|].
{ suff: mnmc_eq_seq m1' m2'.
{ move=> E'; symmetry.
move: E => /eqP ->; rewrite order.Order.POrderTheory.ltxx.
move: E => /eqP ->; rewrite Order.POrderTheory.ltxx.
apply negbTE; apply /negP => K.
by apply (E.lt_not_eq K). }
by apply /mnmc_eq_seqP; rewrite -(Rseqmultinom_eq rm1 rm2). }
move=> nE.
rewrite /mnmc_lt_seq /order.Order.lt /=.
rewrite /mnmc_lt_seq /Order.lt /=.
rewrite mpoly.ltmc_def eq_sym nE /=.
have rmdeg := refine_mdeg n; rewrite refinesE in rmdeg.
rewrite /eq_op /eq_N /lt_op /lt_N.
rewrite /mnmc_le.
rewrite order.Order.SeqLexiOrder.Exports.lexi_cons.
rewrite Order.SeqLexiOrder.Exports.lexi_cons.
rewrite (rmdeg _ _ (refinesP rm1)) (rmdeg _ _ (refinesP rm2)) => {rmdeg}.
rewrite /order.Order.le /=.
rewrite (_ : order.Order.SeqLexiOrder.le _ _ = mnmc_lt_seq_aux m1' m2').
rewrite /Order.le /=.
rewrite (_ : Order.SeqLexiOrder.le _ _ = mnmc_lt_seq_aux m1' m2').
{ rewrite leq_eqVlt.
apply/idP/idP.
{ case eqP => /= He.
Expand Down Expand Up @@ -713,12 +713,12 @@
{ by move: (@refine_size _ _ _ rm2)=> /= /eqP; rewrite eqSS=> /eqP. }
move=> i; move: (refine_nth (fintype.lift ord0 i) rm2).
by rewrite /= =>->; rewrite !multinomE !(tnth_nth 0%N) /=. }
rewrite /order.Order.lt /= /eq_op /eq_N /lt_op /lt_N.
rewrite /Order.lt /= /eq_op /eq_N /lt_op /lt_N.
move: (@refine_nth _ _ _ ord0 rm1) => /=.
rewrite multinomE /spec_N (tnth_nth 0%N) /= => <-.
move: (@refine_nth _ _ _ ord0 rm2) => /=.
rewrite multinomE /spec_N (tnth_nth 0%N) /= => <-.
rewrite /order.Order.le /=.
rewrite /Order.le /=.
apply/idP/idP.
{ rewrite leq_eqVlt.
move=> /andP [/orP [Heq12|Hlt12] /implyP Himpl].
Expand Down Expand Up @@ -1003,7 +1003,7 @@
by rewrite -/(path.sorted _ (h' :: t')) -Ht'; apply IH. }
case_eq l=> [//|h t Hl] /= /(path.pathP (@mnm0_seq n, 0)) H.
apply/(path.pathP 0%MM)=> i; rewrite size_map=> Hi.
rewrite /mnmc_le -leEmnm order.Order.POrderTheory.le_eqVlt; apply/orP; right.
rewrite /mnmc_le -leEmnm Order.POrderTheory.le_eqVlt; apply/orP; right.
rewrite (nth_map (@mnm0_seq n, 0)) //; move/allP in Hs.
move: (H _ Hi); rewrite /lef/is_true=><-; apply refinesP.
eapply refines_apply; [eapply refines_apply; [by apply refine_mnmc_lt|]|].
Expand Down
Loading