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