1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSetoids".
19 (* $Id.v,v 1.18 2002/11/25 14:43:42 lcf Exp $ *)
21 (*#* printing [=] %\ensuremath{\equiv}% #≡# *)
23 (*#* printing [~=] %\ensuremath{\mathrel{\not\equiv}}% #≠# *)
25 (*#* printing [#] %\ensuremath{\mathrel\#}% *)
27 (*#* printing ex_unq %\ensuremath{\exists^1}% #∃<sup>1</sup># *)
29 (*#* printing [o] %\ensuremath\circ% #⋅# *)
31 (*#* printing [-C-] %\ensuremath\diamond% *)
36 Definition of a constructive setoid with apartness,
37 i.e.%\% a set with an equivalence relation and an apartness relation compatible with it.
48 inline cic:/CoRN/algebra/CSetoids/Relation.con.
53 Implicit Arguments Treflexive [A].
57 Implicit Arguments Creflexive [A].
63 Implicit Arguments Tsymmetric [A].
67 Implicit Arguments Csymmetric [A].
71 Implicit Arguments Ttransitive [A].
75 Implicit Arguments Ctransitive [A].
81 Set Implicit Arguments.
85 Unset Strict Implicit.
90 (*#* **Relations necessary for Setoids
91 %\begin{convention}% Let [A:Type].
94 Notice that their type depends on the main logical connective.
98 Section Properties_of_relations.
101 inline cic:/CoRN/algebra/CSetoids/A.var.
103 inline cic:/CoRN/algebra/CSetoids/irreflexive.con.
105 inline cic:/CoRN/algebra/CSetoids/cotransitive.con.
107 inline cic:/CoRN/algebra/CSetoids/tight_apart.con.
109 inline cic:/CoRN/algebra/CSetoids/antisymmetric.con.
112 End Properties_of_relations.
122 Unset Implicit Arguments.
127 (*#* **Definition of Setoid
129 Apartness, being the main relation, needs to be [CProp]-valued. Equality,
130 as it is characterized by a negative statement, lives in [Prop]. *)
132 inline cic:/CoRN/algebra/CSetoids/is_CSetoid.ind.
134 inline cic:/CoRN/algebra/CSetoids/CSetoid.ind.
137 Implicit Arguments cs_eq [c].
141 Implicit Arguments cs_ap [c].
146 inline cic:/CoRN/algebra/CSetoids/cs_neq.con.
149 Implicit Arguments cs_neq [S].
153 %\begin{nameconvention}%
154 In the names of lemmas, we refer to [ [=] ] by [eq], [ [~=] ] by
155 [neq], and [ [#] ] by [ap].
156 %\end{nameconvention}%
159 We want concrete lemmas that state the axiomatic properties of a setoid.
165 (* Begin_SpecReals *)
168 Section CSetoid_axioms.
171 inline cic:/CoRN/algebra/CSetoids/S.var.
173 inline cic:/CoRN/algebra/CSetoids/CSetoid_is_CSetoid.con.
175 inline cic:/CoRN/algebra/CSetoids/ap_irreflexive.con.
177 inline cic:/CoRN/algebra/CSetoids/ap_symmetric.con.
179 inline cic:/CoRN/algebra/CSetoids/ap_cotransitive.con.
181 inline cic:/CoRN/algebra/CSetoids/ap_tight.con.
189 (*#* **Setoid basics%\label{section:setoid-basics}%
190 %\begin{convention}% Let [S] be a setoid.
194 (* Begin_SpecReals *)
197 Section CSetoid_basics.
200 inline cic:/CoRN/algebra/CSetoids/S.var.
205 In `there exists a unique [a:S] such that %\ldots%#...#', we now mean unique with respect to the setoid equality. We use [ex_unq] to denote unique existence.
208 inline cic:/CoRN/algebra/CSetoids/ex_unq.con.
210 inline cic:/CoRN/algebra/CSetoids/eq_reflexive.con.
212 inline cic:/CoRN/algebra/CSetoids/eq_symmetric.con.
214 inline cic:/CoRN/algebra/CSetoids/eq_transitive.con.
217 %\begin{shortcoming}%
218 The lemma [eq_reflexive] above is convertible to
219 [eq_reflexive_unfolded] below. We need the second version too,
220 because the first cannot be applied when an instance of reflexivity is needed.
221 (``I have complained bitterly about this.'' RP)
224 %\begin{nameconvention}%
225 If lemma [a] is just an unfolding of lemma [b], the name of [a] is the name
226 [b] with the suffix ``[_unfolded]''.
227 %\end{nameconvention}%
230 inline cic:/CoRN/algebra/CSetoids/eq_reflexive_unfolded.con.
232 inline cic:/CoRN/algebra/CSetoids/eq_symmetric_unfolded.con.
234 inline cic:/CoRN/algebra/CSetoids/eq_transitive_unfolded.con.
236 inline cic:/CoRN/algebra/CSetoids/eq_wdl.con.
238 (* Begin_SpecReals *)
240 inline cic:/CoRN/algebra/CSetoids/ap_irreflexive_unfolded.con.
244 inline cic:/CoRN/algebra/CSetoids/ap_cotransitive_unfolded.con.
246 inline cic:/CoRN/algebra/CSetoids/ap_symmetric_unfolded.con.
249 %\begin{shortcoming}%
250 We would like to write
252 Lemma eq_equiv_not_ap : forall (x y:S), x [=] y Iff ~(x [#] y).
254 In Coq, however, this lemma cannot be easily applied.
255 Therefore we have to split the lemma into the following two lemmas [eq_imp_not_ap] and [not_ap_imp_eq].
259 inline cic:/CoRN/algebra/CSetoids/eq_imp_not_ap.con.
261 inline cic:/CoRN/algebra/CSetoids/not_ap_imp_eq.con.
263 inline cic:/CoRN/algebra/CSetoids/neq_imp_notnot_ap.con.
265 inline cic:/CoRN/algebra/CSetoids/notnot_ap_imp_neq.con.
267 inline cic:/CoRN/algebra/CSetoids/ap_imp_neq.con.
269 inline cic:/CoRN/algebra/CSetoids/not_neq_imp_eq.con.
271 inline cic:/CoRN/algebra/CSetoids/eq_imp_not_neq.con.
273 (* Begin_SpecReals *)
282 Section product_csetoid.
285 (*#* **The product of setoids *)
287 inline cic:/CoRN/algebra/CSetoids/prod_ap.con.
289 inline cic:/CoRN/algebra/CSetoids/prod_eq.con.
291 inline cic:/CoRN/algebra/CSetoids/prodcsetoid_is_CSetoid.con.
293 inline cic:/CoRN/algebra/CSetoids/ProdCSetoid.con.
300 Implicit Arguments ex_unq [S].
304 Hint Resolve eq_reflexive_unfolded: algebra_r.
308 Hint Resolve eq_symmetric_unfolded: algebra_s.
312 Declare Left Step eq_wdl.
316 Declare Right Step eq_transitive_unfolded.
319 (* Begin_SpecReals *)
321 (*#* **Relations and predicates
322 Here we define the notions of well-definedness and strong extensionality
323 on predicates and relations.
325 %\begin{convention}% Let [S] be a setoid.
328 %\begin{nameconvention}%
329 - ``well-defined'' is abbreviated to [well_def] (or [wd]).
330 - ``strongly extensional'' is abbreviated to [strong_ext] (or [strext]).
332 %\end{nameconvention}%
336 Section CSetoid_relations_and_predicates.
339 inline cic:/CoRN/algebra/CSetoids/S.var.
345 At this stage, we consider [CProp]- and [Prop]-valued predicates on setoids.
347 %\begin{convention}% Let [P] be a predicate on (the carrier of) [S].
352 Section CSetoidPredicates.
355 inline cic:/CoRN/algebra/CSetoids/P.var.
357 inline cic:/CoRN/algebra/CSetoids/pred_strong_ext.con.
359 inline cic:/CoRN/algebra/CSetoids/pred_wd.con.
362 End CSetoidPredicates.
365 inline cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind.
367 inline cic:/CoRN/algebra/CSetoids/csp_wd.con.
369 (*#* Similar, with [Prop] instead of [CProp]. *)
372 Section CSetoidPPredicates.
375 inline cic:/CoRN/algebra/CSetoids/P.var.
377 inline cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con.
379 inline cic:/CoRN/algebra/CSetoids/pred_wd'.con.
382 End CSetoidPPredicates.
385 (*#* ***Definition of a setoid predicate *)
387 inline cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind.
389 inline cic:/CoRN/algebra/CSetoids/csp'_wd.con.
391 (* Begin_SpecReals *)
395 Let [R] be a relation on (the carrier of) [S].
396 %\end{convention}% *)
399 Section CsetoidRelations.
402 inline cic:/CoRN/algebra/CSetoids/R.var.
404 inline cic:/CoRN/algebra/CSetoids/rel_wdr.con.
406 inline cic:/CoRN/algebra/CSetoids/rel_wdl.con.
408 inline cic:/CoRN/algebra/CSetoids/rel_strext.con.
412 inline cic:/CoRN/algebra/CSetoids/rel_strext_lft.con.
414 inline cic:/CoRN/algebra/CSetoids/rel_strext_rht.con.
416 inline cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con.
418 inline cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con.
420 inline cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con.
422 (* Begin_SpecReals *)
425 End CsetoidRelations.
428 (*#* ***Definition of a setoid relation
429 The type of relations over a setoid. *)
431 inline cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind.
433 (*#* ***[CProp] Relations
435 Let [R] be a relation on (the carrier of) [S].
440 Section CCsetoidRelations.
443 inline cic:/CoRN/algebra/CSetoids/R.var.
445 inline cic:/CoRN/algebra/CSetoids/Crel_wdr.con.
447 inline cic:/CoRN/algebra/CSetoids/Crel_wdl.con.
449 inline cic:/CoRN/algebra/CSetoids/Crel_strext.con.
453 inline cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con.
455 inline cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con.
457 inline cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con.
459 inline cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con.
461 inline cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con.
463 (* Begin_SpecReals *)
466 End CCsetoidRelations.
469 (*#* ***Definition of a [CProp] setoid relation
471 The type of relations over a setoid. *)
473 inline cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind.
475 inline cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con.
477 inline cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con.
481 inline cic:/CoRN/algebra/CSetoids/ap_wdr.con.
483 inline cic:/CoRN/algebra/CSetoids/ap_wdl.con.
485 inline cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con.
487 inline cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con.
489 inline cic:/CoRN/algebra/CSetoids/ap_strext.con.
491 inline cic:/CoRN/algebra/CSetoids/predS_well_def.con.
493 (* Begin_SpecReals *)
496 End CSetoid_relations_and_predicates.
500 Declare Left Step ap_wdl_unfolded.
504 Declare Right Step ap_wdr_unfolded.
509 (*#* **Functions between setoids
510 Such functions must preserve the setoid equality
511 and be strongly extensional w.r.t.%\% the apartness, i.e.%\%
512 if [f(x,y) [#] f(x1,y1)], then [x [#] x1 + y [#] y1].
513 For every arity this has to be defined separately.
515 Let [S1], [S2] and [S3] be setoids.
518 First we consider unary functions. *)
520 (* Begin_SpecReals *)
523 Section CSetoid_functions.
526 inline cic:/CoRN/algebra/CSetoids/S1.var.
528 inline cic:/CoRN/algebra/CSetoids/S2.var.
530 inline cic:/CoRN/algebra/CSetoids/S3.var.
533 Section unary_functions.
537 In the following two definitions,
538 [f] is a function from (the carrier of) [S1] to
539 (the carrier of) [S2]. *)
541 inline cic:/CoRN/algebra/CSetoids/f.var.
543 inline cic:/CoRN/algebra/CSetoids/fun_wd.con.
545 inline cic:/CoRN/algebra/CSetoids/fun_strext.con.
549 inline cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con.
551 (* Begin_SpecReals *)
557 inline cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind.
559 inline cic:/CoRN/algebra/CSetoids/csf_wd.con.
563 inline cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con.
565 (* Begin_SpecReals *)
568 Section binary_functions.
572 Now we consider binary functions.
573 In the following two definitions,
574 [f] is a function from [S1] and [S2] to [S3].
577 inline cic:/CoRN/algebra/CSetoids/f.var.
579 inline cic:/CoRN/algebra/CSetoids/bin_fun_wd.con.
581 inline cic:/CoRN/algebra/CSetoids/bin_fun_strext.con.
585 inline cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con.
587 (* Begin_SpecReals *)
590 End binary_functions.
593 inline cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind.
595 inline cic:/CoRN/algebra/CSetoids/csbf_wd.con.
597 inline cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con.
599 inline cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con.
601 inline cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con.
604 End CSetoid_functions.
610 Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.
614 Implicit Arguments fun_wd [S1 S2].
618 Implicit Arguments fun_strext [S1 S2].
621 (* Begin_SpecReals *)
623 (*#* **The unary and binary (inner) operations on a csetoid
624 An operation is a function with domain(s) and co-domain equal.
626 %\begin{nameconvention}%
627 The word ``unary operation'' is abbreviated to [un_op];
628 ``binary operation'' is abbreviated to [bin_op].
629 %\end{nameconvention}%
637 Section csetoid_inner_ops.
640 inline cic:/CoRN/algebra/CSetoids/S.var.
642 (*#* Properties of binary operations *)
644 inline cic:/CoRN/algebra/CSetoids/commutes.con.
646 inline cic:/CoRN/algebra/CSetoids/associative.con.
648 (*#* Well-defined unary operations on a setoid. *)
650 inline cic:/CoRN/algebra/CSetoids/un_op_wd.con.
652 inline cic:/CoRN/algebra/CSetoids/un_op_strext.con.
654 inline cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con.
656 inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con.
660 inline cic:/CoRN/algebra/CSetoids/id_strext.con.
662 inline cic:/CoRN/algebra/CSetoids/id_pres_eq.con.
664 inline cic:/CoRN/algebra/CSetoids/id_un_op.con.
670 (* Begin_SpecReals *)
672 inline cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con.
676 inline cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con.
678 inline cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con.
680 (*#* Well-defined binary operations on a setoid. *)
682 inline cic:/CoRN/algebra/CSetoids/bin_op_wd.con.
684 inline cic:/CoRN/algebra/CSetoids/bin_op_strext.con.
686 (* Begin_SpecReals *)
688 inline cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con.
690 inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con.
694 inline cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con.
696 inline cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con.
698 (* Begin_SpecReals *)
706 inline cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con.
708 inline cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con.
710 inline cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con.
712 inline cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con.
714 inline cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con.
716 inline cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con.
718 inline cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con.
720 inline cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con.
722 (* Begin_SpecReals *)
725 End csetoid_inner_ops.
731 Implicit Arguments commutes [S].
734 (* Begin_SpecReals *)
737 Implicit Arguments associative [S].
743 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
746 (*#* **The binary outer operations on a csetoid
748 Let [S1] and [S2] be setoids.
753 Section csetoid_outer_ops.
756 inline cic:/CoRN/algebra/CSetoids/S1.var.
758 inline cic:/CoRN/algebra/CSetoids/S2.var.
761 Well-defined outer operations on a setoid.
764 inline cic:/CoRN/algebra/CSetoids/outer_op_well_def.con.
766 inline cic:/CoRN/algebra/CSetoids/outer_op_strext.con.
768 inline cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con.
770 inline cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con.
772 inline cic:/CoRN/algebra/CSetoids/csoo_wd.con.
774 inline cic:/CoRN/algebra/CSetoids/csoo_strext.con.
780 inline cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con.
783 End csetoid_outer_ops.
787 Hint Resolve csoo_wd_unfolded: algebra_c.
790 (* Begin_SpecReals *)
794 Let [S] be a setoid, and [P] a predicate on the carrier of [S].
802 inline cic:/CoRN/algebra/CSetoids/S.var.
804 inline cic:/CoRN/algebra/CSetoids/P.var.
806 inline cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind.
808 (*#* Though [scs_elem] is declared as a coercion, it does not satisfy the
809 uniform inheritance condition and will not be inserted. However it will
810 also not be printed, which is handy.
813 inline cic:/CoRN/algebra/CSetoids/restrict_relation.con.
815 inline cic:/CoRN/algebra/CSetoids/Crestrict_relation.con.
817 inline cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con.
819 inline cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con.
823 inline cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con.
825 (* Begin_SpecReals *)
827 inline cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con.
829 inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con.
833 (*#* ***Subsetoid unary operations
835 Let [f] be a unary setoid operation on [S].
840 Section SubCSetoid_unary_operations.
843 inline cic:/CoRN/algebra/CSetoids/f.var.
845 inline cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con.
849 Assume [pr:un_op_pres_pred].
850 %\end{convention}% *)
852 inline cic:/CoRN/algebra/CSetoids/pr.var.
854 inline cic:/CoRN/algebra/CSetoids/restr_un_op.con.
856 inline cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con.
858 inline cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con.
860 inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con.
863 End SubCSetoid_unary_operations.
866 (*#* ***Subsetoid binary operations
868 Let [f] be a binary setoid operation on [S].
873 Section SubCSetoid_binary_operations.
876 inline cic:/CoRN/algebra/CSetoids/f.var.
878 inline cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con.
882 Assume [bin_op_pres_pred].
886 inline cic:/CoRN/algebra/CSetoids/pr.var.
888 inline cic:/CoRN/algebra/CSetoids/restr_bin_op.con.
890 inline cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con.
892 inline cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con.
894 inline cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con.
896 inline cic:/CoRN/algebra/CSetoids/restr_f_assoc.con.
899 End SubCSetoid_binary_operations.
902 (* Begin_SpecReals *)
913 Ltac Step_final x := apply eq_transitive_unfolded with x; Algebra.
919 Tactic Notation "Step_final" constr(c) := Step_final c.
925 inline cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con.
928 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
931 inline cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con.
933 inline cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con.
936 Implicit Arguments nat_less_n_fun [S n].
940 Implicit Arguments nat_less_n_fun' [S n].