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