1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/algebra/CoRN/Setoid".
18 include "higher_order_defs/relations.ma".
21 include "datatypes/constructors.ma".
23 include "logic/equality.ma".
24 (*include "Z/Zminus.ma".*)
27 Definition of a constructive setoid with apartness,
28 i.e. a set with an equivalence relation and an apartness relation compatible with it.
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].
35 N.B. for the moment we use Prop for both (Matita group)
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}.
44 record CSetoid : Type \def
46 cs_eq : relation cs_crr;
47 cs_ap : relation cs_crr;
48 cs_proof : is_CSetoid cs_crr cs_eq cs_ap}.
50 interpretation "setoid equality"
51 'eq x y = (cic:/matita/algebra/CoRN/Setoid/cs_eq.con _ x y).
53 interpretation "setoid apart"
54 'neq x y = (cic:/matita/algebra/CoRN/Setoid/cs_ap.con _ x y).
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.
61 lemma CSetoid_is_CSetoid :
62 \forall S : CSetoid. is_CSetoid S (cs_eq S) (cs_ap S).
63 intro. apply (cs_proof S).
66 lemma ap_irreflexive: \forall S : CSetoid. irreflexive S (cs_ap S).
67 intro. elim (CSetoid_is_CSetoid S). assumption.
70 lemma ap_symmetric : \forall S : CSetoid. symmetric S(cs_ap S).
71 intro. elim (CSetoid_is_CSetoid S). assumption.
74 lemma ap_cotransitive : \forall S : CSetoid. cotransitive S (cs_ap S).
75 intro. elim (CSetoid_is_CSetoid S). assumption.
78 lemma ap_tight : \forall S : CSetoid. tight_apart S (cs_eq S) (cs_ap S).
79 intro. elim (CSetoid_is_CSetoid S). assumption.
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.
87 lemma eq_reflexive : \forall S : CSetoid. reflexive S (cs_eq S).
89 generalize in match (ap_tight S x x).
91 generalize in match (ap_irreflexive S x);
92 elim H. apply H1. assumption.
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.
102 apply H1. unfold. intro. auto.
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.
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.
121 lemma eq_reflexive_unfolded : \forall S:CSetoid. \forall x:S. x = x.
125 lemma eq_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S. x = y \to y = x.
129 lemma eq_transitive_unfolded : \forall S:CSetoid. \forall x,y,z:S. x = y \to y = z \to x = z.
133 lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
135 (* perche' auto non arriva in fondo ??? *)
136 apply (eq_transitive_unfolded ? ? x). auto.
140 lemma ap_irreflexive_unfolded : \forall S:CSetoid. \forall x:S. \not (x \neq x).
141 apply ap_irreflexive.
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.
149 lemma ap_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S.
150 x \neq y \to y \neq x.
154 lemma eq_imp_not_ap : \forall S:CSetoid. \forall x,y:S.
155 x = y \to \not (x \neq y).
157 elim (ap_tight S x y).
158 apply H2. assumption.
161 lemma not_ap_imp_eq : \forall S:CSetoid. \forall x,y:S.
162 \not (x \neq y) \to x = y.
164 elim (ap_tight S x y).
165 apply H1. assumption.
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.
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.
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).
191 lemma not_neq_imp_eq : \forall S:CSetoid. \forall x,y:S.
192 \not (cs_neq S x y) \to x = y.
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.
210 (* -----------------The product of setoids----------------------- *)
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))).
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))).
223 lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
224 is_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B).
226 apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
231 unfold prod_ap. simplify.
234 [apply (ap_irreflexive A t H1)
235 |apply (ap_irreflexive B t1 H1)
241 unfold prod_ap. simplify.
244 [left. apply ap_symmetric. assumption.
245 |right. apply ap_symmetric. assumption
252 unfold prod_ap in H. simplify in H.
253 unfold prod_ap. simplify.
255 [cut ((t \neq t4) \or (t4 \neq t2))
257 [left. left. assumption
258 |right. left. assumption
260 |apply (ap_cotransitive A). assumption
262 |cut ((t1 \neq t5) \or (t5 \neq t3))
264 [left. right. assumption
265 |right. right. assumption
267 |apply (ap_cotransitive B). assumption.
274 unfold prod_ap. simplify.
278 [apply not_ap_imp_eq.
279 unfold. intro. apply H.
281 |apply not_ap_imp_eq.
282 unfold. intro. apply H.
285 |intro. unfold. intro.
288 [apply (eq_imp_not_ap A t t2 H2). assumption
289 |apply (eq_imp_not_ap B t1 t3 H3). assumption
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).
302 (* Relations and predicates
303 Here we define the notions of well-definedness and strong extensionality
304 on predicates and relations.
309 (*-----------------------------------------------------------------------*)
310 (*-------------------------- Predicates on Setoids ----------------------*)
311 (*-----------------------------------------------------------------------*)
313 (* throughout this section consider (S : CSetoid) and (P : S -> Prop) *)
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)).
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.
325 record wd_pred (S: CSetoid) : Type \def
326 {wdp_pred :> S \to Prop;
327 wdp_well_def : pred_wd S wdp_pred}.
329 record CSetoid_predicate (S: CSetoid) : Type \def
330 {csp_pred :> S \to Prop;
331 csp_strext : pred_strong_ext S csp_pred}.
333 lemma csp_wd : \forall S: CSetoid. \forall P: CSetoid_predicate S.
334 pred_wd S (csp_pred S P).
337 simplify.unfold pred_wd.
340 [assumption|apply False_ind.apply (eq_imp_not_ap S x y H2 H3)]
344 (* Same result with CProp instead of Prop: but we just work with Prop (Matita group) *)
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.
349 Record CSetoid_predicate' : Type :=
350 {csp'_pred :> S -> Prop;
351 csp'_strext : pred_strong_ext' csp'_pred}.
353 Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
355 intro x; intros y H H0.
356 elim (csp'_strext P x y H).
363 exact (eq_imp_not_ap _ _ _ H0).
369 (*------------------------------------------------------------------------*)
370 (* --------------------------- Relations on Setoids --------------------- *)
371 (*------------------------------------------------------------------------*)
372 (* throughout this section consider (S : CSetoid) and (R : S -> S -> Prop) *)
375 (* Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z. *)
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) ? *)
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.
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.
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.
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.
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.
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).
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).
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.
418 unfold rel_strext_lft.
420 elim (H x1 x2 y y H1)
423 |absurd (y \neq y) [assumption | apply (ap_irreflexive S y)]
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.
433 unfold rel_strext_rht.
435 elim (H x x y1 y2 H1)
437 [absurd (x \neq x) [assumption | apply (ap_irreflexive S x)]
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.
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
463 (* ---------- Definition of a setoid relation ----------------- *)
464 (* The type of relations over a setoid. *)
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}.
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}.
482 (* ---------- gli stessi risultati di prima ma in CProp ---------*)
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.
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.
493 Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
495 unfold Crel_strext, Crel_strext_lft in |- *; intros H x1 x2 y H0.
496 generalize (H x1 x2 y y).
506 elim (ap_irreflexive _ _ H4).
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.
518 elim (ap_irreflexive _ _ H3).
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.
529 elim (H0 x1 x2 y2 H2); auto.
536 (* ---- e questo ??????? -----*)
538 (*Definition of a [CProp] setoid relation
539 The type of relations over a setoid. *)
541 Record CCSetoid_relation : Type :=
542 {Ccsr_rel :> S -> S -> CProp;
543 Ccsr_strext : Crel_strext Ccsr_rel}.
545 Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
547 red in |- *; intros x y z H H0.
548 elim (Ccsr_strext R x x y z H).
552 intro H1; elimtype False.
555 exact (ap_irreflexive_unfolded _ _ H2).
558 exact (eq_imp_not_ap _ _ _ H0).
561 Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.
563 red in |- *; intros x y z H H0.
564 elim (Ccsr_strext R x z y y H).
568 intro H1; elimtype False.
572 exact (eq_imp_not_ap _ _ _ H0).
574 exact (ap_irreflexive_unfolded _ _ H2).
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.
585 apply ap_symmetric_unfolded.
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.
595 apply ap_symmetric_unfolded.
601 Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
604 Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.
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.
613 case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
618 apply ap_symmetric_unfolded.
622 Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
623 P x -> x [=] y -> P y.
625 End CSetoid_relations_and_predicates.
627 Declare Left Step ap_wdl_unfolded.
628 Declare Right Step ap_wdr_unfolded.
639 (*------------------------------------------------------------------------*)
640 (* ------------------------- Functions between setoids ------------------ *)
641 (*------------------------------------------------------------------------*)
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. *)
648 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2) *)
650 (* First we consider unary functions. *)
653 In the following two definitions,
654 f is a function from (the carrier of) S1 to (the carrier of) S2 *)
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.
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).
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.
672 apply (eq_imp_not_ap ? ? ? H1).
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)}.
681 lemma csf_wd : \forall S1,S2 : CSetoid. \forall f : CSetoid_fun S1 S2. fun_wd S1 S2 (csf_fun S1 S2 f).
683 apply fun_strext_imp_wd.
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)).
690 elim (ap_irreflexive ? ? H).
694 (* ---- Binary functions ------*)
695 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2 \to S3) *)
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.
702 Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
703 f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.
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.
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.
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).
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)}.
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).
729 apply bin_fun_strext_imp_wd.
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'.
736 apply (csf_wd S1 S2 f x x').
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.
743 apply (csf_strext S1 S2 f x y).
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'.
750 apply (csbf_wd S1 S2 S3 f x x' y y'); assumption.
753 (* Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.*)
755 (* The unary and binary (inner) operations on a csetoid
756 An operation is a function with domain(s) and co-domain equal. *)
758 (* Properties of binary operations *)
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.
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.
767 f x (f y z) = f (f x y) z.
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.
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.
777 definition CSetoid_un_op : CSetoid \to Type \def
778 \lambda S:CSetoid. CSetoid_fun S S.
780 definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext S S f \to CSetoid_fun S S
782 \lambda S:CSetoid. \lambda f: S \to S. mk_CSetoid_fun S S f.
784 lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
786 unfold fun_strext.intros.
790 lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x).
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).
800 definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
801 \def \lambda S.\lambda f.f.
803 coercion cic:/matita/algebra/CoRN/Setoid/un_op_fun.con.
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.
808 lemma un_op_wd_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
810 x = y \to (csf_fun S S op) x = (csf_fun S S op) y.
812 apply (csf_wd S S ?).assumption.
815 lemma un_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op 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.
822 (* Well-defined binary operations on a setoid. *)
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.
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.
830 definition CSetoid_bin_op : CSetoid \to Type \def
831 \lambda S:CSetoid. CSetoid_bin_fun S S S.
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.
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.
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.
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.
851 (* Identity Coercion bin_op_bin_fun : CSetoid_bin_op >-> CSetoid_bin_fun. *)
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.
856 coercion cic:/matita/algebra/CoRN/Setoid/bin_op_bin_fun.con.
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.
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.
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 ]
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 ]
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.
888 cut (x \neq y \lor c \neq c)
891 | generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
893 | apply (bin_op_strext_unfolded S op x y c c). assumption.
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.
901 cut (c \neq c \lor x \neq y)
903 [ generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
906 | apply (bin_op_strext_unfolded S op c c x y). assumption.
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).
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).
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).
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).
933 Implicit Arguments commutes [S].
934 Implicit Arguments associative [S].
935 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
938 (*The binary outer operations on a csetoid*)
942 Well-defined outer operations on a setoid.
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.
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.
950 definition CSetoid_outer_op : \forall S1,S2:CSetoid.Type \def
951 \lambda S1,S2:CSetoid.
952 CSetoid_bin_fun S1 S2 S2.
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.
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.
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.
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.
976 coercion cic:/matita/algebra/CoRN/Setoid/outer_op_bin_fun.con.
978 Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
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.
985 apply csoo_wd[assumption|assumption]
989 Hint Resolve csoo_wd_unfolded: algebra_c.
994 (*---------------------------------------------------------------*)
995 (*--------------------------- Subsetoids ------------------------*)
996 (*---------------------------------------------------------------*)
998 (* Let S be a setoid, and P a predicate on the carrier of S *)
999 (* Variable P : S -> CProp *)
1001 record subcsetoid_crr (S: CSetoid) (P: S \to Prop) : Type \def
1003 scs_prf : P scs_elem}.
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.
1010 [ (mk_subcsetoid_crr x H) \Rightarrow
1012 [ (mk_subcsetoid_crr y H) \Rightarrow R x y ]
1015 definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
1016 fun a b : subcsetoid_crr =>
1018 | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
1022 definition subcsetoid_eq : \forall S:CSetoid. \forall P: S \to Prop.
1023 relation (subcsetoid_crr S P)\def
1025 restrict_relation S (cs_eq S).
1027 definition subcsetoid_ap : \forall S:CSetoid. \forall P: S \to Prop.
1028 relation (subcsetoid_crr S P)\def
1030 restrict_relation S (cs_ap S).
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).
1037 remark subcsetoid_equiv : \forall S:CSetoid. \forall P: S \to Prop.
1038 equiv ? (subcsetoid_eq S P).
1039 intros. unfold equiv. 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)
1046 | unfold. intros 2. elim x 2. elim y 2. simplify. exact (eq_symmetric ? c c1).
1050 lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
1051 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
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.]
1057 |unfold. intros 2. elim x. generalize in match H1. elim y.simplify in H3. simplify.
1058 exact (ap_symmetric ? ? ? H3)
1060 |unfold.intros 2. elim x.generalize in match H1. elim y. elim z.simplify. simplify in H3.
1061 apply (ap_cotransitive ? ? ? H3)
1063 |unfold.intros.elim x. elim y.simplify.
1064 apply (ap_tight S ? ?)]
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).
1071 (* Subsetoid unary operations
1072 %\begin{convention}%
1073 Let [f] be a unary setoid operation on [S].
1077 (* Section SubCSetoid_unary_operations.
1078 Variable f : CSetoid_un_op S.
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).
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.
1092 [ (mk_subcsetoid_crr x p) \Rightarrow
1093 (mk_subcsetoid_crr ? ? ((csf_fun S S f) x) (pr x p))].
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).
1100 unfold.unfold.intros 2.elim x 2.elim y 2.
1104 apply (un_op_wd_unfolded ? f ? ? H2).
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).
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).
1123 (* Subsetoid binary operations
1124 Let [f] be a binary setoid operation on [S].
1127 (* Section SubCSetoid_binary_operations.
1128 Variable f : CSetoid_bin_op S.
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).
1137 Assume [bin_op_pres_pred].
1140 (* Variable pr : bin_op_pres_pred. *)
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.
1149 [ (mk_subcsetoid_crr x p) \Rightarrow
1151 [ (mk_subcsetoid_crr y q) \Rightarrow
1152 (mk_subcsetoid_crr ? ? ((csbf_fun S S S f) x y) (pr x y p q))]
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).
1161 unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
1166 apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
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.
1175 apply (cs_bin_op_strext ? f ? ? ? ? H4).
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).
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)).
1193 elim z 2.elim y 2. elim x 2.
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.
1201 [OZ \Rightarrow f O O
1202 |(pos n) \Rightarrow f (S n) O
1203 |(neg n) \Rightarrow f O (S n)].
1206 theorem Zminus_S_S : \forall n,m:nat.
1207 Z_of_nat (S n) - S m = Z_of_nat n - m.
1209 elim n.elim m.simplify. reflexivity.reflexivity.
1210 elim m.simplify.reflexivity.reflexivity.
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).
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)).
1220 apply (nat_case n1).simplify.
1222 intro.simplify.apply eq_reflexive.
1223 intro.simplify.apply eq_reflexive.
1225 rewrite > (Zminus_S_S n1 m1).
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.
1237 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
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')).
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'.