]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/algebra/CSetoids.mma
made executable again
[helm.git] / matita / matita / contribs / procedural / CoRN / algebra / CSetoids.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id.v,v 1.18 2002/11/25 14:43:42 lcf Exp $ *)
20
21 (*#* printing [=] %\ensuremath{\equiv}% #≡# *)
22
23 (*#* printing [~=] %\ensuremath{\mathrel{\not\equiv}}% #≠# *)
24
25 (*#* printing [#] %\ensuremath{\mathrel\#}% *)
26
27 (*#* printing ex_unq %\ensuremath{\exists^1}% #&exist;<sup>1</sup># *)
28
29 (*#* printing [o] %\ensuremath\circ% #&sdot;# *)
30
31 (*#* printing [-C-] %\ensuremath\diamond% *)
32
33 (* Begin_SpecReals *)
34
35 (*#* *Setoids
36 Definition of a constructive setoid with apartness,
37 i.e.%\% a set with an equivalence relation and an apartness relation compatible with it.
38 *)
39
40 include "algebra/CLogic.ma".
41
42 include "tactics/Step.ma".
43
44 inline procedural "cic:/CoRN/algebra/CSetoids/Relation.con" as definition.
45
46 (* End_SpecReals *)
47
48 (* UNEXPORTED
49 Implicit Arguments Treflexive [A].
50 *)
51
52 (* UNEXPORTED
53 Implicit Arguments Creflexive [A].
54 *)
55
56 (* Begin_SpecReals *)
57
58 (* UNEXPORTED
59 Implicit Arguments Tsymmetric [A].
60 *)
61
62 (* UNEXPORTED
63 Implicit Arguments Csymmetric [A].
64 *)
65
66 (* UNEXPORTED
67 Implicit Arguments Ttransitive [A].
68 *)
69
70 (* UNEXPORTED
71 Implicit Arguments Ctransitive [A].
72 *)
73
74 (* begin hide *)
75
76 (* UNEXPORTED
77 Set Implicit Arguments.
78 *)
79
80 (* UNEXPORTED
81 Unset Strict Implicit.
82 *)
83
84 (* end hide *)
85
86 (*#* **Relations necessary for Setoids
87 %\begin{convention}% Let [A:Type].
88 %\end{convention}%
89
90 Notice that their type depends on the main logical connective.
91 *)
92
93 (* UNEXPORTED
94 Section Properties_of_relations
95 *)
96
97 (* UNEXPORTED
98 cic:/CoRN/algebra/CSetoids/Properties_of_relations/A.var
99 *)
100
101 inline procedural "cic:/CoRN/algebra/CSetoids/irreflexive.con" as definition.
102
103 inline procedural "cic:/CoRN/algebra/CSetoids/cotransitive.con" as definition.
104
105 inline procedural "cic:/CoRN/algebra/CSetoids/tight_apart.con" as definition.
106
107 inline procedural "cic:/CoRN/algebra/CSetoids/antisymmetric.con" as definition.
108
109 (* UNEXPORTED
110 End Properties_of_relations
111 *)
112
113 (* begin hide *)
114
115 (* UNEXPORTED
116 Set Strict Implicit.
117 *)
118
119 (* UNEXPORTED
120 Unset Implicit Arguments.
121 *)
122
123 (* end hide *)
124
125 (*#* **Definition of Setoid
126
127 Apartness, being the main relation, needs to be [CProp]-valued.  Equality,
128 as it is characterized by a negative statement, lives in [Prop]. *)
129
130 inline procedural "cic:/CoRN/algebra/CSetoids/is_CSetoid.ind".
131
132 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid.ind".
133
134 (* COERCION
135 cic:/matita/CoRN-Procedural/algebra/CSetoids/cs_crr.con
136 *)
137
138 (* UNEXPORTED
139 Implicit Arguments cs_eq [c].
140 *)
141
142 (* UNEXPORTED
143 Implicit Arguments cs_ap [c].
144 *)
145
146 (* NOTATION
147 Infix "[=]" := cs_eq (at level 70, no associativity).
148 *)
149
150 (* NOTATION
151 Infix "[#]" := cs_ap (at level 70, no associativity).
152 *)
153
154 (* End_SpecReals *)
155
156 inline procedural "cic:/CoRN/algebra/CSetoids/cs_neq.con" as definition.
157
158 (* UNEXPORTED
159 Implicit Arguments cs_neq [S].
160 *)
161
162 (* NOTATION
163 Infix "[~=]" := cs_neq (at level 70, no associativity).
164 *)
165
166 (*#*
167 %\begin{nameconvention}%
168 In the names of lemmas, we refer to [ [=] ] by [eq], [ [~=] ] by
169 [neq], and [ [#] ] by [ap].
170 %\end{nameconvention}%
171
172 ** Setoid axioms
173 We want concrete lemmas that state the axiomatic properties of a setoid.
174 %\begin{convention}%
175 Let [S] be a setoid.
176 %\end{convention}%
177 *)
178
179 (* Begin_SpecReals *)
180
181 (* UNEXPORTED
182 Section CSetoid_axioms
183 *)
184
185 (* UNEXPORTED
186 cic:/CoRN/algebra/CSetoids/CSetoid_axioms/S.var
187 *)
188
189 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_is_CSetoid.con" as lemma.
190
191 inline procedural "cic:/CoRN/algebra/CSetoids/ap_irreflexive.con" as lemma.
192
193 inline procedural "cic:/CoRN/algebra/CSetoids/ap_symmetric.con" as lemma.
194
195 inline procedural "cic:/CoRN/algebra/CSetoids/ap_cotransitive.con" as lemma.
196
197 inline procedural "cic:/CoRN/algebra/CSetoids/ap_tight.con" as lemma.
198
199 (* UNEXPORTED
200 End CSetoid_axioms
201 *)
202
203 (* End_SpecReals *)
204
205 (*#* **Setoid basics%\label{section:setoid-basics}%
206 %\begin{convention}% Let [S] be a setoid.
207 %\end{convention}%
208 *)
209
210 (* Begin_SpecReals *)
211
212 (* UNEXPORTED
213 Section CSetoid_basics
214 *)
215
216 (* UNEXPORTED
217 cic:/CoRN/algebra/CSetoids/CSetoid_basics/S.var
218 *)
219
220 (* End_SpecReals *)
221
222 (*#*
223 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.
224 *)
225
226 inline procedural "cic:/CoRN/algebra/CSetoids/ex_unq.con" as definition.
227
228 inline procedural "cic:/CoRN/algebra/CSetoids/eq_reflexive.con" as lemma.
229
230 inline procedural "cic:/CoRN/algebra/CSetoids/eq_symmetric.con" as lemma.
231
232 inline procedural "cic:/CoRN/algebra/CSetoids/eq_transitive.con" as lemma.
233
234 (*#*
235 %\begin{shortcoming}%
236 The lemma [eq_reflexive] above is convertible to
237 [eq_reflexive_unfolded] below. We need the second version too,
238 because the first cannot be applied when an instance of reflexivity is needed.
239 (``I have complained bitterly about this.'' RP)
240 %\end{shortcoming}%
241
242 %\begin{nameconvention}%
243 If lemma [a] is just an unfolding of lemma [b], the name of [a] is the name
244 [b] with the suffix ``[_unfolded]''.
245 %\end{nameconvention}%
246 *)
247
248 inline procedural "cic:/CoRN/algebra/CSetoids/eq_reflexive_unfolded.con" as lemma.
249
250 inline procedural "cic:/CoRN/algebra/CSetoids/eq_symmetric_unfolded.con" as lemma.
251
252 inline procedural "cic:/CoRN/algebra/CSetoids/eq_transitive_unfolded.con" as lemma.
253
254 inline procedural "cic:/CoRN/algebra/CSetoids/eq_wdl.con" as lemma.
255
256 (* Begin_SpecReals *)
257
258 inline procedural "cic:/CoRN/algebra/CSetoids/ap_irreflexive_unfolded.con" as lemma.
259
260 (* End_SpecReals *)
261
262 inline procedural "cic:/CoRN/algebra/CSetoids/ap_cotransitive_unfolded.con" as lemma.
263
264 inline procedural "cic:/CoRN/algebra/CSetoids/ap_symmetric_unfolded.con" as lemma.
265
266 (*#*
267 %\begin{shortcoming}%
268 We would like to write
269 [[
270 Lemma eq_equiv_not_ap : forall (x y:S), x [=] y Iff ~(x [#] y).
271 ]]
272 In Coq, however, this lemma cannot be easily applied.
273 Therefore we have to split the lemma into the following two lemmas [eq_imp_not_ap] and [not_ap_imp_eq].
274 %\end{shortcoming}%
275 *)
276
277 inline procedural "cic:/CoRN/algebra/CSetoids/eq_imp_not_ap.con" as lemma.
278
279 inline procedural "cic:/CoRN/algebra/CSetoids/not_ap_imp_eq.con" as lemma.
280
281 inline procedural "cic:/CoRN/algebra/CSetoids/neq_imp_notnot_ap.con" as lemma.
282
283 inline procedural "cic:/CoRN/algebra/CSetoids/notnot_ap_imp_neq.con" as lemma.
284
285 inline procedural "cic:/CoRN/algebra/CSetoids/ap_imp_neq.con" as lemma.
286
287 inline procedural "cic:/CoRN/algebra/CSetoids/not_neq_imp_eq.con" as lemma.
288
289 inline procedural "cic:/CoRN/algebra/CSetoids/eq_imp_not_neq.con" as lemma.
290
291 (* Begin_SpecReals *)
292
293 (* UNEXPORTED
294 End CSetoid_basics
295 *)
296
297 (* End_SpecReals *)
298
299 (* UNEXPORTED
300 Section product_csetoid
301 *)
302
303 (*#* **The product of setoids *)
304
305 inline procedural "cic:/CoRN/algebra/CSetoids/prod_ap.con" as definition.
306
307 inline procedural "cic:/CoRN/algebra/CSetoids/prod_eq.con" as definition.
308
309 inline procedural "cic:/CoRN/algebra/CSetoids/prodcsetoid_is_CSetoid.con" as lemma.
310
311 inline procedural "cic:/CoRN/algebra/CSetoids/ProdCSetoid.con" as definition.
312
313 (* UNEXPORTED
314 End product_csetoid
315 *)
316
317 (* UNEXPORTED
318 Implicit Arguments ex_unq [S].
319 *)
320
321 (* UNEXPORTED
322 Hint Resolve eq_reflexive_unfolded: algebra_r.
323 *)
324
325 (* UNEXPORTED
326 Hint Resolve eq_symmetric_unfolded: algebra_s.
327 *)
328
329 (* UNEXPORTED
330 Declare Left Step eq_wdl.
331 *)
332
333 (* UNEXPORTED
334 Declare Right Step eq_transitive_unfolded.
335 *)
336
337 (* Begin_SpecReals *)
338
339 (*#* **Relations and predicates
340 Here we define the notions of well-definedness and strong extensionality
341 on predicates and relations.
342
343 %\begin{convention}% Let [S] be a setoid.
344 %\end{convention}%
345
346 %\begin{nameconvention}%
347 - ``well-defined'' is abbreviated to [well_def] (or [wd]).
348 - ``strongly extensional'' is abbreviated to [strong_ext] (or [strext]).
349
350 %\end{nameconvention}%
351 *)
352
353 (* UNEXPORTED
354 Section CSetoid_relations_and_predicates
355 *)
356
357 (* UNEXPORTED
358 cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/S.var
359 *)
360
361 (* End_SpecReals *)
362
363 (*#* ***Predicates
364
365 At this stage, we consider [CProp]- and [Prop]-valued predicates on setoids.
366
367 %\begin{convention}% Let [P] be a predicate on (the carrier of) [S].
368 %\end{convention}%
369 *)
370
371 (* UNEXPORTED
372 Section CSetoidPredicates
373 *)
374
375 (* UNEXPORTED
376 cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CSetoidPredicates/P.var
377 *)
378
379 inline procedural "cic:/CoRN/algebra/CSetoids/pred_strong_ext.con" as definition.
380
381 inline procedural "cic:/CoRN/algebra/CSetoids/pred_wd.con" as definition.
382
383 (* UNEXPORTED
384 End CSetoidPredicates
385 *)
386
387 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_predicate.ind".
388
389 (* COERCION
390 cic:/matita/CoRN-Procedural/algebra/CSetoids/csp_pred.con
391 *)
392
393 inline procedural "cic:/CoRN/algebra/CSetoids/csp_wd.con" as lemma.
394
395 (*#* Similar, with [Prop] instead of [CProp]. *)
396
397 (* UNEXPORTED
398 Section CSetoidPPredicates
399 *)
400
401 (* UNEXPORTED
402 cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CSetoidPPredicates/P.var
403 *)
404
405 inline procedural "cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con" as definition.
406
407 inline procedural "cic:/CoRN/algebra/CSetoids/pred_wd'.con" as definition.
408
409 (* UNEXPORTED
410 End CSetoidPPredicates
411 *)
412
413 (*#* ***Definition of a setoid predicate *)
414
415 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind".
416
417 (* COERCION
418 cic:/matita/CoRN-Procedural/algebra/CSetoids/csp'_pred.con
419 *)
420
421 inline procedural "cic:/CoRN/algebra/CSetoids/csp'_wd.con" as lemma.
422
423 (* Begin_SpecReals *)
424
425 (*#* ***Relations
426 %\begin{convention}%
427 Let [R] be a relation on (the carrier of) [S].
428 %\end{convention}% *)
429
430 (* UNEXPORTED
431 Section CsetoidRelations
432 *)
433
434 (* UNEXPORTED
435 cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CsetoidRelations/R.var
436 *)
437
438 inline procedural "cic:/CoRN/algebra/CSetoids/rel_wdr.con" as definition.
439
440 inline procedural "cic:/CoRN/algebra/CSetoids/rel_wdl.con" as definition.
441
442 inline procedural "cic:/CoRN/algebra/CSetoids/rel_strext.con" as definition.
443
444 (* End_SpecReals *)
445
446 inline procedural "cic:/CoRN/algebra/CSetoids/rel_strext_lft.con" as definition.
447
448 inline procedural "cic:/CoRN/algebra/CSetoids/rel_strext_rht.con" as definition.
449
450 inline procedural "cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con" as lemma.
451
452 inline procedural "cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con" as lemma.
453
454 inline procedural "cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con" as lemma.
455
456 (* Begin_SpecReals *)
457
458 (* UNEXPORTED
459 End CsetoidRelations
460 *)
461
462 (*#* ***Definition of a setoid relation
463 The type of relations over a setoid.  *)
464
465 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind".
466
467 (* COERCION
468 cic:/matita/CoRN-Procedural/algebra/CSetoids/csr_rel.con
469 *)
470
471 (*#* ***[CProp] Relations
472 %\begin{convention}%
473 Let [R] be a relation on (the carrier of) [S].
474 %\end{convention}%
475 *)
476
477 (* UNEXPORTED
478 Section CCsetoidRelations
479 *)
480
481 (* UNEXPORTED
482 cic:/CoRN/algebra/CSetoids/CSetoid_relations_and_predicates/CCsetoidRelations/R.var
483 *)
484
485 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_wdr.con" as definition.
486
487 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_wdl.con" as definition.
488
489 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_strext.con" as definition.
490
491 (* End_SpecReals *)
492
493 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con" as definition.
494
495 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con" as definition.
496
497 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con" as lemma.
498
499 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con" as lemma.
500
501 inline procedural "cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con" as lemma.
502
503 (* Begin_SpecReals *)
504
505 (* UNEXPORTED
506 End CCsetoidRelations
507 *)
508
509 (*#* ***Definition of a [CProp] setoid relation
510
511 The type of relations over a setoid.  *)
512
513 inline procedural "cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind".
514
515 (* COERCION
516 cic:/matita/CoRN-Procedural/algebra/CSetoids/Ccsr_rel.con
517 *)
518
519 inline procedural "cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con" as lemma.
520
521 inline procedural "cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con" as lemma.
522
523 (* End_SpecReals *)
524
525 inline procedural "cic:/CoRN/algebra/CSetoids/ap_wdr.con" as lemma.
526
527 inline procedural "cic:/CoRN/algebra/CSetoids/ap_wdl.con" as lemma.
528
529 inline procedural "cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con" as lemma.
530
531 inline procedural "cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con" as lemma.
532
533 inline procedural "cic:/CoRN/algebra/CSetoids/ap_strext.con" as lemma.
534
535 inline procedural "cic:/CoRN/algebra/CSetoids/predS_well_def.con" as definition.
536
537 (* Begin_SpecReals *)
538
539 (* UNEXPORTED
540 End CSetoid_relations_and_predicates
541 *)
542
543 (* UNEXPORTED
544 Declare Left Step ap_wdl_unfolded.
545 *)
546
547 (* UNEXPORTED
548 Declare Right Step ap_wdr_unfolded.
549 *)
550
551 (* End_SpecReals *)
552
553 (*#* **Functions between setoids
554 Such functions must preserve the setoid equality
555 and be strongly extensional w.r.t.%\% the apartness, i.e.%\%
556 if [f(x,y) [#] f(x1,y1)], then  [x [#] x1 + y [#] y1].
557 For every arity this has to be defined separately.
558 %\begin{convention}%
559 Let [S1], [S2] and [S3] be setoids.
560 %\end{convention}%
561
562 First we consider unary functions.  *)
563
564 (* Begin_SpecReals *)
565
566 (* UNEXPORTED
567 Section CSetoid_functions
568 *)
569
570 (* UNEXPORTED
571 cic:/CoRN/algebra/CSetoids/CSetoid_functions/S1.var
572 *)
573
574 (* UNEXPORTED
575 cic:/CoRN/algebra/CSetoids/CSetoid_functions/S2.var
576 *)
577
578 (* UNEXPORTED
579 cic:/CoRN/algebra/CSetoids/CSetoid_functions/S3.var
580 *)
581
582 (* UNEXPORTED
583 Section unary_functions
584 *)
585
586 (*#*
587 In the following two definitions,
588 [f] is a function from (the carrier of) [S1] to
589 (the carrier of) [S2].  *)
590
591 (* UNEXPORTED
592 cic:/CoRN/algebra/CSetoids/CSetoid_functions/unary_functions/f.var
593 *)
594
595 inline procedural "cic:/CoRN/algebra/CSetoids/fun_wd.con" as definition.
596
597 inline procedural "cic:/CoRN/algebra/CSetoids/fun_strext.con" as definition.
598
599 (* End_SpecReals *)
600
601 inline procedural "cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con" as lemma.
602
603 (* Begin_SpecReals *)
604
605 (* UNEXPORTED
606 End unary_functions
607 *)
608
609 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind".
610
611 (* COERCION
612 cic:/matita/CoRN-Procedural/algebra/CSetoids/csf_fun.con
613 *)
614
615 inline procedural "cic:/CoRN/algebra/CSetoids/csf_wd.con" as lemma.
616
617 (* End_SpecReals *)
618
619 inline procedural "cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con" as definition.
620
621 (* Begin_SpecReals *)
622
623 (* UNEXPORTED
624 Section binary_functions
625 *)
626
627 (*#*
628 Now we consider binary functions.
629 In the following two definitions,
630 [f] is a function from [S1] and [S2] to [S3].
631 *)
632
633 (* UNEXPORTED
634 cic:/CoRN/algebra/CSetoids/CSetoid_functions/binary_functions/f.var
635 *)
636
637 inline procedural "cic:/CoRN/algebra/CSetoids/bin_fun_wd.con" as definition.
638
639 inline procedural "cic:/CoRN/algebra/CSetoids/bin_fun_strext.con" as definition.
640
641 (* End_SpecReals *)
642
643 inline procedural "cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con" as lemma.
644
645 (* Begin_SpecReals *)
646
647 (* UNEXPORTED
648 End binary_functions
649 *)
650
651 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind".
652
653 (* COERCION
654 cic:/matita/CoRN-Procedural/algebra/CSetoids/csbf_fun.con
655 *)
656
657 inline procedural "cic:/CoRN/algebra/CSetoids/csbf_wd.con" as lemma.
658
659 inline procedural "cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con" as lemma.
660
661 inline procedural "cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con" as lemma.
662
663 inline procedural "cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con" as lemma.
664
665 (* UNEXPORTED
666 End CSetoid_functions
667 *)
668
669 (* End_SpecReals *)
670
671 (* UNEXPORTED
672 Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.
673 *)
674
675 (* UNEXPORTED
676 Implicit Arguments fun_wd [S1 S2].
677 *)
678
679 (* UNEXPORTED
680 Implicit Arguments fun_strext [S1 S2].
681 *)
682
683 (* Begin_SpecReals *)
684
685 (*#* **The unary and binary (inner) operations on a csetoid
686 An operation is a function with domain(s) and co-domain equal.
687
688 %\begin{nameconvention}%
689 The word ``unary operation'' is abbreviated to [un_op];
690 ``binary operation'' is abbreviated to [bin_op].
691 %\end{nameconvention}%
692
693 %\begin{convention}%
694 Let [S] be a setoid.
695 %\end{convention}%
696 *)
697
698 (* UNEXPORTED
699 Section csetoid_inner_ops
700 *)
701
702 (* UNEXPORTED
703 cic:/CoRN/algebra/CSetoids/csetoid_inner_ops/S.var
704 *)
705
706 (*#* Properties of binary operations *)
707
708 inline procedural "cic:/CoRN/algebra/CSetoids/commutes.con" as definition.
709
710 inline procedural "cic:/CoRN/algebra/CSetoids/associative.con" as definition.
711
712 (*#* Well-defined unary operations on a setoid.  *)
713
714 inline procedural "cic:/CoRN/algebra/CSetoids/un_op_wd.con" as definition.
715
716 inline procedural "cic:/CoRN/algebra/CSetoids/un_op_strext.con" as definition.
717
718 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con" as definition.
719
720 inline procedural "cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con" as definition.
721
722 (* End_SpecReals *)
723
724 inline procedural "cic:/CoRN/algebra/CSetoids/id_strext.con" as lemma.
725
726 inline procedural "cic:/CoRN/algebra/CSetoids/id_pres_eq.con" as lemma.
727
728 inline procedural "cic:/CoRN/algebra/CSetoids/id_un_op.con" as definition.
729
730 (* begin hide *)
731
732 (* COERCION
733 cic:/matita/CoRN-Procedural/algebra/CSetoids/un_op_fun.con
734 *)
735
736 (* end hide *)
737
738 (* Begin_SpecReals *)
739
740 inline procedural "cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con" as definition.
741
742 (* End_SpecReals *)
743
744 inline procedural "cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con" as lemma.
745
746 inline procedural "cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con" as lemma.
747
748 (*#* Well-defined binary operations on a setoid.  *)
749
750 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_wd.con" as definition.
751
752 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_strext.con" as definition.
753
754 (* Begin_SpecReals *)
755
756 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con" as definition.
757
758 inline procedural "cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con" as definition.
759
760 (* End_SpecReals *)
761
762 inline procedural "cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con" as definition.
763
764 inline procedural "cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con" as definition.
765
766 (* Begin_SpecReals *)
767
768 (* begin hide *)
769
770 (* COERCION
771 cic:/matita/CoRN-Procedural/algebra/CSetoids/bin_op_bin_fun.con
772 *)
773
774 (* end hide *)
775
776 (* End_SpecReals *)
777
778 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con" as lemma.
779
780 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con" as lemma.
781
782 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con" as lemma.
783
784 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con" as lemma.
785
786 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con" as lemma.
787
788 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con" as lemma.
789
790 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con" as definition.
791
792 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con" as definition.
793
794 (* Begin_SpecReals *)
795
796 (* UNEXPORTED
797 End csetoid_inner_ops
798 *)
799
800 (* End_SpecReals *)
801
802 (* UNEXPORTED
803 Implicit Arguments commutes [S].
804 *)
805
806 (* Begin_SpecReals *)
807
808 (* UNEXPORTED
809 Implicit Arguments associative [S].
810 *)
811
812 (* End_SpecReals *)
813
814 (* UNEXPORTED
815 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
816 *)
817
818 (*#* **The binary outer operations on a csetoid
819 %\begin{convention}%
820 Let [S1] and [S2] be setoids.
821 %\end{convention}%
822 *)
823
824 (* UNEXPORTED
825 Section csetoid_outer_ops
826 *)
827
828 (* UNEXPORTED
829 cic:/CoRN/algebra/CSetoids/csetoid_outer_ops/S1.var
830 *)
831
832 (* UNEXPORTED
833 cic:/CoRN/algebra/CSetoids/csetoid_outer_ops/S2.var
834 *)
835
836 (*#*
837 Well-defined outer operations on a setoid.
838 *)
839
840 inline procedural "cic:/CoRN/algebra/CSetoids/outer_op_well_def.con" as definition.
841
842 inline procedural "cic:/CoRN/algebra/CSetoids/outer_op_strext.con" as definition.
843
844 inline procedural "cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con" as definition.
845
846 inline procedural "cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con" as definition.
847
848 inline procedural "cic:/CoRN/algebra/CSetoids/csoo_wd.con" as definition.
849
850 inline procedural "cic:/CoRN/algebra/CSetoids/csoo_strext.con" as definition.
851
852 (* begin hide *)
853
854 (* COERCION
855 cic:/matita/CoRN-Procedural/algebra/CSetoids/outer_op_bin_fun.con
856 *)
857
858 (* end hide *)
859
860 inline procedural "cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con" as lemma.
861
862 (* UNEXPORTED
863 End csetoid_outer_ops
864 *)
865
866 (* UNEXPORTED
867 Hint Resolve csoo_wd_unfolded: algebra_c.
868 *)
869
870 (* Begin_SpecReals *)
871
872 (*#* **Subsetoids
873 %\begin{convention}%
874 Let [S] be a setoid, and [P] a predicate on the carrier of [S].
875 %\end{convention}%
876 *)
877
878 (* UNEXPORTED
879 Section SubCSetoids
880 *)
881
882 (* UNEXPORTED
883 cic:/CoRN/algebra/CSetoids/SubCSetoids/S.var
884 *)
885
886 (* UNEXPORTED
887 cic:/CoRN/algebra/CSetoids/SubCSetoids/P.var
888 *)
889
890 inline procedural "cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind".
891
892 (* COERCION
893 cic:/matita/CoRN-Procedural/algebra/CSetoids/scs_elem.con
894 *)
895
896 (*#* Though [scs_elem] is declared as a coercion, it does not satisfy the
897 uniform inheritance condition and will not be inserted.  However it will
898 also not be printed, which is handy.
899 *)
900
901 inline procedural "cic:/CoRN/algebra/CSetoids/restrict_relation.con" as definition.
902
903 inline procedural "cic:/CoRN/algebra/CSetoids/Crestrict_relation.con" as definition.
904
905 inline procedural "cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con" as definition.
906
907 inline procedural "cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con" as definition.
908
909 (* End_SpecReals *)
910
911 inline procedural "cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con" as remark.
912
913 (* Begin_SpecReals *)
914
915 inline procedural "cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con" as lemma.
916
917 inline procedural "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con" as definition.
918
919 (* End_SpecReals *)
920
921 (*#* ***Subsetoid unary operations
922 %\begin{convention}%
923 Let [f] be a unary setoid operation on [S].
924 %\end{convention}%
925 *)
926
927 (* UNEXPORTED
928 Section SubCSetoid_unary_operations
929 *)
930
931 (* UNEXPORTED
932 cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_unary_operations/f.var
933 *)
934
935 inline procedural "cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con" as definition.
936
937 (*#*
938 %\begin{convention}%
939 Assume [pr:un_op_pres_pred].
940 %\end{convention}% *)
941
942 (* UNEXPORTED
943 cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_unary_operations/pr.var
944 *)
945
946 inline procedural "cic:/CoRN/algebra/CSetoids/restr_un_op.con" as definition.
947
948 inline procedural "cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con" as lemma.
949
950 inline procedural "cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con" as lemma.
951
952 inline procedural "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con" as definition.
953
954 (* UNEXPORTED
955 End SubCSetoid_unary_operations
956 *)
957
958 (*#* ***Subsetoid binary operations
959 %\begin{convention}%
960 Let [f] be a binary setoid operation on [S].
961 %\end{convention}%
962 *)
963
964 (* UNEXPORTED
965 Section SubCSetoid_binary_operations
966 *)
967
968 (* UNEXPORTED
969 cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_binary_operations/f.var
970 *)
971
972 inline procedural "cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con" as definition.
973
974 (*#*
975 %\begin{convention}%
976 Assume [bin_op_pres_pred].
977 %\end{convention}%
978 *)
979
980 (* UNEXPORTED
981 cic:/CoRN/algebra/CSetoids/SubCSetoids/SubCSetoid_binary_operations/pr.var
982 *)
983
984 inline procedural "cic:/CoRN/algebra/CSetoids/restr_bin_op.con" as definition.
985
986 inline procedural "cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con" as lemma.
987
988 inline procedural "cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con" as lemma.
989
990 inline procedural "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con" as definition.
991
992 inline procedural "cic:/CoRN/algebra/CSetoids/restr_f_assoc.con" as lemma.
993
994 (* UNEXPORTED
995 End SubCSetoid_binary_operations
996 *)
997
998 (* Begin_SpecReals *)
999
1000 (* UNEXPORTED
1001 End SubCSetoids
1002 *)
1003
1004 (* End_SpecReals *)
1005
1006 (* begin hide *)
1007
1008 (* UNEXPORTED
1009 Ltac Step_final x := apply eq_transitive_unfolded with x; Algebra.
1010 *)
1011
1012 (* end hide *)
1013
1014 (* UNEXPORTED
1015 Tactic Notation "Step_final" constr(c) :=  Step_final c.
1016 *)
1017
1018 (*#* **Miscellaneous
1019 *)
1020
1021 inline procedural "cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con" as lemma.
1022
1023 (*#*
1024 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
1025 *)
1026
1027 inline procedural "cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con" as definition.
1028
1029 inline procedural "cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con" as definition.
1030
1031 (* UNEXPORTED
1032 Implicit Arguments nat_less_n_fun [S n].
1033 *)
1034
1035 (* UNEXPORTED
1036 Implicit Arguments nat_less_n_fun' [S n].
1037 *)
1038