matita/library/algebra/CoRN/SetoidFun.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* $Id: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *)
  16
  17 set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun".
  18 include "algebra/CoRN/Setoids.ma".
  19
  20
  21 definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
  22 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
  23  \exists a:A. (csf_fun A B f) a \neq (csf_fun A B g) a.
  24 (* Definition ap_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
  25   {a : A | f a[#]g a}. *)
  26
  27 definition eq_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
  28 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
  29  \forall a:A. (csf_fun A B f) a = (csf_fun A B g) a.
  30 (* Definition eq_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
  31   forall a : A, f a[=]g a. *)
  32
  33 lemma irrefl_apfun : \forall A,B : CSetoid.
  34  irreflexive (CSetoid_fun A B) (ap_fun A B).
  35 intros.
  36 unfold irreflexive. intro f.
  37 unfold ap_fun.
  38 unfold.
  39 intro.
  40 elim H.
  41 cut (csf_fun A B f a = csf_fun A B f a)
  42 [
  43  apply eq_imp_not_ap.
  44  apply A.
  45  assumption.
  46  assumption.
  47  auto.
  48  auto
  49 |
  50  apply eq_reflexive_unfolded
  51 ]
  52 qed.
  53
  54 (*
  55 Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
  56 intros A B.
  57 unfold irreflexive in |- *.
  58 intros f.
  59 unfold ap_fun in |- *.
  60 red in |- *.
  61 intro H.
  62 elim H.
  63 intros a H0.
  64 set (H1 := ap_irreflexive_unfolded B (f a)) in *.
  65 intuition.
  66 Qed.
  67 *)
  68
  69
  70 (*
  71 lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B).
  72 intros (A B).
  73 unfold.
  74 unfold ap_fun.
  75 intros (f g H h).
  76 decompose.
  77 apply ap_cotransitive.
  78 apply (ap_imp_neq B (csf_fun A B x a) (csf_fun A B y a) H1).
  79 (* letin foo \def (\exist a:A.csf_fun A B x a\neq csf_fun A B z a). *)
  80
  81
  82 apply (ap_cotransitive B ? ? H1 ?).
  83
  84 split.
  85 left.
  86 elim H.
  87 clear H.
  88 intros a H.
  89 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
  90 elim H1.
  91 clear H1.
  92 intros H1.
  93 left.
  94 exists a.
  95 exact H1.
  96
  97 clear H1.
  98 intro H1.
  99 right.
 100 exists a.
 101 exact H1.
 102 Qed.
 103 *)
 104
 105 (*
 106 Lemma cotrans_apfun : forall A B : CSetoid, cotransitive (ap_fun A B).
 107 intros A B.
 108 unfold cotransitive in |- *.
 109 unfold ap_fun in |- *.
 110 intros f g H h.
 111 elim H.
 112 clear H.
 113 intros a H.
 114 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
 115 elim H1.
 116 clear H1.
 117 intros H1.
 118 left.
 119 exists a.
 120 exact H1.
 121
 122 clear H1.
 123 intro H1.
 124 right.
 125 exists a.
 126 exact H1.
 127 Qed.
 128 *)
 129
 130 lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
 131 unfold tight_apart.
 132 intros (A B f g).
 133 unfold ap_fun.
 134 unfold eq_fun.
 135 split
 136 [ intros. elim H. unfold in H.
 137 generalize in match H. reduce. simplify .unfold.
 138
 139  |
 140 ]
 141 intros.
 142 red in H.
 143 apply not_ap_imp_eq.
 144 red in |- *.
 145 intros H0.
 146 apply H.
 147 exists a.
 148 exact H0.
 149 intros H.
 150 red in |- *.
 151
 152 intro H1.
 153 elim H1.
 154 intros a X.
 155 set (H2 := eq_imp_not_ap B (f a) (g a) (H a) X) in *.
 156 exact H2.
 157 Qed.
 158
 159 (*
 160 Lemma ta_apfun : forall A B : CSetoid, tight_apart (eq_fun A B) (ap_fun A B).
 161 unfold tight_apart in |- *.
 162 unfold ap_fun in |- *.
 163 unfold eq_fun in |- *.
 164 intros A B f g.
 165 split.
 166 intros H a.
 167 red in H.
 168 apply not_ap_imp_eq.
 169 red in |- *.
 170 intros H0.
 171 apply H.
 172 exists a.
 173 exact H0.
 174 intros H.
 175 red in |- *.
 176
 177 intro H1.
 178 elim H1.
 179 intros a X.
 180 set (H2 := eq_imp_not_ap B (f a) (g a) (H a) X) in *.
 181 exact H2.
 182 Qed.
 183 *)
 184
 185 Lemma sym_apfun : forall A B : CSetoid, Csymmetric (ap_fun A B).
 186 unfold Csymmetric in |- *.
 187 unfold ap_fun in |- *.
 188 intros A B f g H.
 189 elim H.
 190 clear H.
 191 intros a H.
 192 exists a.
 193 apply ap_symmetric_unfolded.
 194 exact H.
 195 Qed.
 196
 197 Definition FS_is_CSetoid (A B : CSetoid) :=
 198   Build_is_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
 199   (irrefl_apfun A B) (sym_apfun A B) (cotrans_apfun A B) (ta_apfun A B).
 200
 201 Definition FS_as_CSetoid (A B : CSetoid) :=
 202   Build_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
 203     (FS_is_CSetoid A B).
 204
 205 (** **Nullary and n-ary operations
 206 *)
 207
 208 Definition is_nullary_operation (S:CSetoid) (s:S):Prop := True.
 209
 210 Fixpoint n_ary_operation (n:nat)(V:CSetoid){struct n}:CSetoid:=
 211 match n with
 212 |0 => V
 213 |(S m)=> (FS_as_CSetoid V (n_ary_operation m V))
 214 end.
 215
 216 Section unary_function_composition.
 217
 218 (** ** Composition of Setoid functions
 219
 220 Let [S1],  [S2] and [S3] be setoids, [f] a
 221 setoid function from [S1] to [S2], and [g] from [S2]
 222 to [S3] in the following definition of composition.  *)
 223
 224 Variables S1 S2 S3 : CSetoid.
 225 Variable f : CSetoid_fun S1 S2.
 226 Variable g : CSetoid_fun S2 S3.
 227
 228 Definition compose_CSetoid_fun : CSetoid_fun S1 S3.
 229 apply (Build_CSetoid_fun _ _ (fun x : S1 => g (f x))).
 230 (* str_ext *)
 231 unfold fun_strext in |- *; intros x y H.
 232 apply (csf_strext _ _ f). apply (csf_strext _ _ g). assumption.
 233 Defined.
 234
 235 End unary_function_composition.
 236
 237 (** ***Composition as operation
 238 *)
 239 Definition comp (A B C : CSetoid) :
 240   FS_as_CSetoid A B -> FS_as_CSetoid B C -> FS_as_CSetoid A C.
 241 intros A B C f g.
 242 set (H := compose_CSetoid_fun A B C f g) in *.
 243 exact H.
 244 Defined.
 245
 246 Definition comp_as_bin_op (A:CSetoid) : CSetoid_bin_op (FS_as_CSetoid A A).
 247 intro A.
 248 unfold CSetoid_bin_op in |- *.
 249 eapply Build_CSetoid_bin_fun with (comp A A A).
 250 unfold bin_fun_strext in |- *.
 251 unfold comp in |- *.
 252 intros f1 f2 g1 g2.
 253 simpl in |- *.
 254 unfold ap_fun in |- *.
 255 unfold compose_CSetoid_fun in |- *.
 256 simpl in |- *.
 257 elim f1.
 258 unfold fun_strext in |- *.
 259 clear f1.
 260 intros f1 Hf1.
 261 elim f2.
 262 unfold fun_strext in |- *.
 263 clear f2.
 264 intros f2 Hf2.
 265 elim g1.
 266 unfold fun_strext in |- *.
 267 clear g1.
 268 intros g1 Hg1.
 269 elim g2.
 270 unfold fun_strext in |- *.
 271 clear g2.
 272 intros g2 Hg2.
 273 simpl in |- *.
 274 intro H.
 275 elim H.
 276 clear H.
 277 intros a H.
 278 set (H0 := ap_cotransitive A (g1 (f1 a)) (g2 (f2 a)) H (g2 (f1 a))) in *.
 279 elim H0.
 280 clear H0.
 281 intro H0.
 282 right.
 283 exists (f1 a).
 284 exact H0.
 285
 286 clear H0.
 287 intro H0.
 288 left.
 289 exists a.
 290 apply Hg2.
 291 exact H0.
 292 Defined.
 293
 294 Lemma assoc_comp : forall A : CSetoid, associative (comp_as_bin_op A).
 295 unfold associative in |- *.
 296 unfold comp_as_bin_op in |- *.
 297 intros A f g h.
 298 simpl in |- *.
 299 unfold eq_fun in |- *.
 300 simpl in |- *.
 301 intuition.
 302 Qed.
 303
 304 Section unary_and_binary_function_composition.
 305
 306 Definition compose_CSetoid_bin_un_fun (A B C : CSetoid)
 307   (f : CSetoid_bin_fun B B C) (g : CSetoid_fun A B) : CSetoid_bin_fun A A C.
 308 intros A B C f g.
 309 apply (Build_CSetoid_bin_fun A A C (fun a0 a1 : A => f (g a0) (g a1))).
 310 intros x1 x2 y1 y2 H0.
 311 assert (H10:= csbf_strext B B C f).
 312 red in H10.
 313 assert (H40 := csf_strext A B g).
 314 red in H40.
 315 elim (H10 (g x1) (g x2) (g y1) (g y2) H0); [left | right]; auto.
 316 Defined.
 317
 318 Definition compose_CSetoid_bin_fun A B C (f g : CSetoid_fun A B)
 319   (h : CSetoid_bin_fun B B C) : CSetoid_fun A C.
 320 intros A B C f g h.
 321 apply (Build_CSetoid_fun A C (fun a : A => h (f a) (g a))).
 322 intros x y H.
 323 elim (csbf_strext _ _ _ _ _ _ _ _ H); apply csf_strext.
 324 Defined.
 325
 326 Definition compose_CSetoid_un_bin_fun A B C (f : CSetoid_bin_fun B B C)
 327  (g : CSetoid_fun C A) : CSetoid_bin_fun B B A.
 328 intros A0 B0 C f g.
 329 apply Build_CSetoid_bin_fun with (fun x y : B0 => g (f x y)).
 330 intros x1 x2 y1 y2.
 331 case f.
 332 simpl in |- *.
 333 unfold bin_fun_strext in |- *.
 334 case g.
 335 simpl in |- *.
 336 unfold fun_strext in |- *.
 337 intros gu gstrext fu fstrext H.
 338 apply fstrext.
 339 apply gstrext.
 340 exact H.
 341 Defined.
 342
 343 End unary_and_binary_function_composition.
 344
 345 (** ***Projections
 346 *)
 347
 348 Section function_projection.
 349
 350 Lemma proj_bin_fun : forall A B C (f : CSetoid_bin_fun A B C) a, fun_strext (f a).
 351 intros A B C f a.
 352 red in |- *.
 353 elim f.
 354 intro fo.
 355 simpl.
 356 intros csbf_strext0 x y H.
 357 elim (csbf_strext0 _ _ _ _ H); intro H0.
 358  elim (ap_irreflexive_unfolded _ _ H0).
 359 exact H0.
 360 Qed.
 361
 362 Definition projected_bin_fun A B C (f : CSetoid_bin_fun A B C) (a : A) :=
 363  Build_CSetoid_fun B C (f a) (proj_bin_fun A B C f a).
 364
 365 End function_projection.
 366
 367 Section BinProj.
 368
 369 Variable S : CSetoid.
 370
 371 Definition binproj1 (x y:S) := x.
 372
 373 Lemma binproj1_strext : bin_fun_strext _ _ _ binproj1.
 374 red in |- *; auto.
 375 Qed.
 376
 377 Definition cs_binproj1 : CSetoid_bin_op S.
 378 red in |- *; apply Build_CSetoid_bin_op with binproj1.
 379 apply binproj1_strext.
 380 Defined.
 381
 382 End BinProj.
 383
 384 (** **Combining operations
 385 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
 386 %\end{convention}%
 387 *)
 388
 389 Section CombiningOperations.
 390 Variables S1 S2 S3 : CSetoid.
 391
 392 (**
 393 In the following definition, we assume [f] is a setoid function from
 394 [S1] to [S2], and [op] is an unary operation on [S2].
 395 Then [opOnFun] is the composition [op] after [f].
 396 *)
 397 Section CombiningUnaryOperations.
 398 Variable f : CSetoid_fun S1 S2.
 399 Variable op : CSetoid_un_op S2.
 400
 401 Definition opOnFun : CSetoid_fun S1 S2.
 402 apply (Build_CSetoid_fun S1 S2 (fun x : S1 => op (f x))).
 403 (* str_ext *)
 404 unfold fun_strext in |- *; intros x y H.
 405 apply (csf_strext _ _ f x y).
 406 apply (csf_strext _ _ op _ _ H).
 407 Defined.
 408
 409 End CombiningUnaryOperations.
 410
 411 End CombiningOperations.
 412
 413 Section p66E2b4.
 414
 415 (** **The Free Setoid
 416 %\begin{convention}% Let [A:CSetoid].
 417 %\end{convention}%
 418 *)
 419 Variable A:CSetoid.
 420
 421 Definition Astar := (list A).
 422
 423 Definition empty_word := (nil A).
 424
 425 Definition appA:= (app A).
 426
 427 Fixpoint eq_fm (m:Astar)(k:Astar){struct m}:Prop:=
 428 match m with
 429 |nil => match k with
 430         |nil => True
 431         |cons a l => False
 432         end
 433 |cons b n => match k with
 434         |nil => False
 435         |cons a l => b[=]a /\ (eq_fm n l)
 436         end
 437 end.
 438
 439 Fixpoint ap_fm (m:Astar)(k:Astar){struct m}: CProp :=
 440 match m with
 441 |nil => match k with
 442         |nil => CFalse
 443         |cons a l => CTrue
 444         end
 445 |cons b n => match k with
 446         |nil => CTrue
 447         |cons a l => b[#]a or (ap_fm n l)
 448         end
 449 end.
 450
 451 Lemma ap_fm_irreflexive: (irreflexive ap_fm).
 452 unfold irreflexive.
 453 intro x.
 454 induction x.
 455 simpl.
 456 red.
 457 intuition.
 458
 459 simpl.
 460 red.
 461 intro H.
 462 apply IHx.
 463 elim H.
 464 clear H.
 465 generalize (ap_irreflexive A a).
 466 unfold Not.
 467 intuition.
 468
 469 intuition.
 470 Qed.
 471
 472
 473 Lemma ap_fm_symmetric: Csymmetric ap_fm.
 474 unfold Csymmetric.
 475 intros x.
 476 induction x.
 477 intro y.
 478 case  y.
 479 simpl.
 480 intuition.
 481
 482 simpl.
 483 intuition.
 484 simpl.
 485 intro y.
 486 case y.
 487 simpl.
 488 intuition.
 489
 490 simpl.
 491 intros c l  H0.
 492 elim H0.
 493 generalize (ap_symmetric A a c).
 494 intuition.
 495 clear H0.
 496 intro H0.
 497 right.
 498 apply IHx.
 499 exact H0.
 500 Qed.
 501
 502 Lemma ap_fm_cotransitive : (cotransitive ap_fm).
 503 unfold cotransitive.
 504 intro x.
 505 induction x.
 506 simpl.
 507 intro y.
 508 case y.
 509 intuition.
 510
 511 intros c l H z.
 512 case z.
 513 simpl.
 514 intuition.
 515
 516 intuition.
 517
 518 simpl.
 519 intro y.
 520 case y.
 521 intros H z.
 522 case z.
 523 intuition.
 524
 525 simpl.
 526 intuition.
 527
 528 intros c l H z.
 529 case z.
 530 intuition.
 531
 532 simpl.
 533 intros c0 l0.
 534 elim H.
 535 clear H.
 536 intro H.
 537 generalize (ap_cotransitive A a c H c0).
 538 intuition.
 539
 540 clear H.
 541 intro H.
 542 generalize (IHx l H l0).
 543 intuition.
 544 Qed.
 545
 546 Lemma ap_fm_tight : (tight_apart eq_fm ap_fm).
 547 unfold tight_apart.
 548 intros x.
 549 induction x.
 550 simpl.
 551 intro y.
 552 case y.
 553 red.
 554 unfold Not.
 555 intuition.
 556
 557 intuition.
 558
 559 intro y.
 560 simpl.
 561 case y.
 562 intuition.
 563
 564 intros c l.
 565 generalize (IHx l).
 566 red.
 567 intro H0.
 568 elim H0.
 569 intros H1 H2.
 570 split.
 571 intro H3.
 572 split.
 573 red in H3.
 574 generalize (ap_tight A a c).
 575 intuition.
 576
 577 apply H1.
 578 intro H4.
 579 apply H3.
 580 right.
 581 exact H4.
 582
 583 intro H3.
 584 elim H3.
 585 clear H3.
 586 intros H3 H4.
 587 intro H5.
 588 elim H5.
 589 generalize (ap_tight A a c).
 590 intuition.
 591
 592 apply H2.
 593 exact H4.
 594 Qed.
 595
 596 Definition free_csetoid_is_CSetoid:(is_CSetoid Astar eq_fm ap_fm):=
 597   (Build_is_CSetoid Astar eq_fm ap_fm ap_fm_irreflexive ap_fm_symmetric
 598   ap_fm_cotransitive ap_fm_tight).
 599
 600 Definition free_csetoid_as_csetoid:CSetoid:=
 601 (Build_CSetoid Astar eq_fm ap_fm free_csetoid_is_CSetoid).
 602
 603 Lemma app_strext:
 604   (bin_fun_strext free_csetoid_as_csetoid free_csetoid_as_csetoid
 605    free_csetoid_as_csetoid appA).
 606 unfold bin_fun_strext.
 607 intros x1.
 608 induction x1.
 609 simpl.
 610 intro x2.
 611 case x2.
 612 simpl.
 613 intuition.
 614
 615 intuition.
 616
 617 intros x2 y1 y2.
 618 simpl.
 619 case x2.
 620 case y2.
 621 simpl.
 622 intuition.
 623
 624 simpl.
 625 intuition.
 626
 627 case y2.
 628 simpl.
 629 simpl in IHx1.
 630 intros c l H.
 631 elim H.
 632 intuition.
 633
 634 clear H.
 635 generalize (IHx1 l y1 (nil A)).
 636 intuition.
 637
 638 simpl.
 639 intros c l c0 l0.
 640 intro H.
 641 elim H.
 642 intuition.
 643
 644 generalize (IHx1 l0 y1 (cons c l)).
 645 intuition.
 646 Qed.
 647
 648 Definition app_as_csb_fun:
 649 (CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
 650   free_csetoid_as_csetoid):=
 651   (Build_CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
 652    free_csetoid_as_csetoid appA app_strext).
 653
 654 Lemma eq_fm_reflexive: forall (x:Astar), (eq_fm x x).
 655 intro x.
 656 induction x.
 657 simpl.
 658 intuition.
 659
 660 simpl.
 661 intuition.
 662 Qed.
 663
 664 End p66E2b4.
 665
 666 (** **Partial Functions
 667
 668 In this section we define a concept of partial function for an
 669 arbitrary setoid.  Essentially, a partial function is what would be
 670 expected---a predicate on the setoid in question and a total function
 671 from the set of points satisfying that predicate to the setoid.  There
 672 is one important limitations to this approach: first, the record we
 673 obtain has type [Type], meaning that we can't use, for instance,
 674 elimination of existential quantifiers.
 675
 676 Furthermore, for reasons we will explain ahead, partial functions will
 677 not be defined via the [CSetoid_fun] record, but the whole structure
 678 will be incorporated in a new record.
 679
 680 Finally, notice that to be completely general the domains of the
 681 functions have to be characterized by a [CProp]-valued predicate;
 682 otherwise, the use you can make of a function will be %\emph{%#<i>#a
 683 priori#</i>#%}% restricted at the moment it is defined.
 684
 685 Before we state our definitions we need to do some work on domains.
 686 *)
 687
 688 Section SubSets_of_G.
 689
 690 (** ***Subsets of Setoids
 691
 692 Subsets of a setoid will be identified with predicates from the
 693 carrier set of the setoid into [CProp].  At this stage, we do not make
 694 any assumptions about these predicates.
 695
 696 We will begin by defining elementary operations on predicates, along
 697 with their basic properties.  In particular, we will work with well
 698 defined predicates, so we will prove that these operations preserve
 699 welldefinedness.
 700
 701 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
 702 %\end{convention}%
 703 *)
 704
 705 Variable S : CSetoid.
 706
 707 Section Conjunction.
 708
 709 Variables P Q : S -> CProp.
 710
 711 Definition conjP (x : S) : CProp := P x and Q x.
 712
 713 Lemma prj1 : forall x : S, conjP x -> P x.
 714 intros x H; inversion_clear H; assumption.
 715 Qed.
 716
 717 Lemma prj2 : forall x : S, conjP x -> Q x.
 718 intros x H; inversion_clear H; assumption.
 719 Qed.
 720
 721 Lemma conj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ conjP.
 722 intros H H0.
 723 red in |- *; intros x y H1 H2.
 724 inversion_clear H1; split.
 725
 726 apply H with x; assumption.
 727
 728 apply H0 with x; assumption.
 729 Qed.
 730
 731 End Conjunction.
 732
 733 Section Disjunction.
 734
 735 Variables P Q : S -> CProp.
 736
 737 (**
 738 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
 739 *)
 740
 741 Definition disj (x : S) : CProp := P x or Q x.
 742
 743 Lemma inj1 : forall x : S, P x -> disj x.
 744 intros; left; assumption.
 745 Qed.
 746
 747 Lemma inj2 : forall x : S, Q x -> disj x.
 748 intros; right; assumption.
 749 Qed.
 750
 751 Lemma disj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ disj.
 752 intros H H0.
 753 red in |- *; intros x y H1 H2.
 754 inversion_clear H1.
 755
 756 left; apply H with x; assumption.
 757
 758 right; apply H0 with x; assumption.
 759 Qed.
 760
 761 End Disjunction.
 762
 763 Section Extension.
 764
 765 (**
 766 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].
 767 *)
 768
 769 Variable P : S -> CProp.
 770 Variable R : forall x : S, P x -> CProp.
 771
 772 Definition extend (x : S) : CProp := P x and (forall H : P x, R x H).
 773
 774 Lemma ext1 : forall x : S, extend x -> P x.
 775 intros x H; inversion_clear H; assumption.
 776 Qed.
 777
 778 Lemma ext2_a : forall x : S, extend x -> {H : P x | R x H}.
 779 intros x H; inversion_clear H.
 780 exists X; auto.
 781 Qed.
 782
 783 Lemma ext2 : forall (x : S) (Hx : extend x), R x (ProjT1 (ext2_a x Hx)).
 784 intros; apply projT2.
 785 Qed.
 786
 787 Lemma extension_wd : pred_wd _ P ->
 788  (forall (x y : S) Hx Hy, x [=] y -> R x Hx -> R y Hy) -> pred_wd _ extend.
 789 intros H H0.
 790 red in |- *; intros x y H1 H2.
 791 elim H1; intros H3 H4; split.
 792
 793 apply H with x; assumption.
 794
 795 intro H5; apply H0 with x H3; [ apply H2 | apply H4 ].
 796 Qed.
 797
 798 End Extension.
 799
 800 End SubSets_of_G.
 801
 802 Notation Conj := (conjP _).
 803 Implicit Arguments disj [S].
 804
 805 Implicit Arguments extend [S].
 806 Implicit Arguments ext1 [S P R x].
 807 Implicit Arguments ext2 [S P R x].
 808
 809 (** ***Operations
 810
 811 We are now ready to define the concept of partial function between arbitrary setoids.
 812 *)
 813
 814 Record BinPartFunct (S1 S2 : CSetoid) : Type :=
 815   {bpfdom  :  S1 -> CProp;
 816    bdom_wd :  pred_wd S1 bpfdom;
 817    bpfpfun :> forall x : S1, bpfdom x -> S2;
 818    bpfstrx :  forall x y Hx Hy, bpfpfun x Hx [#] bpfpfun y Hy -> x [#] y}.
 819
 820
 821 Notation BDom := (bpfdom _ _).
 822 Implicit Arguments bpfpfun [S1 S2].
 823
 824 (**
 825 The next lemma states that every partial function is well defined.
 826 *)
 827
 828 Lemma bpfwdef : forall S1 S2 (F : BinPartFunct S1 S2) x y Hx Hy,
 829  x [=] y -> F x Hx [=] F y Hy.
 830 intros.
 831 apply not_ap_imp_eq; intro H0.
 832 generalize (bpfstrx _ _ _ _ _ _ _ H0).
 833 exact (eq_imp_not_ap _ _ _ H).
 834 Qed.
 835
 836 (** Similar for automorphisms. *)
 837
 838 Record PartFunct (S : CSetoid) : Type :=
 839   {pfdom  :  S -> CProp;
 840    dom_wd :  pred_wd S pfdom;
 841    pfpfun :> forall x : S, pfdom x -> S;
 842    pfstrx :  forall x y Hx Hy, pfpfun x Hx [#] pfpfun y Hy -> x [#] y}.
 843
 844 Notation Dom := (pfdom _).
 845 Notation Part := (pfpfun _).
 846 Implicit Arguments pfpfun [S].
 847
 848 (**
 849 The next lemma states that every partial function is well defined.
 850 *)
 851
 852 Lemma pfwdef : forall S (F : PartFunct S) x y Hx Hy, x [=] y -> F x Hx [=] F y Hy.
 853 intros.
 854 apply not_ap_imp_eq; intro H0.
 855 generalize (pfstrx _ _ _ _ _ _ H0).
 856 exact (eq_imp_not_ap _ _ _ H).
 857 Qed.
 858
 859 (**
 860 A few characteristics of this definition should be explained:
 861  - The domain of the partial function is characterized by a predicate
 862 that is required to be well defined but not strongly extensional.  The
 863 motivation for this choice comes from two facts: first, one very
 864 important subset of real numbers is the compact interval
 865 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
 866 [<=] b], which is not strongly extensional; on the other hand, if we
 867 can apply a function to an element [s] of a setoid [S] it seems
 868 reasonable (and at some point we do have to do it) to apply that same
 869 function to any element [s'] which is equal to [s] from the point of
 870 view of the setoid equality.
 871  - The last two conditions state that [pfpfun] is really a subsetoid
 872 function.  The reason why we do not write it that way is the
 873 following: when applying a partial function [f] to an element [s] of
 874 [S] we also need a proof object [H]; with this definition the object
 875 we get is [f(s,H)], where the proof is kept separate from the object.
 876 Using subsetoid notation, we would get $f(\langle
 877 s,H\rangle)$#f(&lang;s,H&rang;)#; from this we need to apply two
 878 projections to get either the original object or the proof, and we
 879 need to apply an extra constructor to get $f(\langle
 880 s,H\rangle)$#f(&lang;s,H&rang;)# from [s] and [H].  This amounts
 881 to spending more resources when actually working with these objects.
 882  - This record has type [Type], which is very unfortunate, because it
 883 means in particular that we cannot use the well behaved set
 884 existential quantification over partial functions; however, later on
 885 we will manage to avoid this problem in a way that also justifies that
 886 we don't really need to use that kind of quantification.  Another
 887 approach to this definition that completely avoid this complication
 888 would be to make [PartFunct] a dependent type, receiving the predicate
 889 as an argument.  This does work in that it allows us to give
 890 [PartFunct] type [Set] and do some useful stuff with it; however, we
 891 are not able to define something as simple as an operator that gets a
 892 function and returns its domain (because of the restrictions in the
 893 type elimination rules).  This sounds very unnatural, and soon gets us
 894 into strange problems that yield very unlikely definitions, which is
 895 why we chose to altogether do away with this approach.
 896
 897 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
 898 %\end{convention}%
 899
 900 We now present some methods for defining partial functions.
 901 *)
 902
 903 Hint Resolve CI: core.
 904
 905 Section CSetoid_Ops.
 906
 907 Variable S : CSetoid.
 908
 909 (**
 910 To begin with, we want to be able to ``see'' each total function as a partial function.
 911 *)
 912
 913 Definition total_eq_part : CSetoid_un_op S -> PartFunct S.
 914 intros f.
 915 apply
 916  Build_PartFunct with (fun x : S => CTrue) (fun (x : S) (H : CTrue) => f x).
 917 red in |- *; intros; auto.
 918 intros x y Hx Hy H.
 919 exact (csf_strext_unfolded _ _ f _ _ H).
 920 Defined.
 921
 922 Section Part_Function_Const.
 923
 924 (**
 925 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
 926
 927 %\begin{convention}% Let [c:S].
 928 %\end{convention}%
 929 *)
 930
 931 Variable c : S.
 932
 933 Definition Fconst := total_eq_part (Const_CSetoid_fun _ _ c).
 934
 935 End Part_Function_Const.
 936
 937 Section Part_Function_Id.
 938
 939 Definition Fid := total_eq_part (id_un_op S).
 940
 941 End Part_Function_Id.
 942
 943 (**
 944 (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.)
 945
 946 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.
 947
 948 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 949 %\end{convention}%
 950 *)
 951
 952 Section Part_Function_Composition.
 953
 954 Variables G F : PartFunct S.
 955
 956 (* begin hide *)
 957 Let P := Dom F.
 958 Let Q := Dom G.
 959 (* end hide *)
 960 Let R x := {Hx : P x | Q (F x Hx)}.
 961
 962 Lemma part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
 963  G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
 964 intros x y Hx Hy H.
 965 exact (pfstrx _ _ _ _ _ _ (pfstrx _ _ _ _ _ _ H)).
 966 Qed.
 967
 968 Lemma part_function_comp_dom_wd : pred_wd S R.
 969 red in |- *; intros x y H H0.
 970 unfold R in |- *; inversion_clear H.
 971 exists (dom_wd _ F x y x0 H0).
 972 apply (dom_wd _ G) with (F x x0).
 973 assumption.
 974 apply pfwdef; assumption.
 975 Qed.
 976
 977 Definition Fcomp := Build_PartFunct _ R part_function_comp_dom_wd
 978   (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
 979   part_function_comp_strext.
 980
 981 End Part_Function_Composition.
 982
 983 End CSetoid_Ops.
 984
 985 (**
 986 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
 987 %\end{convention}%
 988 *)
 989
 990 Section BinPart_Function_Composition.
 991
 992 Variables S1 S2 S3 : CSetoid.
 993
 994 Variable G : BinPartFunct S2 S3.
 995 Variable F : BinPartFunct S1 S2.
 996
 997 (* begin hide *)
 998 Let P := BDom F.
 999 Let Q := BDom G.
1000 (* end hide *)
1001 Let R x := {Hx : P x | Q (F x Hx)}.
1002
1003 Lemma bin_part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
1004  G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
1005 intros x y Hx Hy H.
1006 exact (bpfstrx _ _ _ _ _ _ _ (bpfstrx _ _ _ _ _ _ _ H)).
1007 Qed.
1008
1009 Lemma bin_part_function_comp_dom_wd : pred_wd S1 R.
1010 red in |- *; intros x y H H0.
1011 unfold R in |- *; inversion_clear H.
1012 exists (bdom_wd _ _ F x y x0 H0).
1013 apply (bdom_wd _ _ G) with (F x x0).
1014 assumption.
1015 apply bpfwdef; assumption.
1016 Qed.
1017
1018 Definition BinFcomp := Build_BinPartFunct _ _ R bin_part_function_comp_dom_wd
1019   (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
1020   bin_part_function_comp_strext.
1021
1022 End BinPart_Function_Composition.
1023
1024 (* Different tokens for compatibility with coqdoc *)
1025
1026 Implicit Arguments Fconst [S].
1027 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
1028
1029 Notation FId := (Fid _).
1030
1031 Implicit Arguments Fcomp [S].
1032 Infix "[o]" := Fcomp (at level 65, no associativity).
1033
1034 Hint Resolve pfwdef bpfwdef: algebra.
1035
1036 Section bijections.
1037 (** **Bijections *)
1038
1039 Definition injective A B (f : CSetoid_fun A B) := (forall a0 a1 : A,
1040  a0 [#] a1 -> f a0 [#] f a1):CProp.
1041
1042 Definition injective_weak A B (f : CSetoid_fun A B) := forall a0 a1 : A,
1043  f a0 [=] f a1 -> a0 [=] a1.
1044
1045 Definition surjective A B (f : CSetoid_fun A B) := (forall b : B, {a : A | f a [=] b}):CProp.
1046
1047 Implicit Arguments injective [A B].
1048 Implicit Arguments injective_weak [A B].
1049 Implicit Arguments surjective [A B].
1050
1051 Lemma injective_imp_injective_weak : forall A B (f : CSetoid_fun A B),
1052  injective f -> injective_weak f.
1053 intros A B f.
1054 unfold injective in |- *.
1055 intro H.
1056 unfold injective_weak in |- *.
1057 intros a0 a1 H0.
1058 apply not_ap_imp_eq.
1059 red in |- *.
1060 intro H1.
1061 set (H2 := H a0 a1 H1) in *.
1062 set (H3 := ap_imp_neq B (f a0) (f a1) H2) in *.
1063 set (H4 := eq_imp_not_neq B (f a0) (f a1) H0) in *.
1064 apply H4.
1065 exact H3.
1066 Qed.
1067
1068 Definition bijective A B (f:CSetoid_fun A B) := injective f and surjective f.
1069
1070 Implicit Arguments bijective [A B].
1071
1072 Lemma id_is_bij : forall A, bijective (id_un_op A).
1073 intro A.
1074 split.
1075  red; simpl; auto.
1076 intro b; exists b; apply eq_reflexive.
1077 Qed.
1078
1079 Lemma comp_resp_bij : forall A B C f g, bijective f -> bijective g ->
1080  bijective (compose_CSetoid_fun A B C f g).
1081 intros A B C f g.
1082 intros H0 H1.
1083 elim H0; clear H0; intros H00 H01.
1084 elim H1; clear H1; intros H10 H11.
1085 split.
1086  intros a0 a1; simpl; intro.
1087  apply H10; apply H00; auto.
1088 intro c; simpl.
1089 elim (H11 c); intros b H20.
1090 elim (H01 b); intros a H30.
1091 exists a.
1092 Step_final (g b).
1093 Qed.
1094
1095 Lemma inv : forall A B (f:CSetoid_fun A B),
1096  bijective f -> forall b : B, {a : A | f a [=] b}.
1097 unfold bijective in |- *.
1098 unfold surjective in |- *.
1099 intuition.
1100 Qed.
1101
1102 Implicit Arguments inv [A B].
1103
1104 Definition invfun A B (f : CSetoid_fun A B) (H : bijective f) : B -> A.
1105 intros A B f H H0.
1106 elim (inv f H H0); intros a H2.
1107 apply a.
1108 Defined.
1109
1110 Implicit Arguments invfun [A B].
1111
1112 Lemma inv1 : forall A B (f : CSetoid_fun A B) (H : bijective f) (b : B),
1113  f (invfun f H b) [=] b.
1114 intros A B f H b.
1115 unfold invfun in |- *; case inv.
1116 simpl; auto.
1117 Qed.
1118
1119 Lemma inv2 : forall A B (f : CSetoid_fun A B) (H : bijective f) (a : A),
1120  invfun f H (f a) [=] a.
1121 intros.
1122 unfold invfun in |- *; case inv; simpl.
1123 elim H; clear H; intros H0 H1.
1124 intro x.
1125 apply injective_imp_injective_weak.
1126 auto.
1127 Qed.
1128
1129 Lemma inv_strext : forall A B (f : CSetoid_fun A B) (H : bijective f),
1130  fun_strext (invfun f H).
1131 intros A B f H x y.
1132 intro H1.
1133 elim H; intros H00 H01.
1134 elim (H01 x); intros a0 H2.
1135 elim (H01 y); intros a1 H3.
1136 astepl (f a0).
1137 astepr (f a1).
1138 apply H00.
1139 astepl (invfun f H x).
1140 astepr (invfun f H y).
1141 exact H1.
1142 astepl (invfun f H (f a1)).
1143 apply inv2.
1144 apply injective_imp_injective_weak with (f := f); auto.
1145 astepl (f a1).
1146 astepl y.
1147 apply eq_symmetric.
1148 apply inv1.
1149 apply eq_symmetric.
1150 apply inv1.
1151 astepl (invfun f H (f a0)).
1152 apply inv2.
1153
1154 apply injective_imp_injective_weak with (f := f); auto.
1155 astepl (f a0).
1156 astepl x.
1157 apply eq_symmetric; apply inv1.
1158 apply eq_symmetric; apply inv1.
1159 Qed.
1160
1161 Definition Inv A B f (H : bijective f) :=
1162   Build_CSetoid_fun B A (invfun f H) (inv_strext A B f H).
1163
1164 Implicit Arguments Inv [A B].
1165
1166 Definition Inv_bij : forall A B (f : CSetoid_fun A B) (H : bijective f),
1167   bijective (Inv f H).
1168 intros A B f H.
1169 unfold bijective in |- *.
1170 split.
1171 unfold injective in |- *.
1172 unfold bijective in H.
1173 unfold surjective in H.
1174 elim H.
1175 intros H0 H1.
1176 intros b0 b1 H2.
1177 elim (H1 b0).
1178 intros a0 H3.
1179 elim (H1 b1).
1180 intros a1 H4.
1181 astepl (Inv f (CAnd_intro _ _ H0 H1) (f a0)).
1182 astepr (Inv f (CAnd_intro _ _ H0 H1) (f a1)).
1183 cut (fun_strext f).
1184 unfold fun_strext in |- *.
1185 intros H5.
1186 apply H5.
1187 astepl (f a0).
1188 astepr (f a1).
1189 astepl b0.
1190 astepr b1.
1191 exact H2.
1192 apply eq_symmetric.
1193 unfold Inv in |- *.
1194 simpl in |- *.
1195 apply inv1.
1196 apply eq_symmetric.
1197 unfold Inv in |- *.
1198 simpl in |- *.
1199 apply inv1.
1200 elim f.
1201 intuition.
1202
1203 unfold surjective in |- *.
1204 intro a.
1205 exists (f a).
1206 unfold Inv in |- *.
1207 simpl in |- *.
1208 apply inv2.
1209 Qed.
1210
1211
1212 End bijections.
1213 Implicit Arguments bijective [A B].
1214 Implicit Arguments injective [A B].
1215 Implicit Arguments injective_weak [A B].
1216 Implicit Arguments surjective [A B].
1217 Implicit Arguments inv [A B].
1218 Implicit Arguments invfun [A B].
1219 Implicit Arguments Inv [A B].
1220
1221 Implicit Arguments conj_wd [S P Q].
1222
1223 Notation Prj1 := (prj1 _ _ _ _).
1224 Notation Prj2 := (prj2 _ _ _ _).