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