matita/contribs/CoRN-Decl/algebra/CSetoids.ma

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