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" 'eq x y = (cs_eq _ x y).
52 interpretation "setoid apart" 'neq x y = (cs_ap _ x y).
54 (* visto che sia "ap" che "eq" vanno in Prop e data la "tight-apartness",
55 "cs_neq" e "ap" non sono la stessa cosa? *)
56 definition cs_neq : \forall S : CSetoid. relation S \def
57 \lambda S : CSetoid. \lambda x,y : S. \not x = y.
59 lemma CSetoid_is_CSetoid :
60 \forall S : CSetoid. is_CSetoid S (cs_eq S) (cs_ap S).
61 intro. apply (cs_proof S).
64 lemma ap_irreflexive: \forall S : CSetoid. irreflexive S (cs_ap S).
65 intro. elim (CSetoid_is_CSetoid S). assumption.
68 lemma ap_symmetric : \forall S : CSetoid. symmetric S(cs_ap S).
69 intro. elim (CSetoid_is_CSetoid S). assumption.
72 lemma ap_cotransitive : \forall S : CSetoid. cotransitive S (cs_ap S).
73 intro. elim (CSetoid_is_CSetoid S). assumption.
76 lemma ap_tight : \forall S : CSetoid. tight_apart S (cs_eq S) (cs_ap S).
77 intro. elim (CSetoid_is_CSetoid S). assumption.
80 definition ex_unq : \forall S : CSetoid. (S \to Prop) \to Prop \def
81 \lambda S : CSetoid. \lambda P : S \to Prop.
82 ex2 S (\lambda x. \forall y : S. P y \to x = y) P.
85 lemma eq_reflexive : \forall S : CSetoid. reflexive S (cs_eq S).
87 generalize in match (ap_tight S x x).
89 generalize in match (ap_irreflexive S x);
90 elim H. apply H1. assumption.
93 axiom eq_symmetric : \forall S : CSetoid. symmetric S (cs_eq S).
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. autobatch.
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.
134 lemma eq_wdl : \forall S:CSetoid. \forall x,y,z:S. x = y \to x = z \to z = y.
136 (* perche' autobatch non arriva in fondo ??? *)
137 apply (eq_transitive_unfolded ? ? x).
138 apply eq_symmetric_unfolded.
144 lemma ap_irreflexive_unfolded : \forall S:CSetoid. \forall x:S. \not (x \neq x).
145 apply ap_irreflexive.
148 lemma ap_cotransitive_unfolded : \forall S:CSetoid. \forall a,b:S. a \neq b \to
149 \forall c:S. a \neq c \or c \neq b.
150 apply ap_cotransitive.
153 lemma ap_symmetric_unfolded : \forall S:CSetoid. \forall x,y:S.
154 x \neq y \to y \neq x.
158 lemma eq_imp_not_ap : \forall S:CSetoid. \forall x,y:S.
159 x = y \to \not (x \neq y).
161 elim (ap_tight S x y).
162 apply H2. assumption.
165 lemma not_ap_imp_eq : \forall S:CSetoid. \forall x,y:S.
166 \not (x \neq y) \to x = y.
168 elim (ap_tight S x y).
169 apply H1. assumption.
172 lemma neq_imp_notnot_ap : \forall S:CSetoid. \forall x,y:S.
173 (cs_neq S x y) \to \not \not (x \neq y).
174 intros. unfold. intro.
180 lemma notnot_ap_imp_neq: \forall S:CSetoid. \forall x,y:S.
181 (\not \not (x \neq y)) \to (cs_neq S x y).
182 intros. unfold. unfold. intro.
188 lemma ap_imp_neq : \forall S:CSetoid. \forall x,y:S.
189 x \neq y \to (cs_neq S x y).
190 intros. unfold. unfold. intro.
191 apply (eq_imp_not_ap S ? ? H1).
195 lemma not_neq_imp_eq : \forall S:CSetoid. \forall x,y:S.
196 \not (cs_neq S x y) \to x = y.
205 lemma eq_imp_not_neq : \forall S:CSetoid. \forall x,y:S.
206 x = y \to \not (cs_neq S x y).
207 intros. unfold. intro.
214 (* -----------------The product of setoids----------------------- *)
216 definition prod_ap: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
217 \lambda A,B : CSetoid.\lambda c,d: Prod A B.
218 ((cs_ap A (fst A B c) (fst A B d)) \or
219 (cs_ap B (snd A B c) (snd A B d))).
221 definition prod_eq: \forall A,B : CSetoid.\forall c,d: Prod A B. Prop \def
222 \lambda A,B : CSetoid.\lambda c,d: Prod A B.
223 ((cs_eq A (fst A B c) (fst A B d)) \and
224 (cs_eq B (snd A B c) (snd A B d))).
227 lemma prodcsetoid_is_CSetoid: \forall A,B: CSetoid.
228 is_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B).
230 apply (mk_is_CSetoid ? (prod_eq A B) (prod_ap A B))
235 unfold prod_ap. simplify.
238 [apply (ap_irreflexive A a H1)
239 |apply (ap_irreflexive B b H1)
245 unfold prod_ap. simplify.
248 [left. apply ap_symmetric. assumption.
249 |right. apply ap_symmetric. assumption
256 unfold prod_ap in H. simplify in H.
257 unfold prod_ap. simplify.
259 [cut ((a \neq a2) \or (a2 \neq a1))
261 [left. left. assumption
262 |right. left. assumption
264 |apply (ap_cotransitive A). assumption
266 |cut ((b \neq b2) \or (b2 \neq b1))
268 [left. right. assumption
269 |right. right. assumption
271 |apply (ap_cotransitive B). assumption.
278 unfold prod_ap. simplify.
282 [apply not_ap_imp_eq.
283 unfold. intro. apply H.
285 |apply not_ap_imp_eq.
286 unfold. intro. apply H.
289 |intro. unfold. intro.
292 [apply (eq_imp_not_ap A a a1 H2). assumption
293 |apply (eq_imp_not_ap B b b1 H3). assumption
300 definition ProdCSetoid : \forall A,B: CSetoid. CSetoid \def
301 \lambda A,B: CSetoid.
302 mk_CSetoid (Prod A B) (prod_eq A B) (prod_ap A B) (prodcsetoid_is_CSetoid A B).
306 (* Relations and predicates
307 Here we define the notions of well-definedness and strong extensionality
308 on predicates and relations.
313 (*-----------------------------------------------------------------------*)
314 (*-------------------------- Predicates on Setoids ----------------------*)
315 (*-----------------------------------------------------------------------*)
317 (* throughout this section consider (S : CSetoid) and (P : S -> Prop) *)
319 (* Definition pred_strong_ext : CProp := forall x y : S, P x -> P y or x [#] y. *)
320 definition pred_strong_ext : \forall S: CSetoid. (S \to Prop) \to Prop \def
321 \lambda S: CSetoid. \lambda P: S \to Prop. \forall x,y: S.
322 P x \to (P y \or (x \neq y)).
324 (* Definition pred_wd : CProp := forall x y : S, P x -> x [=] y -> P y. *)
325 definition pred_wd : \forall S: CSetoid. \forall P :S \to Type. Type \def
326 \lambda S: CSetoid. \lambda P: S \to Type. \forall x,y : S.
327 P x \to x = y \to P y.
329 record wd_pred (S: CSetoid) : Type \def
330 {wdp_pred :> S \to Prop;
331 wdp_well_def : pred_wd S wdp_pred}.
333 record CSetoid_predicate (S: CSetoid) : Type \def
334 {csp_pred :> S \to Prop;
335 csp_strext : pred_strong_ext S csp_pred}.
337 lemma csp_wd : \forall S: CSetoid. \forall P: CSetoid_predicate S.
338 pred_wd S (csp_pred S P).
341 simplify.unfold pred_wd.
344 [assumption|apply False_ind.apply (eq_imp_not_ap S x y H2 H3)]
348 (* Same result with CProp instead of Prop: but we just work with Prop (Matita group) *)
350 Definition pred_strong_ext' : CProp := forall x y : S, P x -> P y or x [#] y.
351 Definition pred_wd' : Prop := forall x y : S, P x -> x [=] y -> P y.
353 Record CSetoid_predicate' : Type :=
354 {csp'_pred :> S -> Prop;
355 csp'_strext : pred_strong_ext' csp'_pred}.
357 Lemma csp'_wd : forall P : CSetoid_predicate', pred_wd' P.
359 intro x; intros y H H0.
360 elim (csp'_strext P x y H).
367 exact (eq_imp_not_ap _ _ _ H0).
373 (*------------------------------------------------------------------------*)
374 (* --------------------------- Relations on Setoids --------------------- *)
375 (*------------------------------------------------------------------------*)
376 (* throughout this section consider (S : CSetoid) and (R : S -> S -> Prop) *)
379 (* Definition rel_wdr : Prop := forall x y z : S, R x y -> y [=] z -> R x z. *)
381 primo tentativo ma R non e' ben tipato: si puo' fare il cast giusto (carrier di S)
382 in modo da sfruttare "relation"?
383 e' concettualmente sbagliato lavorare ad un livello piu' alto (Type) ? *)
385 definition rel_wdr : \forall S: CSetoid. \forall x,y,z: S. \lambda R: relation S. Prop \def
386 \lambda S: CSetoid. \lambda x,y,z: S. \lambda R: relation S.
387 R S x y \to y = z \to R S x z.
389 definition rel_wdr : \forall S: CSetoid. \forall x,y,z: (cs_crr S). \lambda R: relation (cs_crr S). Prop \def
390 \lambda S: CSetoid. \lambda x,y,z: (cs_crr S). \lambda R: relation (cs_crr S).
391 R (cs_crr S) x y \to y = z \to R (cs_crr S) x z.
393 definition rel_wdr : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
394 \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
395 R x y \to y = z \to R x z.
397 (*Definition rel_wdl : Prop := forall x y z : S, R x y -> x [=] z -> R z y.*)
398 definition rel_wdl : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
399 \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y,z: S.
400 R x y \to x = z \to R z y.
402 (* Definition rel_strext : CProp := forall x1 x2 y1 y2 : S, R x1 y1 -> (x1 [#] x2 or y1 [#] y2) or R x2 y2. *)
403 definition rel_strext : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
404 \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y1,y2: S.
405 R x1 y1 \to (x1 \neq x2 \or y1 \neq y2) \or R x2 y2.
408 (* Definition rel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> x1 [#] x2 or R x2 y. *)
409 definition rel_strext_lft : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
410 \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x1,x2,y: S.
411 R x1 y \to (x1 \neq x2 \or R x2 y).
413 (* Definition rel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> y1 [#] y2 or R x y2. *)
414 definition rel_strext_rht : \forall S: CSetoid. (S \to S \to Prop) \to Prop \def
415 \lambda S: CSetoid. \lambda R: (S \to S \to Prop). \forall x,y1,y2: S.
416 R x y1 \to (y1 \neq y2 \or R x y2).
419 lemma rel_strext_imp_lftarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
420 rel_strext S R \to rel_strext_lft S R.
422 unfold rel_strext_lft.
424 elim (H x1 x2 y y H1)
427 |absurd (y \neq y) [assumption | apply (ap_irreflexive S y)]
434 lemma rel_strext_imp_rhtarg : \forall S: CSetoid. \forall R: S \to S \to Prop.
435 rel_strext S R \to rel_strext_rht S R.
437 unfold rel_strext_rht.
439 elim (H x x y1 y2 H1)
441 [absurd (x \neq x) [assumption | apply (ap_irreflexive S x)]
449 lemma rel_strextarg_imp_strext : \forall S: CSetoid. \forall R: S \to S \to Prop.
450 (rel_strext_rht S R) \to (rel_strext_lft S R) \to (rel_strext S R).
451 unfold rel_strext_rht.
452 unfold rel_strext_lft.
455 elim ((H x1 y1 y2) H2)
456 [left. right. assumption
457 |elim ((H1 x1 x2 y1) H2)
458 [left. left. assumption
459 |elim ((H x2 y1 y2) H4)
460 [left. right. assumption
467 (* ---------- Definition of a setoid relation ----------------- *)
468 (* The type of relations over a setoid. *)
471 record CSetoid_relation1 (S: CSetoid) : Type \def
472 {csr_rel : S \to S \to Prop;
473 csr_wdr : rel_wdr S csr_rel;
474 csr_wdl : rel_wdl S csr_rel;
475 csr_strext : rel_strext S csr_rel}.
478 Record CSetoid_relation : Type :=
479 {csr_rel :> S -> S -> Prop;
480 csr_wdr : rel_wdr csr_rel;
481 csr_wdl : rel_wdl csr_rel;
482 csr_strext : rel_strext csr_rel}.
486 (* ---------- gli stessi risultati di prima ma in CProp ---------*)
488 Variable R : S -> S -> CProp.
489 Definition Crel_wdr : CProp := forall x y z : S, R x y -> y [=] z -> R x z.
490 Definition Crel_wdl : CProp := forall x y z : S, R x y -> x [=] z -> R z y.
491 Definition Crel_strext : CProp := forall x1 x2 y1 y2 : S,
492 R x1 y1 -> R x2 y2 or x1 [#] x2 or y1 [#] y2.
494 Definition Crel_strext_lft : CProp := forall x1 x2 y : S, R x1 y -> R x2 y or x1 [#] x2.
495 Definition Crel_strext_rht : CProp := forall x y1 y2 : S, R x y1 -> R x y2 or y1 [#] y2.
497 Lemma Crel_strext_imp_lftarg : Crel_strext -> Crel_strext_lft.
499 unfold Crel_strext, Crel_strext_lft in |- *; intros H x1 x2 y H0.
500 generalize (H x1 x2 y y).
510 elim (ap_irreflexive _ _ H4).
513 Lemma Crel_strext_imp_rhtarg : Crel_strext -> Crel_strext_rht.
514 unfold Crel_strext, Crel_strext_rht in |- *; intros H x y1 y2 H0.
515 generalize (H x x y1 y2 H0); intro H1.
522 elim (ap_irreflexive _ _ H3).
527 Lemma Crel_strextarg_imp_strext :
528 Crel_strext_rht -> Crel_strext_lft -> Crel_strext.
529 unfold Crel_strext, Crel_strext_lft, Crel_strext_rht in |- *;
530 intros H H0 x1 x2 y1 y2 H1.
531 elim (H x1 y1 y2 H1); autobatch.
533 elim (H0 x1 x2 y2 H2); autobatch.
540 (* ---- e questo ??????? -----*)
542 (*Definition of a [CProp] setoid relation
543 The type of relations over a setoid. *)
545 Record CCSetoid_relation : Type :=
546 {Ccsr_rel :> S -> S -> CProp;
547 Ccsr_strext : Crel_strext Ccsr_rel}.
549 Lemma Ccsr_wdr : forall R : CCSetoid_relation, Crel_wdr R.
551 red in |- *; intros x y z H H0.
552 elim (Ccsr_strext R x x y z H).
556 intro H1; elimtype False.
559 exact (ap_irreflexive_unfolded _ _ H2).
562 exact (eq_imp_not_ap _ _ _ H0).
565 Lemma Ccsr_wdl : forall R : CCSetoid_relation, Crel_wdl R.
567 red in |- *; intros x y z H H0.
568 elim (Ccsr_strext R x z y y H).
572 intro H1; elimtype False.
576 exact (eq_imp_not_ap _ _ _ H0).
578 exact (ap_irreflexive_unfolded _ _ H2).
581 Lemma ap_wdr : Crel_wdr (cs_ap (c:=S)).
582 red in |- *; intros x y z H H0.
583 generalize (eq_imp_not_ap _ _ _ H0); intro H1.
584 elim (ap_cotransitive_unfolded _ _ _ H z); intro H2.
589 apply ap_symmetric_unfolded.
593 Lemma ap_wdl : Crel_wdl (cs_ap (c:=S)).
594 red in |- *; intros x y z H H0.
595 generalize (ap_wdr y x z); intro H1.
596 apply ap_symmetric_unfolded.
599 apply ap_symmetric_unfolded.
605 Lemma ap_wdr_unfolded : forall x y z : S, x [#] y -> y [=] z -> x [#] z.
608 Lemma ap_wdl_unfolded : forall x y z : S, x [#] y -> x [=] z -> z [#] y.
611 Lemma ap_strext : Crel_strext (cs_ap (c:=S)).
612 red in |- *; intros x1 x2 y1 y2 H.
613 case (ap_cotransitive_unfolded _ _ _ H x2); intro H0.
617 case (ap_cotransitive_unfolded _ _ _ H0 y2); intro H1.
622 apply ap_symmetric_unfolded.
626 Definition predS_well_def (P : S -> CProp) : CProp := forall x y : S,
627 P x -> x [=] y -> P y.
629 End CSetoid_relations_and_predicates.
631 Declare Left Step ap_wdl_unfolded.
632 Declare Right Step ap_wdr_unfolded.
643 (*------------------------------------------------------------------------*)
644 (* ------------------------- Functions between setoids ------------------ *)
645 (*------------------------------------------------------------------------*)
647 (* Such functions must preserve the setoid equality
648 and be strongly extensional w.r.t. the apartness, i.e.
649 if f(x,y) # f(x1,y1), then x # x1 or y # y1.
650 For every arity this has to be defined separately. *)
652 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2) *)
654 (* First we consider unary functions. *)
657 In the following two definitions,
658 f is a function from (the carrier of) S1 to (the carrier of) S2 *)
660 (* Nota: senza le parentesi di (S1 \to S2) non funziona, perche'? *)
661 definition fun_wd : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
662 \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
665 definition fun_strext : \forall S1,S2 : CSetoid. (S1 \to S2) \to Prop \def
666 \lambda S1,S2 : CSetoid.\lambda f : S1 \to S2. \forall x,y : S1.
667 (f x \neq f y) \to (x \neq y).
669 lemma fun_strext_imp_wd : \forall S1,S2 : CSetoid. \forall f : S1 \to S2.
670 fun_strext S1 S2 f \to fun_wd S1 S2 f.
676 apply (eq_imp_not_ap ? ? ? H1).
680 (* funzioni tra setoidi *)
681 record CSetoid_fun (S1,S2 : CSetoid) : Type \def
682 {csf_fun : S1 \to S2;
683 csf_strext : (fun_strext S1 S2 csf_fun)}.
685 lemma csf_wd : \forall S1,S2 : CSetoid. \forall f : CSetoid_fun S1 S2. fun_wd S1 S2 (csf_fun S1 S2 f).
687 apply fun_strext_imp_wd.
691 definition Const_CSetoid_fun : \forall S1,S2: CSetoid. S2 \to CSetoid_fun S1 S2.
692 intros. apply (mk_CSetoid_fun S1 S2 (\lambda x:S1.c)).
694 elim (ap_irreflexive ? ? H).
698 (* ---- Binary functions ------*)
699 (* throughout this section consider (S1,S2,S3 : CSetoid) and (f : S1 \to S2 \to S3) *)
701 definition bin_fun_wd : \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
702 \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
703 x1 = x2 \to y1 = y2 \to f x1 y1 = f x2 y2.
706 Definition bin_fun_strext : CProp := forall x1 x2 y1 y2,
707 f x1 y1 [#] f x2 y2 -> x1 [#] x2 or y1 [#] y2.
710 definition bin_fun_strext: \forall S1,S2,S3 : CSetoid. (S1 \to S2 \to S3) \to Prop \def
711 \lambda S1,S2,S3 : CSetoid. \lambda f : S1 \to S2 \to S3. \forall x1,x2: S1. \forall y1,y2: S2.
712 f x1 y1 \neq f x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
714 lemma bin_fun_strext_imp_wd : \forall S1,S2,S3: CSetoid.\forall f:S1 \to S2 \to S3.
715 bin_fun_strext ? ? ? f \to bin_fun_wd ? ? ? f.
718 apply not_ap_imp_eq.unfold.intro.
719 elim (H x1 x2 y1 y2 H3).
720 apply (eq_imp_not_ap ? ? ? H1 H4).
721 apply (eq_imp_not_ap ? ? ? H2 H4).
726 record CSetoid_bin_fun (S1,S2,S3: CSetoid) : Type \def
727 {csbf_fun :2> S1 \to S2 \to S3;
728 csbf_strext : (bin_fun_strext S1 S2 S3 csbf_fun)}.
730 lemma csbf_wd : \forall S1,S2,S3: CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3.
731 bin_fun_wd S1 S2 S3 (csbf_fun S1 S2 S3 f).
733 apply bin_fun_strext_imp_wd.
737 lemma csf_wd_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,x' : S1.
738 x = x' \to (csf_fun S1 S2 f) x = (csf_fun S1 S2 f) x'.
740 apply (csf_wd S1 S2 f x x').
744 lemma csf_strext_unfolded : \forall S1,S2: CSetoid. \forall f : CSetoid_fun S1 S2. \forall x,y : S1.
745 (csf_fun S1 S2 f) x \neq (csf_fun S1 S2 f) y \to x \neq y.
747 apply (csf_strext S1 S2 f x y).
751 lemma csbf_wd_unfolded : \forall S1,S2,S3 : CSetoid. \forall f : CSetoid_bin_fun S1 S2 S3. \forall x,x':S1.
752 \forall y,y' : S2. x = x' \to y = y' \to (csbf_fun S1 S2 S3 f) x y = (csbf_fun S1 S2 S3 f) x' y'.
754 apply (csbf_wd S1 S2 S3 f x x' y y'); assumption.
757 (* Hint Resolve csf_wd_unfolded csbf_wd_unfolded: algebra_c.*)
759 (* The unary and binary (inner) operations on a csetoid
760 An operation is a function with domain(s) and co-domain equal. *)
762 (* Properties of binary operations *)
764 definition commutes : \forall S: CSetoid. (S \to S \to S) \to Prop \def
765 \lambda S: CSetoid. \lambda f : S \to S \to S.
766 \forall x,y : S. f x y = f y x.
768 definition CSassociative : \forall S: CSetoid. \forall f: S \to S \to S. Prop \def
769 \lambda S: CSetoid. \lambda f : S \to S \to S.
771 f x (f y z) = f (f x y) z.
773 definition un_op_wd : \forall S:CSetoid. (S \to S) \to Prop \def
774 \lambda S: CSetoid. \lambda f: (S \to S). fun_wd S S f.
777 definition un_op_strext: \forall S:CSetoid. (S \to S) \to Prop \def
778 \lambda S:CSetoid. \lambda f: (S \to S). fun_strext S S f.
781 definition CSetoid_un_op : CSetoid \to Type \def
782 \lambda S:CSetoid. CSetoid_fun S S.
784 definition mk_CSetoid_un_op : \forall S:CSetoid. \forall f: S \to S. fun_strext S S f \to CSetoid_fun S S
786 \lambda S:CSetoid. \lambda f: S \to S. mk_CSetoid_fun S S f.
788 lemma id_strext : \forall S:CSetoid. un_op_strext S (\lambda x:S. x).
796 lemma id_pres_eq : \forall S:CSetoid. un_op_wd S (\lambda x : S.x).
804 definition id_un_op : \forall S:CSetoid. CSetoid_un_op S
805 \def \lambda S: CSetoid. mk_CSetoid_un_op S (\lambda x : cs_crr S.x) (id_strext S).
807 definition un_op_fun: \forall S:CSetoid. CSetoid_un_op S \to CSetoid_fun S S
808 \def \lambda S.\lambda f.f.
810 coercion cic:/matita/algebra/CoRN/Setoids/un_op_fun.con.
812 definition cs_un_op_strext : \forall S:CSetoid. \forall f: CSetoid_fun S S. fun_strext S S (csf_fun S S f) \def
813 \lambda S:CSetoid. \lambda f : CSetoid_fun S S. csf_strext S S f.
815 lemma un_op_wd_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
817 x = y \to (csf_fun S S op) x = (csf_fun S S op) y.
819 apply (csf_wd S S ?).assumption.
822 lemma un_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_un_op S.
824 (csf_fun S S op) x \neq (csf_fun S S op) y \to x \neq y.
825 exact cs_un_op_strext.
829 (* Well-defined binary operations on a setoid. *)
831 definition bin_op_wd : \forall S:CSetoid. (S \to S \to S) \to Prop \def
832 \lambda S:CSetoid. bin_fun_wd S S S.
834 definition bin_op_strext : \forall S:CSetoid. (S \to S \to S) \to Prop \def
835 \lambda S:CSetoid. bin_fun_strext S S S.
837 definition CSetoid_bin_op : CSetoid \to Type \def
838 \lambda S:CSetoid. CSetoid_bin_fun S S S.
841 definition mk_CSetoid_bin_op : \forall S:CSetoid. \forall f: S \to S \to S.
842 bin_fun_strext S S S f \to CSetoid_bin_fun S S S \def
843 \lambda S:CSetoid. \lambda f: S \to S \to S.
844 mk_CSetoid_bin_fun S S S f.
846 (* da controllare che sia ben tipata
847 definition cs_bin_op_wd : \forall S:CSetoid. ? \def
848 \lambda S:CSetoid. csbf_wd S S S.
850 definition cs_bin_op_wd : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_wd S S S (csbf_fun S S S f) \def
851 \lambda S:CSetoid. csbf_wd S S S.
853 definition cs_bin_op_strext : \forall S:CSetoid. \forall f: CSetoid_bin_fun S S S. bin_fun_strext S S S (csbf_fun S S S f) \def
854 \lambda S:CSetoid. csbf_strext S S S.
858 (* Identity Coercion bin_op_bin_fun : CSetoid_bin_op >-> CSetoid_bin_fun. *)
860 definition bin_op_bin_fun: \forall S:CSetoid. CSetoid_bin_op S \to CSetoid_bin_fun S S S
861 \def \lambda S.\lambda f.f.
863 coercion cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con.
868 lemma bin_op_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
869 x1 = x2 \to y1 = y2 \to (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
873 lemma bin_op_strext_unfolded : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall x1, x2, y1, y2 : S.
874 (csbf_fun S S S op) x1 y1 \neq (csbf_fun S S S op) x2 y2 \to x1 \neq x2 \lor y1 \neq y2.
875 exact cs_bin_op_strext.
878 lemma bin_op_is_wd_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
879 un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
880 intros. unfold. unfold.
881 intros. apply bin_op_wd_unfolded [ assumption | apply eq_reflexive_unfolded ]
884 lemma bin_op_is_wd_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
885 un_op_wd S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
886 intros. unfold. unfold.
887 intros. apply bin_op_wd_unfolded [ apply eq_reflexive_unfolded | assumption ]
891 lemma bin_op_is_strext_un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
892 un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) x c)).
893 intros. unfold un_op_strext. unfold fun_strext.
895 cut (x \neq y \lor c \neq c)
898 | generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
900 | apply (bin_op_strext_unfolded S op x y c c). assumption.
904 lemma bin_op_is_strext_un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S. \forall c : cs_crr S.
905 un_op_strext S (\lambda x : cs_crr S. ((csbf_fun S S S op) c x)).
906 intros. unfold un_op_strext. unfold fun_strext.
908 cut (c \neq c \lor x \neq y)
910 [ generalize in match (ap_irreflexive_unfolded ? ? H1). intro. elim H2
913 | apply (bin_op_strext_unfolded S op c c x y). assumption.
917 definition bin_op2un_op_rht : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
918 \forall c : cs_crr S. CSetoid_un_op S \def
919 \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
920 mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) c x))
921 (bin_op_is_strext_un_op_rht S op c).
923 definition bin_op2un_op_lft : \forall S:CSetoid. \forall op : CSetoid_bin_op S.
924 \forall c : cs_crr S. CSetoid_un_op S \def
925 \lambda S:CSetoid. \lambda op: CSetoid_bin_op S. \lambda c : cs_crr S.
926 mk_CSetoid_un_op S (\lambda x:cs_crr S. ((csbf_fun S S S op) x c))
927 (bin_op_is_strext_un_op_lft S op c).
930 Definition bin_op2un_op_rht (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
931 Build_CSetoid_un_op (fun x : S => op c x) (bin_op_is_strext_un_op_rht op c).
934 Definition bin_op2un_op_lft (op : CSetoid_bin_op) (c : S) : CSetoid_un_op :=
935 Build_CSetoid_un_op (fun x : S => op x c) (bin_op_is_strext_un_op_lft op c).
940 Implicit Arguments commutes [S].
941 Implicit Arguments associative [S].
942 Hint Resolve bin_op_wd_unfolded un_op_wd_unfolded: algebra_c.
945 (*The binary outer operations on a csetoid*)
949 Well-defined outer operations on a setoid.
951 definition outer_op_well_def : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
952 \lambda S1,S2:CSetoid. bin_fun_wd S1 S2 S2.
954 definition outer_op_strext : \forall S1,S2:CSetoid. (S1 \to S2 \to S2) \to Prop \def
955 \lambda S1,S2:CSetoid. bin_fun_strext S1 S2 S2.
957 definition CSetoid_outer_op : \forall S1,S2:CSetoid.Type \def
958 \lambda S1,S2:CSetoid.
959 CSetoid_bin_fun S1 S2 S2.
961 definition mk_CSetoid_outer_op : \forall S1,S2:CSetoid.
962 \forall f : S1 \to S2 \to S2.
963 bin_fun_strext S1 S2 S2 f \to CSetoid_bin_fun S1 S2 S2 \def
964 \lambda S1,S2:CSetoid.
965 mk_CSetoid_bin_fun S1 S2 S2.
967 definition csoo_wd : \forall S1,S2:CSetoid. \forall f : CSetoid_bin_fun S1 S2 S2.
968 bin_fun_wd S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
969 \lambda S1,S2:CSetoid.
972 definition csoo_strext : \forall S1,S2:CSetoid.
973 \forall f : CSetoid_bin_fun S1 S2 S2.
974 bin_fun_strext S1 S2 S2 (csbf_fun S1 S2 S2 f) \def
975 \lambda S1,S2:CSetoid.
976 csbf_strext S1 S2 S2.
979 definition outer_op_bin_fun: \forall S:CSetoid.
980 CSetoid_outer_op S S \to CSetoid_bin_fun S S S
981 \def \lambda S.\lambda f.f.
983 coercion cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con.
985 Identity Coercion outer_op_bin_fun : CSetoid_outer_op >-> CSetoid_bin_fun.
988 lemma csoo_wd_unfolded :\forall S:CSetoid. \forall op : CSetoid_outer_op S S.
989 \forall x1, x2, y1, y2 : S.
990 x1 = x2 -> y1 = y2 -> (csbf_fun S S S op) x1 y1 = (csbf_fun S S S op) x2 y2.
992 apply csoo_wd[assumption|assumption]
996 Hint Resolve csoo_wd_unfolded: algebra_c.
1001 (*---------------------------------------------------------------*)
1002 (*--------------------------- Subsetoids ------------------------*)
1003 (*---------------------------------------------------------------*)
1005 (* Let S be a setoid, and P a predicate on the carrier of S *)
1006 (* Variable P : S -> CProp *)
1008 record subcsetoid_crr (S: CSetoid) (P: S \to Prop) : Type \def
1010 scs_prf : P scs_elem}.
1012 definition restrict_relation : \forall S:CSetoid. \forall R : S \to S \to Prop.
1013 \forall P: S \to Prop. relation (subcsetoid_crr S P) \def
1014 \lambda S:CSetoid. \lambda R : S \to S \to Prop.
1015 \lambda P: S \to Prop. \lambda a,b: subcsetoid_crr S P.
1017 [ (mk_subcsetoid_crr x H) \Rightarrow
1019 [ (mk_subcsetoid_crr y H) \Rightarrow R x y ]
1022 definition Crestrict_relation (R : Crelation S) : Crelation subcsetoid_crr :=
1023 fun a b : subcsetoid_crr =>
1025 | Build_subcsetoid_crr x _, Build_subcsetoid_crr y _ => R x y
1029 definition subcsetoid_eq : \forall S:CSetoid. \forall P: S \to Prop.
1030 relation (subcsetoid_crr S P)\def
1032 restrict_relation S (cs_eq S).
1034 definition subcsetoid_ap : \forall S:CSetoid. \forall P: S \to Prop.
1035 relation (subcsetoid_crr S P)\def
1037 restrict_relation S (cs_ap S).
1039 (* N.B. da spostare in relations.ma... *)
1040 definition equiv : \forall A: Type. \forall R: relation A. Prop \def
1041 \lambda A: Type. \lambda R: relation A.
1042 (reflexive A R) \land (transitive A R) \land (symmetric A R).
1044 remark subcsetoid_equiv : \forall S:CSetoid. \forall P: S \to Prop.
1045 equiv ? (subcsetoid_eq S P).
1046 intros. unfold equiv. split
1048 [unfold. intro. elim x. simplify. apply (eq_reflexive S)
1049 |unfold. intros 3. elim y 2.
1050 elim x 2. elim z 2. simplify.
1051 exact (eq_transitive ? c1 c c2)
1053 | unfold. intros 2. elim x 2. elim y 2. simplify. exact (eq_symmetric ? c c1).
1058 axiom subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
1059 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
1062 lemma subcsetoid_is_CSetoid : \forall S:CSetoid. \forall P: S \to Prop.
1063 is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P).
1065 apply (mk_is_CSetoid ? (subcsetoid_eq S P) (subcsetoid_ap S P))
1066 [ unfold. intros.unfold. elim x. exact (ap_irreflexive_unfolded S ? ?)
1067 [ assumption | simplify in H1. exact H1 ]
1069 |unfold. intros 2. elim x. generalize in match H1. elim y.simplify in H3. simplify.
1070 exact (ap_symmetric ? ? ? H3)
1072 |unfold.intros 2. elim x.generalize in match H1. elim y. elim z.simplify. simplify in H3.
1073 apply (ap_cotransitive ? ? ? H3)
1075 |unfold.intros.elim x. elim y.simplify.
1076 apply (ap_tight S ? ?)]
1080 definition mk_SubCSetoid : \forall S:CSetoid. \forall P: S \to Prop. CSetoid \def
1081 \lambda S:CSetoid. \lambda P:S \to Prop.
1082 mk_CSetoid (subcsetoid_crr S P) (subcsetoid_eq S P) (subcsetoid_ap S P) (subcsetoid_is_CSetoid S P).
1084 (* Subsetoid unary operations
1085 %\begin{convention}%
1086 Let [f] be a unary setoid operation on [S].
1090 (* Section SubCSetoid_unary_operations.
1091 Variable f : CSetoid_un_op S.
1094 definition un_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
1095 CSetoid_un_op S \to Prop \def
1096 \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
1097 \forall x : cs_crr S. P x \to P ((csf_fun S S f) x).
1099 definition restr_un_op : \forall S:CSetoid. \forall P: S \to Prop.
1100 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
1101 subcsetoid_crr S P \to subcsetoid_crr S P \def
1102 \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
1103 \lambda pr : un_op_pres_pred S P f.\lambda a: subcsetoid_crr S P.
1105 [ (mk_subcsetoid_crr x p) \Rightarrow
1106 (mk_subcsetoid_crr ? ? ((csf_fun S S f) x) (pr x p))].
1109 lemma restr_un_op_wd : \forall S:CSetoid. \forall P: S \to Prop.
1110 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
1111 un_op_wd (mk_SubCSetoid S P) (restr_un_op S P f pr).
1113 unfold.unfold.intros 2.elim x 2.elim y 2.
1117 apply (un_op_wd_unfolded ? f ? ? H2).
1120 lemma restr_un_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
1121 \forall f: CSetoid_un_op S. \forall pr: un_op_pres_pred S P f.
1122 un_op_strext (mk_SubCSetoid S P) (restr_un_op S P f pr).
1123 intros.unfold.unfold. intros 2.elim y 2. elim x 2.
1124 intros.normalize in H2.
1125 apply (cs_un_op_strext ? f ? ? H2).
1128 definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
1129 \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P).
1131 apply (mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr)).
1134 (* BUG Universe Inconsistency detected
1135 definition mk_SubCSetoid_un_op : \forall S:CSetoid. \forall P: S \to Prop. \forall f: CSetoid_un_op S.
1136 \forall pr:un_op_pres_pred S P f. CSetoid_un_op (mk_SubCSetoid S P) \def
1137 \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_un_op S.
1138 \lambda pr:un_op_pres_pred S P f.
1139 mk_CSetoid_un_op (mk_SubCSetoid S P) (restr_un_op S P f pr) (restr_un_op_strext S P f pr).
1142 (* Subsetoid binary operations
1143 Let [f] be a binary setoid operation on [S].
1146 (* Section SubCSetoid_binary_operations.
1147 Variable f : CSetoid_bin_op S.
1150 definition bin_op_pres_pred : \forall S:CSetoid. \forall P: S \to Prop.
1151 (CSetoid_bin_op S) \to Prop \def
1152 \lambda S:CSetoid. \lambda P: S \to Prop. \lambda f: CSetoid_bin_op S.
1153 \forall x,y : S. P x \to P y \to P ( (csbf_fun S S S f) x y).
1156 Assume [bin_op_pres_pred].
1159 (* Variable pr : bin_op_pres_pred. *)
1161 definition restr_bin_op : \forall S:CSetoid. \forall P:S \to Prop.
1162 \forall f: CSetoid_bin_op S.\forall op : (bin_op_pres_pred S P f).
1163 \forall a, b : subcsetoid_crr S P. subcsetoid_crr S P \def
1164 \lambda S:CSetoid. \lambda P:S \to Prop.
1165 \lambda f: CSetoid_bin_op S. \lambda pr : (bin_op_pres_pred S P f).
1166 \lambda a, b : subcsetoid_crr S P.
1168 [ (mk_subcsetoid_crr x p) \Rightarrow
1170 [ (mk_subcsetoid_crr y q) \Rightarrow
1171 (mk_subcsetoid_crr ? ? ((csbf_fun S S S f) x y) (pr x y p q))]
1176 lemma restr_bin_op_well_def : \forall S:CSetoid. \forall P: S \to Prop.
1177 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1178 bin_op_wd (mk_SubCSetoid S P) (restr_bin_op S P f pr).
1180 unfold.unfold.intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
1185 apply (cs_bin_op_wd ? f ? ? ? ? H4 H5).
1188 lemma restr_bin_op_strext : \forall S:CSetoid. \forall P: S \to Prop.
1189 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1190 bin_op_strext (mk_SubCSetoid S P) (restr_bin_op S P f pr).
1191 intros.unfold.unfold. intros 2.elim x1 2. elim x2 2.intros 2. elim y1 2. elim y2 2.
1194 apply (cs_bin_op_strext ? f ? ? ? ? H4).
1197 definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
1198 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1199 CSetoid_bin_op (mk_SubCSetoid S P).
1201 apply (mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr)).
1204 (* BUG Universe Inconsistency detected
1205 definition mk_SubCSetoid_bin_op : \forall S:CSetoid. \forall P: S \to Prop.
1206 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1207 CSetoid_bin_op (mk_SubCSetoid S P) \def
1208 \lambda S:CSetoid. \lambda P: S \to Prop.
1209 \lambda f: CSetoid_bin_op S. \lambda pr: bin_op_pres_pred S P f.
1210 mk_CSetoid_bin_op (mk_SubCSetoid S P) (restr_bin_op S P f pr)(restr_bin_op_strext S P f pr).
1213 lemma restr_f_assoc : \forall S:CSetoid. \forall P: S \to Prop.
1214 \forall f: CSetoid_bin_op S. \forall pr: bin_op_pres_pred S P f.
1215 CSassociative S (csbf_fun S S S f)
1216 \to CSassociative (mk_SubCSetoid S P) (csbf_fun (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid S P) (mk_SubCSetoid_bin_op S P f pr)).
1221 elim z 2.elim y 2. elim x 2.
1226 definition caseZ_diff: \forall A:Type.Z \to (nat \to nat \to A) \to A \def
1227 \lambda A:Type.\lambda z:Z.\lambda f:nat \to nat \to A.
1229 [OZ \Rightarrow f O O
1230 |(pos n) \Rightarrow f (S n) O
1231 |(neg n) \Rightarrow f O (S n)].
1234 theorem Zminus_S_S : \forall n,m:nat.
1235 Z_of_nat (S n) - S m = Z_of_nat n - m.
1237 elim n.elim m.simplify. reflexivity.reflexivity.
1238 elim m.simplify.reflexivity.reflexivity.
1243 lemma proper_caseZ_diff_CS : \forall CS : CSetoid. \forall f : nat \to nat \to CS.
1244 (\forall m,n,p,q : nat. eq nat (plus m q) (plus n p) \to (f m n) = (f p q)) \to
1245 \forall m,n : nat. caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = (f m n).
1247 (* perche' apply nat_elim2 non funziona?? *)
1248 apply (nat_elim2 (\lambda m,n.caseZ_diff CS (Zminus (Z_of_nat m) (Z_of_nat n)) f = f m n)).
1250 apply (nat_case n1).simplify.
1252 intro.simplify.apply eq_reflexive.
1253 intro.simplify.apply eq_reflexive.
1255 rewrite > (Zminus_S_S n1 m1).
1257 cut (f n1 m1 = f (S n1) (S m1)).
1258 apply eq_symmetric_unfolded.
1259 apply eq_transitive.
1260 apply f. apply n1. apply m1.
1261 apply eq_symmetric_unfolded.assumption.
1262 apply eq_symmetric_unfolded.assumption.
1268 Finally, we characterize functions defined on the natural numbers also as setoid functions, similarly to what we already did for predicates.
1272 definition nat_less_n_fun : \forall S:CSetoid. \forall n:nat. ? \def
1273 \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i:nat. i < n \to S.
1274 \forall i,j : nat. eq nat i j \to (\forall H : i < n.
1275 \forall H' : j < n . (f i H) = (f j H')).
1277 definition nat_less_n_fun' : \forall S:CSetoid. \forall n:nat. ? \def
1278 \lambda S:CSetoid. \lambda n:nat. \lambda f: \forall i: nat. i <= n \to S.
1279 \forall i,j : nat. eq nat i j \to \forall H : i <= n.
1280 \forall H' : j <= n. f i H = f j H'.