helm/software/matita/contribs/CoRN/algebra/CoRN/Setoids.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 set "baseuri" "cic:/matita/algebra/CoRN/Setoid".
  16
  17
  18 include "higher_order_defs/relations.ma".
  19 include "Z/plus.ma".
  20
  21 include "datatypes/constructors.ma".
  22 include "nat/nat.ma".
  23 include "logic/equality.ma".
  24 (*include "Z/Zminus.ma".*)
  25
  26 (* Setoids
  27 Definition of a constructive setoid with apartness,
  28 i.e. a set with an equivalence relation and an apartness relation compatible with it.
  29 *)
  30
  31 (* Definition of Setoid
  32 Apartness, being the main relation, needs to be [CProp]-valued.  Equality,
  33 as it is characterized by a negative statement, lives in [Prop].
  34
  35 N.B. for the moment we use Prop for both (Matita group)
  36 *)
  37
  38 record is_CSetoid (A : Type) (eq : relation A) (ap : relation A) : Prop \def
  39   {ax_ap_irreflexive  : irreflexive A ap;
  40    ax_ap_symmetric    : symmetric A ap;
  41    ax_ap_cotransitive : cotransitive A ap;
  42    ax_ap_tight        : tight_apart A eq ap}.
  43
  44 record CSetoid : Type \def
  45   {cs_crr   :> Type;
  46    cs_eq    :  relation cs_crr;
  47    cs_ap    :  relation cs_crr;
  48    cs_proof :  is_CSetoid cs_crr cs_eq cs_ap}.
  49
  50 interpretation "setoid equality" 'eq x y = (cs_eq ? x y).
  51
  52 interpretation "setoid apart" 'neq x y = (cs_ap ? x y).
  53
  54 (* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
  55 "cs_neq" e "ap" non sono la stessa cosa? *)
  56 definition cs_neq : \forall S : CSetoid. relation S \def
  57  \lambda S : CSetoid. \lambda x,y : S. \not x = y.
  58
  59 lemma CSetoid_is_CSetoid :
  60  \forall S : CSetoid. is_CSetoid S (cs_eq S) (cs_ap S).
  61 intro. apply (cs_proof S).
  62 qed.
  63
  64 lemma ap_irreflexive: \forall S : CSetoid. irreflexive S (cs_ap S).
  65 intro. elim (CSetoid_is_CSetoid S). assumption.
  66 qed.
  67
  68 lemma ap_symmetric : \forall S : CSetoid. symmetric S(cs_ap S).
  69 intro. elim (CSetoid_is_CSetoid S). assumption.
  70 qed.
  71
  72 lemma ap_cotransitive : \forall S : CSetoid. cotransitive S (cs_ap S).
  73 intro. elim (CSetoid_is_CSetoid S). assumption.
  74 qed.
  75
  76 lemma ap_tight : \forall S : CSetoid. tight_apart S (cs_eq S) (cs_ap S).
  77 intro. elim (CSetoid_is_CSetoid S). assumption.
  78 qed.
  79
  80 definition ex_unq : \forall S : CSetoid. (S \to Prop) \to Prop \def
  81  \lambda S : CSetoid. \lambda P : S \to Prop.
  82   ex2 S (\lambda x. \forall y : S. P y \to x = y) P.
  83
  84
  85 lemma eq_reflexive : \forall S : CSetoid. reflexive S (cs_eq S).
  86 intro. unfold. intro.
  87 generalize in match (ap_tight S x x).
  88 intro.
  89 generalize in match (ap_irreflexive S x);
  90 elim H. apply H1. assumption.
  91 qed.
  92
  93 axiom eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
  94 (*
  95 lemma eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
  96 intro. unfold. intros.
  97 generalize in match (ap_tight S x y). intro.
  98 generalize in match (ap_tight S y x). intro.
  99 generalize in match (ap_symmetric S y x). intro.
 100 elim H1. clear H1.
 101 elim H2. clear H2.
 102 apply H1. unfold. intro. autobatch.
 103 qed.
 104 *)
 105 lemma eq_transitive : \forall S : CSetoid. transitive S (cs_eq S).
 106 intro. unfold. intros (x y z H H0).
 107 generalize in match (ap_tight S x y). intro.
 108 generalize in match (ap_tight S y z). intro.
 109 generalize in match (ap_tight S x z). intro.
 110 elim H3.
 111 apply H4. unfold. intro.
 112 generalize in match (ap_cotransitive ? ? ? H6 y). intro H7.
 113 elim H1 (H1' H1''). clear H1.
 114 elim H2 (H2' H2''). clear H2.
 115 elim H3 (H3' H3''). clear H3.
 116 elim H7 (H1). clear H7.
 117 generalize in match H1. apply H1''. assumption. (*non ho capito il secondo passo*)
 118 generalize in match H1. apply H2''. assumption.
 119 qed.
 120
 121 lemma eq_reflexive_unfolded : \forall S:CSetoid. \forall x:S. x = x.
 122 apply eq_reflexive.
 123 qed.
 124
 125 lemma eq_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S. x = y \to y = x.
 126 apply eq_symmetric.
 127 qed.
 128
 129 lemma eq_transitive_unfolded : \forall S:CSetoid. \forall x,y,z:S. x = y \to y = z \to x = z.
 130 apply eq_transitive.
 131 qed.
 132
 133
 134 lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
 135 intros.
 136 (* perche' autobatch non arriva in fondo ??? *)
 137 apply (eq_transitive_unfolded ? ? x).
 138 apply eq_symmetric_unfolded.
 139 exact H1.
 140 exact H.
 141 qed.
 142
 143
 144 lemma ap_irreflexive_unfolded : \forall S:CSetoid. \forall x:S. \not (x \neq x).
 145 apply ap_irreflexive.
 146 qed.
 147
 148 lemma ap_cotransitive_unfolded : \forall S:CSetoid. \forall a,b:S. a \neq b \to
 149  \forall c:S. a \neq c \or c \neq b.
 150 apply ap_cotransitive.
 151 qed.
 152
 153 lemma ap_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S.
 154  x \neq y \to y \neq x.
 155 apply ap_symmetric.
 156 qed.
 157
 158 lemma eq_imp_not_ap : \forall S:CSetoid. \forall x,y:S.
 159  x = y \to \not (x \neq y).
 160 intros.
 161 elim (ap_tight S x y).
 162 apply H2. assumption.
 163 qed.
 164
 165 lemma not_ap_imp_eq : \forall S:CSetoid. \forall x,y:S.
 166  \not (x \neq y) \to x = y.
 167 intros.
 168 elim (ap_tight S x y).
 169 apply H1. assumption.
 170 qed.
 171
 172 lemma neq_imp_notnot_ap : \forall S:CSetoid. \forall x,y:S.
 173  (cs_neq S x y) \to \not \not (x \neq y).
 174 intros. unfold. intro.
 175 apply H.
 176 apply not_ap_imp_eq.
 177 assumption.
 178 qed.
 179
 180 lemma notnot_ap_imp_neq: \forall S:CSetoid. \forall x,y:S.
 181  (\not \not (x \neq y)) \to (cs_neq S x y).
 182 intros. unfold. unfold. intro.
 183 apply H.
 184 apply eq_imp_not_ap.
 185 assumption.
 186 qed.
 187
 188 lemma ap_imp_neq : \forall S:CSetoid. \forall x,y:S.
 189  x \neq y \to (cs_neq S x y).
 190 intros. unfold. unfold. intro.
 191 apply (eq_imp_not_ap S ? ? H1).
 192 assumption.
 193 qed.
 194
 195 lemma not_neq_imp_eq : \forall S:CSetoid. \forall x,y:S.
 196  \not (cs_neq S x y) \to x = y.
 197 intros.
 198 apply not_ap_imp_eq.
 199 unfold. intro.
 200 apply H.
 201 apply ap_imp_neq.
 202 assumption.
 203 qed.
 204
 205 lemma eq_imp_not_neq : \forall S:CSetoid. \forall x,y:S.
 206  x = y \to \not (cs_neq S x y).
 207 intros. unfold. intro.
 208 apply H1.
 209 assumption.
 210 qed.
 211
 212
 213
 214 (* -----------------The product of setoids----------------------- *)
 215
 216 definition prod_ap: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
 217 \lambda A,B : CSetoid.\lambda c,d: Prod A B.
 218   ((cs_ap A (fst A B c) (fst A B d)) \or
 219    (cs_ap B (snd A B c) (snd A B d))).
 220
 221 definition prod_eq: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
 222 \lambda A,B : CSetoid.\lambda c,d: Prod A B.
 223   ((cs_eq A (fst A B c) (fst A B d)) \and
 224    (cs_eq B (snd A B c) (snd A B d))).
 225
 226
 227 lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
 228  is_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B).
 229 intros.
 230 apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
 231   [unfold.
 232    intros.
 233    elim x.
 234    unfold.
 235    unfold prod_ap. simplify.
 236    intros.
 237    elim H
 238    [apply (ap_irreflexive A a H1)
 239    |apply (ap_irreflexive B b H1)
 240    ]
 241  |unfold.
 242   intros 2.
 243   elim x 2.
 244   elim y 2.
 245   unfold prod_ap. simplify.
 246   intro.
 247   elim H
 248   [left. apply ap_symmetric. assumption.
 249   |right. apply ap_symmetric. assumption
 250   ]
 251  |unfold.
 252   intros 2.
 253   elim x 2.
 254   elim y 4.
 255   elim z.
 256   unfold prod_ap in H. simplify in H.
 257   unfold prod_ap. simplify.
 258   elim H
 259   [cut ((a \neq a2) \or (a2 \neq a1))
 260    [elim Hcut
 261     [left. left. assumption
 262     |right. left. assumption
 263     ]
 264    |apply (ap_cotransitive A). assumption
 265    ]
 266   |cut ((b \neq b2) \or (b2 \neq b1))
 267    [elim Hcut
 268     [left. right. assumption
 269     |right. right. assumption
 270     ]
 271   |apply (ap_cotransitive B). assumption.
 272   ]
 273  ]
 274 |unfold.
 275  intros 2.
 276  elim x 2.
 277  elim y 2.
 278  unfold prod_ap. simplify.
 279  split
 280  [intro.
 281   left
 282   [apply not_ap_imp_eq.
 283    unfold. intro. apply H.
 284    left. assumption
 285   |apply not_ap_imp_eq.
 286    unfold. intro. apply H.
 287    right. assumption
 288   ]
 289  |intro. unfold. intro.
 290  elim H.
 291  elim H1
 292   [apply (eq_imp_not_ap A a a1 H2). assumption
 293   |apply (eq_imp_not_ap B b b1 H3). assumption
 294   ]
 295  ]
 296 ]
 297 qed.
 298
 299
 300 definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
 301  \lambda A,B: CSetoid.
 302   mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
 303
 304
 305
 306 (* Relations and predicates
 307 Here we define the notions of well-definedness and strong extensionality
 308 on predicates and relations.
 309 *)
 310
 311
 312
 313 (*-----------------------------------------------------------------------*)
 314 (*-------------------------- Predicates on Setoids ----------------------*)
 315 (*-----------------------------------------------------------------------*)
 316
 317 (* throughout this section consider (S : CSetoid) and (P : S -> Prop) *)
 318
 319 (* Definition pred_strong_ext : CProp := forall x y : S, P x -> P y or x [#] y. *)
 320 definition pred_strong_ext : \forall S: CSetoid. (S \to Prop) \to Prop \def
 321  \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y: S.
 322   P x \to (P y \or (x \neq y)).
 323
 324 (* Definition pred_wd : CProp := forall x y : S, P x -> x [=] y -> P y. *)
 325 definition pred_wd : \forall S: CSetoid. \forall P :S \to Type. Type \def
 326  \lambda S: CSetoid. \lambda P: S \to Type. \forall x,y : S.
 327   P x \to x = y \to P y.
 328
 329 record wd_pred (S: CSetoid) : Type \def
 330   {wdp_pred     :> S \to Prop;
 331    wdp_well_def :  pred_wd S wdp_pred}.
 332
 333 record CSetoid_predicate (S: CSetoid) : Type \def
 334  {csp_pred   :> S \to Prop;
 335   csp_strext :  pred_strong_ext S csp_pred}.
 336
 337 lemma csp_wd : \forall S: CSetoid. \forall P: CSetoid_predicate S.
 338    pred_wd S (csp_pred S P).
 339 intros.
 340 elim P.
 341 simplify.unfold pred_wd.
 342 intros.
 343 elim (H x y H1)
 344  [assumption|apply False_ind.apply (eq_imp_not_ap S x y H2 H3)]
 345 qed.
 346
 347
 348 (* Same result with CProp instead of Prop: but we just work with Prop (Matita group) *)
 349 (*
 350 Definition pred_strong_ext' : CProp := forall x y : S, P x -> P y or x [#] y.
 351 Definition pred_wd' : Prop := forall x y : S, P x -> x [=] y -> P y.
 352
 353 Record CSetoid_predicate' : Type :=
 354  {csp'_pred   :> S -> Prop;
 355   csp'_strext :  pred_strong_ext' csp'_pred}.
 356
 357 Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
 358 intro P.
 359 intro x; intros y H H0.
 360 elim (csp'_strext P x y H).
 361
 362 autobatch.
 363
 364 intro H1.
 365 elimtype False.
 366 generalize H1.
 367 exact (eq_imp_not_ap _ _ _ H0).
 368 Qed.
 369 *)
 370
 371
 372
 373 (*------------------------------------------------------------------------*)
 374 (* --------------------------- Relations on Setoids --------------------- *)
 375 (*------------------------------------------------------------------------*)
 376 (* throughout this section consider (S : CSetoid) and (R : S -> S -> Prop) *)
 377
 378
 379 (* Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z. *)
 380 (*
 381  primo tentativo ma R non e' ben tipato: si puo' fare il cast giusto (carrier di S)
 382  in modo da sfruttare "relation"?
 383  e' concettualmente sbagliato lavorare ad un livello piu' alto (Type) ? *)
 384 (*
 385 definition rel_wdr : \forall S: CSetoid. \forall x,y,z: S. \lambda R: relation S. Prop \def
 386  \lambda S: CSetoid. \lambda x,y,z: S. \lambda R: relation S.
 387   R S x y \to y = z \to R S x z.
 388
 389 definition rel_wdr : \forall S: CSetoid. \forall x,y,z: (cs_crr S). \lambda R: relation (cs_crr S). Prop \def
 390  \lambda S: CSetoid. \lambda x,y,z: (cs_crr S). \lambda R: relation (cs_crr S).
 391  R (cs_crr S) x y \to y = z \to R (cs_crr S) x z.
 392 *)
 393 definition rel_wdr : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
 394  \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
 395   R x y \to y = z \to R x z.
 396
 397 (*Definition rel_wdl : Prop := forall x y z : S, R x y -> x [=] z -> R z y.*)
 398 definition rel_wdl : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
 399  \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
 400   R x y \to x = z \to R z y.
 401
 402 (* Definition rel_strext : CProp := forall x1 x2 y1 y2 : S, R x1 y1 -> (x1 [#] x2 or y1 [#] y2) or R x2 y2. *)
 403 definition rel_strext : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
 404  \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y1,y2: S.
 405   R x1 y1 \to (x1 \neq x2 \or y1 \neq y2) \or R x2 y2.
 406
 407
 408 (* Definition rel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> x1 [#] x2 or R x2 y. *)
 409 definition rel_strext_lft : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
 410  \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y: S.
 411    R x1 y \to (x1 \neq x2 \or R x2 y).
 412
 413 (* Definition rel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> y1 [#] y2 or R x y2. *)
 414 definition rel_strext_rht : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
 415  \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y1,y2: S.
 416    R x y1 \to (y1 \neq y2 \or R x y2).
 417
 418
 419 lemma rel_strext_imp_lftarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
 420   rel_strext S R \to rel_strext_lft S R.
 421 unfold rel_strext.
 422 unfold rel_strext_lft.
 423 intros.
 424 elim (H  x1 x2 y y H1)
 425 [elim H2
 426  [left. assumption
 427  |absurd (y \neq y) [assumption | apply (ap_irreflexive S y)]
 428  ]
 429 |right. assumption
 430 ]
 431 qed.
 432
 433
 434 lemma rel_strext_imp_rhtarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
 435   rel_strext S R \to rel_strext_rht S R.
 436 unfold rel_strext.
 437 unfold rel_strext_rht.
 438 intros.
 439 elim (H x x y1 y2 H1)
 440 [elim H2
 441  [absurd (x \neq x) [assumption | apply (ap_irreflexive S x)]
 442  |left. assumption
 443  ]
 444 |right. assumption
 445 ]
 446 qed.
 447
 448
 449 lemma rel_strextarg_imp_strext : \forall S: CSetoid. \forall R: S \to S \to Prop.
 450  (rel_strext_rht S R) \to (rel_strext_lft S R) \to (rel_strext S R).
 451 unfold rel_strext_rht.
 452 unfold rel_strext_lft.
 453 unfold rel_strext.
 454 intros.
 455 elim ((H x1 y1 y2) H2)
 456 [left. right. assumption
 457 |elim ((H1 x1 x2 y1) H2)
 458  [left. left. assumption
 459  |elim ((H x2 y1 y2) H4)
 460   [left. right. assumption
 461   |right. assumption.
 462   ]
 463  ]
 464 ]
 465 qed.
 466
 467 (* ---------- Definition of a setoid relation ----------------- *)
 468 (* The type of relations over a setoid.  *)
 469
 470 (* TODO
 471 record CSetoid_relation1 (S: CSetoid) : Type \def
 472   {csr_rel    : S \to S \to Prop;
 473    csr_wdr    :  rel_wdr S csr_rel;
 474    csr_wdl    :  rel_wdl S csr_rel;
 475    csr_strext :  rel_strext S csr_rel}.
 476 *)
 477 (* CORN
 478 Record CSetoid_relation : Type :=
 479   {csr_rel    :> S -> S -> Prop;
 480    csr_wdr    :  rel_wdr csr_rel;
 481    csr_wdl    :  rel_wdl csr_rel;
 482    csr_strext :  rel_strext csr_rel}.
 483 *)
 484
 485
 486 (* ---------- gli stessi risultati di prima ma in CProp ---------*)
 487 (*
 488 Variable R : S -> S -> CProp.
 489 Definition Crel_wdr : CProp := forall x y z : S, R x y -> y [=] z -> R x z.
 490 Definition Crel_wdl : CProp := forall x y z : S, R x y -> x [=] z -> R z y.
 491 Definition Crel_strext : CProp := forall x1 x2 y1 y2 : S,
 492  R x1 y1 -> R x2 y2 or x1 [#] x2 or y1 [#] y2.
 493
 494 Definition Crel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> R x2 y or x1 [#] x2.
 495 Definition Crel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> R x y2 or y1 [#] y2.
 496
 497 Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
 498 Proof.
 499 unfold Crel_strext, Crel_strext_lft in |- *; intros H x1 x2 y H0.
 500 generalize (H x1 x2 y y).
 501 intro H1.
 502 elim (H1 H0).
 503
 504 autobatch.
 505
 506 intro H3.
 507 elim H3; intro H4.
 508
 509 autobatch.
 510 elim (ap_irreflexive _ _ H4).
 511 Qed.
 512
 513 Lemma Crel_strext_imp_rhtarg : Crel_strext -> Crel_strext_rht.
 514 unfold Crel_strext, Crel_strext_rht in |- *; intros H x y1 y2 H0.
 515 generalize (H x x y1 y2 H0); intro H1.
 516 elim H1; intro H2.
 517
 518 autobatch.
 519
 520 elim H2; intro H3.
 521
 522 elim (ap_irreflexive _ _ H3).
 523
 524 autobatch.
 525 Qed.
 526
 527 Lemma Crel_strextarg_imp_strext :
 528  Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
 529 unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
 530  intros H H0 x1 x2 y1 y2 H1.
 531 elim (H x1 y1 y2 H1); autobatch.
 532 intro H2.
 533 elim (H0 x1 x2 y2 H2); autobatch.
 534 Qed.
 535 *)
 536
 537
 538
 539
 540 (* ---- e questo ??????? -----*)
 541
 542 (*Definition of a [CProp] setoid relation
 543 The type of relations over a setoid.  *)
 544 (*
 545 Record CCSetoid_relation : Type :=
 546  {Ccsr_rel    :> S -> S -> CProp;
 547   Ccsr_strext :  Crel_strext Ccsr_rel}.
 548
 549 Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
 550 intro R.
 551 red in |- *; intros x y z H H0.
 552 elim (Ccsr_strext R x x y z H).
 553
 554 autobatch.
 555
 556 intro H1; elimtype False.
 557 elim H1; intro H2.
 558
 559 exact (ap_irreflexive_unfolded _ _ H2).
 560
 561 generalize H2.
 562 exact (eq_imp_not_ap _ _ _ H0).
 563 Qed.
 564
 565 Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.
 566 intro R.
 567 red in |- *; intros x y z H H0.
 568 elim (Ccsr_strext R x z y y H).
 569
 570 autobatch.
 571
 572 intro H1; elimtype False.
 573 elim H1; intro H2.
 574
 575 generalize H2.
 576 exact (eq_imp_not_ap _ _ _ H0).
 577
 578 exact (ap_irreflexive_unfolded _ _ H2).
 579 Qed.
 580
 581 Lemma ap_wdr : Crel_wdr (cs_ap (c:=S)).
 582 red in |- *; intros x y z H H0.
 583 generalize (eq_imp_not_ap _ _ _ H0); intro H1.
 584 elim (ap_cotransitive_unfolded _ _ _ H z); intro H2.
 585
 586 assumption.
 587
 588 elim H1.
 589 apply ap_symmetric_unfolded.
 590 assumption.
 591 Qed.
 592
 593 Lemma ap_wdl : Crel_wdl (cs_ap (c:=S)).
 594 red in |- *; intros x y z H H0.
 595 generalize (ap_wdr y x z); intro H1.
 596 apply ap_symmetric_unfolded.
 597 apply H1.
 598
 599 apply ap_symmetric_unfolded.
 600 assumption.
 601
 602 assumption.
 603 Qed.
 604
 605 Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
 606 Proof ap_wdr.
 607
 608 Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.
 609 Proof ap_wdl.
 610
 611 Lemma ap_strext : Crel_strext (cs_ap (c:=S)).
 612 red in |- *; intros x1 x2 y1 y2 H.
 613 case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
 614
 615 autobatch.
 616
 617 case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
 618
 619 autobatch.
 620
 621 right; right.
 622 apply ap_symmetric_unfolded.
 623 assumption.
 624 Qed.
 625
 626 Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
 627  P x -> x [=] y -> P y.
 628
 629 End CSetoid_relations_and_predicates.
 630
 631 Declare Left Step ap_wdl_unfolded.
 632 Declare Right Step ap_wdr_unfolded.
 633 *)
 634
 635
 636
 637
 638
 639
 640
 641
 642
 643 (*------------------------------------------------------------------------*)
 644 (* ------------------------- Functions between setoids ------------------ *)
 645 (*------------------------------------------------------------------------*)
 646
 647 (* Such functions must preserve the setoid equality
 648 and be strongly extensional w.r.t. the apartness, i.e.
 649 if f(x,y) # f(x1,y1), then  x # x1 or y # y1.
 650 For every arity this has to be defined separately. *)
 651
 652 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2) *)
 653
 654 (* First we consider unary functions.  *)
 655
 656 (*
 657 In the following two definitions,
 658 f is a function from (the carrier of) S1 to (the carrier of) S2  *)
 659
 660 (* Nota: senza le parentesi di (S1 \to S2) non funziona, perche'? *)
 661 definition fun_wd : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
 662  \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
 663   x = y \to f x = f y.
 664
 665 definition fun_strext : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
 666  \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
 667   (f x \neq f y) \to (x \neq y).
 668
 669 lemma fun_strext_imp_wd : \forall S1,S2 : CSetoid. \forall f : S1 \to S2.
 670  fun_strext S1 S2 f \to fun_wd S1 S2 f.
 671 unfold fun_strext.
 672 unfold fun_wd.
 673 intros.
 674 apply not_ap_imp_eq.
 675 unfold.intro.
 676 apply (eq_imp_not_ap ? ? ? H1).
 677 apply H.assumption.
 678 qed.
 679
 680 (* funzioni tra setoidi *)
 681 record CSetoid_fun (S1,S2 : CSetoid) : Type \def
 682   {csf_fun    : S1 \to S2;
 683    csf_strext :  (fun_strext S1 S2 csf_fun)}.
 684
 685 lemma csf_wd : \forall S1,S2 : CSetoid. \forall f : CSetoid_fun S1 S2. fun_wd S1 S2 (csf_fun S1 S2 f).
 686 intros.
 687 apply fun_strext_imp_wd.
 688 apply csf_strext.
 689 qed.
 690
 691 definition Const_CSetoid_fun : \forall S1,S2: CSetoid. S2 \to CSetoid_fun S1 S2.
 692 intros. apply (mk_CSetoid_fun S1 S2 (\lambda x:S1.c)).
 693 unfold.intros.
 694 elim (ap_irreflexive ? ? H).
 695 qed.
 696
 697
 698 (* ---- Binary functions ------*)
 699 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2 \to S3) *)
 700
 701 definition bin_fun_wd : \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
 702  \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
 703   x1 = x2 \to y1 = y2 \to f x1 y1 = f x2 y2.
 704
 705 (*
 706 Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
 707  f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.
 708 *)
 709
 710 definition bin_fun_strext: \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
 711  \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
 712   f x1 y1 \neq f x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
 713
 714 lemma bin_fun_strext_imp_wd : \forall S1,S2,S3: CSetoid.\forall f:S1 \to S2 \to S3.
 715 bin_fun_strext ? ? ? f \to bin_fun_wd ? ? ? f.
 716 intros.unfold in H.
 717 unfold.intros.
 718 apply not_ap_imp_eq.unfold.intro.
 719 elim (H x1 x2 y1 y2 H3).
 720 apply (eq_imp_not_ap ? ? ? H1 H4).
 721 apply (eq_imp_not_ap ? ? ? H2 H4).
 722 qed.
 723
 724
 725
 726 record CSetoid_bin_fun (S1,S2,S3: CSetoid) : Type \def
 727  {csbf_fun    :2> S1 \to S2 \to S3;
 728   csbf_strext :  (bin_fun_strext S1 S2 S3 csbf_fun)}.
 729
 730 lemma csbf_wd : \forall S1,S2,S3: CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3.
 731  bin_fun_wd S1 S2 S3 (csbf_fun S1 S2 S3 f).
 732 intros.
 733 apply bin_fun_strext_imp_wd.
 734 apply csbf_strext.
 735 qed.
 736
 737 lemma csf_wd_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,x' : S1.
 738  x = x' \to (csf_fun S1 S2 f) x = (csf_fun S1 S2 f) x'.
 739 intros.
 740 apply (csf_wd S1 S2 f x x').
 741 assumption.
 742 qed.
 743
 744 lemma csf_strext_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,y : S1.
 745 (csf_fun S1 S2 f) x \neq (csf_fun S1 S2 f) y \to x \neq y.
 746 intros.
 747 apply (csf_strext S1 S2 f x y).
 748 assumption.
 749 qed.
 750
 751 lemma csbf_wd_unfolded : \forall S1,S2,S3 : CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3. \forall x,x':S1.
 752 \forall y,y' : S2. x = x' \to y = y' \to (csbf_fun S1 S2 S3 f) x y = (csbf_fun S1 S2 S3 f) x' y'.
 753 intros.
 754 apply (csbf_wd S1 S2 S3 f x x' y y'); assumption.
 755 qed.
 756
 757 (* Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.*)
 758
 759 (* The unary and binary (inner) operations on a csetoid
 760 An operation is a function with domain(s) and co-domain equal. *)
 761
 762 (* Properties of binary operations *)
 763
 764 definition commutes : \forall S: CSetoid. (S \to S \to S)  \to Prop \def
 765  \lambda S: CSetoid. \lambda f : S \to S \to S.
 766  \forall x,y : S. f x y = f y x.
 767
 768 definition CSassociative : \forall S: CSetoid. \forall f: S \to S \to S.  Prop \def
 769 \lambda S: CSetoid. \lambda f : S \to S \to S.
 770 \forall x,y,z : S.
 771  f x (f y z) = f (f x y) z.
 772
 773 definition un_op_wd : \forall S:CSetoid. (S \to S) \to Prop \def
 774 \lambda S: CSetoid. \lambda f: (S \to S).  fun_wd S S f.
 775
 776
 777 definition un_op_strext: \forall S:CSetoid. (S \to S) \to Prop \def
 778 \lambda S:CSetoid. \lambda f: (S \to S).  fun_strext S S f.
 779
 780
 781 definition CSetoid_un_op : CSetoid \to Type \def
 782 \lambda S:CSetoid. CSetoid_fun S S.
 783
 784 definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext S S f \to CSetoid_fun S S
 785  \def
 786 \lambda S:CSetoid. \lambda f: S \to S. mk_CSetoid_fun S S f.
 787
 788 lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
 789 unfold un_op_strext.
 790 unfold fun_strext.
 791 intros.
 792 simplify in H.
 793 exact H.
 794 qed.
 795
 796 lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x).
 797 unfold un_op_wd.
 798 unfold fun_wd.
 799 intros.
 800 simplify.
 801 exact H.
 802 qed.
 803
 804 definition id_un_op : \forall S:CSetoid. CSetoid_un_op S
 805  \def \lambda S: CSetoid. mk_CSetoid_un_op S (\lambda x : cs_crr S.x) (id_strext S).
 806
 807 definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
 808 \def \lambda S.\lambda f.f.
 809
 810 coercion cic:/matita/algebra/CoRN/Setoids/un_op_fun.con.
 811
 812 definition cs_un_op_strext : \forall S:CSetoid. \forall f: CSetoid_fun S S. fun_strext S S (csf_fun S S f) \def
 813 \lambda S:CSetoid. \lambda f : CSetoid_fun S S. csf_strext S S f.
 814
 815 lemma un_op_wd_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
 816 \forall x, y : S.
 817 x = y \to (csf_fun S S op) x =  (csf_fun S S op) y.
 818 intros.
 819 apply (csf_wd S S ?).assumption.
 820 qed.
 821
 822 lemma un_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
 823 \forall x, y : S.
 824  (csf_fun S S op) x \neq (csf_fun S S op) y \to x \neq y.
 825 exact cs_un_op_strext.
 826 qed.
 827
 828
 829 (* Well-defined binary operations on a setoid.  *)
 830
 831 definition bin_op_wd : \forall S:CSetoid. (S \to S \to S) \to Prop \def
 832 \lambda S:CSetoid. bin_fun_wd S S S.
 833
 834 definition bin_op_strext : \forall S:CSetoid. (S \to S \to S) \to Prop \def
 835 \lambda S:CSetoid. bin_fun_strext S S S.
 836
 837 definition CSetoid_bin_op : CSetoid \to Type \def
 838 \lambda S:CSetoid. CSetoid_bin_fun S S S.
 839
 840
 841 definition mk_CSetoid_bin_op : \forall S:CSetoid. \forall f: S \to S \to S.
 842 bin_fun_strext S S S f \to CSetoid_bin_fun S S S \def
 843  \lambda S:CSetoid. \lambda f: S \to S \to S.
 844  mk_CSetoid_bin_fun S S S f.
 845
 846 (* da controllare che sia ben tipata
 847 definition cs_bin_op_wd : \forall S:CSetoid. ? \def
 848 \lambda S:CSetoid.  csbf_wd S S S.
 849 *)
 850 definition cs_bin_op_wd : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_wd S S S (csbf_fun S S S f) \def
 851 \lambda S:CSetoid. csbf_wd S S S.
 852
 853 definition cs_bin_op_strext : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_strext S S S (csbf_fun S S S f) \def
 854 \lambda S:CSetoid. csbf_strext S S S.
 855
 856
 857
 858 (* Identity Coercion bin_op_bin_fun : CSetoid_bin_op >-> CSetoid_bin_fun. *)
 859
 860 definition bin_op_bin_fun: \forall S:CSetoid. CSetoid_bin_op S \to CSetoid_bin_fun S S S
 861 \def \lambda S.\lambda f.f.
 862
 863 coercion cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con.
 864
 865
 866
 867
 868 lemma bin_op_wd_unfolded :\forall S:CSetoid.  \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
 869  x1 = x2 \to y1 = y2 \to (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
 870 exact cs_bin_op_wd.
 871 qed.
 872
 873 lemma bin_op_strext_unfolded : \forall S:CSetoid.  \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
 874  (csbf_fun S S S op) x1 y1 \neq (csbf_fun S S S op) x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
 875 exact cs_bin_op_strext.
 876 qed.
 877
 878 lemma bin_op_is_wd_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
 879  un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
 880 intros. unfold. unfold.
 881 intros. apply bin_op_wd_unfolded [ assumption | apply eq_reflexive_unfolded ]
 882 qed.
 883
 884 lemma bin_op_is_wd_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
 885  un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
 886 intros. unfold. unfold.
 887 intros. apply bin_op_wd_unfolded [ apply eq_reflexive_unfolded | assumption ]
 888 qed.
 889
 890
 891 lemma bin_op_is_strext_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
 892  un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
 893 intros. unfold un_op_strext. unfold fun_strext.
 894 intros.
 895 cut (x \neq y \lor c \neq c)
 896 [ elim Hcut
 897   [ assumption
 898   | generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
 899   ]
 900 | apply (bin_op_strext_unfolded S op x y c c). assumption.
 901 ]
 902 qed.
 903
 904 lemma bin_op_is_strext_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
 905  un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
 906 intros. unfold un_op_strext. unfold fun_strext.
 907 intros.
 908 cut (c \neq c \lor x \neq y)
 909 [ elim Hcut
 910   [ generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
 911   | assumption
 912   ]
 913 | apply (bin_op_strext_unfolded S op c c x y). assumption.
 914 ]
 915 qed.
 916
 917 definition bin_op2un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
 918 \forall  c : cs_crr S. CSetoid_un_op S \def
 919  \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda  c : cs_crr S.
 920   mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) c x))
 921    (bin_op_is_strext_un_op_rht S op c).
 922
 923 definition bin_op2un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
 924 \forall  c : cs_crr S. CSetoid_un_op S \def
 925  \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda  c : cs_crr S.
 926   mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) x c))
 927    (bin_op_is_strext_un_op_lft S op c).
 928
 929 (*
 930 Definition bin_op2un_op_rht (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
 931   Build_CSetoid_un_op (fun x : S => op c x) (bin_op_is_strext_un_op_rht op c).
 932
 933
 934 Definition bin_op2un_op_lft (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
 935   Build_CSetoid_un_op (fun x : S => op x c) (bin_op_is_strext_un_op_lft op c).
 936 *)
 937
 938
 939 (*
 940 Implicit Arguments commutes [S].
 941 Implicit Arguments associative [S].
 942 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
 943 *)
 944
 945 (*The binary outer operations on a csetoid*)
 946
 947
 948 (*
 949 Well-defined outer operations on a setoid.
 950 *)
 951 definition outer_op_well_def : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
 952 \lambda S1,S2:CSetoid. bin_fun_wd S1 S2 S2.
 953
 954 definition outer_op_strext : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
 955 \lambda S1,S2:CSetoid. bin_fun_strext S1 S2 S2.
 956
 957 definition CSetoid_outer_op : \forall S1,S2:CSetoid.Type \def
 958 \lambda S1,S2:CSetoid.
 959  CSetoid_bin_fun S1 S2 S2.
 960
 961 definition mk_CSetoid_outer_op : \forall S1,S2:CSetoid.
 962 \forall f : S1 \to S2 \to S2.
 963 bin_fun_strext S1 S2 S2 f \to CSetoid_bin_fun S1 S2 S2 \def
 964 \lambda S1,S2:CSetoid.
 965 mk_CSetoid_bin_fun S1 S2 S2.
 966
 967 definition csoo_wd : \forall S1,S2:CSetoid. \forall f : CSetoid_bin_fun S1 S2 S2.
 968 bin_fun_wd S1 S2 S2 (csbf_fun S1 S2 S2 f)  \def
 969 \lambda S1,S2:CSetoid.
 970 csbf_wd S1 S2 S2.
 971
 972 definition csoo_strext : \forall S1,S2:CSetoid.
 973 \forall f : CSetoid_bin_fun S1 S2 S2.
 974 bin_fun_strext S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
 975 \lambda S1,S2:CSetoid.
 976 csbf_strext S1 S2 S2.
 977
 978
 979 definition outer_op_bin_fun: \forall S:CSetoid.
 980 CSetoid_outer_op S S \to CSetoid_bin_fun S S S
 981 \def \lambda S.\lambda f.f.
 982
 983 coercion cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con.
 984 (* begin hide
 985 Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
 986 end hide *)
 987
 988 lemma csoo_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_outer_op S S.
 989 \forall x1, x2, y1, y2 : S.
 990  x1 = x2 -> y1 = y2 -> (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
 991 intros.
 992 apply csoo_wd[assumption|assumption]
 993 qed.
 994
 995 (*
 996 Hint Resolve csoo_wd_unfolded: algebra_c.
 997 *)
 998
 999
1000
1001 (*---------------------------------------------------------------*)
1002 (*--------------------------- Subsetoids ------------------------*)
1003 (*---------------------------------------------------------------*)
1004
1005 (* Let S be a setoid, and P a predicate on the carrier of S *)
1006 (* Variable P : S -> CProp *)
1007
1008 record subcsetoid_crr (S: CSetoid) (P: S \to Prop) : Type \def
1009  {scs_elem :> S;
1010   scs_prf  :  P scs_elem}.
1011
1012 definition restrict_relation : \forall S:CSetoid. \forall R : S \to S \to Prop.
1013  \forall P: S \to Prop. relation (subcsetoid_crr S P) \def
1014   \lambda S:CSetoid. \lambda R : S \to S \to Prop.
1015   \lambda P: S \to Prop. \lambda a,b: subcsetoid_crr S P.
1016   match a with
1017   [ (mk_subcsetoid_crr x H) \Rightarrow
1018     match b with
1019     [ (mk_subcsetoid_crr y H) \Rightarrow R x y ]
1020   ].
1021 (* CPROP
1022 definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
1023   fun a b : subcsetoid_crr =>
1024   match a, b with
1025   | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
1026   end.
1027 *)
1028
1029 definition subcsetoid_eq : \forall S:CSetoid. \forall P: S \to Prop.
1030  relation (subcsetoid_crr S P)\def
1031   \lambda S:CSetoid.
1032   restrict_relation S (cs_eq S).
1033
1034 definition subcsetoid_ap : \forall S:CSetoid. \forall P: S \to Prop.
1035  relation (subcsetoid_crr S P)\def
1036   \lambda S:CSetoid.
1037   restrict_relation S (cs_ap S).
1038
1039 (* N.B. da spostare in relations.ma... *)
1040 definition equiv : \forall A: Type. \forall R: relation A. Prop \def
1041  \lambda A: Type. \lambda R: relation A.
1042  (reflexive A R) \land (transitive A R) \land (symmetric A R).
1043
1044 remark subcsetoid_equiv : \forall S:CSetoid. \forall P: S \to Prop.
1045 equiv ? (subcsetoid_eq S P).
1046 intros. unfold equiv. split
1047 [split
1048  [unfold. intro. elim x. simplify. apply (eq_reflexive S)
1049  |unfold. intros 3. elim y 2.
1050   elim x 2. elim z 2. simplify.
1051   exact (eq_transitive ? c1 c c2)
1052  ]
1053 | unfold. intros 2. elim x 2. elim y 2. simplify. exact (eq_symmetric ? c c1).
1054 ]
1055 qed.
1056
1057 (*
1058 axiom subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
1059 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
1060 *)
1061
1062 lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
1063 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
1064 intros.
1065 apply (mk_is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P))
1066 [ unfold. intros.unfold. elim x. exact (ap_irreflexive_unfolded S ? ?)
1067  [ assumption | simplify in H1. exact H1 ]
1068  (* irreflexive *)
1069 |unfold. intros 2. elim x. generalize in match H1. elim y.simplify in H3. simplify.
1070 exact (ap_symmetric ? ? ? H3)
1071 (* cotransitive *)
1072 |unfold.intros 2. elim x.generalize in match H1. elim y. elim z.simplify. simplify in H3.
1073 apply (ap_cotransitive ? ? ? H3)
1074 (* tight *)
1075 |unfold.intros.elim x. elim y.simplify.
1076 apply (ap_tight S ? ?)]
1077 qed.
1078
1079
1080 definition mk_SubCSetoid : \forall S:CSetoid. \forall P: S \to Prop. CSetoid \def
1081 \lambda S:CSetoid. \lambda P:S \to Prop.
1082 mk_CSetoid (subcsetoid_crr S P) (subcsetoid_eq S P) (subcsetoid_ap S P) (subcsetoid_is_CSetoid S P).
1083
1084 (* Subsetoid unary operations
1085 %\begin{convention}%
1086 Let [f] be a unary setoid operation on [S].
1087 %\end{convention}%
1088 *)
1089
1090 (* Section SubCSetoid_unary_operations.
1091 Variable f : CSetoid_un_op S.
1092 *)
1093
1094 definition un_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
1095  CSetoid_un_op S \to Prop \def
1096  \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
1097  \forall x : cs_crr S. P x \to P ((csf_fun S S f) x).
1098
1099 definition restr_un_op : \forall S:CSetoid. \forall P: S \to Prop.
1100   \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
1101   subcsetoid_crr S P \to subcsetoid_crr S P \def
1102   \lambda S:CSetoid.  \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
1103   \lambda pr : un_op_pres_pred S P f.\lambda a: subcsetoid_crr S P.
1104   match a with
1105   [ (mk_subcsetoid_crr x p) \Rightarrow
1106     (mk_subcsetoid_crr ? ? ((csf_fun S S f) x) (pr x p))].
1107
1108 (* TODO *)
1109 lemma restr_un_op_wd  : \forall S:CSetoid. \forall P: S \to Prop.
1110 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
1111 un_op_wd (mk_SubCSetoid S P) (restr_un_op S P f pr).
1112 intros.
1113 unfold.unfold.intros 2.elim x 2.elim y 2.
1114 simplify.
1115 intro.
1116 normalize in H2.
1117 apply (un_op_wd_unfolded ? f ? ? H2).
1118 qed.
1119
1120 lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
1121 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
1122 un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
1123 intros.unfold.unfold. intros 2.elim y 2. elim x 2.
1124 intros.normalize in H2.
1125 apply (cs_un_op_strext ? f ? ? H2).
1126 qed.
1127
1128 definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
1129  \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P).
1130  intros (S P f pr).
1131  apply (mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr)).
1132  qed.
1133
1134 (* BUG Universe Inconsistency detected
1135  definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
1136  \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P) \def
1137  \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
1138   \lambda pr:un_op_pres_pred S P f.
1139   mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr).
1140 *)
1141
1142 (* Subsetoid binary operations
1143 Let [f] be a binary setoid operation on [S].
1144 *)
1145
1146 (* Section SubCSetoid_binary_operations.
1147 Variable f : CSetoid_bin_op S.
1148 *)
1149
1150 definition bin_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
1151 (CSetoid_bin_op S) \to Prop \def
1152  \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_bin_op S.
1153  \forall x,y : S. P x \to P y \to P ( (csbf_fun S S S f) x y).
1154
1155 (*
1156 Assume [bin_op_pres_pred].
1157 *)
1158
1159 (* Variable pr : bin_op_pres_pred. *)
1160
1161 definition restr_bin_op : \forall S:CSetoid. \forall P:S \to Prop.
1162  \forall f: CSetoid_bin_op S.\forall op : (bin_op_pres_pred S P f).
1163  \forall a, b : subcsetoid_crr S P. subcsetoid_crr S P \def
1164  \lambda S:CSetoid. \lambda P:S \to Prop.
1165  \lambda f: CSetoid_bin_op S. \lambda pr : (bin_op_pres_pred S P f).
1166  \lambda a, b : subcsetoid_crr S P.
1167   match a with
1168   [ (mk_subcsetoid_crr x p) \Rightarrow
1169     match b with
1170     [ (mk_subcsetoid_crr y q) \Rightarrow
1171         (mk_subcsetoid_crr ? ? ((csbf_fun S S S f) x y) (pr x y p q))]
1172   ].
1173
1174
1175 (* TODO *)
1176 lemma restr_bin_op_well_def  : \forall S:CSetoid. \forall P: S \to Prop.
1177 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1178 bin_op_wd (mk_SubCSetoid S P) (restr_bin_op S P f pr).
1179 intros.
1180 unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
1181 simplify.
1182 intros.
1183 normalize in H4.
1184 normalize in H5.
1185 apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
1186 qed.
1187
1188 lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
1189 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1190 bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
1191 intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
1192 simplify.intros.
1193 normalize in H4.
1194 apply (cs_bin_op_strext ? f ? ? ? ? H4).
1195 qed.
1196
1197 definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
1198   \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1199   CSetoid_bin_op (mk_SubCSetoid S P).
1200   intros (S P f pr).
1201   apply (mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr)).
1202   qed.
1203
1204 (* BUG Universe Inconsistency detected
1205 definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
1206   \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1207   CSetoid_bin_op (mk_SubCSetoid S P) \def
1208   \lambda S:CSetoid. \lambda P: S \to Prop.
1209   \lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
1210     mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).
1211 *)
1212
1213 lemma restr_f_assoc : \forall S:CSetoid. \forall P: S \to Prop.
1214   \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1215     CSassociative S (csbf_fun S S S f)
1216     \to CSassociative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)).
1217 intros 4.
1218 intro.
1219 unfold.
1220 intros 3.
1221 elim z 2.elim y 2. elim x 2.
1222 whd.
1223 apply H.
1224 qed.
1225
1226 definition caseZ_diff: \forall A:Type.Z \to (nat \to nat \to A) \to A \def
1227 \lambda A:Type.\lambda z:Z.\lambda f:nat \to nat \to A.
1228   match z with
1229   [OZ \Rightarrow f O O
1230   |(pos n) \Rightarrow f (S n) O
1231   |(neg n) \Rightarrow f O (S n)].
1232
1233 (* Zminus.ma *)
1234 theorem Zminus_S_S : \forall n,m:nat.
1235 Z_of_nat (S n) - S m = Z_of_nat n - m.
1236 intros.
1237 elim n.elim m.simplify. reflexivity.reflexivity.
1238 elim m.simplify.reflexivity.reflexivity.
1239 qed.
1240
1241
1242
1243 lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
1244  (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
1245  \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
1246 intros.
1247 (* perche' apply nat_elim2 non funziona?? *)
1248 apply (nat_elim2 (\lambda m,n.caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = f m n)).
1249 intro.simplify.
1250 apply (nat_case n1).simplify.
1251 apply eq_reflexive.
1252 intro.simplify.apply eq_reflexive.
1253 intro.simplify.apply eq_reflexive.
1254 intros 2.
1255 rewrite > (Zminus_S_S n1 m1).
1256 intros.
1257 cut (f n1 m1 = f (S n1) (S m1)).
1258 apply eq_symmetric_unfolded.
1259 apply eq_transitive.
1260 apply f. apply n1. apply m1.
1261 apply eq_symmetric_unfolded.assumption.
1262 apply eq_symmetric_unfolded.assumption.
1263 apply H.
1264 autobatch.
1265 qed.
1266
1267 (*
1268 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
1269 *)
1270
1271
1272 definition nat_less_n_fun :  \forall S:CSetoid. \forall n:nat. ? \def
1273  \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i:nat. i < n \to S.
1274   \forall i,j : nat. eq nat i j \to (\forall H : i < n.
1275    \forall H' : j < n . (f i H) =  (f j H')).
1276
1277 definition nat_less_n_fun' : \forall S:CSetoid. \forall n:nat. ? \def
1278   \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i: nat. i <= n \to S.
1279    \forall i,j : nat. eq nat i j \to \forall H : i <= n.
1280   \forall H' : j <= n. f i H = f j H'.