Setoids

Definition of a constructive setoid with apartness, i.e. a set with an equivalence relation and an apartness relation compatible with it.


Definition Relation := Trelation.






Relations necessary for Setoids

Let A:Type.

Notice that their type depends on the main logical connective.

Section Properties_of_relations.
Variable A : Type.

Definition irreflexive (R : Crelation A) : Prop := forall x : A, ~ (R x x).

Definition cotransitive (R : Crelation A) : CProp := forall x y : A,
 R x y -> forall z : A, R x z or R z y.

Definition tight_apart (eq : Relation A) (ap : Crelation A) : Prop := forall x y : A,
 ~ (ap x y) <-> eq x y.

Definition antisymmetric (R : Crelation A) : Prop := forall x y : A,
 R x y -> ~ (R y x).

End Properties_of_relations.

Definition of Setoid



Apartness, being the main relation, needs to be CProp-valued. Equality, as it is characterized by a negative statement, lives in Prop.

Record is_CSetoid (A : Type) (eq : Relation A) (ap : Crelation A) : CProp :=
  {ax_ap_irreflexive : irreflexive ap;
   ax_ap_symmetric : Csymmetric ap;
   ax_ap_cotransitive : cotransitive ap;
   ax_ap_tight : tight_apart eq ap}.

Record CSetoid : Type := makeCSetoid
  {cs_crr :> Setoid;
   cs_ap : Crelation cs_crr;
   cs_proof : is_CSetoid cs_crr (@st_eq cs_crr) cs_ap}.

Notation cs_eq := st_eq (only parsing).

Infix "≡" := cs_eq (at level 70, no associativity).
Infix "[#]" := cs_ap (at level 70, no associativity).


Definition cs_neq (S : CSetoid) : Relation S := fun x y : S => ~ x [=] y.


Infix "≠" := cs_neq (at level 70, no associativity).

In the names of lemmas, we refer to ≡ by eq, ≠ by neq, and [#] by ap.

Setoid axioms

We want concrete lemmas that state the axiomatic properties of a setoid. Let S be a setoid.


Section CSetoid_axioms.
Variable S : CSetoid.

Lemma CSetoid_is_CSetoid : is_CSetoid S (cs_eq (s:=S)) (cs_ap (c:=S)).

Lemma ap_irreflexive : irreflexive (cs_ap (c:=S)).

Lemma ap_symmetric : Csymmetric (cs_ap (c:=S)).

Lemma ap_cotransitive : cotransitive (cs_ap (c:=S)).

Lemma ap_tight : tight_apart (cs_eq (s:=S)) (cs_ap (c:=S)).

End CSetoid_axioms.


Setoid basics

Let S be a setoid.


Lemma is_CSetoid_Setoid : forall S eq ap, is_CSetoid S eq ap -> Setoid_Theory S eq.

Definition Build_CSetoid (X:Type) (eq:Relation X) (ap:Crelation X) (p:is_CSetoid X eq ap) : CSetoid.
Defined.

Section CSetoid_basics.
Variable S : CSetoid.


In `there exists a unique a:S such that ...', we now mean unique with respect to the setoid equality. We use ∃1 to denote unique existence.

Definition ∃1 (P : S -> CProp) := {x : S | forall y : S, P y -> x [=] y | P x}.

Lemma eq_reflexive : Treflexive (cs_eq (s:=S)).

Lemma eq_symmetric : Tsymmetric (cs_eq (s:=S)).

Lemma eq_transitive : Ttransitive (cs_eq (s:=S)).

The lemma eq_reflexive above is convertible to eq_reflexive_unfolded below. We need the second version too, because the first cannot be applied when an instance of reflexivity is needed. (``I have complained bitterly about this.'' RP) tes If lemma a is just an unfolding of lemma b, the name of a is the name b with the suffix ``_unfolded''.

Lemma eq_reflexive_unfolded : forall x : S, x [=] x.

Lemma eq_symmetric_unfolded : forall x y : S, x [=] y -> y [=] x.

Lemma eq_transitive_unfolded : forall x y z : S, x [=] y -> y [=] z -> x [=] z.

Lemma eq_wdl : forall x y z : S, x [=] y -> x [=] z -> z [=] y.


Lemma ap_irreflexive_unfolded : forall x : S, ~ (x [#] x).


Lemma ap_cotransitive_unfolded : forall a b : S, a [#] b -> forall c : S, a [#] c or c [#] b.

Lemma ap_symmetric_unfolded : forall x y : S, x [#] y -> y [#] x.

We would like to write
Lemma eq_equiv_not_ap : forall (x y:S), x [=] y ⇔ ~(x [#] y).
]] In Coq, however, this lemma cannot be easily applied. Therefore we have to split the lemma into the following two lemmas eq_imp_not_ap and not_ap_imp_eq.

Lemma eq_imp_not_ap : forall x y : S, x [=] y -> ~ (x [#] y).

Lemma not_ap_imp_eq : forall x y : S, ~ (x [#] y) -> x [=] y.

Lemma neq_imp_notnot_ap : forall x y : S, x [~=] y -> ~ ~ (x [#] y).

Lemma notnot_ap_imp_neq : forall x y : S, ~ ~ (x [#] y) -> x [~=] y.

Lemma ap_imp_neq : forall x y : S, x [#] y -> x [~=] y.

Lemma not_neq_imp_eq : forall x y : S, ~ x [~=] y -> x [=] y.

Lemma eq_imp_not_neq : forall x y : S, x [=] y -> ~ x [~=] y.


End CSetoid_basics.


Section product_csetoid.

The product of setoids


Definition prod_ap (A B : CSetoid) (c d : prodT A B) : CProp.
Defined.

Definition prod_eq (A B : CSetoid) (c d : prodT A B) : Prop.
Defined.

Lemma prodcsetoid_is_CSetoid : forall A B : CSetoid,
 is_CSetoid (prodT A B) (prod_eq A B) (prod_ap A B).

Definition ProdCSetoid (A B : CSetoid) : CSetoid := Build_CSetoid
 (prodT A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).

End product_csetoid.




Relations and predicates

Here we define the notions of well-definedness and strong extensionality on predicates and relations.

Let S be a setoid.

  • ``well-defined'' is abbreviated to well_def (or wd).
  • ``strongly extensional'' is abbreviated to strong_ext (or strext).



Section CSetoid_relations_and_predicates.
Variable S : CSetoid.


Predicates



At this stage, we consider CProp- and Prop-valued predicates on setoids.

Let P be a predicate on (the carrier of) S.

Section CSetoidPredicates.
Variable P : S -> CProp.

Definition pred_strong_ext : CProp := forall x y : S, P x -> P y or x [#] y.

Definition pred_wd : CProp := forall x y : S, P x -> x [=] y -> P y.

End CSetoidPredicates.

Record wd_pred : Type :=
  {wdp_pred :> S -> CProp;
   wdp_well_def : pred_wd wdp_pred}.

Record CSetoid_predicate : Type :=
 {csp_pred :> S -> CProp;
  csp_strext : pred_strong_ext csp_pred}.

Lemma csp_wd : forall P : CSetoid_predicate, pred_wd P.

Similar, with Prop instead of CProp.

Section CSetoidPPredicates.
Variable P : S -> Prop.

Definition pred_strong_ext' : CProp := forall x y : S, P x -> P y or x [#] y.

Definition pred_wd' : Prop := forall x y : S, P x -> x [=] y -> P y.

End CSetoidPPredicates.

Definition of a setoid predicate


Record CSetoid_predicate' : Type :=
 {csp'_pred :> S -> Prop;
  csp'_strext : pred_strong_ext' csp'_pred}.

Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.


Relations

Let R be a relation on (the carrier of) S.

Section CsetoidRelations.
Variable R : S -> S -> Prop.

Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z.

Definition rel_wdl : Prop := forall x y z : S, R x y -> x [=] z -> R z y.

Definition rel_strext : CProp := forall x1 x2 y1 y2 : S,
 R x1 y1 -> (x1 [#] x2 or y1 [#] y2) or R x2 y2.


Definition rel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> x1 [#] x2 or R x2 y.

Definition rel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> y1 [#] y2 or R x y2.

Lemma rel_strext_imp_lftarg : rel_strext -> rel_strext_lft.

Lemma rel_strext_imp_rhtarg : rel_strext -> rel_strext_rht.

Lemma rel_strextarg_imp_strext :
 rel_strext_rht -> rel_strext_lft -> rel_strext.


End CsetoidRelations.

Definition of a setoid relation

The type of relations over a setoid.

Record CSetoid_relation : Type :=
  {csr_rel :> S -> S -> Prop;
   csr_wdr : rel_wdr csr_rel;
   csr_wdl : rel_wdl csr_rel;
   csr_strext : rel_strext csr_rel}.

CProp Relations

Let R be a relation on (the carrier of) S.

Section CCsetoidRelations.

Variable R : S -> S -> CProp.

Definition Crel_wdr : CProp := forall x y z : S, R x y -> y [=] z -> R x z.

Definition Crel_wdl : CProp := forall x y z : S, R x y -> x [=] z -> R z y.

Definition Crel_strext : CProp := forall x1 x2 y1 y2 : S,
 R x1 y1 -> R x2 y2 or x1 [#] x2 or y1 [#] y2.


Definition Crel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> R x2 y or x1 [#] x2.

Definition Crel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> R x y2 or y1 [#] y2.

Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.

Lemma Crel_strext_imp_rhtarg : Crel_strext -> Crel_strext_rht.

Lemma Crel_strextarg_imp_strext :
 Crel_strext_rht -> Crel_strext_lft -> Crel_strext.


End CCsetoidRelations.

Definition of a CProp setoid relation



The type of relations over a setoid.

Record CCSetoid_relation : Type :=
 {Ccsr_rel :> S -> S -> CProp;
  Ccsr_strext : Crel_strext Ccsr_rel}.

Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.

Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.


Lemma ap_wdr : Crel_wdr (cs_ap (c:=S)).

Lemma ap_wdl : Crel_wdl (cs_ap (c:=S)).

Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.

Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.

Lemma ap_strext : Crel_strext (cs_ap (c:=S)).

Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
 P x -> x [=] y -> P y.


End CSetoid_relations_and_predicates.



Functions between setoids

Such functions must preserve the setoid equality and be strongly extensional w.r.t. the apartness, i.e. if f(x,y) [#] f(x1,y1), then x [#] x1 + y [#] y1. For every arity this has to be defined separately. Let S1, S2 and S3 be setoids.

First we consider unary functions.


Section CSetoid_functions.
Variables S1 S2 S3 : CSetoid.

Section unary_functions.

In the following two definitions, f is a function from (the carrier of) S1 to (the carrier of) S2.

Variable f : S1 -> S2.

Definition fun_wd : Prop := forall x y : S1, x [=] y -> f x [=] f y.

Definition fun_strext : CProp := forall x y : S1, f x [#] f y -> x [#] y.


Lemma fun_strext_imp_wd : fun_strext -> fun_wd.


End unary_functions.

Record CSetoid_fun : Type :=
  {csf_fun :> S1 -> S2;
   csf_strext : fun_strext csf_fun}.

Lemma csf_wd : forall f : CSetoid_fun, fun_wd f.


Definition Const_CSetoid_fun : S2 -> CSetoid_fun.
Defined.


Section binary_functions.

Now we consider binary functions. In the following two definitions, f is a function from S1 and S2 to S3.
Variable f : S1 -> S2 -> S3.

Definition bin_fun_wd : Prop := forall x1 x2 y1 y2,
 x1 [=] x2 -> y1 [=] y2 -> f x1 y1 [=] f x2 y2.

Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
 f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.


Lemma bin_fun_strext_imp_wd : bin_fun_strext -> bin_fun_wd.


End binary_functions.

Record CSetoid_bin_fun : Type :=
 {csbf_fun :> S1 -> S2 -> S3;
  csbf_strext : bin_fun_strext csbf_fun}.

Lemma csbf_wd : forall f : CSetoid_bin_fun, bin_fun_wd f.

Lemma csf_wd_unfolded : forall (f : CSetoid_fun) (x x' : S1), x [=] x' -> f x [=] f x'.

Lemma csf_strext_unfolded : forall (f : CSetoid_fun) (x y : S1), f x [#] f y -> x [#] y.

Lemma csbf_wd_unfolded : forall (f : CSetoid_bin_fun) (x x' : S1) (y y' : S2),
 x [=] x' -> y [=] y' -> f x y [=] f x' y'.

End CSetoid_functions.

Lemma bin_fun_is_wd_fun_lft : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S2),
 fun_wd _ _ (fun x : S1 => f x c).


Lemma bin_fun_is_wd_fun_rht : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S1),
 fun_wd _ _ (fun x : S2 => f c x).


Lemma bin_fun_is_strext_fun_lft : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S2),
 fun_strext _ _ (fun x : S1 => f x c).




Lemma bin_fun_is_strext_fun_rht : forall S1 S2 S3 (f : CSetoid_bin_fun S1 S2 S3) (c : S1),
 fun_strext _ _ (fun x : S2 => f c x).




Definition bin_fun2fun_rht (S1 S2 S3:CSetoid) (f : CSetoid_bin_fun S1 S2 S3) (c : S1) : CSetoid_fun S2 S3 :=
  Build_CSetoid_fun _ _ (fun x : S2 => f c x) (bin_fun_is_strext_fun_rht _ _ _ f c).

Definition bin_fun2fun_lft (S1 S2 S3:CSetoid) (f : CSetoid_bin_fun S1 S2 S3) (c : S2) : CSetoid_fun S1 S3 :=
  Build_CSetoid_fun _ _ (fun x : S1 => f x c) (bin_fun_is_strext_fun_lft _ _ _ f c).





The unary and binary (inner) operations on a csetoid

An operation is a function with domain(s) and co-domain equal.

The word ``unary operation'' is abbreviated to un_op; ``binary operation'' is abbreviated to bin_op.

Let S be a setoid.

Section csetoid_inner_ops.
Variable S : CSetoid.

Properties of binary operations

Definition commutes (f : S -> S -> S) : Prop := forall x y : S, f x y [=] f y x.

Definition associative (f : S -> S -> S) : Prop := forall x y z : S,
 f x (f y z) [=] f (f x y) z.

Well-defined unary operations on a setoid.

Definition un_op_wd := fun_wd (S1:=S) (S2:=S).

Definition un_op_strext := fun_strext (S1:=S) (S2:=S).

Definition CSetoid_un_op : Type := CSetoid_fun S S.

Definition Build_CSetoid_un_op := Build_CSetoid_fun S S.


Lemma id_strext : un_op_strext (fun x : S => x).

Lemma id_pres_eq : un_op_wd (fun x : S => x).

Definition id_un_op := Build_CSetoid_un_op (fun x : S => x) id_strext.


Definition cs_un_op_strext := csf_strext S S.


Lemma un_op_wd_unfolded : forall (op : CSetoid_un_op) (x y : S),
 x [=] y -> op x [=] op y.

Lemma un_op_strext_unfolded : forall (op : CSetoid_un_op) (x y : S),
 op x [#] op y -> x [#] y.

Well-defined binary operations on a setoid.

Definition bin_op_wd := bin_fun_wd S S S.
Definition bin_op_strext := bin_fun_strext S S S.


Definition CSetoid_bin_op : Type := CSetoid_bin_fun S S S.
Definition Build_CSetoid_bin_op := Build_CSetoid_bin_fun S S S.


Definition cs_bin_op_wd := csbf_wd S S S.
Definition cs_bin_op_strext := csbf_strext S S S.


Lemma bin_op_wd_unfolded : forall (op : CSetoid_bin_op) (x1 x2 y1 y2 : S),
 x1 [=] x2 -> y1 [=] y2 -> op x1 y1 [=] op x2 y2.

Lemma bin_op_strext_unfolded : forall (op : CSetoid_bin_op) (x1 x2 y1 y2 : S),
 op x1 y1 [#] op x2 y2 -> x1 [#] x2 or y1 [#] y2.

Lemma bin_op_is_wd_un_op_lft : forall (op : CSetoid_bin_op) (c : S),
 un_op_wd (fun x : S => op x c).

Lemma bin_op_is_wd_un_op_rht : forall (op : CSetoid_bin_op) (c : S),
 un_op_wd (fun x : S => op c x).

Lemma bin_op_is_strext_un_op_lft : forall (op : CSetoid_bin_op) (c : S),
 un_op_strext (fun x : S => op x c).

Lemma bin_op_is_strext_un_op_rht : forall (op : CSetoid_bin_op) (c : S),
 un_op_strext (fun x : S => op c x).

Definition bin_op2un_op_rht (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
  bin_fun2fun_rht _ _ _ op c.

Definition bin_op2un_op_lft (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
  bin_fun2fun_lft _ _ _ op c.


End csetoid_inner_ops.







The binary outer operations on a csetoid

Let S1 and S2 be setoids.

Section csetoid_outer_ops.
Variables S1 S2 : CSetoid.

Well-defined outer operations on a setoid.
Definition outer_op_well_def := bin_fun_wd S1 S2 S2.
Definition outer_op_strext := bin_fun_strext S1 S2 S2.

Definition CSetoid_outer_op : Type := CSetoid_bin_fun S1 S2 S2.
Definition Build_CSetoid_outer_op := Build_CSetoid_bin_fun S1 S2 S2.
Definition csoo_wd := csbf_wd S1 S2 S2.
Definition csoo_strext := csbf_strext S1 S2 S2.


Lemma csoo_wd_unfolded : forall (op : CSetoid_outer_op) x1 x2 y1 y2,
 x1 [=] x2 -> y1 [=] y2 -> op x1 y1 [=] op x2 y2.

End csetoid_outer_ops.


Subsetoids

Let S be a setoid, and P a predicate on the carrier of S.

Section SubCSetoids.
Variable S : CSetoid.
Variable P : S -> CProp.

Record subcsetoid_crr : Type :=
 {scs_elem :> S;
  scs_prf : P scs_elem}.

Though scs_elem is declared as a coercion, it does not satisfy the uniform inheritance condition and will not be inserted. However it will also not be printed, which is handy.

Definition restrict_relation (R : Relation S) : Relation subcsetoid_crr :=
  fun a b : subcsetoid_crr =>
  match a, b with
  | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
  end.

Definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
  fun a b : subcsetoid_crr =>
  match a, b with
  | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
  end.

Definition subcsetoid_eq : Relation subcsetoid_crr :=
  restrict_relation (cs_eq (s:=S)).

Definition subcsetoid_ap : Crelation subcsetoid_crr :=
  Crestrict_relation (cs_ap (c:=S)).


Remark subcsetoid_equiv : Tequiv _ subcsetoid_eq.


Lemma subcsetoid_is_CSetoid : is_CSetoid _ subcsetoid_eq subcsetoid_ap.





Definition Build_SubCSetoid : CSetoid := Build_CSetoid
 subcsetoid_crr subcsetoid_eq subcsetoid_ap subcsetoid_is_CSetoid.


Subsetoid unary operations

Let f be a unary setoid operation on S.

Section SubCSetoid_unary_operations.
Variable f : CSetoid_un_op S.
Definition un_op_pres_pred : CProp := forall x : S, P x -> P (f x).

Assume pr:un_op_pres_pred.

Variable pr : un_op_pres_pred.

Definition restr_un_op (a : subcsetoid_crr) : subcsetoid_crr :=
  match a with
  | Build_subcsetoid_crr x p => Build_subcsetoid_crr (f x) (pr x p)
  end.

Lemma restr_un_op_wd : un_op_wd Build_SubCSetoid restr_un_op.


Lemma restr_un_op_strext : un_op_strext Build_SubCSetoid restr_un_op.


Definition Build_SubCSetoid_un_op : CSetoid_un_op Build_SubCSetoid :=
  Build_CSetoid_un_op Build_SubCSetoid restr_un_op restr_un_op_strext.

End SubCSetoid_unary_operations.

Subsetoid binary operations

Let f be a binary setoid operation on S.

Section SubCSetoid_binary_operations.

Variable f : CSetoid_bin_op S.

Definition bin_op_pres_pred : CProp := forall x y : S, P x -> P y -> P (f x y).

Assume bin_op_pres_pred.

Variable pr : bin_op_pres_pred.

Definition restr_bin_op (a b : subcsetoid_crr) : subcsetoid_crr :=
  match a, b with
  | Build_subcsetoid_crr x p, Build_subcsetoid_crr y q =>
      Build_subcsetoid_crr (f x y) (pr x y p q)
  end.

Lemma restr_bin_op_well_def : bin_op_wd Build_SubCSetoid restr_bin_op.


Lemma restr_bin_op_strext : bin_op_strext Build_SubCSetoid restr_bin_op.


Definition Build_SubCSetoid_bin_op : CSetoid_bin_op Build_SubCSetoid :=
  Build_CSetoid_bin_op Build_SubCSetoid restr_bin_op restr_bin_op_strext.

Lemma restr_f_assoc : associative f -> associative Build_SubCSetoid_bin_op.


End SubCSetoid_binary_operations.


End SubCSetoids.



Tactic Notation "Step_final" constr(c) := Step_final c.

Miscellaneous


Lemma proper_caseZ_diff_CS : forall (S : CSetoid) (f : N -> N -> S),
 (forall m n p q : N, m + q = n + p -> f m n [=] f p q) ->
 forall m n : N, caseZ_diff (m - n) f [=] f m n.

Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.

Definition nat_less_n_fun (S : CSetoid) (n : N) (f : forall i : N, i < n -> S) :=
  forall i j : N, i = j -> forall (H : i < n) (H' : j < n), f i H [=] f j H'.

Definition nat_less_n_fun' (S : CSetoid) (n : N) (f : forall i : N, i <= n -> S) :=
  forall i j : N, i = j -> forall (H : i <= n) (H' : j <= n), f i H [=] f j H'.


Add Parametric Relation c : (cs_crr c) (@cs_eq c)
  reflexivity proved by (eq_reflexive c)
  symmetry proved by (eq_symmetric c)
  transitivity proved by (eq_transitive c)
  as CSetoid_eq_Setoid.

Add Parametric Morphism (c1 c2 c3 : CSetoid) f: (csbf_fun c1 c2 c3 f) with signature (@cs_eq c1) ==> (@cs_eq c2) ==> (@cs_eq c3) as csbf_fun_wd.
Qed.

Add Parametric Morphism (c1 c2 : CSetoid) f: (@csf_fun c1 c2 f) with signature (@cs_eq c1) ==> (@cs_eq c2) as csf_fun_wd.
Qed.