helm/software/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 inline "cic:/CoRN/algebra/CSetoidFun/S1.var".
  36
  37 inline "cic:/CoRN/algebra/CSetoidFun/S2.var".
  38
  39 inline "cic:/CoRN/algebra/CSetoidFun/S3.var".
  40
  41 inline "cic:/CoRN/algebra/CSetoidFun/f.var".
  42
  43 inline "cic:/CoRN/algebra/CSetoidFun/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 inline "cic:/CoRN/algebra/CSetoidFun/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 inline "cic:/CoRN/algebra/CSetoidFun/S1.var".
 106
 107 inline "cic:/CoRN/algebra/CSetoidFun/S2.var".
 108
 109 inline "cic:/CoRN/algebra/CSetoidFun/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 inline "cic:/CoRN/algebra/CSetoidFun/f.var".
 122
 123 inline "cic:/CoRN/algebra/CSetoidFun/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 inline "cic:/CoRN/algebra/CSetoidFun/S.var".
 177
 178 (* UNEXPORTED
 179 Section Conjunction.
 180 *)
 181
 182 inline "cic:/CoRN/algebra/CSetoidFun/P.var".
 183
 184 inline "cic:/CoRN/algebra/CSetoidFun/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 inline "cic:/CoRN/algebra/CSetoidFun/P.var".
 203
 204 inline "cic:/CoRN/algebra/CSetoidFun/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 inline "cic:/CoRN/algebra/CSetoidFun/P.var".
 231
 232 inline "cic:/CoRN/algebra/CSetoidFun/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 (* UNEXPORTED
 253 Implicit Arguments disj [S].
 254 *)
 255
 256 (* UNEXPORTED
 257 Implicit Arguments extend [S].
 258 *)
 259
 260 (* UNEXPORTED
 261 Implicit Arguments ext1 [S P R x].
 262 *)
 263
 264 (* UNEXPORTED
 265 Implicit Arguments ext2 [S P R x].
 266 *)
 267
 268 (*#* ***Operations
 269
 270 We are now ready to define the concept of partial function between arbitrary setoids.
 271 *)
 272
 273 inline "cic:/CoRN/algebra/CSetoidFun/BinPartFunct.ind".
 274
 275 coercion "cic:/matita/CoRN-Decl/algebra/CSetoidFun/bpfpfun.con" 0 (* compounds *).
 276
 277 (* UNEXPORTED
 278 Implicit Arguments bpfpfun [S1 S2].
 279 *)
 280
 281 (*#*
 282 The next lemma states that every partial function is well defined.
 283 *)
 284
 285 inline "cic:/CoRN/algebra/CSetoidFun/bpfwdef.con".
 286
 287 (*#* Similar for automorphisms. *)
 288
 289 inline "cic:/CoRN/algebra/CSetoidFun/PartFunct.ind".
 290
 291 coercion "cic:/matita/CoRN-Decl/algebra/CSetoidFun/pfpfun.con" 0 (* compounds *).
 292
 293 (* UNEXPORTED
 294 Implicit Arguments pfpfun [S].
 295 *)
 296
 297 (*#*
 298 The next lemma states that every partial function is well defined.
 299 *)
 300
 301 inline "cic:/CoRN/algebra/CSetoidFun/pfwdef.con".
 302
 303 (*#*
 304 A few characteristics of this definition should be explained:
 305  - The domain of the partial function is characterized by a predicate
 306 that is required to be well defined but not strongly extensional.  The
 307 motivation for this choice comes from two facts: first, one very
 308 important subset of real numbers is the compact interval
 309 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
 310 [<=] b], which is not strongly extensional; on the other hand, if we
 311 can apply a function to an element [s] of a setoid [S] it seems
 312 reasonable (and at some point we do have to do it) to apply that same
 313 function to any element [s'] which is equal to [s] from the point of
 314 view of the setoid equality.
 315  - The last two conditions state that [pfpfun] is really a subsetoid
 316 function.  The reason why we do not write it that way is the
 317 following: when applying a partial function [f] to an element [s] of
 318 [S] we also need a proof object [H]; with this definition the object
 319 we get is [f(s,H)], where the proof is kept separate from the object.
 320 Using subsetoid notation, we would get $f(\langle
 321 s,H\rangle)$#f(&lang;s,H&rang;)#; from this we need to apply two
 322 projections to get either the original object or the proof, and we
 323 need to apply an extra constructor to get $f(\langle
 324 s,H\rangle)$#f(&lang;s,H&rang;)# from [s] and [H].  This amounts
 325 to spending more resources when actually working with these objects.
 326  - This record has type [Type], which is very unfortunate, because it
 327 means in particular that we cannot use the well behaved set
 328 existential quantification over partial functions; however, later on
 329 we will manage to avoid this problem in a way that also justifies that
 330 we don't really need to use that kind of quantification.  Another
 331 approach to this definition that completely avoid this complication
 332 would be to make [PartFunct] a dependent type, receiving the predicate
 333 as an argument.  This does work in that it allows us to give
 334 [PartFunct] type [Set] and do some useful stuff with it; however, we
 335 are not able to define something as simple as an operator that gets a
 336 function and returns its domain (because of the restrictions in the
 337 type elimination rules).  This sounds very unnatural, and soon gets us
 338 into strange problems that yield very unlikely definitions, which is
 339 why we chose to altogether do away with this approach.
 340
 341 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
 342 %\end{convention}%
 343
 344 We now present some methods for defining partial functions.
 345 *)
 346
 347 (* UNEXPORTED
 348 Hint Resolve CI: core.
 349 *)
 350
 351 (* UNEXPORTED
 352 Section CSetoid_Ops.
 353 *)
 354
 355 inline "cic:/CoRN/algebra/CSetoidFun/S.var".
 356
 357 (*#*
 358 To begin with, we want to be able to ``see'' each total function as a partial function.
 359 *)
 360
 361 inline "cic:/CoRN/algebra/CSetoidFun/total_eq_part.con".
 362
 363 (* UNEXPORTED
 364 Section Part_Function_Const.
 365 *)
 366
 367 (*#*
 368 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
 369
 370 %\begin{convention}% Let [c:S].
 371 %\end{convention}%
 372 *)
 373
 374 inline "cic:/CoRN/algebra/CSetoidFun/c.var".
 375
 376 inline "cic:/CoRN/algebra/CSetoidFun/Fconst.con".
 377
 378 (* UNEXPORTED
 379 End Part_Function_Const.
 380 *)
 381
 382 (* UNEXPORTED
 383 Section Part_Function_Id.
 384 *)
 385
 386 inline "cic:/CoRN/algebra/CSetoidFun/Fid.con".
 387
 388 (* UNEXPORTED
 389 End Part_Function_Id.
 390 *)
 391
 392 (*#*
 393 (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.)
 394
 395 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.
 396
 397 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 398 %\end{convention}%
 399 *)
 400
 401 (* UNEXPORTED
 402 Section Part_Function_Composition.
 403 *)
 404
 405 inline "cic:/CoRN/algebra/CSetoidFun/G.var".
 406
 407 inline "cic:/CoRN/algebra/CSetoidFun/F.var".
 408
 409 (* begin hide *)
 410
 411 inline "cic:/CoRN/algebra/CSetoidFun/P.con".
 412
 413 inline "cic:/CoRN/algebra/CSetoidFun/Q.con".
 414
 415 (* end hide *)
 416
 417 inline "cic:/CoRN/algebra/CSetoidFun/R.con".
 418
 419 inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_strext.con".
 420
 421 inline "cic:/CoRN/algebra/CSetoidFun/part_function_comp_dom_wd.con".
 422
 423 inline "cic:/CoRN/algebra/CSetoidFun/Fcomp.con".
 424
 425 (* UNEXPORTED
 426 End Part_Function_Composition.
 427 *)
 428
 429 (* UNEXPORTED
 430 End CSetoid_Ops.
 431 *)
 432
 433 (*#*
 434 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 435 %\end{convention}%
 436 *)
 437
 438 (* UNEXPORTED
 439 Section BinPart_Function_Composition.
 440 *)
 441
 442 inline "cic:/CoRN/algebra/CSetoidFun/S1.var".
 443
 444 inline "cic:/CoRN/algebra/CSetoidFun/S2.var".
 445
 446 inline "cic:/CoRN/algebra/CSetoidFun/S3.var".
 447
 448 inline "cic:/CoRN/algebra/CSetoidFun/G.var".
 449
 450 inline "cic:/CoRN/algebra/CSetoidFun/F.var".
 451
 452 (* begin hide *)
 453
 454 inline "cic:/CoRN/algebra/CSetoidFun/P.con".
 455
 456 inline "cic:/CoRN/algebra/CSetoidFun/Q.con".
 457
 458 (* end hide *)
 459
 460 inline "cic:/CoRN/algebra/CSetoidFun/R.con".
 461
 462 inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_strext.con".
 463
 464 inline "cic:/CoRN/algebra/CSetoidFun/bin_part_function_comp_dom_wd.con".
 465
 466 inline "cic:/CoRN/algebra/CSetoidFun/BinFcomp.con".
 467
 468 (* UNEXPORTED
 469 End BinPart_Function_Composition.
 470 *)
 471
 472 (* Different tokens for compatibility with coqdoc *)
 473
 474 (* UNEXPORTED
 475 Implicit Arguments Fconst [S].
 476 *)
 477
 478 (* UNEXPORTED
 479 Implicit Arguments Fcomp [S].
 480 *)
 481
 482 (* UNEXPORTED
 483 Hint Resolve pfwdef bpfwdef: algebra.
 484 *)
 485
 486 (* UNEXPORTED
 487 Section bijections.
 488 *)
 489
 490 (*#* **Bijections *)
 491
 492 inline "cic:/CoRN/algebra/CSetoidFun/injective.con".
 493
 494 inline "cic:/CoRN/algebra/CSetoidFun/injective_weak.con".
 495
 496 inline "cic:/CoRN/algebra/CSetoidFun/surjective.con".
 497
 498 (* UNEXPORTED
 499 Implicit Arguments injective [A B].
 500 *)
 501
 502 (* UNEXPORTED
 503 Implicit Arguments injective_weak [A B].
 504 *)
 505
 506 (* UNEXPORTED
 507 Implicit Arguments surjective [A B].
 508 *)
 509
 510 inline "cic:/CoRN/algebra/CSetoidFun/injective_imp_injective_weak.con".
 511
 512 inline "cic:/CoRN/algebra/CSetoidFun/bijective.con".
 513
 514 (* UNEXPORTED
 515 Implicit Arguments bijective [A B].
 516 *)
 517
 518 inline "cic:/CoRN/algebra/CSetoidFun/id_is_bij.con".
 519
 520 inline "cic:/CoRN/algebra/CSetoidFun/comp_resp_bij.con".
 521
 522 inline "cic:/CoRN/algebra/CSetoidFun/inv.con".
 523
 524 (* UNEXPORTED
 525 Implicit Arguments inv [A B].
 526 *)
 527
 528 inline "cic:/CoRN/algebra/CSetoidFun/invfun.con".
 529
 530 (* UNEXPORTED
 531 Implicit Arguments invfun [A B].
 532 *)
 533
 534 inline "cic:/CoRN/algebra/CSetoidFun/inv1.con".
 535
 536 inline "cic:/CoRN/algebra/CSetoidFun/inv2.con".
 537
 538 inline "cic:/CoRN/algebra/CSetoidFun/inv_strext.con".
 539
 540 inline "cic:/CoRN/algebra/CSetoidFun/Inv.con".
 541
 542 (* UNEXPORTED
 543 Implicit Arguments Inv [A B].
 544 *)
 545
 546 inline "cic:/CoRN/algebra/CSetoidFun/Inv_bij.con".
 547
 548 (* UNEXPORTED
 549 End bijections.
 550 *)
 551
 552 (* UNEXPORTED
 553 Implicit Arguments bijective [A B].
 554 *)
 555
 556 (* UNEXPORTED
 557 Implicit Arguments injective [A B].
 558 *)
 559
 560 (* UNEXPORTED
 561 Implicit Arguments injective_weak [A B].
 562 *)
 563
 564 (* UNEXPORTED
 565 Implicit Arguments surjective [A B].
 566 *)
 567
 568 (* UNEXPORTED
 569 Implicit Arguments inv [A B].
 570 *)
 571
 572 (* UNEXPORTED
 573 Implicit Arguments invfun [A B].
 574 *)
 575
 576 (* UNEXPORTED
 577 Implicit Arguments Inv [A B].
 578 *)
 579
 580 (* UNEXPORTED
 581 Implicit Arguments conj_wd [S P Q].
 582 *)
 583