gistfile1.coq

Require Import Program.Basics.
Require Import Arith.Le.
Require Import Omega.
Require Import Classes.Equivalence.
Require Import Classes.SetoidClass.

Set Implicit Arguments.
Unset Strict Implicit.

Class Category (T:Type)(Mor : T -> T -> Type)(smor : forall A B, Setoid (Mor A B)) := {
(* existence of id and compose *)
    idC : forall {A}, Mor A A
  ; composeC : forall {A B C}, Mor B C -> Mor A B -> Mor A C

(* Proofs
  ; left_identity : forall A B (f:Mor A B),
      equiv (composeC idC f) f
  ; right_identity : forall A B (f:Mor A B),
      equiv (composeC f idC) f
  ; associativity : forall A B C D (f:Mor A B)(g:Mor B C)(h:Mor C D),
      equiv (composeC (composeC h g) f) (composeC h (composeC g f))
*)
}.

Section Commutativity.

Variable T : Type.
Variable Mor : T -> T -> Type.
Variable smor : forall A B, Setoid (Mor A B).
Variable Cat : Category smor.
Variable A B C : T.

Definition commute (f : Mor A B)(g : Mor B C)(h : Mor A C) :=
  composeC g f == h.

End Commutativity.

Section Products.
Variable T : Type.
Variable Mor : T -> T -> Type.
Variable smor : forall A B, Setoid (Mor A B).

Class Product P (CP : Category smor) := {
    proj1 : forall {A B}, Mor (P A B) A
  ; proj2 : forall {A B}, Mor (P A B) B
  ; mediating : forall {A B X}, Mor X A -> Mor X B -> Mor X (P A B)

(* Proofs
  ; med_commute1 : forall A B X (f : Mor X A)(g : Mor X B),
      commute CP (mediating f g) proj1 f
  ; med_commute2 : forall A B X (f : Mor X A)(g : Mor X B),
      commute CP(mediating f g) proj2 g
  ; med_unique : forall A B X (f : Mor X A)(g : Mor X B)(h : Mor X (P A B)),
      commute CP h proj1 f -> commute CP h proj2 g
        -> h == mediating f g
*)
}.

(* mediating = (&&&) *)

End Products.

Section Parallel.

Variable T : Type.
Variable Mor : T -> T -> Type.
Variable smor : forall A B, Setoid (Mor A B).
Variable CP : Category smor.
Variable P : T -> T -> T.
Variable Prod : Product P CP.

Variable A B C D : T.

Definition parallel (f : Mor A B)(g : Mor C D) : Mor (P A C) (P B D) :=
  mediating (composeC f (@proj1 T Mor smor P CP Prod A C))
   (composeC g (@proj2 T Mor smor P CP Prod A C)).

(* parallel = (***) *)

End Parallel.

Section Functions.
(* Ordinal tuples are products *)

Definition Map A B := A -> B.

Definition eq_ext {A B}(f g : A -> B) := forall x, f x = g x.

Theorem refl_ext : forall A B f, (@eq_ext A B) f f.
Proof.
unfold eq_ext. auto.
Qed.

Theorem symm_ext : forall A B (f g :A -> B),
  eq_ext f g -> eq_ext g f.
Proof.
unfold eq_ext. auto.
Qed.

Theorem trans_ext : forall A B (f g h : A -> B),
  eq_ext f g -> eq_ext g h -> eq_ext f h.
Proof.
unfold eq_ext. eauto using eq_trans.
Qed.

Instance ReflExt : forall A B, Reflexive (@eq_ext A B) := {
    reflexivity := (@refl_ext A B)
}.

Instance SymmExt : forall A B, Symmetric (@eq_ext A B) := {
    symmetry := @symm_ext A B
}.

Instance TransExt : forall A B, Transitive (@eq_ext A B) := {
    transitivity := @trans_ext A B
}.

Instance EquivExt : forall A B, Equivalence (@eq_ext A B) := {
    Equivalence_Reflexive := @ReflExt A B
  ; Equivalence_Symmetric := @SymmExt A B
  ; Equivalence_Transitive := @TransExt A B
}.

Instance EqMor : forall A B, Setoid (Map A B) := {
    equiv := eq_ext
}.

Instance Func : Category EqMor := {
    idC A := id
  ; composeC A B C := compose
}.

Instance Prod : Product prod Func := {
    proj1 A B := fst
  ; proj2 A B := snd
  ; mediating A B X := fun f g x => (f x, g x)
}.

End Functions.

Section Orders.
(* max of nat is a product *)

Theorem ge_n : forall n, n >= n.
Proof.
auto with arith.
Qed.

Theorem ge_trans' : forall n m p, m >= p -> n >= m -> n >= p.
Proof.
intros. eauto using le_trans.
Qed.

Definition eq_ge n m (p q : ge n m) := True.

Instance EquivGe : forall n m, Equivalence (@eq_ge n m).
Proof.
intros. constructor;constructor.
Qed. 

Instance EqGe : forall n m, Setoid (ge n m) := {
    equiv := (@eq_ge n m)
}.

Instance Order : Category EqGe := {
    idC := ge_n
  ; composeC := ge_trans'
}.

Lemma max_val : forall n m, max n m = n \/ max n m = m.
Proof.
intros.
destruct (le_or_lt n m);[right|left];[apply max_r|apply max_l]; auto with arith.
Qed.

Theorem max_med : forall n m x, n <= x -> m <= x -> max n m <= x.
Proof.
intros.
destruct (max_val n m); intuition.
Qed.

Theorem max_ge1 : forall n m, max n m >= n.
Proof.
intros.
destruct (max_val n m); intuition.
Qed.

Theorem max_ge2 : forall n m, max n m >= m.
Proof.
intros.
destruct (max_val n m); intuition.
Qed.

Instance Max : Product max Order := {
    proj1 := max_ge1
  ; proj2 := max_ge2
  ; mediating := max_med
}.

(* an application of parralel (***) *)

Theorem parralel_max : forall n m l k, n >= m -> l >= k -> max n l >= max m k.
Proof.
apply (@parallel nat ge EqGe Order).
apply Max.
Qed.

End Orders.