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}% #&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 "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