matita/contribs/CoRN-Decl/algebra/CSetoidFun.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/CSetoidFun".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: CSetoidFun.v,v 1.10 2004/04/23 10:00:53 lcf Exp $ *)
  22
  23 include "algebra/CSetoids.ma".
  24
  25 (* UNEXPORTED
  26 Section unary_function_composition
  27 *)
  28
  29 (*#* ** Composition of Setoid functions
  30
  31 Let [S1],  [S2] and [S3] be setoids, [f] a
  32 setoid function from [S1] to [S2], and [g] from [S2]
  33 to [S3] in the following definition of composition.  *)
  34
  35 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S1.var".
  36
  37 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S2.var".
  38
  39 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/S3.var".
  40
  41 alias id "f" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/f.var".
  42
  43 alias id "g" = "cic:/CoRN/algebra/CSetoidFun/unary_function_composition/g.var".
  44
  45 inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_fun.con".
  46
  47 (* UNEXPORTED
  48 End unary_function_composition
  49 *)
  50
  51 (* UNEXPORTED
  52 Section unary_and_binary_function_composition
  53 *)
  54
  55 inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_un_fun.con".
  56
  57 inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_bin_fun.con".
  58
  59 inline "cic:/CoRN/algebra/CSetoidFun/compose_CSetoid_un_bin_fun.con".
  60
  61 (* UNEXPORTED
  62 End unary_and_binary_function_composition
  63 *)
  64
  65 (*#* ***Projections
  66 *)
  67
  68 (* UNEXPORTED
  69 Section function_projection
  70 *)
  71
  72 inline "cic:/CoRN/algebra/CSetoidFun/proj_bin_fun.con".
  73
  74 inline "cic:/CoRN/algebra/CSetoidFun/projected_bin_fun.con".
  75
  76 (* UNEXPORTED
  77 End function_projection
  78 *)
  79
  80 (* UNEXPORTED
  81 Section BinProj
  82 *)
  83
  84 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/BinProj/S.var".
  85
  86 inline "cic:/CoRN/algebra/CSetoidFun/binproj1.con".
  87
  88 inline "cic:/CoRN/algebra/CSetoidFun/binproj1_strext.con".
  89
  90 inline "cic:/CoRN/algebra/CSetoidFun/cs_binproj1.con".
  91
  92 (* UNEXPORTED
  93 End BinProj
  94 *)
  95
  96 (*#* **Combining operations
  97 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
  98 %\end{convention}%
  99 *)
 100
 101 (* UNEXPORTED
 102 Section CombiningOperations
 103 *)
 104
 105 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S1.var".
 106
 107 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S2.var".
 108
 109 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/S3.var".
 110
 111 (*#*
 112 In the following definition, we assume [f] is a setoid function from
 113 [S1] to [S2], and [op] is an unary operation on [S2].
 114 Then [opOnFun] is the composition [op] after [f].
 115 *)
 116
 117 (* UNEXPORTED
 118 Section CombiningUnaryOperations
 119 *)
 120
 121 alias id "f" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/f.var".
 122
 123 alias id "op" = "cic:/CoRN/algebra/CSetoidFun/CombiningOperations/CombiningUnaryOperations/op.var".
 124
 125 inline "cic:/CoRN/algebra/CSetoidFun/opOnFun.con".
 126
 127 (* UNEXPORTED
 128 End CombiningUnaryOperations
 129 *)
 130
 131 (* UNEXPORTED
 132 End CombiningOperations
 133 *)
 134
 135 (*#* **Partial Functions
 136
 137 In this section we define a concept of partial function for an
 138 arbitrary setoid.  Essentially, a partial function is what would be
 139 expected---a predicate on the setoid in question and a total function
 140 from the set of points satisfying that predicate to the setoid.  There
 141 is one important limitations to this approach: first, the record we
 142 obtain has type [Type], meaning that we can't use, for instance,
 143 elimination of existential quantifiers.
 144
 145 Furthermore, for reasons we will explain ahead, partial functions will
 146 not be defined via the [CSetoid_fun] record, but the whole structure
 147 will be incorporated in a new record.
 148
 149 Finally, notice that to be completely general the domains of the
 150 functions have to be characterized by a [CProp]-valued predicate;
 151 otherwise, the use you can make of a function will be %\emph{%#<i>#a
 152 priori#</i>#%}% restricted at the moment it is defined.
 153
 154 Before we state our definitions we need to do some work on domains.
 155 *)
 156
 157 (* UNEXPORTED
 158 Section SubSets_of_G
 159 *)
 160
 161 (*#* ***Subsets of Setoids
 162
 163 Subsets of a setoid will be identified with predicates from the
 164 carrier set of the setoid into [CProp].  At this stage, we do not make
 165 any assumptions about these predicates.
 166
 167 We will begin by defining elementary operations on predicates, along
 168 with their basic properties.  In particular, we will work with well
 169 defined predicates, so we will prove that these operations preserve
 170 welldefinedness.
 171
 172 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
 173 %\end{convention}%
 174 *)
 175
 176 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/S.var".
 177
 178 (* UNEXPORTED
 179 Section Conjunction
 180 *)
 181
 182 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/P.var".
 183
 184 alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Conjunction/Q.var".
 185
 186 inline "cic:/CoRN/algebra/CSetoidFun/conjP.con".
 187
 188 inline "cic:/CoRN/algebra/CSetoidFun/prj1.con".
 189
 190 inline "cic:/CoRN/algebra/CSetoidFun/prj2.con".
 191
 192 inline "cic:/CoRN/algebra/CSetoidFun/conj_wd.con".
 193
 194 (* UNEXPORTED
 195 End Conjunction
 196 *)
 197
 198 (* UNEXPORTED
 199 Section Disjunction
 200 *)
 201
 202 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/P.var".
 203
 204 alias id "Q" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Disjunction/Q.var".
 205
 206 (*#*
 207 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
 208 *)
 209
 210 inline "cic:/CoRN/algebra/CSetoidFun/disj.con".
 211
 212 inline "cic:/CoRN/algebra/CSetoidFun/inj1.con".
 213
 214 inline "cic:/CoRN/algebra/CSetoidFun/inj2.con".
 215
 216 inline "cic:/CoRN/algebra/CSetoidFun/disj_wd.con".
 217
 218 (* UNEXPORTED
 219 End Disjunction
 220 *)
 221
 222 (* UNEXPORTED
 223 Section Extension
 224 *)
 225
 226 (*#*
 227 The next definition is a bit tricky, and is useful for choosing among the elements that satisfy a predicate [P] those that also satisfy [R] in the case where [R] is only defined for elements satisfying [P]---consider [R] to be a condition on the image of an object via a function with domain [P].  We chose to call this operation [extension].
 228 *)
 229
 230 alias id "P" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/P.var".
 231
 232 alias id "R" = "cic:/CoRN/algebra/CSetoidFun/SubSets_of_G/Extension/R.var".
 233
 234 inline "cic:/CoRN/algebra/CSetoidFun/extend.con".
 235
 236 inline "cic:/CoRN/algebra/CSetoidFun/ext1.con".
 237
 238 inline "cic:/CoRN/algebra/CSetoidFun/ext2_a.con".
 239
 240 inline "cic:/CoRN/algebra/CSetoidFun/ext2.con".
 241
 242 inline "cic:/CoRN/algebra/CSetoidFun/extension_wd.con".
 243
 244 (* UNEXPORTED
 245 End Extension
 246 *)
 247
 248 (* UNEXPORTED
 249 End SubSets_of_G
 250 *)
 251
 252 (* NOTATION
 253 Notation Conj := (conjP _).
 254 *)
 255
 256 (* UNEXPORTED
 257 Implicit Arguments disj [S].
 258 *)
 259
 260 (* UNEXPORTED
 261 Implicit Arguments extend [S].
 262 *)
 263
 264 (* UNEXPORTED
 265 Implicit Arguments ext1 [S P R x].
 266 *)
 267
 268 (* UNEXPORTED
 269 Implicit Arguments ext2 [S P R x].
 270 *)
 271
 272 (*#* ***Operations
 273
 274 We are now ready to define the concept of partial function between arbitrary setoids.
 275 *)
 276
 277 inline "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind".
 278
 279 coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con 0 (* compounds *).
 280
 281 (* NOTATION
 282 Notation BDom := (bpfdom _ _).
 283 *)
 284
 285 (* UNEXPORTED
 286 Implicit Arguments bpfpfun [S1 S2].
 287 *)
 288
 289 (*#*
 290 The next lemma states that every partial function is well defined.
 291 *)
 292
 293 inline "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con".
 294
 295 (*#* Similar for automorphisms. *)
 296
 297 inline "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind".
 298
 299 coercion cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con 0 (* compounds *).
 300
 301 (* NOTATION
 302 Notation Dom := (pfdom _).
 303 *)
 304
 305 (* NOTATION
 306 Notation Part := (pfpfun _).
 307 *)
 308
 309 (* UNEXPORTED
 310 Implicit Arguments pfpfun [S].
 311 *)
 312
 313 (*#*
 314 The next lemma states that every partial function is well defined.
 315 *)
 316
 317 inline "cic:/CoRN/algebra/CSetoidFun/pfwdef.con".
 318
 319 (*#*
 320 A few characteristics of this definition should be explained:
 321  - The domain of the partial function is characterized by a predicate
 322 that is required to be well defined but not strongly extensional.  The
 323 motivation for this choice comes from two facts: first, one very
 324 important subset of real numbers is the compact interval
 325 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
 326 [<=] b], which is not strongly extensional; on the other hand, if we
 327 can apply a function to an element [s] of a setoid [S] it seems
 328 reasonable (and at some point we do have to do it) to apply that same
 329 function to any element [s'] which is equal to [s] from the point of
 330 view of the setoid equality.
 331  - The last two conditions state that [pfpfun] is really a subsetoid
 332 function.  The reason why we do not write it that way is the
 333 following: when applying a partial function [f] to an element [s] of
 334 [S] we also need a proof object [H]; with this definition the object
 335 we get is [f(s,H)], where the proof is kept separate from the object.
 336 Using subsetoid notation, we would get $f(\langle
 337 s,H\rangle)$#f(&lang;s,H&rang;)#; from this we need to apply two
 338 projections to get either the original object or the proof, and we
 339 need to apply an extra constructor to get $f(\langle
 340 s,H\rangle)$#f(&lang;s,H&rang;)# from [s] and [H].  This amounts
 341 to spending more resources when actually working with these objects.
 342  - This record has type [Type], which is very unfortunate, because it
 343 means in particular that we cannot use the well behaved set
 344 existential quantification over partial functions; however, later on
 345 we will manage to avoid this problem in a way that also justifies that
 346 we don't really need to use that kind of quantification.  Another
 347 approach to this definition that completely avoid this complication
 348 would be to make [PartFunct] a dependent type, receiving the predicate
 349 as an argument.  This does work in that it allows us to give
 350 [PartFunct] type [Set] and do some useful stuff with it; however, we
 351 are not able to define something as simple as an operator that gets a
 352 function and returns its domain (because of the restrictions in the
 353 type elimination rules).  This sounds very unnatural, and soon gets us
 354 into strange problems that yield very unlikely definitions, which is
 355 why we chose to altogether do away with this approach.
 356
 357 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
 358 %\end{convention}%
 359
 360 We now present some methods for defining partial functions.
 361 *)
 362
 363 (* UNEXPORTED
 364 Hint Resolve CI: core.
 365 *)
 366
 367 (* UNEXPORTED
 368 Section CSetoid_Ops
 369 *)
 370
 371 alias id "S" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/S.var".
 372
 373 (*#*
 374 To begin with, we want to be able to ``see'' each total function as a partial function.
 375 *)
 376
 377 inline "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con".
 378
 379 (* UNEXPORTED
 380 Section Part_Function_Const
 381 *)
 382
 383 (*#*
 384 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
 385
 386 %\begin{convention}% Let [c:S].
 387 %\end{convention}%
 388 *)
 389
 390 alias id "c" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Const/c.var".
 391
 392 inline "cic:/CoRN/algebra/CSetoidFun/Fconst.con".
 393
 394 (* UNEXPORTED
 395 End Part_Function_Const
 396 *)
 397
 398 (* UNEXPORTED
 399 Section Part_Function_Id
 400 *)
 401
 402 inline "cic:/CoRN/algebra/CSetoidFun/Fid.con".
 403
 404 (* UNEXPORTED
 405 End Part_Function_Id
 406 *)
 407
 408 (*#*
 409 (These happen to be always total functions, but that is more or less obvious, as we have no information on the setoid; however, we will be able to define partial functions just applying other operators to these ones.)
 410
 411 If we have two setoid functions [F] and [G] we can always compose them.  The domain of our new function will be the set of points [s] in the domain of [F] for which [F(s)] is in the domain of [G]#. #%\footnote{%Notice that the use of extension here is essential.%}.%  The inversion in the order of the variables is done to maintain uniformity with the usual mathematical notation.
 412
 413 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 414 %\end{convention}%
 415 *)
 416
 417 (* UNEXPORTED
 418 Section Part_Function_Composition
 419 *)
 420
 421 alias id "G" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/G.var".
 422
 423 alias id "F" = "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/F.var".
 424
 425 (* begin hide *)
 426
 427 inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/P.con" "CSetoid_Ops__Part_Function_Composition__".
 428
 429 inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/Q.con" "CSetoid_Ops__Part_Function_Composition__".
 430
 431 (* end hide *)
 432
 433 inline "cic:/CoRN/algebra/CSetoidFun/CSetoid_Ops/Part_Function_Composition/R.con" "CSetoid_Ops__Part_Function_Composition__".
 434
 435 inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con".
 436
 437 inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con".
 438
 439 inline "cic:/CoRN/algebra/CSetoidFun/Fcomp.con".
 440
 441 (* UNEXPORTED
 442 End Part_Function_Composition
 443 *)
 444
 445 (* UNEXPORTED
 446 End CSetoid_Ops
 447 *)
 448
 449 (*#*
 450 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 451 %\end{convention}%
 452 *)
 453
 454 (* UNEXPORTED
 455 Section BinPart_Function_Composition
 456 *)
 457
 458 alias id "S1" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S1.var".
 459
 460 alias id "S2" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S2.var".
 461
 462 alias id "S3" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/S3.var".
 463
 464 alias id "G" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/G.var".
 465
 466 alias id "F" = "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/F.var".
 467
 468 (* begin hide *)
 469
 470 inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/P.con" "BinPart_Function_Composition__".
 471
 472 inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/Q.con" "BinPart_Function_Composition__".
 473
 474 (* end hide *)
 475
 476 inline "cic:/CoRN/algebra/CSetoidFun/BinPart_Function_Composition/R.con" "BinPart_Function_Composition__".
 477
 478 inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con".
 479
 480 inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con".
 481
 482 inline "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con".
 483
 484 (* UNEXPORTED
 485 End BinPart_Function_Composition
 486 *)
 487
 488 (* Different tokens for compatibility with coqdoc *)
 489
 490 (* UNEXPORTED
 491 Implicit Arguments Fconst [S].
 492 *)
 493
 494 (* NOTATION
 495 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
 496 *)
 497
 498 (* NOTATION
 499 Notation FId := (Fid _).
 500 *)
 501
 502 (* UNEXPORTED
 503 Implicit Arguments Fcomp [S].
 504 *)
 505
 506 (* NOTATION
 507 Infix "[o]" := Fcomp (at level 65, no associativity).
 508 *)
 509
 510 (* UNEXPORTED
 511 Hint Resolve pfwdef bpfwdef: algebra.
 512 *)
 513
 514 (* UNEXPORTED
 515 Section bijections
 516 *)
 517
 518 (*#* **Bijections *)
 519
 520 inline "cic:/CoRN/algebra/CSetoidFun/injective.con".
 521
 522 inline "cic:/CoRN/algebra/CSetoidFun/injective_weak.con".
 523
 524 inline "cic:/CoRN/algebra/CSetoidFun/surjective.con".
 525
 526 (* UNEXPORTED
 527 Implicit Arguments injective [A B].
 528 *)
 529
 530 (* UNEXPORTED
 531 Implicit Arguments injective_weak [A B].
 532 *)
 533
 534 (* UNEXPORTED
 535 Implicit Arguments surjective [A B].
 536 *)
 537
 538 inline "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con".
 539
 540 inline "cic:/CoRN/algebra/CSetoidFun/bijective.con".
 541
 542 (* UNEXPORTED
 543 Implicit Arguments bijective [A B].
 544 *)
 545
 546 inline "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con".
 547
 548 inline "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con".
 549
 550 inline "cic:/CoRN/algebra/CSetoidFun/inv.con".
 551
 552 (* UNEXPORTED
 553 Implicit Arguments inv [A B].
 554 *)
 555
 556 inline "cic:/CoRN/algebra/CSetoidFun/invfun.con".
 557
 558 (* UNEXPORTED
 559 Implicit Arguments invfun [A B].
 560 *)
 561
 562 inline "cic:/CoRN/algebra/CSetoidFun/inv1.con".
 563
 564 inline "cic:/CoRN/algebra/CSetoidFun/inv2.con".
 565
 566 inline "cic:/CoRN/algebra/CSetoidFun/inv_strext.con".
 567
 568 inline "cic:/CoRN/algebra/CSetoidFun/Inv.con".
 569
 570 (* UNEXPORTED
 571 Implicit Arguments Inv [A B].
 572 *)
 573
 574 inline "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con".
 575
 576 (* UNEXPORTED
 577 End bijections
 578 *)
 579
 580 (* UNEXPORTED
 581 Implicit Arguments bijective [A B].
 582 *)
 583
 584 (* UNEXPORTED
 585 Implicit Arguments injective [A B].
 586 *)
 587
 588 (* UNEXPORTED
 589 Implicit Arguments injective_weak [A B].
 590 *)
 591
 592 (* UNEXPORTED
 593 Implicit Arguments surjective [A B].
 594 *)
 595
 596 (* UNEXPORTED
 597 Implicit Arguments inv [A B].
 598 *)
 599
 600 (* UNEXPORTED
 601 Implicit Arguments invfun [A B].
 602 *)
 603
 604 (* UNEXPORTED
 605 Implicit Arguments Inv [A B].
 606 *)
 607
 608 (* UNEXPORTED
 609 Implicit Arguments conj_wd [S P Q].
 610 *)
 611
 612 (* NOTATION
 613 Notation Prj1 := (prj1 _ _ _ _).
 614 *)
 615
 616 (* NOTATION
 617 Notation Prj2 := (prj2 _ _ _ _).
 618 *)
 619