# Library CoLoR.Util.Algebra.OrdSemiRing

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2009-03-19 (setoid)
Semi-ring equipped with two (strict and non-strict) orders.

Semi-rings equipped with orders

Module Type OrdSemiRingType.

Declare Module Export SR : SemiRingType.

Parameter gt : relation A.
Parameter ge : relation A.

Notation "x >> y" := (gt x y) (at level 70).
Notation "x >>= y" := (ge x y) (at level 70).

Parameter eq_ge_compat : forall x y, x =A= y -> x >>= y.

Declare Instance ge_refl : Reflexive ge.
Declare Instance ge_trans : Transitive ge.
Declare Instance gt_trans : Transitive gt.

Parameter ge_dec : rel_dec ge.
Parameter gt_dec : rel_dec gt.

Parameter ge_gt_compat : forall x y z, x >>= y -> y >> z -> x >> z.
Parameter ge_gt_compat2 : forall x y z, x >> y -> y >>= z -> x >> z.

Parameter plus_gt_compat : forall m n m' n',
m >> m' -> n >> n' -> m + n >> m' + n'.
Parameter plus_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m + n >>= m' + n'.

Parameter mult_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m * n >>= m' * n'.

Hint Resolve ge_refl : arith.

End OrdSemiRingType.

Module OrdSemiRing (OSR : OrdSemiRingType).

Module Export SR := SemiRing OSR.SR.
Export OSR.

Instance ge_mor : Proper (eqA ==> eqA ==> iff) ge.

Instance gt_mor : Proper (eqA ==> eqA ==> iff) gt.

End OrdSemiRing.

Natural numbers semi-rings with natural order

Module NOrdSemiRingT <: OrdSemiRingType.

Module Export SR := NSemiRingT.

Definition gt := Peano.gt.
Definition ge := Peano.ge.

Lemma eq_ge_compat : forall x y, x = y -> x >= y.

Instance ge_refl : Reflexive ge.

Instance ge_trans : Transitive ge.

Lemma ge_antisym : antisymmetric ge.

Definition gt_irrefl := Gt.gt_irrefl.

Definition gt_trans := Gt.gt_trans.

Definition ge_dec := ge_dec.

Definition gt_dec := gt_dec.

Lemma gt_WF : WF gt.

Lemma ge_gt_compat : forall x y z, x >= y -> y > z -> x > z.

Lemma ge_gt_compat2 : forall x y z, x > y -> y >= z -> x > z.

Lemma plus_gt_compat : forall m n m' n',
m > m' -> n > n' -> m + n > m' + n'.

Lemma plus_gt_compat_l : forall m n m' n',
m > m' -> n >= n' -> m + n > m' + n'.

Lemma plus_gt_compat_r : forall m n m' n',
m >= m' -> n > n' -> m + n > m' + n'.

Lemma plus_ge_compat : forall m n m' n',
m >= m' -> n >= n' -> m + n >= m' + n'.

Lemma mult_ge_compat : forall m n m' n',
m >= m' -> n >= n' -> m * n >= m' * n'.

End NOrdSemiRingT.

Module NOrdSemiRing := OrdSemiRing NOrdSemiRingT.

BigN natural numbers semi-rings with natural order

Module BigNOrdSemiRingT <: OrdSemiRingType.

Module Export SR := BigNSemiRingT.

Import BigNUtil.

Definition gt x y := BigN.lt y x.
Definition ge x y := BigN.le y x.

Lemma eq_ge_compat : forall x y, eqA x y -> x >= y.

Definition ge_refl := BigN.le_refl.

Instance ge_trans : Transitive ge.

Instance gt_trans : Transitive gt.

Lemma ge_dec : forall x y, {ge x y}+{~ge x y}.

Lemma gt_dec : forall x y, {gt x y}+{~gt x y}.

Definition gt_WF := wf_transp_WF BigN.lt_wf_0.

Lemma ge_gt_compat : forall x y z, ge x y -> gt y z -> gt x z.

Lemma ge_gt_compat2 : forall x y z, gt x y -> ge y z -> gt x z.

Lemma plus_gt_compat :
forall m n m' n', gt m m' -> gt n n' -> gt (m + n) (m' + n').

Lemma plus_gt_compat_l :
forall m n m' n', gt m m' -> ge n n' -> gt (m + n) (m' + n').

Lemma plus_gt_compat_r :
forall m n m' n', ge m m' -> gt n n' -> gt (m + n) (m' + n').

Lemma plus_ge_compat :
forall m n m' n', ge m m' -> ge n n' -> ge (m + n) (m' + n').

Lemma mult_ge_compat :
forall m n m' n', ge m m' -> ge n n' -> ge (m * n) (m' * n').

Lemma mult_lt_compat_lr : forall i j k l,
i <= j -> j > 0 -> k < l -> i * k < j * l.

End BigNOrdSemiRingT.

Module BigNOrdSemiRing := OrdSemiRing BigNOrdSemiRingT.

Arctic ordered semi-ring

Module ArcticOrdSemiRingT <: OrdSemiRingType.

Module Export SR := ArcticSemiRingT.

Definition gt m n :=
match m, n with
| MinusInf, _ => False
| Pos _, MinusInf => True
| Pos m, Pos n => m > n
end.

Definition ge m n := gt m n \/ m = n.

Lemma eq_ge_compat : forall x y, x = y -> ge x y.

Lemma gt_irrefl : irreflexive gt.

Instance gt_trans : Transitive gt.

Lemma gt_asym x y : gt x y -> ~gt y x.

Lemma gt_dec : rel_dec gt.

Lemma gt_WF : WF gt.

Instance ge_refl : Reflexive ge.

Instance ge_trans : Transitive ge.

Lemma ge_antisym : antisymmetric ge.

Lemma ge_dec : rel_dec ge.

Notation "x + y" := (Aplus x y).
Notation "x * y" := (Amult x y).
Notation "x >>= y" := (ge x y) (at level 70).
Notation "x >> y" := (gt x y) (at level 70).

Lemma ge_gt_eq : forall x y, x >>= y -> x >> y \/ x = y.

Lemma ge_gt_compat : forall x y z, x >>= y -> y >> z -> x >> z.

Lemma ge_gt_compat2 : forall x y z, x >> y -> y >>= z -> x >> z.

Lemma pos_ord : forall m n,
Pos m >>= Pos n -> Peano.ge m n.

Lemma plus_inf_dec : forall m n,
{ exists p, (m = Pos p \/ n = Pos p) /\ m + n = Pos p} +
{ m + n = MinusInf /\ m = MinusInf /\ n = MinusInf }.

Lemma mult_inf_dec : forall m n,
{ exists mi, exists ni,
m = Pos mi /\ n = Pos ni /\ m * n = Pos (mi + ni) } +
{ m * n = MinusInf /\ (m = MinusInf \/ n = MinusInf) }.

Lemma ge_impl_pos_ge : forall m n, (m >= n)%nat -> Pos m >>= Pos n.

Lemma pos_ge_impl_ge : forall m n, Pos m >>= Pos n -> (m >= n)%nat.

Ltac arctic_ord :=
match goal with
| H: MinusInf >> Pos _ |- _ =>
contr
| H: MinusInf >>= Pos _ |- _ =>
destruct H; [ contr | discr ]
| H: Pos ?m >>= Pos ?n |- _ =>
assert ((m >= n)%nat);
[ apply pos_ge_impl_ge; hyp
| clear H; arctic_ord
]
| |- Pos _ >>= MinusInf => left; simpl; trivial
| |- Pos ?m >>= Pos ?n => apply ge_impl_pos_ge
| _ => try solve [contr | discr]
end.

Lemma plus_gt_compat : forall m n m' n',
m >> m' -> n >> n' -> m + n >> m' + n'.

Lemma plus_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m + n >>= m' + n'.

Lemma mult_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m * n >>= m' * n'.

Lemma not_minusInf_ge_A1 : forall a, a <> MinusInf -> a >>= A1.

Lemma ge_A1_not_minusInf : forall a, a >>= A1 -> a <> MinusInf.

End ArcticOrdSemiRingT.

Module ArcticOrdSemiRing := OrdSemiRing ArcticOrdSemiRingT.

Arctic below-zero ordered semi-ring

Module ArcticBZOrdSemiRingT <: OrdSemiRingType.

Local Open Scope Z_scope.

Module Export SR := ArcticBZSemiRingT.

Definition gt m n :=
match m, n with
| MinusInfBZ, _ => False
| Fin _, MinusInfBZ => True
| Fin m, Fin n => m > n
end.

Definition ge m n := gt m n \/ m = n.

Definition is_above_zero v :=
match v with
| MinusInfBZ => false
| Fin z => is_not_neg z
end.

Lemma is_above_zero_ok :
forall v, is_above_zero v = true <-> ge v (Fin 0).

Lemma eq_ge_compat : forall x y, x = y -> ge x y.

Instance ge_refl : Reflexive ge.

Instance gt_trans : Transitive gt.

Lemma gt_irrefl : irreflexive gt.

Lemma gt_asym : forall m n, gt m n -> ~gt n m.

Instance ge_trans : Transitive ge.

Lemma ge_antisym : antisymmetric ge.

Lemma gt_dec : rel_dec gt.

Lemma ge_dec : rel_dec ge.

Notation "x + y" := (Aplus x y).
Notation "x * y" := (Amult x y).
Notation "x >> y" := (gt x y) (at level 70).
Notation "x >>= y" := (ge x y) (at level 70).

Lemma ge_gt_eq : forall x y, x >>= y -> x >> y \/ x = y.

Lemma ge_gt_compat : forall x y z, x >>= y -> y >> z -> x >> z.

Lemma ge_gt_compat2 : forall x y z, x >> y -> y >>= z -> x >> z.

Lemma fin_ge_Zge : forall m n,
Fin m >>= Fin n -> (m >= n)%Z.

Lemma plus_inf_dec : forall m n,
{ exists p, (m = Fin p \/ n = Fin p) /\ m + n = Fin p} +
{ m + n = MinusInfBZ /\ m = MinusInfBZ /\ n = MinusInfBZ }.

Lemma mult_inf_dec : forall m n,
{exists mi, exists ni, m = Fin mi /\ n = Fin ni /\ m * n = Fin (mi + ni)}
+ {m * n = MinusInfBZ /\ (m = MinusInfBZ \/ n = MinusInfBZ)}.

Lemma minusInf_ge_min : forall a, a >>= MinusInfBZ.

Lemma ge_impl_fin_ge : forall m n, (m >= n)%Z -> Fin m >>= Fin n.

Lemma fin_ge_impl_ge : forall m n, Fin m >>= Fin n -> (m >= n)%Z.

Ltac arctic_ord :=
match goal with
| H: MinusInfBZ >> Fin _ |- _ =>
contr
| H: MinusInfBZ >>= Fin _ |- _ =>
destruct H; [ contr | discr ]
| H: Fin ?m >>= Fin ?n |- _ =>
assert ((m >= n)%Z);
[ apply fin_ge_impl_ge; hyp
| clear H; arctic_ord
]
| |- Fin _ >>= MinusInfBZ => left; simpl; trivial
| |- Fin ?m >>= Fin ?n => apply ge_impl_fin_ge
| _ => try solve [contr | discr]
end.

Lemma plus_gt_compat : forall m n m' n',
m >> m' -> n >> n' -> m + n >> m' + n'.

Lemma plus_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m + n >>= m' + n'.

Lemma mult_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m * n >>= m' * n'.

Lemma arctic_plus_ge_monotone : forall (a b c : A),
a >>= c -> Aplus a b >>= c.

Lemma ge_A1_not_minusInf : forall a, a >>= A1 -> a <> MinusInfBZ.

End ArcticBZOrdSemiRingT.

Module ArcticBZOrdSemiRing := OrdSemiRing ArcticBZOrdSemiRingT.

Tropical ordered semi-ring

Module TropicalOrdSemiRingT <: OrdSemiRingType.

Module Export SR := TropicalSemiRingT.

Definition gt m n :=
match m, n with
| PlusInf, PlusInf => False
| PlusInf, _ => True
| TPos _, PlusInf => False
| TPos m, TPos n => m > n
end.

Definition ge m n := gt m n \/ m = n.

Lemma eq_ge_compat : forall x y, x = y -> ge x y.

Lemma gt_irrefl : irreflexive gt.

Instance gt_trans : Transitive gt.

Lemma gt_asym x y : gt x y -> ~gt y x.

Lemma gt_dec : rel_dec gt.

Lemma gt_Fin_WF x : Acc (transp gt) (TPos x).

Hint Resolve gt_Fin_WF.

Lemma gt_WF : WF gt.

Instance ge_refl : Reflexive ge.

Instance ge_trans : Transitive ge.

Lemma ge_antisym : antisymmetric ge.

Lemma ge_dec : rel_dec ge.

Notation "x + y" := (Aplus x y).
Notation "x * y" := (Amult x y).
Notation "x >>= y" := (ge x y) (at level 70).
Notation "x >> y" := (gt x y) (at level 70).

Lemma ge_gt_eq : forall x y, x >>= y -> x >> y \/ x = y.

Lemma ge_gt_compat : forall x y z, x >>= y -> y >> z -> x >> z.

Lemma ge_gt_compat2 : forall x y z, x >> y -> y >>= z -> x >> z.

Lemma pos_ord : forall m n,
TPos m >>= TPos n -> Peano.ge m n.

Lemma plus_inf_dec : forall m n,
{ exists p, (m = TPos p \/ n = TPos p) /\ m + n = TPos p} +
{ m + n = PlusInf /\ m = PlusInf /\ n = PlusInf }.

Lemma mult_inf_dec : forall m n,
{ exists mi, exists ni,
m = TPos mi /\ n = TPos ni /\ m * n = TPos (mi + ni) } +
{ m * n = PlusInf /\ (m = PlusInf \/ n = PlusInf) }.

Lemma ge_impl_pos_ge : forall m n, (m >= n)%nat -> TPos m >>= TPos n.

Lemma pos_ge_impl_ge : forall m n, TPos m >>= TPos n -> (m >= n)%nat.

Ltac tropical_ord :=
match goal with
| H: _ >> PlusInf |- _ => contr
| H: TPos _ >>= PlusInf |- _ =>
destruct H; [ contr | discr ]
| H: TPos ?m >>= TPos ?n |- _ =>
assert ((m >= n)%nat);
[ apply pos_ge_impl_ge; hyp
| clear H; tropical_ord
]
| |- PlusInf >>= TPos _ => left; simpl; trivial
| |- TPos ?m >>= TPos ?n => apply ge_impl_pos_ge
| _ => try solve [contr | discr]
end.

Lemma plus_gt_compat : forall m n m' n',
m >> m' -> n >> n' -> m + n >> m' + n'.

Lemma plus_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m + n >>= m' + n'.

Lemma mult_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m * n >>= m' * n'.

Lemma not_minusInf_ge_A1 : forall a, a <> PlusInf -> a >>= A1.

Lemma tropical_plus_inf_max : forall x, x <> PlusInf -> PlusInf >> x.

End TropicalOrdSemiRingT.

Module TropicalOrdSemiRing := OrdSemiRing TropicalOrdSemiRingT.

Semi-ring of booleans with order True > False

Module BOrdSemiRingT <: OrdSemiRingType.

Module Export SR := BSemiRingT.

Definition gt x y :=
match x, y with
| true, false => True
| _, _ => False
end.

Definition ge x y :=
match x, y with
| false, true => False
| _, _ => True
end.

Lemma eq_ge_compat : forall x y, x = y -> ge x y.

Notation "x + y" := (Aplus x y).
Notation "x * y" := (Amult x y).
Notation "x >> y" := (gt x y) (at level 70).
Notation "x >>= y" := (ge x y) (at level 70).

Instance ge_refl : Reflexive ge.

Instance ge_trans : Transitive ge.

Lemma ge_antisym : antisymmetric ge.

Lemma gt_irrefl : irreflexive gt.

Instance gt_trans : Transitive gt.

Lemma ge_dec : rel_dec ge.

Lemma gt_dec : rel_dec gt.

Lemma gt_WF : WF gt.

Lemma ge_gt_compat : forall x y z, x >>= y -> y >> z -> x >> z.

Lemma ge_gt_compat2 : forall x y z, x >> y -> y >>= z -> x >> z.

Lemma plus_gt_compat : forall m n m' n',
m >> m' -> n >> n' -> m + n >> m' + n'.

Lemma plus_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m + n >>= m' + n'.

Lemma mult_ge_compat : forall m n m' n',
m >>= m' -> n >>= n' -> m * n >>= m' * n'.

End BOrdSemiRingT.

Module BOrdSemiRing := OrdSemiRing BOrdSemiRingT.