Library Algebra.Monoid.Monomial_order
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Support for monomial orders.
Monomial orders are homogeneous binary relations on finite families of an
Abelian monoid that are strict or nonstrict total orders, and are compatible
with the operation of the monoid.
Let G : AbelianMonoid.
Let R : G → G → Prop be an homogeneous binary relation on G.
Let Rn : 'G^n → 'G^n → Prop be an homogeneous binary relation on 'G^n.
[Cox_etal]
David A. Cox, John Little, Donal O'Shea,
Ideals, Varieties, and Algorithms,
fourth edition, Springer, 2015.
[MO] https://en.wikipedia.org/wiki/Monomial_order.
This module may be used through the import of Algebra.Monoid.Monoid,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Elementary monomial properties
- br_plus_compat_l R means that any relation R x1 x2 is kept when "adding on the left" the same value to both arguments.
- br_plus_compat_r R means that any relation R x1 x2 is kept when
"adding on the right" the same value to both arguments.
- br_plus_reg_l R means that any relation R (x + x1) (x + x2) is kept when removing both "x +", ie when "subtracting on the left".
- br_plus_reg_r R means that any relation R (x1 + x) (x2 + x) is kept
when removing both "+ x", ie when "subtracting on the right".
- zero_is_left R means that 0 is comparable on the left to all elements.
- zero_is_right R means that 0 is comparable on the right to all elements.
Compound monomial properties
- monomial_order R means that R is irreflexive, asymmetric, transitive, connected and compatible with plus on the right, ie it is a strict total order compatible with plus.
- monomial_order_zl R means that R is a monomial order for which 0 is comparable on the left to all elements.
- monomial_order_zr R means that R is a monomial order for which 0 is comparable on the right to all elements.
- monomial_order_ns R means that R is reflexive, antisymmetric, transitive, strongly connected and compatible with plus on the right, ie it is a total order compatible with plus.
Operator
- graded R Rn compares the sum of the arguments with R, and in case of
equality, use Rn.
- grlex R is graded R (lex R).
- grcolex R is graded R (colex R).
- grsymlex R is graded R (symlex R).
- grevlex R is graded R (revlex R).
Bibliography
Usage
From Requisite Require Import stdlib ssr_wMC.
From Coquelicot Require Import Hierarchy.
Close Scope R_scope.
From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid_compl Monoid_sum.
Local Open Scope Monoid_scope.
Section Monomial_order_Def.
Context {G : AbelianMonoid}.
Definition plus_is_reg_l : Prop :=
∀ (x x1 x2 : G), x + x1 = x + x2 → x1 = x2.
Definition plus_is_reg_r : Prop :=
∀ (x x1 x2 : G), x1 + x = x2 + x → x1 = x2.
Variable R : G → G → Prop.
Elementary monomial properties.
"br" stands for "binary relation".
Definition br_plus_compat_l : Prop :=
∀ x x1 x2, R x1 x2 → R (x + x1) (x + x2).
Definition br_plus_compat_r : Prop :=
∀ x x1 x2, R x1 x2 → R (x1 + x) (x2 + x).
∀ x x1 x2, R x1 x2 → R (x + x1) (x + x2).
Definition br_plus_compat_r : Prop :=
∀ x x1 x2, R x1 x2 → R (x1 + x) (x2 + x).
"br" stands for "binary relation".
Definition br_plus_reg_l : Prop :=
∀ x x1 x2, R (x + x1) (x + x2) → R x1 x2.
Definition br_plus_reg_r : Prop :=
∀ x x1 x2, R (x1 + x) (x2 + x) → R x1 x2.
Definition zero_is_left : Prop := ∀ x, x ≠ 0 → R 0 x.
Definition zero_is_right : Prop := ∀ x, x ≠ 0 → R x 0.
∀ x x1 x2, R (x + x1) (x + x2) → R x1 x2.
Definition br_plus_reg_r : Prop :=
∀ x x1 x2, R (x1 + x) (x2 + x) → R x1 x2.
Definition zero_is_left : Prop := ∀ x, x ≠ 0 → R 0 x.
Definition zero_is_right : Prop := ∀ x, x ≠ 0 → R x 0.
Compound monomial properties.
"br" stands for "binary relation".
Definition br_monoid_compat_zl : Prop :=
br_plus_compat_r ∧ zero_is_left.
Definition br_monoid_compat_zr : Prop :=
br_plus_compat_r ∧ zero_is_right.
Definition monomial_order : Prop := strict_total_order R ∧ br_plus_compat_r.
Definition monomial_order_zl : Prop :=
strict_total_order R ∧ br_monoid_compat_zl.
Definition monomial_order_zr : Prop :=
strict_total_order R ∧ br_monoid_compat_zr.
br_plus_compat_r ∧ zero_is_left.
Definition br_monoid_compat_zr : Prop :=
br_plus_compat_r ∧ zero_is_right.
Definition monomial_order : Prop := strict_total_order R ∧ br_plus_compat_r.
Definition monomial_order_zl : Prop :=
strict_total_order R ∧ br_monoid_compat_zl.
Definition monomial_order_zr : Prop :=
strict_total_order R ∧ br_monoid_compat_zr.
"ns" stands for "nonstrict".
Definition monomial_order_ns : Prop := total_order R ∧ br_plus_compat_r.
End Monomial_order_Def.
Section Monomial_order_Facts1.
Context {G : AbelianMonoid}.
End Monomial_order_Def.
Section Monomial_order_Facts1.
Context {G : AbelianMonoid}.
Lemma plus_is_reg_equiv : @plus_is_reg_l G ↔ @plus_is_reg_r G.
Proof.
split; intros H x x1 x2;
[rewrite !(plus_comm _ x) | rewrite !(plus_comm x)]; apply H.
Qed.
About the br_plus_compat_l / br_plus_compat_r /
br_plus_reg_l / br_plus_reg_r elementary properties.
Lemma br_plus_compat_equiv :
∀ {R : G → G → Prop}, br_plus_compat_l R ↔ br_plus_compat_r R.
Proof.
intro; split; intros H x x1 x2;
[rewrite !(plus_comm _ x) | rewrite !(plus_comm x)]; apply H.
Qed.
Lemma br_plus_reg_equiv :
∀ {R : G → G → Prop}, br_plus_reg_l R ↔ br_plus_reg_r R.
Proof.
intro; split; intros H x x1 x2;
[rewrite -!(plus_comm x) | rewrite !(plus_comm x)]; apply H.
Qed.
Lemma br_plus_compat_reg_r :
∀ {R : G → G → Prop},
eq_dec G → irreflexive R → asymmetric R → connected R →
br_plus_compat_r R → br_plus_reg_r R.
Proof.
intros R HG H1 H2 H3 H4 x x1 x2 H5; destruct (HG x1 x2) as [H6 | H6].
exfalso; subst; apply (H1 _ H5).
destruct (H3 _ _ H6) as [H7 | H7]; [easy | exfalso].
apply (H2 (x1 + x) (x2 + x)); [easy | apply (H4 _ _ _ H7)].
Qed.
Lemma br_plus_compat_reg_l :
∀ {R : G → G → Prop},
eq_dec G → irreflexive R → asymmetric R → connected R →
br_plus_compat_l R → br_plus_reg_l R.
Proof.
intros R HG; rewrite br_plus_compat_equiv br_plus_reg_equiv; move: HG.
apply br_plus_compat_reg_r.
Qed.
Lemma br_plus_compat_is_reg_r :
∀ {R : G → G → Prop},
irreflexive R → connected R → br_plus_compat_r R → @plus_is_reg_r G.
Proof.
move=>> H1 /conn_equiv_contra H2 H3 x x1 x2 H4; apply H2; intros H5;
apply (H1 (x1 + x)); [rewrite {2}H4 | rewrite {1}H4]; apply H3; easy.
Qed.
Lemma br_plus_compat_is_reg_l :
∀ {R : G → G → Prop},
irreflexive R → connected R → br_plus_compat_l R → @plus_is_reg_l G.
Proof.
intro; rewrite br_plus_compat_equiv plus_is_reg_equiv.
apply br_plus_compat_is_reg_r.
Qed.
About the monomial_order / monomial_order_ns compound properties.
Lemma monomial_order_sto :
∀ {R : G → G → Prop}, monomial_order R → strict_total_order R.
Proof. intros R [H _]; easy. Qed.
Lemma monomial_order_irrefl :
∀ {R : G → G → Prop}, monomial_order R → irreflexive R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_asym :
∀ {R : G → G → Prop}, monomial_order R → asymmetric R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_trans :
∀ {R : G → G → Prop}, monomial_order R → transitive R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_conn :
∀ {R : G → G → Prop}, monomial_order R → connected R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_br_plus_compat_r :
∀ {R : G → G → Prop}, monomial_order R → br_plus_compat_r R.
Proof. intros R [_ H]; easy. Qed.
Lemma monomial_order_br_plus_compat_l :
∀ {R : G → G → Prop}, monomial_order R → br_plus_compat_l R.
Proof.
intro; rewrite br_plus_compat_equiv; apply monomial_order_br_plus_compat_r.
Qed.
Lemma monomial_order_br_plus_reg_r :
∀ {R : G → G → Prop}, eq_dec G → monomial_order R → br_plus_reg_r R.
Proof.
intros R HG H; apply (br_plus_compat_reg_r HG); move: H.
apply monomial_order_irrefl.
apply monomial_order_asym.
apply monomial_order_conn.
apply monomial_order_br_plus_compat_r.
Qed.
Lemma monomial_order_br_plus_reg_l :
∀ {R : G → G → Prop}, eq_dec G → monomial_order R → br_plus_reg_l R.
Proof.
intros R H; rewrite br_plus_reg_equiv; apply (monomial_order_br_plus_reg_r H).
Qed.
Lemma monomial_order_plus_is_reg_r :
∀ {R : G → G → Prop}, monomial_order R → @plus_is_reg_r G.
Proof.
intros R H; apply (@br_plus_compat_is_reg_r R); move: H.
apply monomial_order_irrefl.
apply monomial_order_conn.
apply monomial_order_br_plus_compat_r.
Qed.
Lemma monomial_order_plus_is_reg_l :
∀ {R : G → G → Prop}, monomial_order R → @plus_is_reg_l G.
Proof.
intro; rewrite plus_is_reg_equiv; apply monomial_order_plus_is_reg_r.
Qed.
Lemma monomial_order_ns_to :
∀ {R : G → G → Prop}, monomial_order_ns R → total_order R.
Proof. intros R [H _]; easy. Qed.
Lemma monomial_order_ns_refl :
∀ {R : G → G → Prop}, monomial_order_ns R → reflexive R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_ns_antisym :
∀ {R : G → G → Prop}, monomial_order_ns R → antisymmetric R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_ns_trans :
∀ {R : G → G → Prop}, monomial_order_ns R → transitive R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_ns_str_conn :
∀ {R : G → G → Prop}, monomial_order_ns R → strongly_connected R.
Proof. intros R [H _]; apply H. Qed.
Lemma monomial_order_ns_br_plus_compat_r :
∀ {R : G → G → Prop}, monomial_order_ns R → br_plus_compat_r R.
Proof. intros R [_ H]; easy. Qed.
Lemma monomial_order_ns_br_plus_compat_l :
∀ {R : G → G → Prop}, monomial_order_ns R → br_plus_compat_l R.
Proof.
intro; rewrite br_plus_compat_equiv; apply monomial_order_ns_br_plus_compat_r.
Qed.
Nonstrict monomial orders are reflexive, thus they cannot satisfy
regularity properties br_plus_reg_l / br_plus_reg_r since those need
irreflexivity, which is incompatible with reflexivity.
In the same way, nonstrict monomial orders do not imply regularity of plus
(ie plus_is_reg_l / plus_is_reg_r hold in the ambient abelian monoid).
Compatibility results of monomial properties with operators.
With the converse operator.
Lemma br_plus_compat_l_conv :
∀ {R : G → G → Prop},
br_plus_compat_l R → br_plus_compat_l (converse R).
Proof. intros R H x x1 x2; apply (H x x2 x1). Qed.
Lemma br_plus_compat_l_conv_equiv :
∀ {R : G → G → Prop},
br_plus_compat_l (converse R) ↔ br_plus_compat_l R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply br_plus_compat_l_conv.
Qed.
Lemma br_plus_compat_r_conv :
∀ {R : G → G → Prop},
br_plus_compat_r R → br_plus_compat_r (converse R).
Proof. intros R H x x1 x2; apply (H x x2 x1). Qed.
Lemma br_plus_compat_r_conv_equiv :
∀ {R : G → G → Prop},
br_plus_compat_r (converse R) ↔ br_plus_compat_r R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply br_plus_compat_r_conv.
Qed.
Lemma br_plus_reg_l_conv :
∀ {R : G → G → Prop}, br_plus_reg_l R → br_plus_reg_l (converse R).
Proof. intros R H x x1 x2; apply (H x x2 x1). Qed.
Lemma br_plus_reg_l_conv_equiv :
∀ {R : G → G → Prop}, br_plus_reg_l (converse R) ↔ br_plus_reg_l R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply br_plus_reg_l_conv.
Qed.
Lemma br_plus_reg_r_conv :
∀ {R : G → G → Prop}, br_plus_reg_r R → br_plus_reg_r (converse R).
Proof. intros R H x x1 x2; apply (H x x2 x1). Qed.
Lemma br_plus_reg_r_conv_equiv :
∀ {R : G → G → Prop}, br_plus_reg_r (converse R) ↔ br_plus_reg_r R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply br_plus_reg_r_conv.
Qed.
Lemma zero_is_left_conv :
∀ {R : G → G → Prop}, zero_is_right R → zero_is_left (converse R).
Proof. intros R H x; apply H. Qed.
Lemma zero_is_right_conv :
∀ {R : G → G → Prop}, zero_is_left R → zero_is_right (converse R).
Proof. intros R H x; apply H. Qed.
Lemma zero_is_left_conv_equiv :
∀ {R : G → G → Prop}, zero_is_left (converse R) ↔ zero_is_right R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |];
[apply zero_is_right_conv | apply zero_is_left_conv].
Qed.
Lemma zero_is_right_conv_equiv :
∀ {R : G → G → Prop}, zero_is_right (converse R) ↔ zero_is_left R.
Proof. intro; rewrite zero_is_left_conv_equiv; easy. Qed.
Lemma br_monoid_compat_zl_conv :
∀ {R : G → G → Prop},
br_monoid_compat_zr R → br_monoid_compat_zl (converse R).
Proof.
intro; apply modus_ponens_and;
[apply br_plus_compat_r_conv | apply zero_is_left_conv].
Qed.
Lemma br_monoid_compat_zr_conv :
∀ {R : G → G → Prop},
br_monoid_compat_zl R → br_monoid_compat_zr (converse R).
Proof.
intro; apply modus_ponens_and;
[apply br_plus_compat_r_conv | apply zero_is_right_conv].
Qed.
Lemma br_monoid_compat_zl_conv_equiv :
∀ {R : G → G → Prop},
br_monoid_compat_zl (converse R) ↔ br_monoid_compat_zr R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |];
[apply br_monoid_compat_zr_conv | apply br_monoid_compat_zl_conv].
Qed.
Lemma br_monoid_compat_zr_conv_equiv :
∀ {R : G → G → Prop},
br_monoid_compat_zr (converse R) ↔ br_monoid_compat_zl R.
Proof. intro; rewrite br_monoid_compat_zl_conv_equiv; easy. Qed.
Lemma monomial_order_conv :
∀ {R : G → G → Prop}, monomial_order R → monomial_order (converse R).
Proof.
intro; apply modus_ponens_and;
[apply conv_strict_total_order | apply br_plus_compat_r_conv].
Qed.
Lemma monomial_order_conv_equiv :
∀ {R : G → G → Prop},
monomial_order (converse R) ↔ monomial_order R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply monomial_order_conv.
Qed.
Lemma monomial_order_zl_conv :
∀ {R : G → G → Prop},
monomial_order_zr R → monomial_order_zl (converse R).
Proof.
intro; apply modus_ponens_and;
[apply conv_strict_total_order | apply br_monoid_compat_zl_conv].
Qed.
Lemma monomial_order_zr_conv :
∀ {R : G → G → Prop},
monomial_order_zl R → monomial_order_zr (converse R).
Proof.
intro; apply modus_ponens_and;
[apply conv_strict_total_order | apply br_monoid_compat_zr_conv].
Qed.
Lemma monomial_order_zl_conv_equiv :
∀ {R : G → G → Prop},
monomial_order_zl (converse R) ↔ monomial_order_zr R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |];
[apply monomial_order_zr_conv | apply monomial_order_zl_conv].
Qed.
Lemma monomial_order_zr_conv_equiv :
∀ {R : G → G → Prop},
monomial_order_zr (converse R) ↔ monomial_order_zl R.
Proof. intro; rewrite monomial_order_zl_conv_equiv; easy. Qed.
Lemma monomial_order_ns_conv :
∀ {R : G → G → Prop},
eq_dec G → monomial_order_ns R → monomial_order_ns (converse R).
Proof.
intros R HG; apply modus_ponens_and;
[apply conv_total_order; easy | apply br_plus_compat_r_conv].
Qed.
Lemma monomial_order_ns_conv_equiv :
∀ {R : G → G → Prop},
eq_dec G →
monomial_order_ns (converse R) ↔ monomial_order_ns R.
Proof.
intros R HG; split;
[rewrite -{2}(conv_invol R) |]; apply monomial_order_ns_conv; easy.
Qed.
With the complementary operator.
Lemma br_plus_compat_l_compl :
∀ {R : G → G → Prop},
br_plus_reg_l R → br_plus_compat_l (complementary R).
Proof. intros R H x x1 x2; rewrite -contra_equiv; apply H. Qed.
Lemma br_plus_compat_r_compl :
∀ {R : G → G → Prop},
br_plus_reg_r R → br_plus_compat_r (complementary R).
Proof. intros R H x x1 x2; rewrite -contra_equiv; apply H. Qed.
Lemma br_plus_reg_l_compl :
∀ {R : G → G → Prop},
br_plus_compat_l R → br_plus_reg_l (complementary R).
Proof. intros R H x x1 x2; rewrite -contra_equiv; apply H. Qed.
Lemma br_plus_reg_r_compl :
∀ {R : G → G → Prop},
br_plus_compat_r R → br_plus_reg_r (complementary R).
Proof. intros R H x x1 x2; rewrite -contra_equiv; apply H. Qed.
Lemma br_plus_compat_l_compl_equiv :
∀ {R : G → G → Prop},
br_plus_compat_l (complementary R) ↔ br_plus_reg_l R.
Proof.
intros R; split; [rewrite -{2}(br_compl_invol R) |];
[apply br_plus_reg_l_compl | apply br_plus_compat_l_compl].
Qed.
Lemma br_plus_compat_r_compl_equiv :
∀ {R : G → G → Prop},
br_plus_compat_r (complementary R) ↔ br_plus_reg_r R.
Proof.
intros R; split; [rewrite -{2}(br_compl_invol R) |];
[apply br_plus_reg_r_compl | apply br_plus_compat_r_compl].
Qed.
Lemma br_plus_reg_l_compl_equiv :
∀ {R : G → G → Prop},
br_plus_reg_l (complementary R) ↔ br_plus_compat_l R.
Proof.
intros R; rewrite -{2}(br_compl_invol R) br_plus_compat_l_compl_equiv; easy.
Qed.
Lemma br_plus_reg_r_compl_equiv :
∀ {R : G → G → Prop},
br_plus_reg_r (complementary R) ↔ br_plus_compat_r R.
Proof.
intros R; rewrite -{2}(br_compl_invol R) br_plus_compat_r_compl_equiv; easy.
Qed.
Properties zero_is_left / zero_is_right / br_monoid_compat_zl /
br_monoid_compat_zr / monomial_order_zl / monomial_order_zl are not
compatible with the operator complementary.
Lemma monomial_order_compl :
∀ {R : G → G → Prop},
eq_dec G → total_order R → br_plus_reg_r R →
monomial_order (complementary R).
Proof.
intros; split;
[apply compl_strict_total_order | apply br_plus_compat_r_compl]; easy.
Qed.
Lemma monomial_order_compl_equiv :
∀ {R : G → G → Prop},
eq_dec G →
monomial_order (complementary R) ↔ total_order R ∧ br_plus_reg_r R.
Proof.
intros; apply and_iff_compat; [apply compl_strict_total_order_equiv; easy |
apply br_plus_compat_r_compl_equiv].
Qed.
Lemma monomial_order_ns_compl :
∀ {R : G → G → Prop},
eq_dec G → strict_total_order R → br_plus_reg_r R →
monomial_order_ns (complementary R).
Proof.
intros; split;
[apply compl_total_order | apply br_plus_compat_r_compl]; easy.
Qed.
Lemma monomial_order_ns_compl_equiv :
∀ {R : G → G → Prop},
eq_dec G →
monomial_order_ns (complementary R) ↔
strict_total_order R ∧ br_plus_reg_r R.
Proof.
intros; apply and_iff_compat; [apply compl_total_order_equiv; easy |
apply br_plus_compat_r_compl_equiv].
Qed.
With the conv_compl operator.
Lemma br_plus_compat_l_conv_compl :
∀ {R : G → G → Prop},
br_plus_reg_l R → br_plus_compat_l (conv_compl R).
Proof. intros; apply br_plus_compat_l_conv, br_plus_compat_l_compl; easy. Qed.
Lemma br_plus_compat_r_conv_compl :
∀ {R : G → G → Prop},
br_plus_reg_r R → br_plus_compat_r (conv_compl R).
Proof. intros; apply br_plus_compat_r_conv, br_plus_compat_r_compl; easy. Qed.
Lemma br_plus_reg_l_conv_compl :
∀ {R : G → G → Prop},
br_plus_compat_l R → br_plus_reg_l (conv_compl R).
Proof. intros; apply br_plus_reg_l_conv, br_plus_reg_l_compl; easy. Qed.
Lemma br_plus_reg_r_conv_compl :
∀ {R : G → G → Prop},
br_plus_compat_r R → br_plus_reg_r (conv_compl R).
Proof. intros; apply br_plus_reg_r_conv, br_plus_reg_r_compl; easy. Qed.
Lemma br_plus_compat_l_conv_compl_equiv :
∀ {R : G → G → Prop},
br_plus_compat_l (conv_compl R) ↔ br_plus_reg_l R.
Proof.
intros; rewrite br_plus_compat_l_conv_equiv br_plus_compat_l_compl_equiv; easy.
Qed.
Lemma br_plus_compat_r_conv_compl_equiv :
∀ {R : G → G → Prop},
br_plus_compat_r (conv_compl R) ↔ br_plus_reg_r R.
Proof.
intros; rewrite br_plus_compat_r_conv_equiv br_plus_compat_r_compl_equiv; easy.
Qed.
Lemma br_plus_reg_l_conv_compl_equiv :
∀ {R : G → G → Prop},
br_plus_reg_l (conv_compl R) ↔ br_plus_compat_l R.
Proof.
intros; rewrite br_plus_reg_l_conv_equiv br_plus_reg_l_compl_equiv; easy.
Qed.
Lemma br_plus_reg_r_conv_compl_equiv :
∀ {R : G → G → Prop},
br_plus_reg_r (conv_compl R) ↔ br_plus_compat_r R.
Proof.
intros; rewrite br_plus_reg_r_conv_equiv br_plus_reg_r_compl_equiv; easy.
Qed.
Properties zero_is_left / zero_is_right / br_monoid_compat_zl /
br_monoid_compat_zr / monomial_order_zl / monomial_order_zl are not
compatible with the operator conv_compl.
Lemma monomial_order_conv_compl :
∀ {R : G → G → Prop},
eq_dec G → total_order R → br_plus_reg_r R →
monomial_order (conv_compl R).
Proof. intros; apply monomial_order_conv, monomial_order_compl; easy. Qed.
Lemma monomial_order_conv_compl_equiv :
∀ {R : G → G → Prop},
eq_dec G →
monomial_order (conv_compl R) ↔ total_order R ∧ br_plus_reg_r R.
Proof.
intros; rewrite monomial_order_conv_equiv monomial_order_compl_equiv; easy.
Qed.
Lemma monomial_order_ns_conv_compl :
∀ {R : G → G → Prop},
eq_dec G → strict_total_order R → br_plus_reg_r R →
monomial_order_ns (conv_compl R).
Proof.
intros; apply monomial_order_ns_conv, monomial_order_ns_compl; easy.
Qed.
Lemma monomial_order_ns_conv_compl_equiv :
∀ {R : G → G → Prop},
eq_dec G →
monomial_order_ns (conv_compl R) ↔
strict_total_order R ∧ br_plus_reg_r R.
Proof.
intros R HG; rewrite (monomial_order_ns_conv_equiv HG)
monomial_order_ns_compl_equiv; easy.
Qed.
End Monomial_order_Facts2.
Section Lex_order_Facts.
Compatibility results of the *lex operators with monomial properties.
With the br_plus_compat_r / br_plus_compat_l elementary properties.
Lemma lex_br_plus_compat_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_r R → ∀ {n}, br_plus_compat_r (@lex _ R n).
Proof.
intros R H1 H2 n x x1 x2; induction n; [easy |].
rewrite !lex_S; rewrite !fct_plus_eq; intros [[H3 H4] | [H3 H4]].
left; split; [contradict H3; apply H1 with (x ord0) | apply H2]; easy.
right; split; [apply plus_compat_r | apply IHn]; easy.
Qed.
Lemma colex_br_plus_compat_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_r R → ∀ {n}, br_plus_compat_r (@colex _ R n).
Proof.
intros R H1 H2 n x x1 x2; induction n; [easy |].
rewrite !colex_S; rewrite !fct_plus_eq; intros [[H3 H4] | [H3 H4]].
left; split; [contradict H3; apply H1 with (x ord_max) | apply H2]; easy.
right; split; [apply plus_compat_r | apply IHn]; easy.
Qed.
Lemma symlex_br_plus_compat_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_r R → ∀ {n}, br_plus_compat_r (@symlex _ R n).
Proof. intros; apply br_plus_compat_r_conv, lex_br_plus_compat_r; easy. Qed.
Lemma revlex_br_plus_compat_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_r R → ∀ {n}, br_plus_compat_r (@revlex _ R n).
Proof. intros; apply br_plus_compat_r_conv, colex_br_plus_compat_r; easy. Qed.
Lemma lex_br_plus_compat_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_l R → ∀ {n}, br_plus_compat_l (@lex _ R n).
Proof.
intros R H1 H2 n; move: H2; rewrite !br_plus_compat_equiv; intros H2.
apply lex_br_plus_compat_r; easy.
Qed.
Lemma colex_br_plus_compat_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_l R → ∀ {n}, br_plus_compat_l (@colex _ R n).
Proof.
intros R H1 H2 n; move: H2; rewrite !br_plus_compat_equiv; intros H2.
apply colex_br_plus_compat_r; easy.
Qed.
Lemma symlex_br_plus_compat_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_l R → ∀ {n}, br_plus_compat_l (@symlex _ R n).
Proof. intros; apply br_plus_compat_l_conv, lex_br_plus_compat_l; easy. Qed.
Lemma revlex_br_plus_compat_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_compat_l R → ∀ {n}, br_plus_compat_l (@revlex _ R n).
Proof. intros; apply br_plus_compat_l_conv, colex_br_plus_compat_l; easy. Qed.
With the br_plus_reg_r / br_plus_reg_l elementary properties.
Lemma lex_br_plus_reg_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_r R → ∀ {n}, br_plus_reg_r (@lex _ R n).
Proof.
intros R H1 H2 n x x1 x2; induction n; [easy |].
rewrite !lex_S; rewrite !fct_plus_eq; intros [[H3 H4] | [H3 H4]].
left; split;
[contradict H3; apply plus_compat_r | apply H2 with (x ord0)]; easy.
right; split;
[apply H1 with (x ord0) | apply IHn with (skipF x ord0)]; easy.
Qed.
Lemma colex_br_plus_reg_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_r R → ∀ {n}, br_plus_reg_r (@colex _ R n).
Proof.
intros R H1 H2 n x x1 x2; induction n; [easy |].
rewrite !colex_S; rewrite !fct_plus_eq; intros [[H3 H4] | [H3 H4]].
left; split;
[contradict H3; apply plus_compat_r | apply H2 with (x ord_max)]; easy.
right; split;
[apply H1 with (x ord_max) | apply IHn with (skipF x ord_max)]; easy.
Qed.
Lemma symlex_br_plus_reg_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_r R → ∀ {n}, br_plus_reg_r (@symlex _ R n).
Proof. intros; apply br_plus_reg_r_conv, lex_br_plus_reg_r; easy. Qed.
Lemma revlex_br_plus_reg_r :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_r R → ∀ {n}, br_plus_reg_r (@revlex _ R n).
Proof. intros; apply br_plus_reg_r_conv, colex_br_plus_reg_r; easy. Qed.
Lemma lex_br_plus_reg_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_l R → ∀ {n}, br_plus_reg_l (@lex _ R n).
Proof.
intros R H1 H2 n; move: H2; rewrite !br_plus_reg_equiv; intros H2.
apply lex_br_plus_reg_r; easy.
Qed.
Lemma colex_br_plus_reg_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_l R → ∀ {n}, br_plus_reg_l (@colex _ R n).
Proof.
intros R H1 H2 n; move: H2; rewrite !br_plus_reg_equiv; intros H2.
apply colex_br_plus_reg_r; easy.
Qed.
Lemma symlex_br_plus_reg_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_l R → ∀ {n}, br_plus_reg_l (@symlex _ R n).
Proof. intros; apply br_plus_reg_l_conv, lex_br_plus_reg_l; easy. Qed.
Lemma revlex_br_plus_reg_l :
∀ {R : G → G → Prop},
@plus_is_reg_r G →
br_plus_reg_l R → ∀ {n}, br_plus_reg_l (@revlex _ R n).
Proof. intros; apply br_plus_reg_l_conv, colex_br_plus_reg_l; easy. Qed.
With the zero_is_left / zero_is_right elementary properties.
Lemma lex_zero_is_left :
∀ {R : G → G → Prop},
eq_dec G → zero_is_left R → ∀ {n}, zero_is_left (@lex _ R n).
Proof.
intros R HG H n x Hx; induction n; [contradict Hx; apply hat0F_unit |].
rewrite lex_S; destruct (HG 0 (x ord0)) as [Hx0 | Hx0].
rewrite -Hx0; right; split; [easy |].
apply IHn; contradict Hx; apply extF_skipF with ord0; easy.
left; split; [| apply H, neq_sym_equiv]; easy.
Qed.
Lemma colex_zero_is_left :
∀ {R : G → G → Prop},
eq_dec G → zero_is_left R → ∀ {n}, zero_is_left (@colex _ R n).
Proof.
intros R HG H n x Hx; induction n; [contradict Hx; apply hat0F_unit |].
rewrite colex_S; destruct (HG 0 (x ord_max)) as [Hxn | Hxn].
rewrite -Hxn; right; split; [easy |].
apply IHn; contradict Hx; apply extF_skipF with ord_max; easy.
left; split; [| apply H, neq_sym_equiv]; easy.
Qed.
Lemma symlex_zero_is_right :
∀ {R : G → G → Prop},
eq_dec G → zero_is_left R → ∀ {n}, zero_is_right (@symlex _ R n).
Proof. intros; apply zero_is_right_conv, lex_zero_is_left; easy. Qed.
Lemma revlex_zero_is_right :
∀ {R : G → G → Prop},
eq_dec G → zero_is_left R → ∀ {n}, zero_is_right (@revlex _ R n).
Proof. intros; apply zero_is_right_conv, colex_zero_is_left; easy. Qed.
Lemma lex_zero_is_right :
∀ {R : G → G → Prop},
eq_dec G → zero_is_right R → ∀ {n}, zero_is_right (@lex _ R n).
Proof.
intros R HG H n x Hx; induction n; [contradict Hx; apply hat0F_unit |].
rewrite lex_S; destruct (HG (x ord0) 0) as [Hx0 | Hx0].
rewrite Hx0; right; split; [easy |].
apply IHn; contradict Hx; apply extF_skipF with ord0; easy.
left; split; [| apply H]; easy.
Qed.
Lemma colex_zero_is_right :
∀ {R : G → G → Prop},
eq_dec G → zero_is_right R → ∀ {n}, zero_is_right (@colex _ R n).
Proof.
intros R HG H n x Hx; induction n; [contradict Hx; apply hat0F_unit |].
rewrite colex_S; destruct (HG (x ord_max) 0) as [Hxn | Hxn].
rewrite Hxn; right; split; [easy |].
apply IHn; contradict Hx; apply extF_skipF with ord_max; easy.
left; split; [| apply H]; easy.
Qed.
Lemma symlex_zero_is_left :
∀ {R : G → G → Prop},
eq_dec G → zero_is_right R → ∀ {n}, zero_is_left (@symlex _ R n).
Proof. intros; apply zero_is_left_conv, lex_zero_is_right; easy. Qed.
Lemma revlex_zero_is_left :
∀ {R : G → G → Prop},
eq_dec G → zero_is_right R → ∀ {n}, zero_is_left (@revlex _ R n).
Proof. intros; apply zero_is_left_conv, colex_zero_is_right; easy. Qed.
With the br_monoid_compat_zl / br_monoid_compat_zr compound properties.
Lemma lex_br_monoid_compat_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zl R → ∀ {n}, br_monoid_compat_zl (@lex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply lex_br_plus_compat_r | apply lex_zero_is_left]; easy.
Qed.
Lemma colex_br_monoid_compat_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zl R → ∀ {n}, br_monoid_compat_zl (@colex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply colex_br_plus_compat_r | apply colex_zero_is_left]; easy.
Qed.
Lemma symlex_br_monoid_compat_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zl R → ∀ {n}, br_monoid_compat_zr (@symlex _ R n).
Proof.
intros; apply br_monoid_compat_zr_conv, lex_br_monoid_compat_zl; easy.
Qed.
Lemma revlex_br_monoid_compat_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zl R → ∀ {n}, br_monoid_compat_zr (@revlex _ R n).
Proof.
intros; apply br_monoid_compat_zr_conv, colex_br_monoid_compat_zl; easy.
Qed.
Lemma lex_br_monoid_compat_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zr R → ∀ {n}, br_monoid_compat_zr (@lex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply lex_br_plus_compat_r | apply lex_zero_is_right]; easy.
Qed.
Lemma colex_br_monoid_compat_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zr R → ∀ {n}, br_monoid_compat_zr (@colex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply colex_br_plus_compat_r | apply colex_zero_is_right]; easy.
Qed.
Lemma symlex_br_monoid_compat_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zr R → ∀ {n}, br_monoid_compat_zl (@symlex _ R n).
Proof.
intros; apply br_monoid_compat_zl_conv, lex_br_monoid_compat_zr; easy.
Qed.
Lemma revlex_br_monoid_compat_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zr R → ∀ {n}, br_monoid_compat_zl (@revlex _ R n).
Proof.
intros; apply br_monoid_compat_zl_conv, colex_br_monoid_compat_zr; easy.
Qed.
With the monomial_order / monomial_order_zl / monomial_order_zr /
monomial_order_ns compound properties.
Lemma lex_monomial_order :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order R → ∀ {n}, monomial_order (@lex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply lex_strict_total_order | apply lex_br_plus_compat_r];
[apply inhabited_m | easy..].
Qed.
Lemma colex_monomial_order :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order R → ∀ {n}, monomial_order (@colex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply colex_strict_total_order | apply colex_br_plus_compat_r];
[apply inhabited_m | easy..].
Qed.
Lemma symlex_monomial_order :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order R → ∀ {n}, monomial_order (@symlex _ R n).
Proof. intros; apply monomial_order_conv, lex_monomial_order; easy. Qed.
Lemma revlex_monomial_order :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order R → ∀ {n}, monomial_order (@revlex _ R n).
Proof. intros; apply monomial_order_conv, colex_monomial_order; easy. Qed.
Lemma lex_monomial_order_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zl R → ∀ {n}, monomial_order_zl (@lex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply lex_strict_total_order | apply lex_br_monoid_compat_zl];
[apply inhabited_m | easy..].
Qed.
Lemma colex_monomial_order_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zl R → ∀ {n}, monomial_order_zl (@colex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply colex_strict_total_order | apply colex_br_monoid_compat_zl];
[apply inhabited_m | easy..].
Qed.
Lemma symlex_monomial_order_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zl R → ∀ {n}, monomial_order_zr (@symlex _ R n).
Proof. intros; apply monomial_order_zr_conv, lex_monomial_order_zl; easy. Qed.
Lemma revlex_monomial_order_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zl R → ∀ {n}, monomial_order_zr (@revlex _ R n).
Proof.
intros; apply monomial_order_zr_conv, colex_monomial_order_zl; easy.
Qed.
Lemma lex_monomial_order_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zr R → ∀ {n}, monomial_order_zr (@lex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply lex_strict_total_order | apply lex_br_monoid_compat_zr];
[apply inhabited_m | easy..].
Qed.
Lemma colex_monomial_order_zr :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zr R → ∀ {n}, monomial_order_zr (@colex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply colex_strict_total_order | apply colex_br_monoid_compat_zr];
[apply inhabited_m | easy..].
Qed.
Lemma symlex_monomial_order_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zr R → ∀ {n}, monomial_order_zl (@symlex _ R n).
Proof. intros; apply monomial_order_zl_conv, lex_monomial_order_zr; easy. Qed.
Lemma revlex_monomial_order_zl :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_zr R → ∀ {n}, monomial_order_zl (@revlex _ R n).
Proof.
intros; apply monomial_order_zl_conv, colex_monomial_order_zr; easy.
Qed.
Lemma lex_monomial_order_ns :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_ns R → ∀ {n}, monomial_order_ns (@lex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply lex_total_order | apply lex_br_plus_compat_r]; easy.
Qed.
Lemma colex_monomial_order_ns :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_ns R → ∀ {n}, monomial_order_ns (@colex _ R n).
Proof.
intros R HG H1 H2 n; move: H2; apply modus_ponens_and; intros H2;
[apply colex_total_order | apply colex_br_plus_compat_r]; easy.
Qed.
Lemma symlex_monomial_order_ns :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_ns R → ∀ {n}, monomial_order_ns (@symlex _ R n).
Proof.
intros; apply monomial_order_ns_conv;
[apply eq_decF | apply lex_monomial_order_ns]; easy.
Qed.
Lemma revlex_monomial_order_ns :
∀ {R : G → G → Prop},
eq_dec G → @plus_is_reg_r G →
monomial_order_ns R → ∀ {n}, monomial_order_ns (@revlex _ R n).
Proof.
intros; apply monomial_order_ns_conv;
[apply eq_decF | apply colex_monomial_order_ns]; easy.
Qed.
End Lex_order_Facts.
Section Graded_monomial_order_Def.
Graded monomial orders.
Context {G : AbelianMonoid}.
Variable R : G → G → Prop.
Context {n : nat}.
Definition graded (Rn : 'G^n → 'G^n → Prop) (x y : 'G^n) : Prop :=
sum x ≠ sum y ∧ R (sum x) (sum y) ∨ sum x = sum y ∧ Rn x y.
Definition grlex : 'G^n → 'G^n → Prop := graded (@lex _ R n).
Definition grcolex : 'G^n → 'G^n → Prop := graded (@colex _ R n).
Definition grsymlex : 'G^n → 'G^n → Prop := graded (@symlex _ R n).
Definition grevlex : 'G^n → 'G^n → Prop := graded (@revlex _ R n).
End Graded_monomial_order_Def.
Section Graded_monomial_order_Facts1.
General properties of graded monomial orders.
Context {G : AbelianMonoid}.
Lemma graded_l :
∀ (R : G → G → Prop) {n} (Rn : 'G^n → 'G^n → Prop) x y,
sum x ≠ sum y → R (sum x) (sum y) → graded R Rn x y.
Proof. intros; left; easy. Qed.
Lemma graded_r :
∀ (R : G → G → Prop) {n} (Rn : 'G^n → 'G^n → Prop) x y,
sum x = sum y → Rn x y → graded R Rn x y.
Proof. intros; right; easy. Qed.
Lemma graded_idem :
∀ {R1 : G → G → Prop} R2 {n} {Rn : 'G^n → 'G^n → Prop},
graded R1 (graded R2 Rn) = graded R1 Rn.
Proof.
intros; apply fun_ext2; intros; apply prop_ext; split; intros [H | H];
[left; easy | right | left; easy | right]; split; [easy | | easy |].
destruct H as [H1 [H2 | H2]]; easy.
right; easy.
Qed.
Lemma graded_eq : ∀ {n}, graded eq (@eq 'G^n) = eq.
Proof.
intros; apply fun_ext2; intros; apply prop_ext; split;
[intros [H | H] | intros; subst; right]; easy.
Qed.
Lemma graded_neq : ∀ {n}, eq_dec G → graded neq (@neq 'G^n) = neq.
Proof.
intros n HG; apply fun_ext2; intros x y; apply prop_ext; split.
intros [[H _] | H]; [unfold neq; contradict H; subst |]; easy.
intros H; destruct (HG (sum x) (sum y)); [right | left]; easy.
Qed.
End Graded_monomial_order_Facts1.
Section Graded_monomial_order_Facts2.
Compatibility results of graded monomial orders with operators on
homogeneous binary relations.
Context {G : AbelianMonoid}.
Lemma graded_conv :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
graded (converse R) (converse Rn) = converse (graded R Rn).
Proof.
intros; apply fun_ext2; intros; apply prop_ext; split;
(intros [H | H]; [left; rewrite neq_sym_equiv | right]; easy).
Qed.
Lemma graded_compl :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G →
graded (complementary R) (complementary Rn) = complementary (graded R Rn).
Proof.
unfold complementary; intros R n Rn HG; apply fun_ext2; intros x y;
apply prop_ext; rewrite not_or_equiv !not_and_equiv NNPP_equiv; split.
intros [H | H]; split; [right | left | left | right]; easy.
intros [[H1 | H1] [H2 | H2]]; [..| destruct (HG (sum x) (sum y))];
[| right | left | right | left]; easy.
Qed.
Lemma graded_conv_compl :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G →
graded (conv_compl R) (conv_compl Rn) = conv_compl (graded R Rn).
Proof. intros; rewrite !conv_compl_eq graded_conv graded_compl; easy. Qed.
Lemma graded_br_and :
∀ {R1 R2 : G → G → Prop} {n} {R1n R2n : 'G^n → 'G^n → Prop},
graded (br_and R1 R2) (br_and R1n R2n) =
br_and (graded R1 R1n) (graded R2 R2n).
Proof.
intros; apply fun_ext2; intros; apply prop_ext; split.
intros [[H1 [H2 H3]] | [H1 [H2 H3]]]; split; [left | left | right..]; easy.
intros [[H1 | H1] [H2 | H2]]; [left |..| right]; easy.
Qed.
Lemma graded_br_or :
∀ {R1 R2 : G → G → Prop} {n} {R1n R2n : 'G^n → 'G^n → Prop},
graded (br_or R1 R2) (br_or R1n R2n) =
br_or (graded R1 R1n) (graded R2 R2n).
Proof.
intros; apply fun_ext2; intros; apply prop_ext; split.
intros [[H1 [H2 | H2]] | [H1 [H2 | H2]]];
[left; left | right; left | left; right | right; right]; easy.
intros [[H | H] | [H | H]]; [left | right | left | right]; (split; [easy |]);
[left | left | right | right]; easy.
Qed.
Lemma graded_br_and_neq :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G →
graded (br_and_neq R) (br_and_neq Rn) = br_and_neq (graded R Rn).
Proof. intros; rewrite !br_and_neq_eq graded_br_and graded_neq; easy. Qed.
Lemma graded_br_or_eq :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
graded (br_or_eq R) (br_or_eq Rn) = br_or_eq (graded R Rn).
Proof. intros; rewrite !br_or_eq_eq graded_br_or graded_eq; easy. Qed.
Lemma graded_strict :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G →
graded (strict R) (strict Rn) = strict (graded R Rn).
Proof. intros; rewrite !strict_eq graded_br_and graded_conv_compl; easy. Qed.
Lemma graded_equivalent :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
graded (equivalent R) (equivalent Rn) = equivalent (graded R Rn).
Proof. intros; rewrite !equivalent_eq graded_br_and graded_conv; easy. Qed.
Lemma graded_compar :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
graded (comparable R) (comparable Rn) = comparable (graded R Rn).
Proof. intros; rewrite !compar_eq graded_br_or graded_conv; easy. Qed.
Lemma graded_incompar :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G →
graded (incomparable R) (incomparable Rn) = incomparable (graded R Rn).
Proof.
move=>> HG; rewrite !incompar_eq graded_br_and
(graded_compl HG) graded_conv_compl; easy.
Qed.
End Graded_monomial_order_Facts2.
Section Graded_monomial_order_Facts3.
Compatibility results of graded monomial orders with elementary properties
of homogeneous binary relations.
Context {G : AbelianMonoid}.
Lemma graded_refl :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
reflexive Rn → reflexive (graded R Rn).
Proof. move=>> Hn x; right; split; easy. Qed.
Lemma graded_irrefl :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
irreflexive Rn → irreflexive (graded R Rn).
Proof. move=>> Hn x [[Hx _] | [_ Hx]]; [easy | apply (Hn _ Hx)]. Qed.
Lemma graded_sym :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
symmetric R → symmetric Rn → symmetric (graded R Rn).
Proof.
move=>> /sym_equiv H /sym_equiv Hn x y [H1 | H1];
[left; rewrite neq_sym_equiv H | right; rewrite Hn]; easy.
Qed.
Lemma graded_antisym :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
antisymmetric R → antisymmetric Rn → antisymmetric (graded R Rn).
Proof.
move=>> H Hn x y [[H1 H2] | [H1 H2]] [[H3 H4] | [H3 H4]].
contradict H1; apply (H _ _ H2 H4).
rewrite H3 in H1; easy.
rewrite H1 in H3; easy.
apply (Hn _ _ H2 H4).
Qed.
Lemma graded_asym :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
asymmetric R → asymmetric Rn → asymmetric (graded R Rn).
Proof.
move=>>; rewrite !asym_equiv_irrefl_antisym; apply modus_ponens_and3;
[intros _; apply graded_irrefl | apply graded_antisym].
Qed.
Lemma graded_conn :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G → connected R → connected Rn → connected (graded R Rn).
Proof.
move=>> HG H Hn x y H1; destruct (HG (sum x) (sum y)) as [H2 | H2].
destruct (Hn _ _ H1) as [H3 | H3]; [left | right]; right; easy.
destruct (H (sum x) (sum y) H2) as [H3 | H3]; [left | right]; left;
[| split; [apply not_eq_sym |]]; easy.
Qed.
Lemma graded_str_conn :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G → strongly_connected R → strongly_connected Rn →
strongly_connected (graded R Rn).
Proof.
intros R n Rn HG; assert (HGn : eq_dec 'G^n) by now apply eq_decF.
rewrite (str_conn_equiv_refl_conn HG) !(str_conn_equiv_refl_conn HGn).
apply modus_ponens_and3; [intros _; apply graded_refl | apply graded_conn, HG].
Qed.
Lemma graded_tricho :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G →
trichotomous R → trichotomous Rn → trichotomous (graded R Rn).
Proof.
intros R n Rn HG; assert (HGn : eq_dec 'G^n) by now apply eq_decF.
rewrite (tricho_equiv_asym_conn HG) !(tricho_equiv_asym_conn HGn).
apply modus_ponens_and3; [apply graded_asym | apply graded_conn, HG].
Qed.
Lemma graded_trans :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
transitive (br_and_neq R) → transitive Rn → transitive (graded R Rn).
Proof.
move=>> H Hn x y z [[H1 H2] | [H1 H2]] [[H3 H4] | [H3 H4]].
left; apply (H (sum x) (sum y) (sum z)); easy.
left; rewrite -H3; easy.
left; rewrite H1; easy.
right; split; [rewrite H1 | apply Hn with y]; easy.
Qed.
Lemma graded_neg_trans :
∀ {R : G → G → Prop} {n} {Rn : 'G^n → 'G^n → Prop},
eq_dec G →
negatively_transitive (br_or_eq R) → negatively_transitive Rn →
negatively_transitive (graded R Rn).
Proof.
intros R n Rn HG H Hn x y z; rewrite -!compl_alt -(graded_compl HG).
apply graded_trans; [rewrite br_and_neq_compl |]; easy.
Qed.
End Graded_monomial_order_Facts3.
Section Graded_monomial_order_Facts4.
Compatibility results of graded monomial orders with compound properties
of homogeneous binary relations.
Context {G : AbelianMonoid}.
Variable R : G → G → Prop.
Context {n : nat}.
Variable Rn : 'G^n → 'G^n → Prop.
Lemma graded_partial_order :
partial_order R → partial_order Rn → partial_order (graded R Rn).
Proof.
intros H Hn; repeat split.
apply graded_refl, Hn.
apply graded_antisym; [apply H | apply Hn].
apply graded_trans; [apply br_and_neq_trans; apply H | apply Hn].
Qed.
Lemma graded_total_order :
eq_dec G →
total_order R → total_order Rn → total_order (graded R Rn).
Proof.
intros HG; move: (eq_decF HG n) ⇒ HGn.
rewrite (total_order_equiv_po HG) !(total_order_equiv_po HGn);
apply modus_ponens_and3;
[apply graded_partial_order | apply graded_conn; easy].
Qed.
Lemma graded_strict_partial_order :
strict_partial_order R → strict_partial_order Rn →
strict_partial_order (graded R Rn).
Proof.
intros H Hn; rewrite strict_partial_order_equiv_no_asym; split.
apply graded_irrefl, Hn.
apply graded_trans; [| apply Hn].
apply br_and_neq_trans; [apply asym_antisym |]; apply H.
Qed.
Lemma graded_strict_total_order :
eq_dec G →
strict_total_order R → strict_total_order Rn →
strict_total_order (graded R Rn).
Proof.
intro; rewrite !strict_total_order_equiv_spo; apply modus_ponens_and3;
[apply graded_strict_partial_order | apply graded_conn; easy].
Qed.
End Graded_monomial_order_Facts4.
Section Graded_monomial_order_Facts5.
Compatibility results of graded monomial orders with monomial properties.
Context {G : AbelianMonoid}.
Variable R : G → G → Prop.
Context {n : nat}.
Variable Rn : 'G^n → 'G^n → Prop.
Lemma graded_br_plus_compat_r :
@plus_is_reg_r G →
br_plus_compat_r R → br_plus_compat_r Rn →
br_plus_compat_r (graded R Rn).
Proof.
intros HG H Hn x x1 x2 [[Hx1 Hx2] | [Hx1 Hx2]].
left; rewrite !sum_plus; split;
[contradict Hx1; apply (HG (sum x)) | apply H]; easy.
right; split; [rewrite !sum_plus Hx1 | apply Hn]; easy.
Qed.
Lemma graded_br_plus_compat_l :
@plus_is_reg_l G →
br_plus_compat_l R → br_plus_compat_l Rn →
br_plus_compat_l (graded R Rn).
Proof.
rewrite plus_is_reg_equiv !br_plus_compat_equiv; apply graded_br_plus_compat_r.
Qed.
Lemma graded_zero_is_left :
eq_dec G → zero_is_left R → zero_is_left Rn → zero_is_left (graded R Rn).
Proof.
intros HG H Hn x Hx; destruct (HG (sum x) 0) as [Hx1 | Hx1].
right; rewrite sum_zero Hx1; split; [| apply Hn]; easy.
left; rewrite sum_zero; split; [contradict Hx1 | apply H]; easy.
Qed.
Lemma graded_zero_is_right :
eq_dec G →
zero_is_right R → zero_is_right Rn → zero_is_right (graded R Rn).
Proof.
intros HG H Hn x Hx; destruct (HG (sum x) 0) as [Hx1 | Hx1].
right; rewrite sum_zero Hx1; split; [| apply Hn]; easy.
left; rewrite sum_zero; split; [contradict Hx1 | apply H]; easy.
Qed.
Lemma graded_br_monoid_compat_zl :
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zl R → br_monoid_compat_zl Rn →
br_monoid_compat_zl (graded R Rn).
Proof.
intros HG1 HG2; apply modus_ponens_and3;
[apply graded_br_plus_compat_r | apply graded_zero_is_left]; easy.
Qed.
Lemma graded_br_monoid_compat_zr :
eq_dec G → @plus_is_reg_r G →
br_monoid_compat_zr R → br_monoid_compat_zr Rn →
br_monoid_compat_zr (graded R Rn).
Proof.
intros HG1 HG2; apply modus_ponens_and3;
[apply graded_br_plus_compat_r | apply graded_zero_is_right]; easy.
Qed.
Lemma graded_monomial_order :
eq_dec G → @plus_is_reg_r G →
monomial_order R → monomial_order Rn → monomial_order (graded R Rn).
Proof.
intros HG1 HG2; apply modus_ponens_and3;
[apply graded_strict_total_order | apply graded_br_plus_compat_r]; easy.
Qed.
Lemma graded_monomial_order_zl :
eq_dec G → @plus_is_reg_r G →
monomial_order_zl R → monomial_order_zl Rn →
monomial_order_zl (graded R Rn).
Proof.
intros HG1 HG2; apply modus_ponens_and3;
[apply graded_strict_total_order | apply graded_br_monoid_compat_zl]; easy.
Qed.
Lemma graded_monomial_order_zr :
eq_dec G → @plus_is_reg_r G →
monomial_order_zr R → monomial_order_zr Rn →
monomial_order_zr (graded R Rn).
Proof.
intros HG1 HG2; apply modus_ponens_and3;
[apply graded_strict_total_order | apply graded_br_monoid_compat_zr]; easy.
Qed.
End Graded_monomial_order_Facts5.