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