helm/software/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_notation.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 inline "cic:/CoRN/algebra/CSetoids/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 (* 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 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csp_pred.con" 0 (* compounds *).
 368
 369 inline "cic:/CoRN/algebra/CSetoids/csp_wd.con".
 370
 371 (*#* Similar, with [Prop] instead of [CProp]. *)
 372
 373 (* UNEXPORTED
 374 Section CSetoidPPredicates.
 375 *)
 376
 377 inline "cic:/CoRN/algebra/CSetoids/P.var".
 378
 379 inline "cic:/CoRN/algebra/CSetoids/pred_strong_ext'.con".
 380
 381 inline "cic:/CoRN/algebra/CSetoids/pred_wd'.con".
 382
 383 (* UNEXPORTED
 384 End CSetoidPPredicates.
 385 *)
 386
 387 (*#* ***Definition of a setoid predicate *)
 388
 389 inline "cic:/CoRN/algebra/CSetoids/CSetoid_predicate'.ind".
 390
 391 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csp'_pred.con" 0 (* compounds *).
 392
 393 inline "cic:/CoRN/algebra/CSetoids/csp'_wd.con".
 394
 395 (* Begin_SpecReals *)
 396
 397 (*#* ***Relations
 398 %\begin{convention}%
 399 Let [R] be a relation on (the carrier of) [S].
 400 %\end{convention}% *)
 401
 402 (* UNEXPORTED
 403 Section CsetoidRelations.
 404 *)
 405
 406 inline "cic:/CoRN/algebra/CSetoids/R.var".
 407
 408 inline "cic:/CoRN/algebra/CSetoids/rel_wdr.con".
 409
 410 inline "cic:/CoRN/algebra/CSetoids/rel_wdl.con".
 411
 412 inline "cic:/CoRN/algebra/CSetoids/rel_strext.con".
 413
 414 (* End_SpecReals *)
 415
 416 inline "cic:/CoRN/algebra/CSetoids/rel_strext_lft.con".
 417
 418 inline "cic:/CoRN/algebra/CSetoids/rel_strext_rht.con".
 419
 420 inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_lftarg.con".
 421
 422 inline "cic:/CoRN/algebra/CSetoids/rel_strext_imp_rhtarg.con".
 423
 424 inline "cic:/CoRN/algebra/CSetoids/rel_strextarg_imp_strext.con".
 425
 426 (* Begin_SpecReals *)
 427
 428 (* UNEXPORTED
 429 End CsetoidRelations.
 430 *)
 431
 432 (*#* ***Definition of a setoid relation
 433 The type of relations over a setoid.  *)
 434
 435 inline "cic:/CoRN/algebra/CSetoids/CSetoid_relation.ind".
 436
 437 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csr_rel.con" 0 (* compounds *).
 438
 439 (*#* ***[CProp] Relations
 440 %\begin{convention}%
 441 Let [R] be a relation on (the carrier of) [S].
 442 %\end{convention}%
 443 *)
 444
 445 (* UNEXPORTED
 446 Section CCsetoidRelations.
 447 *)
 448
 449 inline "cic:/CoRN/algebra/CSetoids/R.var".
 450
 451 inline "cic:/CoRN/algebra/CSetoids/Crel_wdr.con".
 452
 453 inline "cic:/CoRN/algebra/CSetoids/Crel_wdl.con".
 454
 455 inline "cic:/CoRN/algebra/CSetoids/Crel_strext.con".
 456
 457 (* End_SpecReals *)
 458
 459 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_lft.con".
 460
 461 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_rht.con".
 462
 463 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_lftarg.con".
 464
 465 inline "cic:/CoRN/algebra/CSetoids/Crel_strext_imp_rhtarg.con".
 466
 467 inline "cic:/CoRN/algebra/CSetoids/Crel_strextarg_imp_strext.con".
 468
 469 (* Begin_SpecReals *)
 470
 471 (* UNEXPORTED
 472 End CCsetoidRelations.
 473 *)
 474
 475 (*#* ***Definition of a [CProp] setoid relation
 476
 477 The type of relations over a setoid.  *)
 478
 479 inline "cic:/CoRN/algebra/CSetoids/CCSetoid_relation.ind".
 480
 481 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/Ccsr_rel.con" 0 (* compounds *).
 482
 483 inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdr.con".
 484
 485 inline "cic:/CoRN/algebra/CSetoids/Ccsr_wdl.con".
 486
 487 (* End_SpecReals *)
 488
 489 inline "cic:/CoRN/algebra/CSetoids/ap_wdr.con".
 490
 491 inline "cic:/CoRN/algebra/CSetoids/ap_wdl.con".
 492
 493 inline "cic:/CoRN/algebra/CSetoids/ap_wdr_unfolded.con".
 494
 495 inline "cic:/CoRN/algebra/CSetoids/ap_wdl_unfolded.con".
 496
 497 inline "cic:/CoRN/algebra/CSetoids/ap_strext.con".
 498
 499 inline "cic:/CoRN/algebra/CSetoids/predS_well_def.con".
 500
 501 (* Begin_SpecReals *)
 502
 503 (* UNEXPORTED
 504 End CSetoid_relations_and_predicates.
 505 *)
 506
 507 (* UNEXPORTED
 508 Declare Left Step ap_wdl_unfolded.
 509 *)
 510
 511 (* UNEXPORTED
 512 Declare Right Step ap_wdr_unfolded.
 513 *)
 514
 515 (* End_SpecReals *)
 516
 517 (*#* **Functions between setoids
 518 Such functions must preserve the setoid equality
 519 and be strongly extensional w.r.t.%\% the apartness, i.e.%\%
 520 if [f(x,y) [#] f(x1,y1)], then  [x [#] x1 + y [#] y1].
 521 For every arity this has to be defined separately.
 522 %\begin{convention}%
 523 Let [S1], [S2] and [S3] be setoids.
 524 %\end{convention}%
 525
 526 First we consider unary functions.  *)
 527
 528 (* Begin_SpecReals *)
 529
 530 (* UNEXPORTED
 531 Section CSetoid_functions.
 532 *)
 533
 534 inline "cic:/CoRN/algebra/CSetoids/S1.var".
 535
 536 inline "cic:/CoRN/algebra/CSetoids/S2.var".
 537
 538 inline "cic:/CoRN/algebra/CSetoids/S3.var".
 539
 540 (* UNEXPORTED
 541 Section unary_functions.
 542 *)
 543
 544 (*#*
 545 In the following two definitions,
 546 [f] is a function from (the carrier of) [S1] to
 547 (the carrier of) [S2].  *)
 548
 549 inline "cic:/CoRN/algebra/CSetoids/f.var".
 550
 551 inline "cic:/CoRN/algebra/CSetoids/fun_wd.con".
 552
 553 inline "cic:/CoRN/algebra/CSetoids/fun_strext.con".
 554
 555 (* End_SpecReals *)
 556
 557 inline "cic:/CoRN/algebra/CSetoids/fun_strext_imp_wd.con".
 558
 559 (* Begin_SpecReals *)
 560
 561 (* UNEXPORTED
 562 End unary_functions.
 563 *)
 564
 565 inline "cic:/CoRN/algebra/CSetoids/CSetoid_fun.ind".
 566
 567 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csf_fun.con" 0 (* compounds *).
 568
 569 inline "cic:/CoRN/algebra/CSetoids/csf_wd.con".
 570
 571 (* End_SpecReals *)
 572
 573 inline "cic:/CoRN/algebra/CSetoids/Const_CSetoid_fun.con".
 574
 575 (* Begin_SpecReals *)
 576
 577 (* UNEXPORTED
 578 Section binary_functions.
 579 *)
 580
 581 (*#*
 582 Now we consider binary functions.
 583 In the following two definitions,
 584 [f] is a function from [S1] and [S2] to [S3].
 585 *)
 586
 587 inline "cic:/CoRN/algebra/CSetoids/f.var".
 588
 589 inline "cic:/CoRN/algebra/CSetoids/bin_fun_wd.con".
 590
 591 inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext.con".
 592
 593 (* End_SpecReals *)
 594
 595 inline "cic:/CoRN/algebra/CSetoids/bin_fun_strext_imp_wd.con".
 596
 597 (* Begin_SpecReals *)
 598
 599 (* UNEXPORTED
 600 End binary_functions.
 601 *)
 602
 603 inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_fun.ind".
 604
 605 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/csbf_fun.con" 0 (* compounds *).
 606
 607 inline "cic:/CoRN/algebra/CSetoids/csbf_wd.con".
 608
 609 inline "cic:/CoRN/algebra/CSetoids/csf_wd_unfolded.con".
 610
 611 inline "cic:/CoRN/algebra/CSetoids/csf_strext_unfolded.con".
 612
 613 inline "cic:/CoRN/algebra/CSetoids/csbf_wd_unfolded.con".
 614
 615 (* UNEXPORTED
 616 End CSetoid_functions.
 617 *)
 618
 619 (* End_SpecReals *)
 620
 621 (* UNEXPORTED
 622 Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.
 623 *)
 624
 625 (* UNEXPORTED
 626 Implicit Arguments fun_wd [S1 S2].
 627 *)
 628
 629 (* UNEXPORTED
 630 Implicit Arguments fun_strext [S1 S2].
 631 *)
 632
 633 (* Begin_SpecReals *)
 634
 635 (*#* **The unary and binary (inner) operations on a csetoid
 636 An operation is a function with domain(s) and co-domain equal.
 637
 638 %\begin{nameconvention}%
 639 The word ``unary operation'' is abbreviated to [un_op];
 640 ``binary operation'' is abbreviated to [bin_op].
 641 %\end{nameconvention}%
 642
 643 %\begin{convention}%
 644 Let [S] be a setoid.
 645 %\end{convention}%
 646 *)
 647
 648 (* UNEXPORTED
 649 Section csetoid_inner_ops.
 650 *)
 651
 652 inline "cic:/CoRN/algebra/CSetoids/S.var".
 653
 654 (*#* Properties of binary operations *)
 655
 656 inline "cic:/CoRN/algebra/CSetoids/commutes.con".
 657
 658 inline "cic:/CoRN/algebra/CSetoids/associative.con".
 659
 660 (*#* Well-defined unary operations on a setoid.  *)
 661
 662 inline "cic:/CoRN/algebra/CSetoids/un_op_wd.con".
 663
 664 inline "cic:/CoRN/algebra/CSetoids/un_op_strext.con".
 665
 666 inline "cic:/CoRN/algebra/CSetoids/CSetoid_un_op.con".
 667
 668 inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_un_op.con".
 669
 670 (* End_SpecReals *)
 671
 672 inline "cic:/CoRN/algebra/CSetoids/id_strext.con".
 673
 674 inline "cic:/CoRN/algebra/CSetoids/id_pres_eq.con".
 675
 676 inline "cic:/CoRN/algebra/CSetoids/id_un_op.con".
 677
 678 (* begin hide *)
 679
 680 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/un_op_fun.con" 0 (* compounds *).
 681
 682 (* end hide *)
 683
 684 (* Begin_SpecReals *)
 685
 686 inline "cic:/CoRN/algebra/CSetoids/cs_un_op_strext.con".
 687
 688 (* End_SpecReals *)
 689
 690 inline "cic:/CoRN/algebra/CSetoids/un_op_wd_unfolded.con".
 691
 692 inline "cic:/CoRN/algebra/CSetoids/un_op_strext_unfolded.con".
 693
 694 (*#* Well-defined binary operations on a setoid.  *)
 695
 696 inline "cic:/CoRN/algebra/CSetoids/bin_op_wd.con".
 697
 698 inline "cic:/CoRN/algebra/CSetoids/bin_op_strext.con".
 699
 700 (* Begin_SpecReals *)
 701
 702 inline "cic:/CoRN/algebra/CSetoids/CSetoid_bin_op.con".
 703
 704 inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_bin_op.con".
 705
 706 (* End_SpecReals *)
 707
 708 inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_wd.con".
 709
 710 inline "cic:/CoRN/algebra/CSetoids/cs_bin_op_strext.con".
 711
 712 (* Begin_SpecReals *)
 713
 714 (* begin hide *)
 715
 716 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/bin_op_bin_fun.con" 0 (* compounds *).
 717
 718 (* end hide *)
 719
 720 (* End_SpecReals *)
 721
 722 inline "cic:/CoRN/algebra/CSetoids/bin_op_wd_unfolded.con".
 723
 724 inline "cic:/CoRN/algebra/CSetoids/bin_op_strext_unfolded.con".
 725
 726 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_lft.con".
 727
 728 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_wd_un_op_rht.con".
 729
 730 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_lft.con".
 731
 732 inline "cic:/CoRN/algebra/CSetoids/bin_op_is_strext_un_op_rht.con".
 733
 734 inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_rht.con".
 735
 736 inline "cic:/CoRN/algebra/CSetoids/bin_op2un_op_lft.con".
 737
 738 (* Begin_SpecReals *)
 739
 740 (* UNEXPORTED
 741 End csetoid_inner_ops.
 742 *)
 743
 744 (* End_SpecReals *)
 745
 746 (* UNEXPORTED
 747 Implicit Arguments commutes [S].
 748 *)
 749
 750 (* Begin_SpecReals *)
 751
 752 (* UNEXPORTED
 753 Implicit Arguments associative [S].
 754 *)
 755
 756 (* End_SpecReals *)
 757
 758 (* UNEXPORTED
 759 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
 760 *)
 761
 762 (*#* **The binary outer operations on a csetoid
 763 %\begin{convention}%
 764 Let [S1] and [S2] be setoids.
 765 %\end{convention}%
 766 *)
 767
 768 (* UNEXPORTED
 769 Section csetoid_outer_ops.
 770 *)
 771
 772 inline "cic:/CoRN/algebra/CSetoids/S1.var".
 773
 774 inline "cic:/CoRN/algebra/CSetoids/S2.var".
 775
 776 (*#*
 777 Well-defined outer operations on a setoid.
 778 *)
 779
 780 inline "cic:/CoRN/algebra/CSetoids/outer_op_well_def.con".
 781
 782 inline "cic:/CoRN/algebra/CSetoids/outer_op_strext.con".
 783
 784 inline "cic:/CoRN/algebra/CSetoids/CSetoid_outer_op.con".
 785
 786 inline "cic:/CoRN/algebra/CSetoids/Build_CSetoid_outer_op.con".
 787
 788 inline "cic:/CoRN/algebra/CSetoids/csoo_wd.con".
 789
 790 inline "cic:/CoRN/algebra/CSetoids/csoo_strext.con".
 791
 792 (* begin hide *)
 793
 794 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/outer_op_bin_fun.con" 0 (* compounds *).
 795
 796 (* end hide *)
 797
 798 inline "cic:/CoRN/algebra/CSetoids/csoo_wd_unfolded.con".
 799
 800 (* UNEXPORTED
 801 End csetoid_outer_ops.
 802 *)
 803
 804 (* UNEXPORTED
 805 Hint Resolve csoo_wd_unfolded: algebra_c.
 806 *)
 807
 808 (* Begin_SpecReals *)
 809
 810 (*#* **Subsetoids
 811 %\begin{convention}%
 812 Let [S] be a setoid, and [P] a predicate on the carrier of [S].
 813 %\end{convention}%
 814 *)
 815
 816 (* UNEXPORTED
 817 Section SubCSetoids.
 818 *)
 819
 820 inline "cic:/CoRN/algebra/CSetoids/S.var".
 821
 822 inline "cic:/CoRN/algebra/CSetoids/P.var".
 823
 824 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_crr.ind".
 825
 826 coercion "cic:/matita/CoRN-Decl/algebra/CSetoids/scs_elem.con" 0 (* compounds *).
 827
 828 (*#* Though [scs_elem] is declared as a coercion, it does not satisfy the
 829 uniform inheritance condition and will not be inserted.  However it will
 830 also not be printed, which is handy.
 831 *)
 832
 833 inline "cic:/CoRN/algebra/CSetoids/restrict_relation.con".
 834
 835 inline "cic:/CoRN/algebra/CSetoids/Crestrict_relation.con".
 836
 837 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_eq.con".
 838
 839 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_ap.con".
 840
 841 (* End_SpecReals *)
 842
 843 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_equiv.con".
 844
 845 (* Begin_SpecReals *)
 846
 847 inline "cic:/CoRN/algebra/CSetoids/subcsetoid_is_CSetoid.con".
 848
 849 inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid.con".
 850
 851 (* End_SpecReals *)
 852
 853 (*#* ***Subsetoid unary operations
 854 %\begin{convention}%
 855 Let [f] be a unary setoid operation on [S].
 856 %\end{convention}%
 857 *)
 858
 859 (* UNEXPORTED
 860 Section SubCSetoid_unary_operations.
 861 *)
 862
 863 inline "cic:/CoRN/algebra/CSetoids/f.var".
 864
 865 inline "cic:/CoRN/algebra/CSetoids/un_op_pres_pred.con".
 866
 867 (*#*
 868 %\begin{convention}%
 869 Assume [pr:un_op_pres_pred].
 870 %\end{convention}% *)
 871
 872 inline "cic:/CoRN/algebra/CSetoids/pr.var".
 873
 874 inline "cic:/CoRN/algebra/CSetoids/restr_un_op.con".
 875
 876 inline "cic:/CoRN/algebra/CSetoids/restr_un_op_wd.con".
 877
 878 inline "cic:/CoRN/algebra/CSetoids/restr_un_op_strext.con".
 879
 880 inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_un_op.con".
 881
 882 (* UNEXPORTED
 883 End SubCSetoid_unary_operations.
 884 *)
 885
 886 (*#* ***Subsetoid binary operations
 887 %\begin{convention}%
 888 Let [f] be a binary setoid operation on [S].
 889 %\end{convention}%
 890 *)
 891
 892 (* UNEXPORTED
 893 Section SubCSetoid_binary_operations.
 894 *)
 895
 896 inline "cic:/CoRN/algebra/CSetoids/f.var".
 897
 898 inline "cic:/CoRN/algebra/CSetoids/bin_op_pres_pred.con".
 899
 900 (*#*
 901 %\begin{convention}%
 902 Assume [bin_op_pres_pred].
 903 %\end{convention}%
 904 *)
 905
 906 inline "cic:/CoRN/algebra/CSetoids/pr.var".
 907
 908 inline "cic:/CoRN/algebra/CSetoids/restr_bin_op.con".
 909
 910 inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_well_def.con".
 911
 912 inline "cic:/CoRN/algebra/CSetoids/restr_bin_op_strext.con".
 913
 914 inline "cic:/CoRN/algebra/CSetoids/Build_SubCSetoid_bin_op.con".
 915
 916 inline "cic:/CoRN/algebra/CSetoids/restr_f_assoc.con".
 917
 918 (* UNEXPORTED
 919 End SubCSetoid_binary_operations.
 920 *)
 921
 922 (* Begin_SpecReals *)
 923
 924 (* UNEXPORTED
 925 End SubCSetoids.
 926 *)
 927
 928 (* End_SpecReals *)
 929
 930 (* begin hide *)
 931
 932 (* UNEXPORTED
 933 Ltac Step_final x := apply eq_transitive_unfolded with x; Algebra.
 934 *)
 935
 936 (* end hide *)
 937
 938 (* UNEXPORTED
 939 Tactic Notation "Step_final" constr(c) :=  Step_final c.
 940 *)
 941
 942 (*#* **Miscellaneous
 943 *)
 944
 945 inline "cic:/CoRN/algebra/CSetoids/proper_caseZ_diff_CS.con".
 946
 947 (*#*
 948 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
 949 *)
 950
 951 inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun.con".
 952
 953 inline "cic:/CoRN/algebra/CSetoids/nat_less_n_fun'.con".
 954
 955 (* UNEXPORTED
 956 Implicit Arguments nat_less_n_fun [S n].
 957 *)
 958
 959 (* UNEXPORTED
 960 Implicit Arguments nat_less_n_fun' [S n].
 961 *)
 962