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