semiring.v

Set Implicit Arguments.
Unset Strict Implicit.

Generalizable All Variables.

Require Export Basics Tactics Coq.Setoids.Setoid Morphisms.

Structure Setoid :=
  {
    carrier:> Type;
    equal: relation carrier;

    prf_Setoid:> Equivalence equal
  }.
Existing Instance prf_Setoid.
Notation Setoid_of eq := (@Build_Setoid _ eq _).

Notation "(== :> S )" := (equal (s:=S)).
Notation "(==)" := (== :> _).
Notation "x == y" := (equal x y) (at level 70, no associativity).
Notation "x == y :> S" := (equal (s:=S) x y)
  (at level 70, y at next level, no associativity).

Class isMap (X Y: Setoid)(f: X -> Y) :=
  map_subst:> Proper ((==) ==> (==)) f.

Structure Map (X Y: Setoid) :=
  {
    map_body:> X -> Y;

    prf_Map:> isMap map_body
  }.
Existing Instance prf_Map.
Notation makeMap f := (@Build_Map _ _ f _).
Notation "[ x .. y :-> p ]" := 
  (makeMap (fun x => .. (makeMap (fun y => p)) ..))
    (at level 200, x binder, y binder, right associativity,
     format "'[' [ x .. y :-> '/ ' p ] ']'"): map_scope.
Delimit Scope map_scope with map.

Class isBinop (X: Setoid)(op: X -> X -> X) :=
  binop_subst:> Proper ((==) ==> (==) ==> (==)) op.

Structure Binop (X: Setoid) :=
  {
    binop:> X -> X -> X;
    prf_Binop:> isBinop binop
  }.
Existing Instance prf_Binop.


Class Associative `(op: Binop X): Prop :=
  associative:>
    forall (x y z: X), op x (op y z) == op (op x y) z.

Class LIdentical `(op: Binop X)(e: X): Prop :=
  left_identical:> forall x: X, op e x == x.

Class RIdentical `(op: Binop X)(e: X): Prop :=
  right_identical:> forall x: X, op x e == x.

Class Identical `(op: Binop X)(e: X): Prop :=
  {
    identical_l:> LIdentical op e;
    identical_r:> RIdentical op e
  }.
Existing Instance identical_l.
Existing Instance identical_r.
Coercion identical_l: Identical >-> LIdentical.
Coercion identical_r: Identical >-> RIdentical.

Class LInvertible `{Identical X op e}(inv: Map X X): Prop :=
  left_invertible:>
    forall (x: X), op (inv x) x == e.

Class RInvertible `{Identical X op e}(inv: Map X X): Prop :=
  right_invertible:>
    forall (x: X), op x (inv x) == e.

Class Invertible `{Identical X op e}(inv: Map X X): Prop :=
  {
    invertible_l:> LInvertible inv;
    invertible_r:> RInvertible inv
  }.
Coercion invertible_l: Invertible >-> LInvertible.
Coercion invertible_r: Invertible >-> RInvertible.

Class Divisible `(op: Binop X)(divL divR: Binop X): Prop :=
  {
    divisible_l:>
      forall (a b: X), op (divL a b) a == b;
    divisible_r:>
      forall (a b: X), op a (divR a b) == b
  }.

Class Commute `(op: Binop X): Prop :=
  commute:>
    forall a b, op a b == op b a.

Class Distributive (X: Setoid)(add mul: Binop X) :=
  {
    distributive_l:>
      forall a b c, mul a (add b c) = add (mul a b) (mul a c);

    distributive_r:>
      forall a b c, mul (add a b) c = add (mul a c) (mul b c)
  }.

Module Monoid.
  Class spec (M: Setoid)(op: Binop M)(e: M) :=
    proof {
        associative:> Associative op;
        identical:> Identical op e
      }.

  Structure type :=
    make {
        carrier: Setoid;
        op: Binop carrier;
        e: carrier;

        prf: spec op e
      }.

  Module Ex.
    Existing Instance associative.
    Existing Instance identical.
    Existing Instance prf.

    Notation isMonoid := spec.
    Notation Monoid := type.

    Coercion associative: isMonoid >-> Associative.
    Coercion identical: isMonoid >-> Identical.
    Coercion carrier: Monoid >-> Setoid.
    Coercion prf: Monoid >-> isMonoid.

    Delimit Scope monoid_scope with monoid.
    Notation "x * y" := (op _ x y) (at level 40, left associativity): monoid_scope.
    Notation "'1'" := (e _): monoid_scope.
  End Ex.

End Monoid.
Export Monoid.Ex.

Section MonoidProps.
  Variable (M: Monoid).
  Open Scope monoid_scope.

  Lemma left_op:
    forall x y z: M,
      y == z -> x * y == x * z.
  Proof.
    intros.
    now rewrite H.
  Qed.

  Lemma right_op:
    forall x y z: M,
      x == y -> x * z == y * z.
  Proof.
    intros.
    now rewrite H.
  Qed.


  Lemma commute_l:
    forall `{Commute M (Monoid.op M)}(x y z: M), x * (y * z) == y * (x * z).
  Proof.
    intros; repeat rewrite associative.
    now rewrite (commute x y).
  Qed.
End MonoidProps.

Module SemiRing.
  Class spec (S: Setoid)(add: Binop S)(z: S)(mul: Binop S)(e: S) :=
    proof {
        add_monoid: isMonoid add z;
        add_commute:> Commute add;
        mul_monoid: isMonoid mul e;

        zero_l:
          forall a: S, mul z a == z;
        zero_r:
          forall a: S, mul a z == z
      }.

  Structure type :=
    make {
        carrier: Setoid;

        add: Binop carrier;
        z: carrier;

        mul: Binop carrier;
        e: carrier;

        prf: spec add z mul e
      }.

  Module Ex.
    Existing Instance add_monoid.
    Existing Instance add_commute.
    Existing Instance mul_monoid.
    Existing Instance prf.

    Notation isSemiRing := spec.
    Notation SemiRing := type.

    Coercion add_commute: isSemiRing >-> Commute.
    Coercion carrier: SemiRing >-> Setoid.
    Coercion prf: SemiRing >-> isSemiRing.

    Delimit Scope semiring_scope with srng.

    Notation "x + y" := (add _ x y): semiring_scope.
    Notation "x * y" := (mul _ x y): semiring_scope.
    Notation "'0'" := (z _): semiring_scope.
    Notation "'1'" := (e _): semiring_scope.
  End Ex.
  Import Ex.

  Canonical Structure a_monoid (R: SemiRing) := Monoid.make (add_monoid (S:=R)).
  Canonical Structure m_monoid (R: SemiRing) := Monoid.make (mul_monoid (S:=R)).

  Definition add_id_l {R: SemiRing}(x: R) := (@left_identical R (add R) (z R) (add_monoid (spec:=R)) x).
  Definition add_id_r {R: SemiRing}(x: R) := (@right_identical R (add R) (z R) (add_monoid (spec:=R)) x).
  Definition add_commute_l {R: SemiRing}(x y z: R) := (commute_l (M:=a_monoid R) x y z).

  Definition mul_id_l {R: SemiRing}(x: R) := (@left_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).
  Definition mul_id_r {R: SemiRing}(x: R) := (@right_identical R (mul R) (e R) (mul_monoid (spec:=R)) x).

End SemiRing.
Export SemiRing.Ex.

(* examples *)
Require Import Arith.

Canonical Structure nat_setoid := Setoid_of (@eq nat).

Program Instance plus_is_binop: isBinop (X:=nat_setoid) plus.
Canonical Structure plus_binop := Build_Binop plus_is_binop.

Program Instance plus_is_monoid: isMonoid plus_binop 0.
Next Obligation.
  intros x y z; simpl.
  apply plus_assoc.
Qed.
Next Obligation.
  split.
  - intros x; simpl; auto.
  - intros x; simpl.
    apply plus_0_r.
Qed.

Program Instance mult_is_binop: isBinop (X:=nat_setoid) mult.
Canonical Structure mult_binop := Build_Binop mult_is_binop.

Program Instance mult_is_monoid: isMonoid mult_binop 1.
Next Obligation.
  intros x y z; simpl.
  apply mult_assoc.
Qed.
Next Obligation.
  split.
  - intros x; simpl; auto.
  - intros x; simpl.
    apply mult_1_r.
Qed.

Program Instance plus_mult_is_semiring: isSemiRing plus_binop 0 mult_binop 1.
Next Obligation.
  intros x y; simpl.
  apply plus_comm.
Qed.
Canonical Structure plus_mult_semiring: SemiRing := SemiRing.make plus_mult_is_semiring.
Notation pms := plus_mult_semiring.

Open Scope semiring_scope.

Compute (3 + 2).
     (* = 5 *)
     (* : pms *)

Compute (3 * 2).
     (* = 6 *)
     (* : pms *)

Compute (0 + 4).
     (* = 4 *)
     (* : pms *)

Compute (0 * 4).
     (* = 0 *)
     (* : pms *)


Require Import Min.

(* nat with infinity *)
Inductive nat_inf :=
| num: nat -> nat_inf
| inf: nat_inf.

Notation "! n" := (num n) (at level 0).

Definition min_inf (n m: nat_inf): nat_inf :=
  match n, m with
  | inf, _ => m
  | _, inf => n
  | !n, !m => !(min n m)
  end.

Definition plus_inf (n m: nat_inf): nat_inf :=
  match n, m with
  | inf, _ | _, inf => inf
  | !n, !m => !(plus n m)
  end.

Canonical Structure nat_inf_setoid := Setoid_of (@eq nat_inf).

Program Instance min_inf_is_binop: isBinop (X:=nat_inf_setoid) min_inf.
Canonical Structure min_inf_binop := Build_Binop min_inf_is_binop.

Program Instance min_inf_is_monoid: isMonoid min_inf_binop inf.
Next Obligation.
  intros [x|] [y|] [z|]; simpl; auto.
  now rewrite min_assoc.
Qed.
Next Obligation.
  split; intros [x|]; simpl; auto.
Qed.


Program Instance plus_inf_is_binop: isBinop (X:=nat_inf_setoid) plus_inf.
Canonical Structure plus_inf_binop := Build_Binop plus_inf_is_binop.

Program Instance plus_inf_is_monoid: isMonoid plus_inf_binop !0.
Next Obligation.
  intros [x|] [y|] [z|]; simpl; auto.
  now rewrite plus_assoc.
Qed.
Next Obligation.
  split; intros [x|]; simpl; auto.
Qed.


Program Instance min_plus_is_semiring: isSemiRing min_inf_binop inf plus_inf_binop !0.
Next Obligation.
  intros [x|] [y|]; simpl; auto.
  now rewrite min_comm.
Qed.
Next Obligation.
  destruct a as [x|]; simpl; auto.
Qed.
Canonical Structure min_plus_semiring := SemiRing.make min_plus_is_semiring.

Notation mps := min_plus_semiring.
Open Scope semiring_scope.

Compute (!3 + !2).
     (* = !(2) *)
     (* : mps *)

Compute (!3 * !2).
     (* = !(5) *)
     (* : mps *)

Compute (!1 + !2).
     (* = !(1) *)
     (* : mps *)

Compute (!1 * !2).
     (* = !(3) *)
     (* : mps *)

Compute (inf + !4).
     (* = !(4) *)
     (* : mps *)

Compute (inf * !4).
     (* = inf *)
     (* : mps *)

Compute (!0 + inf).
     (* = !(0) *)
     (* : mps *)

Compute (!0 * inf).
     (* = inf *)
     (* : mps *)


Compute (!(5 + 2) + !6).
     (* = !(6) *)
     (* : mps *)

Compute (inf * !(3 + 1)).
     (* = inf *)
     (* : mps *)