(* 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.