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)
  • Adam Koprowski, 2007-04-14
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 Aplus_comm := SRadd_comm A_semi_ring.
  Definition Aplus_assoc := SRadd_assoc A_semi_ring.
  Definition Aplus_0_l := SRadd_0_l A_semi_ring.
  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.

  Add Ring Aring : A_semi_ring.

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.

  Definition Aplus := BigN.add.

  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.

  Definition Aplus := BigZ.add.

  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.