Require Export Relations.
Implicits reflexive   [1].
Implicits symmetric   [1].
Implicits transitive  [1].

Record is_Setoid [A:Set; eq:(relation A)] : Prop :=
  { ax_eq_reflexive    : (reflexive eq);
    ax_eq_symmetric    : (symmetric eq);
    ax_eq_transitive   : (transitive eq)
  }.

Record Setoid : Type :=
  { crr   :> Set;
    eq    :  (relation crr);
    proof :  (is_Setoid crr eq)
  }.

Implicits eq [1].

Infix NONA 8 "[=]" eq.
Syntax constr level 8:
  eq_infix [ (eq $_ $e1 $e2) ] ->
    [[<hov 1> $e1:L [0 1] " [=] " $e2:L]].


Definition neq [S: Setoid] : (relation S)
                               := [x,y:S]~(x [=] y).

Implicits neq [1].

Infix NONA 8 "[~=]" neq.
Syntax constr level 8:
  neq_infix [(neq $_ $e1 $e2)] ->
    [[<hov 1> $e1:L [0 1] " [~=] " $e2:L]].

Check eq.
Check Build_Setoid.
Check Setoid.
Print Setoid.

Section Setoid_basics.
Variable S : Setoid.

Lemma eq_reflexive_unfolded : (x:S)(x [=] x).
Intro x.
Apply ax_eq_reflexive. 
Apply proof. 
Qed.

Lemma eq_symmetric_unfolded : (x,y:S)(x [=] y)->(y [=] x).
Intros x y Hxy.
Apply ax_eq_symmetric. 
Apply proof. 
Assumption.
Qed.


Lemma eq_transitive_unfolded : (x,y,z:S)(x [=] y)->(y [=] z)->(x [=] z).
Intros x y z Hxy Hyz.
Exact (ax_eq_transitive ?? (proof S) x y z Hxy Hyz). 
Qed.


Section setoid_functions.
Variables S1, S2, S3 :Setoid.

Section binary_functions.

Variable f : S1 -> S2 -> S3.

Definition bin_fun_well_def : Prop :=
  (x1, x2: S1)(y1, y2: S2)
   (x1 [=] x2) -> (y1 [=] y2) -> ((f x1 y1) [=] (f x2 y2)).

End binary_functions.

Record Setoid_bin_fun : Set :=
  { bf_fun      :> S1 -> S2 -> S3;
    bf_well_def :  (bin_fun_well_def bf_fun)
  }.

Lemma bf_wd : (f:Setoid_bin_fun)(bin_fun_well_def f).
Intro f.
Apply bf_well_def.
Qed.

Lemma csetoid_bfun_wd_unfolded : (f:Setoid_bin_fun)(x,x':S1)(y,y':S2)
	(x[=]x')->(y[=]y')->((f x y)[=](f x' y')).
Proof.
Intros f x x' y y' Hx Hy.
Apply (bf_wd f x x' y y').
Assumption.
Assumption.
Qed.
End setoid_functions.

(* Exercise 1a: Define 
   "Is_Monoid [A:Setoid; one:A; op:(Setoid_bin_fun A A A)] : Prop 
   via a Record type construction as above *)

(* Exercise 1b: Define the Record Type Monoid : Type 
   with a coercion to Setoid *)

(* Exercise 2a: Make the natural numbers into a Setoid *)

(* Exercise 2b: Make the natural numbers into a Monoid *)

(* Exercise 3a: Define equality on binary functions, i.e. define
   fun_eq [f,g : (Setoid_bin_fun S1 S2 S3)] : Prop 
   representing function equality

(* Exercise 3b: Construct the Setoid of Binary functions *)

(* Exercise 3c: Construct the Monoid of Binary functions over a setoid,
   so the elements are now the f : (Setoid_bin_fun S S S)
   and the monoid operation is composition *)