Coq Nat Mon

nat.thy

Inductive Nat : Type :=
  | z : Nat
  | suc : Nat -> Nat.

Print Nat_ind.


Fixpoint plus (n m : Nat): Nat :=
  match n with
  | z => m
  | (suc x) => suc (plus x m)
  end.

Notation "n + m" := (plus n m).


Theorem test : forall (n : Nat), z + n = n.
Proof. intros n. auto. Qed.



Theorem test2 : forall (n : Nat), n + z = n.
Proof.
  intros n. induction n.
  - simpl. reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.


Theorem plusassoc : forall (a b c : Nat), a + (b + c) = (a + b) + c.
Proof.
  intros .
  induction a.
  - simpl. reflexivity.
  - simpl. rewrite IHa. reflexivity.
Qed.

// Defining a Semigroup on a carrier (set/type) A
Record SemiGroup (A : Type) := {
  op : A -> A -> A ;
  assoc : forall (a b c : A), op a (op  b c) = op (op a b) c 
}.

Definition natsemi : SemiGroup Nat := 
 {|
    op := plus;
    assoc := plusassoc
  |}.


// Defining a Monoid with a carrier (set/type) A
Record Monoid (A : Type) := {
  e : A;
  mop : A -> A -> A ;

  massoc : forall (a b c : A), mop a (mop b c) = mop (mop a b) c;
  lunit : forall (a : A), mop e a = a ;
  runit : forall (a : A), mop a e = a
}.

Definition natMon : Monoid Nat := 
  {|
    e := z;
    mop := plus;
    massoc := plusassoc;
    lunit := test;
    runit := test2
  |}.