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