(* MGS 08 : COQ

2nd exercise

*)

Section georg.

(* Show that a commutative, idempotent monoid induces a partial order
   inspired by Georg's course.
 *)

Variable A:Set.

Variable add : A -> A -> A.
Variable zero : A.

Notation "a + b" := (add a b).

Axiom assoc : forall a b c:A,a + (b + c) = (a + b) + c.
Axiom unit : forall a:A,zero + a = a.
Axiom comm : forall a b:A,a + b = b + a.
Axiom idem : forall a:A, a+a = a.

Definition le (a b : A) : Prop := a+b = b.

Notation "a <= b" := (le a b).

Lemma le_refl : forall a:A,a <= a.

Lemma le_trans : forall a b c:A,a<=b -> b<=c -> a<=c.

Lemma le_antisym : forall a b:A,a <= b -> b <= a -> a=b.

Lemma le_toni : forall a a' b : A, a <= a' -> a+b <= a'+b.

Lemma le_unit : forall a:A, unite <= A. 

End georg.

Section graham.

(* Show that the composite of injective/surjective functions
   is injective/surjective.
   Suggested by Graham Hutton.
*)

Set Implicit Arguments.

Section defs.

Variables A B C : Set.

Definition inj (f : A -> B) : Prop :=
  forall a b:A, f a = f b -> a = b.

Definition surj (f : A -> B) : Prop :=
  forall b:B,exists a:A,f a = b.

Definition comp (g : B -> C) (f : A -> B) : A -> C :=
  fun a:A => g (f a).

End defs.

Variables A B C : Set.
Variable f : A -> B.
Variable g : B -> C.

Lemma inj_comp : inj f -> inj g -> inj (comp g f).

Lemma surj_comp : surj f -> surj g -> surj (comp g f).

End graham.