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