Setoids

(* DEFINITION OF SETOID, i. e. a set with an equivalence relation.  *)
(*    Venanzio Capretta, January 1999.                              *)
(*    Coq version 6.2.3                                             *)

Require Export Relations.
Require Export Eqdep.

Syntactic Definition Reflexive := (reflexive ?).
Syntactic Definition Symmetric := (symmetric ?).
Syntactic Definition Transitive := (transitive ?).
Syntactic Definition Equiv := (equiv ?).

Implicit Arguments On.

Record Setoid : Type := setoid
  { s_el :> Set;
    s_eq : (relation s_el);
    s_proof : (Equiv s_eq)
  }.

(* We define an infix notation for equality of setoid elements. *)
Infix 5 "[=]" s_eq.

(* We want functions that extract the proofs from a setoid. *)

Lemma s_reflexivity : (S:Setoid)(x:S)x[=]x.

Lemma s_symmetry : (S:Setoid)(x,y:S)x[=]y -> y[=]x.

Lemma s_transitivity : (S:Setoid)(x,y,z:S)x[=]y -> y[=]z -> x[=]z.

Hints Resolve s_reflexivity s_symmetry s_transitivity : setoids.

(* The hint s_transitivity is only used by EAuto with sets setoids, not by Auto with sets setoids. *)

(* SETS AS SETOIDS                                     *)
(* A type with Leibniz equality is trivially a setoid. *)

Section Set_setoids.

Variable A : Set.

Remark eq_equiv : (Equiv (eq A)).

Definition S_set : Setoid := (!setoid A (eq A) eq_equiv).

End Set_setoids.

(* UNIT SETOID *)

Definition S_unit := (S_set unit).

(* PREDICATES OVER A SETOID.                      *)
(* They must be invariant by the setoid equality. *)

Definition Predicate_well_defined : (S : Setoid)(S -> Prop) -> Prop :=
  [S : Setoid][pred : S -> Prop]
  (x, y : S)(x [=] y) -> (pred x) -> (pred y).

(* The type of predicates over a setoid S. *)
Record Setoid_predicate [S : Setoid] : Type := setoid_predicate
  { sp_pred :> S -> Prop;
    sp_proof : (Predicate_well_defined sp_pred)
  }.

(* RELATIONS OVER A SETOID. *)

Definition Relation_well_defined : (S : Setoid)(relation S) -> Prop :=
  [S, rel](x1,x2,y1,y2:S)(x1 [=] x2) -> (y1 [=] y2) ->
                         (rel x1 y1) -> (rel x2 y2).

(* The type of relations over a setoid S. *)
Record Setoid_relation [S : Setoid] : Type := setoid_relation
  { sr_rel :> S -> S -> Prop;
    sr_proof : (Relation_well_defined sr_rel)
  }.

(* The type of equivalence relations over a setoid. *)
Record Setoid_equivalence [S:Setoid] : Type := setoid_equivalence
  { se_rel :> (Setoid_relation S);
    se_proof : (Equiv se_rel)
  }.

(* For a setoid with Leibniz equality, every predicate or relation *)
(* is well-defined.                                                *)

Section Leibniz_Equality_Predicates_Relations.

Variable A : Set.
Variable P : A -> Prop.

Local S := (S_set A).

Remark leibniz_pred_well_defined : (Predicate_well_defined 1!S P).

(* So every predicate is a setoid predicate. *)
Definition leibniz_eq_predicate : (Setoid_predicate S) :=
  (setoid_predicate leibniz_pred_well_defined).

Variable R : (relation A).

Remark leibniz_rel_well_defined : (Relation_well_defined 1!S R).

Definition leibniz_eq_relation : (Setoid_relation S) :=
  (setoid_relation leibniz_rel_well_defined).

End Leibniz_Equality_Predicates_Relations.

(* SUBSETOIDS. *)

(* If P is a predicate over the setoid S, then we want to define   *)
(* the setoid whose elements are the elements of S that satisfy P. *)
(* This is done with a sigma type.                                 *)

Section Subsetoids.

Variable S : Setoid.

Variable P : (Setoid_predicate S).

Definition subsetoid_carrier : Set := (sig S P).

Definition sub_s_elem : (x:S)(P x) -> subsetoid_carrier :=
  (exist S P).

(* The definition of the equality for the subsetoid is inherited from *)
(* the setoid S. The equality does not depend on the proof of (P x).  *)

Definition subsetoid_eq : (relation subsetoid_carrier) :=
  [a, b : subsetoid_carrier]
  (proj1_sig ? ? a) [=] (proj1_sig ? ? b).

Lemma subsetoid_eq_equiv : (Equiv subsetoid_eq).

Definition subsetoid : Setoid :=
  (setoid subsetoid_eq_equiv).

Definition s_inj : subsetoid -> S :=
  [a : subsetoid](proj1_sig ? ? a).

Definition subsetoid_el := (s_el subsetoid).

(* It would be nice to be able to declare s_inj as a coercion :   *)
(* Coercion s_inj : subsetoid_carrier >-> s_el.                   *)
(* But this would cause some side effects: the coercion from      *)
(* S_Fun to Setoid_function (defined below) would not work.       *)
(* This is due to the fact that s_el would be at the same time a  *)
(* coercion and a class.                                          *)

(* This extracts the proof that the given element satisfies  *)
(* the defining predicate.                                   *)
Definition ss_proof : (a : subsetoid)(P (s_inj a)) :=
  [a : subsetoid](proj2_sig ? ? a).

End Subsetoids.

(* PRODUCTS OF SETOIDS *)

Section Setoid_Product.

Variables S1, S2 : Setoid.

Local C := S1*S2.

Local C_eq : (relation C) :=
  [z1, z2 : C](Fst z1) [=] (Fst z2) /\
              (Snd z1) [=] (Snd z2).

Remark C_equivalence : (Equiv C_eq).

Definition S_prod : Setoid := (setoid C_equivalence).

End Setoid_Product.

Infix 7 "[*]" S_prod.

(* FUNCTIONS FROM A SETOID TO ANOTHER SETOID.        *)
(* Such functions must preserve the setoid equality. *)

Section Setoid_functions.

Variables S1, S2 : Setoid.

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

Record Setoid_function : Set := setoid_function
  { s_function :> S1 -> S2;
    s_fun_proof : (fun_well_defined s_function)
  }.

(* Extensional equality of functions. *)
Definition extensional_eq : (relation Setoid_function) :=
  [f, g : Setoid_function]
  (x : S1)(f x)[=](g x).

(* Extensional equality is an equivalence relation. *)

Lemma extensional_eq_reflexive : (Reflexive extensional_eq).

Lemma extensional_eq_symmetric : (Symmetric extensional_eq).

Lemma extensional_eq_transitive : (Transitive extensional_eq).

Lemma extensional_eq_equivalence : (Equiv extensional_eq).

(* So the functions between two setoid form a setoid. *)
Definition S_Fun : Setoid :=
  (setoid extensional_eq_equivalence).

(* Applying equal functions to equal object yields equal results. *)
Lemma eq_fun_args
  : (f1, f2 : S_Fun)f1[=]f2 ->
    (x1, x2 : S1) x1[=]x2 ->
    (f1 x1)[=](f2 x2).

Hints Resolve eq_fun_args : setoids.

(* Definition of injection, surjection and bijection  *)
(* between setoids.                                   *)

Definition injective : S_Fun -> Prop :=
  [f : S_Fun]
  (x, y : S1)(f x) [=] (f y) -> x [=] y.

Definition weak_surjective : S_Fun -> Prop :=
  [f : S_Fun]
  (y : S2)(EX x:S1 | (f x) [=] y).

Definition weak_bijective : S_Fun -> Prop :=
  [f : S_Fun]
  (injective f) /\ (weak_surjective f).

(* In Coq it is not possible to define an element of a Set by *)
(* elimination over a Prop, and therefore with the previous   *)
(* it is not possible to build an inverse of f.               *)
(* We then need the following stronger definition.            *)
Definition surjective : S_Fun -> Set :=
  [f : S_Fun]
  (y : S2)(sig S1 [x:S1](f x) [=] y).

(* Note that we cannot define (bijective f) as                      *)
(* (injective f) /\ (surjective f) because (surjective f) is a Set  *)
(* not a Prop. Also (bijective f) must be a Set if we want to be    *)
(* able to define an inverse.                                       *)
Inductive bijective : S_Fun -> Set :=
  is_bijective : (f : S_Fun)
                 (injective f) -> (surjective f) ->
                 (bijective f).

(* Being and injection or a surjection is an invariant property  *)
(* with respect to the extensional equality.                     *)

Lemma injective_well_defined :
  (Predicate_well_defined injective).

Lemma surjective_well_defined :
  (f, g : S_Fun)f [=] g -> (surjective f) -> (surjective g).

Record Bijection : Set := bijection
  { b_function : S_Fun;
    b_proof : (bijective b_function)
  }.

(* Bijection cannot be defined as a subsetoid of S_Fun because   *)
(* the predicate bijective needs to be a Set predicate in order  *)
(* to be able to extract an inverse function.                    *)

Lemma bijection_is_injective :
  (f : Bijection)(injective (b_function f)).

Lemma bijection_is_surjective :
  (f : Bijection)(surjective (b_function f)).

End Setoid_functions.

Infix RIGHTA 7 "[->]" S_Fun.

(* The identity is always a setoid bijection. *)

Section Setoid_Identity.

Variable S : Setoid.

Local id_funct : S -> S := [x:S]x.

Lemma id_well_defined : (fun_well_defined id_funct).

Definition s_id : S [->] S :=
  (setoid_function id_well_defined).

Lemma id_inj : (injective s_id).

Lemma id_surj : (surjective s_id).

Lemma id_bij : (bijective s_id).

Definition s_id_bij : (Bijection S S) := (bijection id_bij).

End Setoid_Identity.

(* Composition of setoid fuctions. *)

Section Setoid_Functions_Composition.

Variables S1, S2, S3 : Setoid.

Variable g : S2 [->] S3.
Variable f : S1 [->] S2.

Local fun_comp : S1 -> S3 :=
  [x : S1](g (f x)).

Lemma fun_comp_well_defined : (fun_well_defined fun_comp).

Definition s_fun_comp : S1 [->] S3 :=
  (setoid_function fun_comp_well_defined).

End Setoid_Functions_Composition.

Infix 7 "[o]" s_fun_comp.

(* Inverse of a bijection. *)

Section Inverse.

Variables S1, S2 : Setoid.
Variable f : (Bijection S1 S2).

Local f_is_bij := (b_proof f).

Local f_is_inj := (bijection_is_injective 3!f).
Local f_is_surj := (bijection_is_surjective f).

(* Notice the difference in the two definitions above:  *)
(* the function is an implicit argument for injective.  *)

Definition bijection_inverse_fun : S2 -> S1 :=
  [y : S2](proj1_sig ? ? (f_is_surj y)).

Lemma inverse_fun_is_left_inverse :
  (y : S2)
  ((b_function f) (bijection_inverse_fun y)) [=] y.

Lemma inverse_well_defined : (fun_well_defined bijection_inverse_fun).

Definition bijection_inverse : S2 [->] S1 :=
  (setoid_function inverse_well_defined).

(* One could now also proof that the inverse is an element of  *)
(* (Bijection S2 S1). This is best done by first proving that  *)
(* a function that has and inverse is a bijection.             *)
(* All this is left as an exercise.                            *)

End Inverse.

(* The type of unary operations on a setoid. *)

Definition Un_operaton : Setoid -> Type := [S:Setoid]S [->] S.

(* The type of binary operations on a setoid. *)

Definition Bin_operation : Setoid -> Type := [S:Setoid]S [->] S [->] S.

(* Properties of binary operations *)

Definition commutativity : (S : Setoid)(Bin_operation S) -> Prop :=
  [ S : Setoid ]
  [ op : (Bin_operation S) ]
  (x, y : S)((op x) y) [=] ((op y) x).

Definition associativity : (S : Setoid)(Bin_operation S) -> Prop :=
  [ S : Setoid ]
  [ op : (Bin_operation S) ]
  (x,y,z : S)((op x) ((op y) z)) [=] ((op ((op x) y)) z).

Implicit Arguments Off.

(* We now prove that eq_rec preserves setoid equality.    The proof require the use of the axiom eq_rec_eq contained    in the library module Eqdep. *)

Theorem eq_rec_setoid :
  (A : Set)(x : A)(P : A -> Setoid)
  (p1, p2 : (P x))p1 [=] p2 ->
  (y : A)(p : x=y)
  (eq_rec A x P p1 y p) [=] (eq_rec A x P p2 y p).

25/02/99, 14:36