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)
  • Adam Koprowski, 2007-04-14
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.