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 (* $Id: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *)
17 set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun".
18 include "algebra/Setoids.ma".
21 definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
22 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
23 \exists a:A. (csf_fun A B f) a \neq (csf_fun A B g) a.
24 (* Definition ap_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
25 {a : A | f a[#]g a}. *)
27 definition eq_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def
28 \lambda A,B : CSetoid. \lambda f,g : CSetoid_fun A B.
29 \forall a:A. (csf_fun A B f) a = (csf_fun A B g) a.
30 (* Definition eq_fun (A B : CSetoid) (f g : CSetoid_fun A B) :=
31 forall a : A, f a[=]g a. *)
33 lemma irrefl_apfun : \forall A,B : CSetoid.
34 irreflexive (CSetoid_fun A B) (ap_fun A B).
36 unfold irreflexive. intro f.
41 cut (csf_fun A B f a = csf_fun A B f a)
42 [ apply (eq_imp_not_ap A)
44 assumption|assumption|apply eq_reflexive_unfolded|
45 apply (csf_strext_unfolded A B f).
48 |apply eq_reflexive_unfolded
53 Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
55 unfold irreflexive in |- *.
57 unfold ap_fun in |- *.
62 set (H1 := ap_irreflexive_unfolded B (f a)) in *.
68 lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B).
74 lapply (ap_cotransitive ? ? ? H1 (csf_fun A B h a)).
77 apply (ex_intro ? ? a H2).
79 apply (ex_intro ? ? a H2).
82 lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
88 [ intros. apply not_ap_imp_eq.
90 apply (ex_intro ? ? a).assumption.
91 | intros.unfold.intro.
93 apply (eq_imp_not_ap ? ? ? ? H2).
98 lemma sym_apfun : \forall A, B : CSetoid. symmetric (ap_fun A B).
103 apply (ex_intro ? ? a).
104 apply ap_symmetric_unfolded.
108 definition FS_is_CSetoid : \forall A, B : CSetoid. ? \def
109 \lambda A, B : CSetoid.
110 mk_is_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
111 (irrefl_apfun A B) (sym_apfun A B) (cotrans_apfun A B) (ta_apfun A B).
113 definition FS_as_CSetoid : \forall A, B : CSetoid. ? \def
114 \lambda A, B : CSetoid.
115 mk_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
118 (* Nullary and n-ary operations
121 definition is_nullary_operation : \forall S:CSetoid. \forall s:S. Prop \def
122 \lambda S:CSetoid. \lambda s:S. True.
125 Definition is_nullary_operation (S:CSetoid) (s:S):Prop := True.
128 let rec n_ary_operation (n:nat) (V:CSetoid) on n : CSetoid \def
131 |(S m) \Rightarrow (FS_as_CSetoid V (n_ary_operation m V))].
134 (* Section unary_function_composition. *)
136 (* Composition of Setoid functions
138 Let [S1], [S2] and [S3] be setoids, [f] a
139 setoid function from [S1] to [S2], and [g] from [S2]
140 to [S3] in the following definition of composition. *)
142 (* Variables S1 S2 S3 : CSetoid.
143 Variable f : CSetoid_fun S1 S2.
144 Variable g : CSetoid_fun S2 S3. *)
147 definition compose_CSetoid_fun : \forall S1,S2,S3 :CSetoid. \forall f: (CSetoid_fun S1 S2). \forall g: (CSetoid_fun S2 S3).
149 intros (S1 S2 S3 f g).
150 apply (mk_CSetoid_fun ? ? (\lambda x :cs_crr S1. csf_fun S2 S3 g (csf_fun S1 S2 f x))).
154 apply (csf_strext ? ? f).
155 apply (csf_strext ? ? g).
159 (* End unary_function_composition. *)
161 (* Composition as operation *)
162 definition comp : \forall A, B, C : CSetoid.
163 FS_as_CSetoid A B \to FS_as_CSetoid B C \to FS_as_CSetoid A C.
165 letin H \def (compose_CSetoid_fun A B C f g).
169 definition comp_as_bin_op : \forall A:CSetoid. CSetoid_bin_op (FS_as_CSetoid A A).
171 unfold CSetoid_bin_op.
172 apply (mk_CSetoid_bin_fun ? ? ? (comp A A A)).
173 unfold bin_fun_strext.
175 intros 4 (f1 f2 g1 g2).
177 unfold compose_CSetoid_fun.
200 letin H0 \def (ap_cotransitive A (g1 (f1 a)) (g2 (f2 a)) H (g2 (f1 a))).
219 (* Questa coercion composta non e' stata generata automaticamente *)
220 lemma mycor: ∀S. CSetoid_bin_op S → (S → S → S).
225 coercion cic:/matita/algebra/CoRN/SetoidFun/mycor.con 2.
227 (* Mettendola a mano con una beta-espansione funzionerebbe *)
228 (*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (\lambda e.mycor ? (comp_as_bin_op A) e)).*)
229 (* Questo sarebbe anche meglio: senza beta-espansione *)
230 (*lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (mycor ? (comp_as_bin_op A))).*)
231 (* QUESTO E' QUELLO ORIGINALE MA NON FUNZIONANTE *)
232 (* lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)). *)
233 lemma assoc_comp : \forall A : CSetoid. (CSassociative ? (comp_as_bin_op A)).
234 unfold associative in |- *.
235 unfold comp_as_bin_op in |- *.
238 unfold eq_fun in |- *.
243 Lemma assoc_comp : forall A : CSetoid, associative (comp_as_bin_op A).
244 unfold associative in |- *.
245 unfold comp_as_bin_op in |- *.
248 unfold eq_fun in |- *.
253 Section unary_and_binary_function_composition.
255 Definition compose_CSetoid_bin_un_fun (A B C : CSetoid)
256 (f : CSetoid_bin_fun B B C) (g : CSetoid_fun A B) : CSetoid_bin_fun A A C.
258 apply (Build_CSetoid_bin_fun A A C (fun a0 a1 : A => f (g a0) (g a1))).
259 intros x1 x2 y1 y2 H0.
260 assert (H10:= csbf_strext B B C f).
262 assert (H40 := csf_strext A B g).
264 elim (H10 (g x1) (g x2) (g y1) (g y2) H0); [left | right]; auto.
267 Definition compose_CSetoid_bin_fun A B C (f g : CSetoid_fun A B)
268 (h : CSetoid_bin_fun B B C) : CSetoid_fun A C.
270 apply (Build_CSetoid_fun A C (fun a : A => h (f a) (g a))).
272 elim (csbf_strext _ _ _ _ _ _ _ _ H); apply csf_strext.
275 Definition compose_CSetoid_un_bin_fun A B C (f : CSetoid_bin_fun B B C)
276 (g : CSetoid_fun C A) : CSetoid_bin_fun B B A.
278 apply Build_CSetoid_bin_fun with (fun x y : B0 => g (f x y)).
282 unfold bin_fun_strext in |- *.
285 unfold fun_strext in |- *.
286 intros gu gstrext fu fstrext H.
292 End unary_and_binary_function_composition.
297 Section function_projection.
299 Lemma proj_bin_fun : forall A B C (f : CSetoid_bin_fun A B C) a, fun_strext (f a).
305 intros csbf_strext0 x y H.
306 elim (csbf_strext0 _ _ _ _ H); intro H0.
307 elim (ap_irreflexive_unfolded _ _ H0).
311 Definition projected_bin_fun A B C (f : CSetoid_bin_fun A B C) (a : A) :=
312 Build_CSetoid_fun B C (f a) (proj_bin_fun A B C f a).
314 End function_projection.
318 Variable S : CSetoid.
320 Definition binproj1 (x y:S) := x.
322 Lemma binproj1_strext : bin_fun_strext _ _ _ binproj1.
326 Definition cs_binproj1 : CSetoid_bin_op S.
327 red in |- *; apply Build_CSetoid_bin_op with binproj1.
328 apply binproj1_strext.
333 (** **Combining operations
334 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
338 Section CombiningOperations.
339 Variables S1 S2 S3 : CSetoid.
342 In the following definition, we assume [f] is a setoid function from
343 [S1] to [S2], and [op] is an unary operation on [S2].
344 Then [opOnFun] is the composition [op] after [f].
346 Section CombiningUnaryOperations.
347 Variable f : CSetoid_fun S1 S2.
348 Variable op : CSetoid_un_op S2.
350 Definition opOnFun : CSetoid_fun S1 S2.
351 apply (Build_CSetoid_fun S1 S2 (fun x : S1 => op (f x))).
353 unfold fun_strext in |- *; intros x y H.
354 apply (csf_strext _ _ f x y).
355 apply (csf_strext _ _ op _ _ H).
358 End CombiningUnaryOperations.
360 End CombiningOperations.
364 (** **The Free Setoid
365 %\begin{convention}% Let [A:CSetoid].
370 Definition Astar := (list A).
372 Definition empty_word := (nil A).
374 Definition appA:= (app A).
376 Fixpoint eq_fm (m:Astar)(k:Astar){struct m}:Prop:=
382 |cons b n => match k with
384 |cons a l => b[=]a /\ (eq_fm n l)
388 Fixpoint ap_fm (m:Astar)(k:Astar){struct m}: CProp :=
394 |cons b n => match k with
396 |cons a l => b[#]a or (ap_fm n l)
400 Lemma ap_fm_irreflexive: (irreflexive ap_fm).
414 generalize (ap_irreflexive A a).
422 Lemma ap_fm_symmetric: Csymmetric ap_fm.
442 generalize (ap_symmetric A a c).
451 Lemma ap_fm_cotransitive : (cotransitive ap_fm).
486 generalize (ap_cotransitive A a c H c0).
491 generalize (IHx l H l0).
495 Lemma ap_fm_tight : (tight_apart eq_fm ap_fm).
523 generalize (ap_tight A a c).
538 generalize (ap_tight A a c).
545 Definition free_csetoid_is_CSetoid:(is_CSetoid Astar eq_fm ap_fm):=
546 (Build_is_CSetoid Astar eq_fm ap_fm ap_fm_irreflexive ap_fm_symmetric
547 ap_fm_cotransitive ap_fm_tight).
549 Definition free_csetoid_as_csetoid:CSetoid:=
550 (Build_CSetoid Astar eq_fm ap_fm free_csetoid_is_CSetoid).
553 (bin_fun_strext free_csetoid_as_csetoid free_csetoid_as_csetoid
554 free_csetoid_as_csetoid appA).
555 unfold bin_fun_strext.
584 generalize (IHx1 l y1 (nil A)).
593 generalize (IHx1 l0 y1 (cons c l)).
597 Definition app_as_csb_fun:
598 (CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
599 free_csetoid_as_csetoid):=
600 (Build_CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
601 free_csetoid_as_csetoid appA app_strext).
603 Lemma eq_fm_reflexive: forall (x:Astar), (eq_fm x x).
615 (** **Partial Functions
617 In this section we define a concept of partial function for an
618 arbitrary setoid. Essentially, a partial function is what would be
619 expected---a predicate on the setoid in question and a total function
620 from the set of points satisfying that predicate to the setoid. There
621 is one important limitations to this approach: first, the record we
622 obtain has type [Type], meaning that we can't use, for instance,
623 elimination of existential quantifiers.
625 Furthermore, for reasons we will explain ahead, partial functions will
626 not be defined via the [CSetoid_fun] record, but the whole structure
627 will be incorporated in a new record.
629 Finally, notice that to be completely general the domains of the
630 functions have to be characterized by a [CProp]-valued predicate;
631 otherwise, the use you can make of a function will be %\emph{%#<i>#a
632 priori#</i>#%}% restricted at the moment it is defined.
634 Before we state our definitions we need to do some work on domains.
637 Section SubSets_of_G.
639 (** ***Subsets of Setoids
641 Subsets of a setoid will be identified with predicates from the
642 carrier set of the setoid into [CProp]. At this stage, we do not make
643 any assumptions about these predicates.
645 We will begin by defining elementary operations on predicates, along
646 with their basic properties. In particular, we will work with well
647 defined predicates, so we will prove that these operations preserve
650 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
654 Variable S : CSetoid.
658 Variables P Q : S -> CProp.
660 Definition conjP (x : S) : CProp := P x and Q x.
662 Lemma prj1 : forall x : S, conjP x -> P x.
663 intros x H; inversion_clear H; assumption.
666 Lemma prj2 : forall x : S, conjP x -> Q x.
667 intros x H; inversion_clear H; assumption.
670 Lemma conj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ conjP.
672 red in |- *; intros x y H1 H2.
673 inversion_clear H1; split.
675 apply H with x; assumption.
677 apply H0 with x; assumption.
684 Variables P Q : S -> CProp.
687 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
690 Definition disj (x : S) : CProp := P x or Q x.
692 Lemma inj1 : forall x : S, P x -> disj x.
693 intros; left; assumption.
696 Lemma inj2 : forall x : S, Q x -> disj x.
697 intros; right; assumption.
700 Lemma disj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ disj.
702 red in |- *; intros x y H1 H2.
705 left; apply H with x; assumption.
707 right; apply H0 with x; assumption.
715 The next definition is a bit tricky, and is useful for choosing among the elements that satisfy a predicate [P] those that also satisfy [R] in the case where [R] is only defined for elements satisfying [P]---consider [R] to be a condition on the image of an object via a function with domain [P]. We chose to call this operation [extension].
718 Variable P : S -> CProp.
719 Variable R : forall x : S, P x -> CProp.
721 Definition extend (x : S) : CProp := P x and (forall H : P x, R x H).
723 Lemma ext1 : forall x : S, extend x -> P x.
724 intros x H; inversion_clear H; assumption.
727 Lemma ext2_a : forall x : S, extend x -> {H : P x | R x H}.
728 intros x H; inversion_clear H.
732 Lemma ext2 : forall (x : S) (Hx : extend x), R x (ProjT1 (ext2_a x Hx)).
733 intros; apply projT2.
736 Lemma extension_wd : pred_wd _ P ->
737 (forall (x y : S) Hx Hy, x [=] y -> R x Hx -> R y Hy) -> pred_wd _ extend.
739 red in |- *; intros x y H1 H2.
740 elim H1; intros H3 H4; split.
742 apply H with x; assumption.
744 intro H5; apply H0 with x H3; [ apply H2 | apply H4 ].
751 Notation Conj := (conjP _).
752 Implicit Arguments disj [S].
754 Implicit Arguments extend [S].
755 Implicit Arguments ext1 [S P R x].
756 Implicit Arguments ext2 [S P R x].
760 We are now ready to define the concept of partial function between arbitrary setoids.
763 Record BinPartFunct (S1 S2 : CSetoid) : Type :=
764 {bpfdom : S1 -> CProp;
765 bdom_wd : pred_wd S1 bpfdom;
766 bpfpfun :> forall x : S1, bpfdom x -> S2;
767 bpfstrx : forall x y Hx Hy, bpfpfun x Hx [#] bpfpfun y Hy -> x [#] y}.
770 Notation BDom := (bpfdom _ _).
771 Implicit Arguments bpfpfun [S1 S2].
774 The next lemma states that every partial function is well defined.
777 Lemma bpfwdef : forall S1 S2 (F : BinPartFunct S1 S2) x y Hx Hy,
778 x [=] y -> F x Hx [=] F y Hy.
780 apply not_ap_imp_eq; intro H0.
781 generalize (bpfstrx _ _ _ _ _ _ _ H0).
782 exact (eq_imp_not_ap _ _ _ H).
785 (** Similar for automorphisms. *)
787 Record PartFunct (S : CSetoid) : Type :=
789 dom_wd : pred_wd S pfdom;
790 pfpfun :> forall x : S, pfdom x -> S;
791 pfstrx : forall x y Hx Hy, pfpfun x Hx [#] pfpfun y Hy -> x [#] y}.
793 Notation Dom := (pfdom _).
794 Notation Part := (pfpfun _).
795 Implicit Arguments pfpfun [S].
798 The next lemma states that every partial function is well defined.
801 Lemma pfwdef : forall S (F : PartFunct S) x y Hx Hy, x [=] y -> F x Hx [=] F y Hy.
803 apply not_ap_imp_eq; intro H0.
804 generalize (pfstrx _ _ _ _ _ _ H0).
805 exact (eq_imp_not_ap _ _ _ H).
809 A few characteristics of this definition should be explained:
810 - The domain of the partial function is characterized by a predicate
811 that is required to be well defined but not strongly extensional. The
812 motivation for this choice comes from two facts: first, one very
813 important subset of real numbers is the compact interval
814 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
815 [<=] b], which is not strongly extensional; on the other hand, if we
816 can apply a function to an element [s] of a setoid [S] it seems
817 reasonable (and at some point we do have to do it) to apply that same
818 function to any element [s'] which is equal to [s] from the point of
819 view of the setoid equality.
820 - The last two conditions state that [pfpfun] is really a subsetoid
821 function. The reason why we do not write it that way is the
822 following: when applying a partial function [f] to an element [s] of
823 [S] we also need a proof object [H]; with this definition the object
824 we get is [f(s,H)], where the proof is kept separate from the object.
825 Using subsetoid notation, we would get $f(\langle
826 s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two
827 projections to get either the original object or the proof, and we
828 need to apply an extra constructor to get $f(\langle
829 s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts
830 to spending more resources when actually working with these objects.
831 - This record has type [Type], which is very unfortunate, because it
832 means in particular that we cannot use the well behaved set
833 existential quantification over partial functions; however, later on
834 we will manage to avoid this problem in a way that also justifies that
835 we don't really need to use that kind of quantification. Another
836 approach to this definition that completely avoid this complication
837 would be to make [PartFunct] a dependent type, receiving the predicate
838 as an argument. This does work in that it allows us to give
839 [PartFunct] type [Set] and do some useful stuff with it; however, we
840 are not able to define something as simple as an operator that gets a
841 function and returns its domain (because of the restrictions in the
842 type elimination rules). This sounds very unnatural, and soon gets us
843 into strange problems that yield very unlikely definitions, which is
844 why we chose to altogether do away with this approach.
846 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
849 We now present some methods for defining partial functions.
852 Hint Resolve CI: core.
856 Variable S : CSetoid.
859 To begin with, we want to be able to ``see'' each total function as a partial function.
862 Definition total_eq_part : CSetoid_un_op S -> PartFunct S.
865 Build_PartFunct with (fun x : S => CTrue) (fun (x : S) (H : CTrue) => f x).
866 red in |- *; intros; auto.
868 exact (csf_strext_unfolded _ _ f _ _ H).
871 Section Part_Function_Const.
874 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
876 %\begin{convention}% Let [c:S].
882 Definition Fconst := total_eq_part (Const_CSetoid_fun _ _ c).
884 End Part_Function_Const.
886 Section Part_Function_Id.
888 Definition Fid := total_eq_part (id_un_op S).
890 End Part_Function_Id.
893 (These happen to be always total functions, but that is more or less obvious, as we have no information on the setoid; however, we will be able to define partial functions just applying other operators to these ones.)
895 If we have two setoid functions [F] and [G] we can always compose them. The domain of our new function will be the set of points [s] in the domain of [F] for which [F(s)] is in the domain of [G]#. #%\footnote{%Notice that the use of extension here is essential.%}.% The inversion in the order of the variables is done to maintain uniformity with the usual mathematical notation.
897 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
901 Section Part_Function_Composition.
903 Variables G F : PartFunct S.
909 Let R x := {Hx : P x | Q (F x Hx)}.
911 Lemma part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
912 G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
914 exact (pfstrx _ _ _ _ _ _ (pfstrx _ _ _ _ _ _ H)).
917 Lemma part_function_comp_dom_wd : pred_wd S R.
918 red in |- *; intros x y H H0.
919 unfold R in |- *; inversion_clear H.
920 exists (dom_wd _ F x y x0 H0).
921 apply (dom_wd _ G) with (F x x0).
923 apply pfwdef; assumption.
926 Definition Fcomp := Build_PartFunct _ R part_function_comp_dom_wd
927 (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
928 part_function_comp_strext.
930 End Part_Function_Composition.
935 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
939 Section BinPart_Function_Composition.
941 Variables S1 S2 S3 : CSetoid.
943 Variable G : BinPartFunct S2 S3.
944 Variable F : BinPartFunct S1 S2.
950 Let R x := {Hx : P x | Q (F x Hx)}.
952 Lemma bin_part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
953 G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
955 exact (bpfstrx _ _ _ _ _ _ _ (bpfstrx _ _ _ _ _ _ _ H)).
958 Lemma bin_part_function_comp_dom_wd : pred_wd S1 R.
959 red in |- *; intros x y H H0.
960 unfold R in |- *; inversion_clear H.
961 exists (bdom_wd _ _ F x y x0 H0).
962 apply (bdom_wd _ _ G) with (F x x0).
964 apply bpfwdef; assumption.
967 Definition BinFcomp := Build_BinPartFunct _ _ R bin_part_function_comp_dom_wd
968 (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
969 bin_part_function_comp_strext.
971 End BinPart_Function_Composition.
973 (* Different tokens for compatibility with coqdoc *)
975 Implicit Arguments Fconst [S].
976 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
978 Notation FId := (Fid _).
980 Implicit Arguments Fcomp [S].
981 Infix "[o]" := Fcomp (at level 65, no associativity).
983 Hint Resolve pfwdef bpfwdef: algebra.
988 Definition injective A B (f : CSetoid_fun A B) := (forall a0 a1 : A,
989 a0 [#] a1 -> f a0 [#] f a1):CProp.
991 Definition injective_weak A B (f : CSetoid_fun A B) := forall a0 a1 : A,
992 f a0 [=] f a1 -> a0 [=] a1.
994 Definition surjective A B (f : CSetoid_fun A B) := (forall b : B, {a : A | f a [=] b}):CProp.
996 Implicit Arguments injective [A B].
997 Implicit Arguments injective_weak [A B].
998 Implicit Arguments surjective [A B].
1000 Lemma injective_imp_injective_weak : forall A B (f : CSetoid_fun A B),
1001 injective f -> injective_weak f.
1003 unfold injective in |- *.
1005 unfold injective_weak in |- *.
1007 apply not_ap_imp_eq.
1010 set (H2 := H a0 a1 H1) in *.
1011 set (H3 := ap_imp_neq B (f a0) (f a1) H2) in *.
1012 set (H4 := eq_imp_not_neq B (f a0) (f a1) H0) in *.
1017 Definition bijective A B (f:CSetoid_fun A B) := injective f and surjective f.
1019 Implicit Arguments bijective [A B].
1021 Lemma id_is_bij : forall A, bijective (id_un_op A).
1025 intro b; exists b; apply eq_reflexive.
1028 Lemma comp_resp_bij : forall A B C f g, bijective f -> bijective g ->
1029 bijective (compose_CSetoid_fun A B C f g).
1032 elim H0; clear H0; intros H00 H01.
1033 elim H1; clear H1; intros H10 H11.
1035 intros a0 a1; simpl; intro.
1036 apply H10; apply H00; auto.
1038 elim (H11 c); intros b H20.
1039 elim (H01 b); intros a H30.
1044 Lemma inv : forall A B (f:CSetoid_fun A B),
1045 bijective f -> forall b : B, {a : A | f a [=] b}.
1046 unfold bijective in |- *.
1047 unfold surjective in |- *.
1051 Implicit Arguments inv [A B].
1053 Definition invfun A B (f : CSetoid_fun A B) (H : bijective f) : B -> A.
1055 elim (inv f H H0); intros a H2.
1059 Implicit Arguments invfun [A B].
1061 Lemma inv1 : forall A B (f : CSetoid_fun A B) (H : bijective f) (b : B),
1062 f (invfun f H b) [=] b.
1064 unfold invfun in |- *; case inv.
1068 Lemma inv2 : forall A B (f : CSetoid_fun A B) (H : bijective f) (a : A),
1069 invfun f H (f a) [=] a.
1071 unfold invfun in |- *; case inv; simpl.
1072 elim H; clear H; intros H0 H1.
1074 apply injective_imp_injective_weak.
1078 Lemma inv_strext : forall A B (f : CSetoid_fun A B) (H : bijective f),
1079 fun_strext (invfun f H).
1082 elim H; intros H00 H01.
1083 elim (H01 x); intros a0 H2.
1084 elim (H01 y); intros a1 H3.
1088 astepl (invfun f H x).
1089 astepr (invfun f H y).
1091 astepl (invfun f H (f a1)).
1093 apply injective_imp_injective_weak with (f := f); auto.
1100 astepl (invfun f H (f a0)).
1103 apply injective_imp_injective_weak with (f := f); auto.
1106 apply eq_symmetric; apply inv1.
1107 apply eq_symmetric; apply inv1.
1110 Definition Inv A B f (H : bijective f) :=
1111 Build_CSetoid_fun B A (invfun f H) (inv_strext A B f H).
1113 Implicit Arguments Inv [A B].
1115 Definition Inv_bij : forall A B (f : CSetoid_fun A B) (H : bijective f),
1116 bijective (Inv f H).
1118 unfold bijective in |- *.
1120 unfold injective in |- *.
1121 unfold bijective in H.
1122 unfold surjective in H.
1130 astepl (Inv f (CAnd_intro _ _ H0 H1) (f a0)).
1131 astepr (Inv f (CAnd_intro _ _ H0 H1) (f a1)).
1133 unfold fun_strext in |- *.
1152 unfold surjective in |- *.
1162 Implicit Arguments bijective [A B].
1163 Implicit Arguments injective [A B].
1164 Implicit Arguments injective_weak [A B].
1165 Implicit Arguments surjective [A B].
1166 Implicit Arguments inv [A B].
1167 Implicit Arguments invfun [A B].
1168 Implicit Arguments Inv [A B].
1170 Implicit Arguments conj_wd [S P Q].
1172 Notation Prj1 := (prj1 _ _ _ _).
1173 Notation Prj2 := (prj2 _ _ _ _).