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 axiom eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
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.
104 apply H1. unfold. intro. auto.
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.
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.
123 lemma eq_reflexive_unfolded : \forall S:CSetoid. \forall x:S. x = x.
127 lemma eq_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S. x = y \to y = x.
131 lemma eq_transitive_unfolded : \forall S:CSetoid. \forall x,y,z:S. x = y \to y = z \to x = z.
136 lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
138 (* perche' auto non arriva in fondo ??? *)
139 apply (eq_transitive_unfolded ? ? x).
140 apply eq_symmetric_unfolded.
146 lemma ap_irreflexive_unfolded : \forall S:CSetoid. \forall x:S. \not (x \neq x).
147 apply ap_irreflexive.
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.
155 lemma ap_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S.
156 x \neq y \to y \neq x.
160 lemma eq_imp_not_ap : \forall S:CSetoid. \forall x,y:S.
161 x = y \to \not (x \neq y).
163 elim (ap_tight S x y).
164 apply H2. assumption.
167 lemma not_ap_imp_eq : \forall S:CSetoid. \forall x,y:S.
168 \not (x \neq y) \to x = y.
170 elim (ap_tight S x y).
171 apply H1. assumption.
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.
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.
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).
197 lemma not_neq_imp_eq : \forall S:CSetoid. \forall x,y:S.
198 \not (cs_neq S x y) \to x = y.
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.
216 (* -----------------The product of setoids----------------------- *)
218 definition prod_ap: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
219 \lambda A,B : CSetoid.\lambda c,d: ProdT A B.
220 ((cs_ap A (fstT A B c) (fstT A B d)) \or
221 (cs_ap B (sndT A B c) (sndT A B d))).
223 definition prod_eq: \forall A,B : CSetoid.\forall c,d: ProdT A B. Prop \def
224 \lambda A,B : CSetoid.\lambda c,d: ProdT A B.
225 ((cs_eq A (fstT A B c) (fstT A B d)) \and
226 (cs_eq B (sndT A B c) (sndT A B d))).
229 lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
230 is_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B).
232 apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
237 unfold prod_ap. simplify.
240 [apply (ap_irreflexive A t H1)
241 |apply (ap_irreflexive B t1 H1)
247 unfold prod_ap. simplify.
250 [left. apply ap_symmetric. assumption.
251 |right. apply ap_symmetric. assumption
258 unfold prod_ap in H. simplify in H.
259 unfold prod_ap. simplify.
261 [cut ((t \neq t4) \or (t4 \neq t2))
263 [left. left. assumption
264 |right. left. assumption
266 |apply (ap_cotransitive A). assumption
268 |cut ((t1 \neq t5) \or (t5 \neq t3))
270 [left. right. assumption
271 |right. right. assumption
273 |apply (ap_cotransitive B). assumption.
280 unfold prod_ap. simplify.
284 [apply not_ap_imp_eq.
285 unfold. intro. apply H.
287 |apply not_ap_imp_eq.
288 unfold. intro. apply H.
291 |intro. unfold. intro.
294 [apply (eq_imp_not_ap A t t2 H2). assumption
295 |apply (eq_imp_not_ap B t1 t3 H3). assumption
302 definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
303 \lambda A,B: CSetoid.
304 mk_CSetoid (ProdT A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
308 (* Relations and predicates
309 Here we define the notions of well-definedness and strong extensionality
310 on predicates and relations.
315 (*-----------------------------------------------------------------------*)
316 (*-------------------------- Predicates on Setoids ----------------------*)
317 (*-----------------------------------------------------------------------*)
319 (* throughout this section consider (S : CSetoid) and (P : S -> Prop) *)
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)).
326 (* Definition pred_wd : CProp := forall x y : S, P x -> x [=] y -> P y. *)
327 definition pred_wd : \forall S: CSetoid. (S \to Prop) \to Prop \def
328 \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y : S.
329 P x \to x = y \to P y.
331 record wd_pred (S: CSetoid) : Type \def
332 {wdp_pred :> S \to Prop;
333 wdp_well_def : pred_wd S wdp_pred}.
335 record CSetoid_predicate (S: CSetoid) : Type \def
336 {csp_pred :> S \to Prop;
337 csp_strext : pred_strong_ext S csp_pred}.
339 lemma csp_wd : \forall S: CSetoid. \forall P: CSetoid_predicate S.
340 pred_wd S (csp_pred S P).
343 simplify.unfold pred_wd.
346 [assumption|apply False_ind.apply (eq_imp_not_ap S x y H2 H3)]
350 (* Same result with CProp instead of Prop: but we just work with Prop (Matita group) *)
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.
355 Record CSetoid_predicate' : Type :=
356 {csp'_pred :> S -> Prop;
357 csp'_strext : pred_strong_ext' csp'_pred}.
359 Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
361 intro x; intros y H H0.
362 elim (csp'_strext P x y H).
369 exact (eq_imp_not_ap _ _ _ H0).
375 (*------------------------------------------------------------------------*)
376 (* --------------------------- Relations on Setoids --------------------- *)
377 (*------------------------------------------------------------------------*)
378 (* throughout this section consider (S : CSetoid) and (R : S -> S -> Prop) *)
381 (* Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z. *)
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) ? *)
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.
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.
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.
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.
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.
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).
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).
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.
424 unfold rel_strext_lft.
426 elim (H x1 x2 y y H1)
429 |absurd (y \neq y) [assumption | apply (ap_irreflexive S y)]
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.
439 unfold rel_strext_rht.
441 elim (H x x y1 y2 H1)
443 [absurd (x \neq x) [assumption | apply (ap_irreflexive S x)]
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.
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
469 (* ---------- Definition of a setoid relation ----------------- *)
470 (* The type of relations over a setoid. *)
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}.
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}.
488 (* ---------- gli stessi risultati di prima ma in CProp ---------*)
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.
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.
499 Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
501 unfold Crel_strext, Crel_strext_lft in |- *; intros H x1 x2 y H0.
502 generalize (H x1 x2 y y).
512 elim (ap_irreflexive _ _ H4).
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.
524 elim (ap_irreflexive _ _ H3).
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); auto.
535 elim (H0 x1 x2 y2 H2); auto.
542 (* ---- e questo ??????? -----*)
544 (*Definition of a [CProp] setoid relation
545 The type of relations over a setoid. *)
547 Record CCSetoid_relation : Type :=
548 {Ccsr_rel :> S -> S -> CProp;
549 Ccsr_strext : Crel_strext Ccsr_rel}.
551 Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
553 red in |- *; intros x y z H H0.
554 elim (Ccsr_strext R x x y z H).
558 intro H1; elimtype False.
561 exact (ap_irreflexive_unfolded _ _ H2).
564 exact (eq_imp_not_ap _ _ _ H0).
567 Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.
569 red in |- *; intros x y z H H0.
570 elim (Ccsr_strext R x z y y H).
574 intro H1; elimtype False.
578 exact (eq_imp_not_ap _ _ _ H0).
580 exact (ap_irreflexive_unfolded _ _ H2).
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.
591 apply ap_symmetric_unfolded.
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.
601 apply ap_symmetric_unfolded.
607 Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
610 Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.
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.
619 case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
624 apply ap_symmetric_unfolded.
628 Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
629 P x -> x [=] y -> P y.
631 End CSetoid_relations_and_predicates.
633 Declare Left Step ap_wdl_unfolded.
634 Declare Right Step ap_wdr_unfolded.
645 (*------------------------------------------------------------------------*)
646 (* ------------------------- Functions between setoids ------------------ *)
647 (*------------------------------------------------------------------------*)
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. *)
654 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2) *)
656 (* First we consider unary functions. *)
659 In the following two definitions,
660 f is a function from (the carrier of) S1 to (the carrier of) S2 *)
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.
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).
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.
678 apply (eq_imp_not_ap ? ? ? H1).
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)}.
687 lemma csf_wd : \forall S1,S2 : CSetoid. \forall f : CSetoid_fun S1 S2. fun_wd S1 S2 (csf_fun S1 S2 f).
689 apply fun_strext_imp_wd.
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)).
696 elim (ap_irreflexive ? ? H).
700 (* ---- Binary functions ------*)
701 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2 \to S3) *)
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.
708 Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
709 f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.
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.
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.
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).
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)}.
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).
735 apply bin_fun_strext_imp_wd.
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'.
742 apply (csf_wd S1 S2 f x x').
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.
749 apply (csf_strext S1 S2 f x y).
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'.
756 apply (csbf_wd S1 S2 S3 f x x' y y'); assumption.
759 (* Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.*)
761 (* The unary and binary (inner) operations on a csetoid
762 An operation is a function with domain(s) and co-domain equal. *)
764 (* Properties of binary operations *)
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.
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.
773 f x (f y z) = f (f x y) z.
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.
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.
783 definition CSetoid_un_op : CSetoid \to Type \def
784 \lambda S:CSetoid. CSetoid_fun S S.
786 definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext S S f \to CSetoid_fun S S
788 \lambda S:CSetoid. \lambda f: S \to S. mk_CSetoid_fun S S f.
790 lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
798 lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x).
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).
809 definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
810 \def \lambda S.\lambda f.f.
812 coercion cic:/matita/algebra/CoRN/Setoid/un_op_fun.con.
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.
817 lemma un_op_wd_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
819 x = y \to (csf_fun S S op) x = (csf_fun S S op) y.
821 apply (csf_wd S S ?).assumption.
824 lemma un_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op 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.
831 (* Well-defined binary operations on a setoid. *)
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.
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.
839 definition CSetoid_bin_op : CSetoid \to Type \def
840 \lambda S:CSetoid. CSetoid_bin_fun S S S.
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.
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.
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.
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.
860 (* Identity Coercion bin_op_bin_fun : CSetoid_bin_op >-> CSetoid_bin_fun. *)
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.
865 coercion cic:/matita/algebra/CoRN/Setoid/bin_op_bin_fun.con.
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.
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.
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 ]
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 ]
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.
897 cut (x \neq y \lor c \neq c)
900 | generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
902 | apply (bin_op_strext_unfolded S op x y c c). assumption.
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.
910 cut (c \neq c \lor x \neq y)
912 [ generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
915 | apply (bin_op_strext_unfolded S op c c x y). assumption.
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).
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).
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).
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).
942 Implicit Arguments commutes [S].
943 Implicit Arguments associative [S].
944 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
947 (*The binary outer operations on a csetoid*)
951 Well-defined outer operations on a setoid.
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.
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.
959 definition CSetoid_outer_op : \forall S1,S2:CSetoid.Type \def
960 \lambda S1,S2:CSetoid.
961 CSetoid_bin_fun S1 S2 S2.
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.
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.
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.
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.
985 coercion cic:/matita/algebra/CoRN/Setoid/outer_op_bin_fun.con.
987 Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
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.
994 apply csoo_wd[assumption|assumption]
998 Hint Resolve csoo_wd_unfolded: algebra_c.
1003 (*---------------------------------------------------------------*)
1004 (*--------------------------- Subsetoids ------------------------*)
1005 (*---------------------------------------------------------------*)
1007 (* Let S be a setoid, and P a predicate on the carrier of S *)
1008 (* Variable P : S -> CProp *)
1010 record subcsetoid_crr (S: CSetoid) (P: S \to Prop) : Type \def
1012 scs_prf : P scs_elem}.
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.
1019 [ (mk_subcsetoid_crr x H) \Rightarrow
1021 [ (mk_subcsetoid_crr y H) \Rightarrow R x y ]
1024 definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
1025 fun a b : subcsetoid_crr =>
1027 | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
1031 definition subcsetoid_eq : \forall S:CSetoid. \forall P: S \to Prop.
1032 relation (subcsetoid_crr S P)\def
1034 restrict_relation S (cs_eq S).
1036 definition subcsetoid_ap : \forall S:CSetoid. \forall P: S \to Prop.
1037 relation (subcsetoid_crr S P)\def
1039 restrict_relation S (cs_ap S).
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).
1046 remark subcsetoid_equiv : \forall S:CSetoid. \forall P: S \to Prop.
1047 equiv ? (subcsetoid_eq S P).
1048 intros. unfold equiv. 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)
1055 | unfold. intros 2. elim x 2. elim y 2. simplify. exact (eq_symmetric ? c c1).
1060 axiom subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
1061 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
1064 lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
1065 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
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 ]
1071 |unfold. intros 2. elim x. generalize in match H1. elim y.simplify in H3. simplify.
1072 exact (ap_symmetric ? ? ? H3)
1074 |unfold.intros 2. elim x.generalize in match H1. elim y. elim z.simplify. simplify in H3.
1075 apply (ap_cotransitive ? ? ? H3)
1077 |unfold.intros.elim x. elim y.simplify.
1078 apply (ap_tight S ? ?)]
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).
1086 (* Subsetoid unary operations
1087 %\begin{convention}%
1088 Let [f] be a unary setoid operation on [S].
1092 (* Section SubCSetoid_unary_operations.
1093 Variable f : CSetoid_un_op S.
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).
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.
1107 [ (mk_subcsetoid_crr x p) \Rightarrow
1108 (mk_subcsetoid_crr ? ? ((csf_fun S S f) x) (pr x p))].
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).
1115 unfold.unfold.intros 2.elim x 2.elim y 2.
1119 apply (un_op_wd_unfolded ? f ? ? H2).
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.reduce in H2.
1127 apply (cs_un_op_strext ? f ? ? H2).
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.
1132 CSetoid_un_op (mk_SubCSetoid S P) \def
1133 \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
1134 \lambda pr:un_op_pres_pred S P f.
1135 mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr).
1138 (* Subsetoid binary operations
1139 Let [f] be a binary setoid operation on [S].
1142 (* Section SubCSetoid_binary_operations.
1143 Variable f : CSetoid_bin_op S.
1146 definition bin_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
1147 (CSetoid_bin_op S) \to Prop \def
1148 \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_bin_op S.
1149 \forall x,y : S. P x \to P y \to P ( (csbf_fun S S S f) x y).
1152 Assume [bin_op_pres_pred].
1155 (* Variable pr : bin_op_pres_pred. *)
1157 definition restr_bin_op : \forall S:CSetoid. \forall P:S \to Prop.
1158 \forall f: CSetoid_bin_op S.\forall op : (bin_op_pres_pred S P f).
1159 \forall a, b : subcsetoid_crr S P. subcsetoid_crr S P \def
1160 \lambda S:CSetoid. \lambda P:S \to Prop.
1161 \lambda f: CSetoid_bin_op S. \lambda pr : (bin_op_pres_pred S P f).
1162 \lambda a, b : subcsetoid_crr S P.
1164 [ (mk_subcsetoid_crr x p) \Rightarrow
1166 [ (mk_subcsetoid_crr y q) \Rightarrow
1167 (mk_subcsetoid_crr ? ? ((csbf_fun S S S f) x y) (pr x y p q))]
1172 lemma restr_bin_op_well_def : \forall S:CSetoid. \forall P: S \to Prop.
1173 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1174 bin_op_wd (mk_SubCSetoid S P) (restr_bin_op S P f pr).
1176 unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
1181 apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
1184 lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
1185 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1186 bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
1187 intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
1190 apply (cs_bin_op_strext ? f ? ? ? ? H4).
1193 definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
1194 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1195 CSetoid_bin_op (mk_SubCSetoid S P) \def
1196 \lambda S:CSetoid. \lambda P: S \to Prop.
1197 \lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
1198 mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).
1200 lemma restr_f_assoc : \forall S:CSetoid. \forall P: S \to Prop.
1201 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1202 CSassociative S (csbf_fun S S S f)
1203 \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)).
1208 elim z 2.elim y 2. elim x 2.
1213 definition caseZ_diff: \forall A:Type.Z \to (nat \to nat \to A) \to A \def
1214 \lambda A:Type.\lambda z:Z.\lambda f:nat \to nat \to A.
1216 [OZ \Rightarrow f O O
1217 |(pos n) \Rightarrow f (S n) O
1218 |(neg n) \Rightarrow f O (S n)].
1221 theorem Zminus_S_S : \forall n,m:nat.
1222 Z_of_nat (S n) - S m = Z_of_nat n - m.
1224 elim n.elim m.simplify. reflexivity.reflexivity.
1225 elim m.simplify.reflexivity.reflexivity.
1230 lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
1231 (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
1232 \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
1234 (* perche' apply nat_elim2 non funziona?? *)
1235 apply (nat_elim2 (\lambda m,n.caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = f m n)).
1237 apply (nat_case n1).simplify.
1239 intro.simplify.apply eq_reflexive.
1240 intro.simplify.apply eq_reflexive.
1242 rewrite > (Zminus_S_S n1 m1).
1244 cut (f n1 m1 = f (S n1) (S m1)).
1245 apply eq_symmetric_unfolded.
1246 apply eq_transitive.
1247 apply f. apply n1. apply m1.
1248 apply eq_symmetric_unfolded.assumption.
1249 apply eq_symmetric_unfolded.assumption.
1255 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
1259 definition nat_less_n_fun : \forall S:CSetoid. \forall n:nat. ? \def
1260 \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i:nat. i < n \to S.
1261 \forall i,j : nat. eq nat i j \to (\forall H : i < n.
1262 \forall H' : j < n . (f i H) = (f j H')).
1264 definition nat_less_n_fun' : \forall S:CSetoid. \forall n:nat. ? \def
1265 \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i: nat. i <= n \to S.
1266 \forall i,j : nat. eq nat i j \to \forall H : i <= n.
1267 \forall H' : j <= n. f i H = f j H'.