# Library CoLoR.Util.Algebra.SemiRing

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2009-03-19 (setoid)
Semi-ring structure.

Semi-ring structure type

Module Type SemiRingType.

Declare Module Export ES : Eqset_dec.

Parameters A0 A1 : A.

Parameter Aplus : A -> A -> A.
Notation "x + y" := (Aplus x y).

Declare Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Parameter Amult : A -> A -> A.
Notation "x * y" := (Amult x y).

Declare Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Parameter A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.

End SemiRingType.

Some derived results about the semi-ring structure

Module SemiRing (SR : SemiRingType).

Export SR.

Definition Amult_comm := SRmul_comm A_semi_ring.
Definition Amult_assoc := SRmul_assoc A_semi_ring.
Definition Amult_0_l := SRmul_0_l A_semi_ring.
Definition Amult_1_l := SRmul_1_l A_semi_ring.
Definition A_plus_mult_distr_l := SRdistr_l A_semi_ring.

Lemma Aplus_0_r n : n + A0 =A= n.

Lemma Amult_0_r n : n * A0 =A= A0.

Lemma Amult_1_r n : n * A1 =A= n.

Lemma A_plus_mult_distr_r m n p : m * (n + p) =A= m * n + m * p.

Hint Rewrite Aplus_0_l Aplus_0_r Amult_0_l Amult_0_r
Amult_1_l Amult_1_r : arith.

End SemiRing.

Natural numbers as a semi-ring

Module Nat <: SetA.
Definition A := nat.
End Nat.

Module Nat_Eqset := Eqset_def Nat.

Module Nat_Eqset_dec <: Eqset_dec.
Module Export Eq := Nat_Eqset.
Definition eqA_dec := dec_beq beq_nat_ok.
End Nat_Eqset_dec.

Module NSemiRingT <: SemiRingType.

Module Export ES := Nat_Eqset_dec.

Definition A0 := 0.
Definition A1 := 1.

Definition Aplus := plus.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult := mult.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Definition A_semi_ring := natSRth.

End NSemiRingT.

Module NSemiRing := SemiRing NSemiRingT.

BigN natural numbers as a semi-ring

Module BigNat_Eqset <: Eqset.
Definition A := bigN.
Definition eqA := BigN.eq.
Instance eqA_Equivalence : Equivalence eqA.
End BigNat_Eqset.

Module BigNat_Eqset_dec <: Eqset_dec.
Module Export Eq := BigNat_Eqset.
Lemma eqA_dec : forall x y, {eqA x y}+{~eqA x y}.
End BigNat_Eqset_dec.

Module BigNSemiRingT <: SemiRingType.

Module Export ES := BigNat_Eqset_dec.

Definition A0 := BigN.zero.
Definition A1 := BigN.one.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult := BigN.mul.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Definition A_semi_ring := BigNring.

End BigNSemiRingT.

Module BigNSemiRing := SemiRing BigNSemiRingT.

Integers as a semi-ring

Module Int <: SetA.
Definition A := Z.
End Int.

Module Int_Eqset := Eqset_def Int.

Module Int_Eqset_dec <: Eqset_dec.
Module Export Eq := Int_Eqset.
Definition eqA_dec := dec_beq beq_Z_ok.
End Int_Eqset_dec.

Module ZSemiRingT <: SemiRingType.

Module Export ES := Int_Eqset_dec.

Definition A0 := 0%Z.
Definition A1 := 1%Z.

Definition Aplus := Zplus.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult := Zmult.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.

End ZSemiRingT.

Module ZSemiRing := SemiRing ZSemiRingT.

BigZ integers as a semi-ring

Module BigInt_Eqset <: Eqset.
Definition A := bigZ.
Definition eqA := BigZ.eq.
Instance eqA_Equivalence : Equivalence eqA.
End BigInt_Eqset.

Module BigInt_Eqset_dec <: Eqset_dec.
Module Export Eq := BigInt_Eqset.
Lemma eqA_dec : forall x y, {eqA x y}+{~eqA x y}.
End BigInt_Eqset_dec.

Module BigZSemiRingT <: SemiRingType.

Module Export ES := BigInt_Eqset_dec.

Definition A0 := BigZ.zero.
Definition A1 := BigZ.one.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult := BigZ.mul.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.

End BigZSemiRingT.

Module BigZSemiRing := SemiRing BigZSemiRingT.

Arctic semi-ring over naturals with minus infinity and plus-max operations

Inductive ArcticDom : Type :=
| Pos (n : nat)
| MinusInf.

Definition beq_ArcticDom x y :=
match x, y with
| Pos x', Pos y' => beq_nat x' y'
| MinusInf, MinusInf => true
| _, _ => false
end.

Lemma beq_ArcticDom_ok : forall x y, beq_ArcticDom x y = true <-> x = y.

Definition is_finite v :=
match v with
| MinusInf => false
| _ => true
end.

Lemma is_finite_ok : forall v, is_finite v = true <-> v <> MinusInf.

Module Arctic <: SetA.
Definition A := ArcticDom.
End Arctic.

Module Arctic_Eqset := Eqset_def Arctic.

Module Arctic_Eqset_dec <: Eqset_dec.
Module Export Eq := Arctic_Eqset.
Definition eqA_dec := dec_beq beq_ArcticDom_ok.
End Arctic_Eqset_dec.

Module ArcticSemiRingT <: SemiRingType.

Module Export ES := Arctic_Eqset_dec.

Definition A0 := MinusInf.
Definition A1 := Pos 0.

Definition Aplus m n :=
match m, n with
| MinusInf, n => n
| m, MinusInf => m
| Pos m, Pos n => Pos (max m n)
end.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult m n :=
match m, n with
| MinusInf, _ => MinusInf
| _, MinusInf => MinusInf
| Pos m, Pos n => Pos (m + n)
end.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Lemma A_plus_comm m n : Aplus m n = Aplus n m.

Lemma A_plus_assoc m n p : Aplus m (Aplus n p) = Aplus (Aplus m n) p.

Lemma A_mult_comm m n : Amult m n = Amult n m.

Lemma A_mult_assoc m n p : Amult m (Amult n p) = Amult (Amult m n) p.

Import Compare. Import Max.

Lemma A_mult_plus_distr m n p :
Amult (Aplus m n) p = Aplus (Amult m p) (Amult n p).

Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.

Lemma arctic_plus_notInf_left a b : a <> MinusInf -> Aplus a b <> MinusInf.

Lemma arctic_mult_notInf a b :
a <> MinusInf -> b <> MinusInf -> Amult a b <> MinusInf.

End ArcticSemiRingT.

Module ArcticSemiRing := SemiRing ArcticSemiRingT.

Arctic semi-ring over integers with minus infinity and plus-max operations

Inductive ArcticBZDom : Type :=
| Fin (z : Z)
| MinusInfBZ.

Definition beq_ArcticBZDom x y :=
match x, y with
| Fin x', Fin y' => beq_Z x' y'
| MinusInfBZ, MinusInfBZ => true
| _, _ => false
end.

Lemma beq_ArcticBZDom_ok x y : beq_ArcticBZDom x y = true <-> x = y.

Module ArcticBZ <: SetA.
Definition A := ArcticBZDom.
End ArcticBZ.

Module ArcticBZ_Eqset := Eqset_def ArcticBZ.

Module ArcticBZ_Eqset_dec <: Eqset_dec.
Module Export Eq := ArcticBZ_Eqset.
Definition eqA_dec := dec_beq beq_ArcticBZDom_ok.
End ArcticBZ_Eqset_dec.

Module ArcticBZSemiRingT <: SemiRingType.

Module Export ES := ArcticBZ_Eqset_dec.

Definition A0 := MinusInfBZ.
Definition A1 := Fin 0.

Definition Aplus m n :=
match m, n with
| MinusInfBZ, n => n
| m, MinusInfBZ => m
| Fin m, Fin n => Fin (Zmax m n)
end.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult m n :=
match m, n with
| MinusInfBZ, _ => MinusInfBZ
| _, MinusInfBZ => MinusInfBZ
| Fin m, Fin n => Fin (m + n)
end.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Lemma A_plus_comm m n : Aplus m n = Aplus n m.

Lemma A_plus_assoc m n p : Aplus m (Aplus n p) = Aplus (Aplus m n) p.

Lemma A_mult_comm m n : Amult m n = Amult n m.

Lemma A_mult_assoc m n p : Amult m (Amult n p) = Amult (Amult m n) p.

Lemma A_mult_plus_distr m n p :
Amult (Aplus m n) p = Aplus (Amult m p) (Amult n p).

Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.

Lemma arctic_plus_notInf_left a b :
a <> MinusInfBZ -> Aplus a b <> MinusInfBZ.

Lemma arctic_mult_notInf a b :
a <> MinusInfBZ -> b <> MinusInfBZ -> Amult a b <> MinusInfBZ.

End ArcticBZSemiRingT.

Module ArcticBZSemiRing := SemiRing ArcticBZSemiRingT.

Tropical semi-ring over naturals with plus infinity and plus-min operations

Inductive TropicalDom : Type :=
| TPos (n : nat)
| PlusInf.

Definition tropical_is_finite v :=
match v with
| PlusInf => false
| _ => true
end.

Lemma tropical_is_finite_ok v : tropical_is_finite v = true <-> v <> PlusInf.

Definition beq_TropicalDom x y :=
match x, y with
| TPos x', TPos y' => beq_nat x' y'
| PlusInf, PlusInf => true
| _, _ => false
end.

Lemma beq_TropicalDom_ok x y : beq_TropicalDom x y = true <-> x = y.

Module Tropical <: SetA.
Definition A := TropicalDom.
End Tropical.

Module Tropical_Eqset := Eqset_def Tropical.

Module Tropical_Eqset_dec <: Eqset_dec.
Module Export Eq := Tropical_Eqset.
Definition eqA_dec := dec_beq beq_TropicalDom_ok.
End Tropical_Eqset_dec.

Module TropicalSemiRingT <: SemiRingType.

Module Export ES := Tropical_Eqset_dec.

Definition A0 := PlusInf.
Definition A1 := TPos 0.

Definition Aplus m n :=
match m, n with
| PlusInf, n => n
| m, PlusInf => m
| TPos m, TPos n => TPos (min m n)
end.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult m n :=
match m, n with
| PlusInf, _ => PlusInf
| _, PlusInf => PlusInf
| TPos m, TPos n => TPos (m + n)
end.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Lemma A_plus_comm m n : Aplus m n = Aplus n m.

Lemma A_plus_assoc m n p : Aplus m (Aplus n p) = Aplus (Aplus m n) p.

Lemma A_mult_comm m n : Amult m n = Amult n m.

Lemma A_mult_assoc m n p : Amult m (Amult n p) = Amult (Amult m n) p.

Import Compare. Import Min.

Lemma A_mult_plus_distr m n p :
Amult (Aplus m n) p = Aplus (Amult m p) (Amult n p).

Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.

Lemma tropical_plus_notInf_left a b :
a <> PlusInf -> Aplus a b <> PlusInf.

Lemma tropical_mult_notInf a b :
a <> PlusInf -> b <> PlusInf -> Amult a b <> PlusInf.

End TropicalSemiRingT.

Module TropicalSemiRing := SemiRing TropicalSemiRingT.

Semi-ring of booleans with 'or' and 'and'

Module Bool <: SetA.
Definition A := bool.
End Bool.

Module Bool_Eqset := Eqset_def Bool.

Module Bool_Eqset_dec <: Eqset_dec.
Module Export Eq := Bool_Eqset.
Definition eqA_dec := bool_dec.
End Bool_Eqset_dec.

Module BSemiRingT <: SemiRingType.

Module Export ES := Bool_Eqset_dec.

Definition A0 := false.
Definition A1 := true.

Definition Aplus := orb.

Instance Aplus_mor : Proper (eqA ==> eqA ==> eqA) Aplus.

Definition Amult := andb.

Instance Amult_mor : Proper (eqA ==> eqA ==> eqA) Amult.

Lemma A_semi_ring : semi_ring_theory A0 A1 Aplus Amult eqA.

End BSemiRingT.

Module BSemiRing := SemiRing BSemiRingT.