Example of a setoid: N



We will show that the natural numbers form a CSetoid.

Lemma ap_nat_irreflexive : irreflexive (A:=nat) ap_nat.

Lemma ap_nat_symmetric : Csymmetric ap_nat.

Lemma ap_nat_cotransitive : cotransitive (A:=nat) ap_nat.

Lemma ap_nat_tight : tight_apart (A:=nat) (eq (A:=nat)) ap_nat.

Definition ap_nat_is_apartness := Build_is_CSetoid N (eq (A:=nat)) ap_nat
 ap_nat_irreflexive ap_nat_symmetric ap_nat_cotransitive ap_nat_tight.

Definition nat_as_CSetoid := Build_CSetoid _ _ _ ap_nat_is_apartness.
Canonical Structure nat_as_CSetoid.

Addition


Lemma plus_wd : bin_fun_wd nat_as_CSetoid nat_as_CSetoid nat_as_CSetoid plus.

Lemma plus_strext : bin_fun_strext nat_as_CSetoid nat_as_CSetoid nat_as_CSetoid plus.

Definition plus_is_bin_fun := Build_CSetoid_bin_fun _ _ _ _ plus_strext.
Canonical Structure plus_is_bin_fun.

It is associative and commutative.

Lemma plus_is_assoc : associative plus_is_bin_fun.

Lemma plus_is_commut : commutes plus_is_bin_fun.

Multiplication


Lemma mult_strext : bin_fun_strext
 nat_as_CSetoid nat_as_CSetoid nat_as_CSetoid mult.

Definition mult_as_bin_fun := Build_CSetoid_bin_fun _ _ _ _ mult_strext.
Canonical Structure mult_as_bin_fun.

Ternary addition


Definition plus1 (n:nat)(m:nat): (n_ary_operation 1 nat_as_CSetoid).
Defined.

Lemma to_plus1_strext:forall (n:nat), fun_strext (S1:=nat_as_CSetoid)
     (S2:=FS_as_CSetoid nat_as_CSetoid nat_as_CSetoid)
     (fun m : N => plus1 n m).

Definition plus2 (n:nat): (n_ary_operation 2 nat_as_CSetoid).
Defined.

Lemma to_plus2_strext:fun_strext (S1:=nat_as_CSetoid)
     (S2:=FS_as_CSetoid nat_as_CSetoid
            (FS_as_CSetoid nat_as_CSetoid nat_as_CSetoid))
     (fun m : N => plus2 m).

Definition plus3 :(n_ary_operation 3 nat_as_CSetoid).
Defined.

Definition on: nat_as_CSetoid -> nat_as_CSetoid -> nat_as_CSetoid ->
(n_ary_operation 3 nat_as_CSetoid)-> nat_as_CSetoid.
Defined.

Let ex_3_ary: (on 3 5 7 plus3)[=] 3+5+7.
Qed.