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/CoRN/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)
50 apply eq_reflexive_unfolded
55 Lemma irrefl_apfun : forall A B : CSetoid, irreflexive (ap_fun A B).
57 unfold irreflexive in |- *.
59 unfold ap_fun in |- *.
64 set (H1 := ap_irreflexive_unfolded B (f a)) in *.
71 lemma cotrans_apfun : \forall A,B : CSetoid. cotransitive (CSetoid_fun A B) (ap_fun A B).
77 apply ap_cotransitive.
78 apply (ap_imp_neq B (csf_fun A B x a) (csf_fun A B y a) H1).
79 (* letin foo \def (\exist a:A.csf_fun A B x a\neq csf_fun A B z a). *)
82 apply (ap_cotransitive B ? ? H1 ?).
89 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
106 Lemma cotrans_apfun : forall A B : CSetoid, cotransitive (ap_fun A B).
108 unfold cotransitive in |- *.
109 unfold ap_fun in |- *.
114 set (H1 := ap_cotransitive B (f a) (g a) H (h a)) in *.
130 lemma ta_apfun : \forall A, B : CSetoid. tight_apart (CSetoid_fun A B) (eq_fun A B) (ap_fun A B).
136 [ intros. elim H. unfold in H.
137 generalize in match H. reduce. simplify .unfold.
155 set (H2 := eq_imp_not_ap B (f a) (g a) (H a) X) in *.
160 Lemma ta_apfun : forall A B : CSetoid, tight_apart (eq_fun A B) (ap_fun A B).
161 unfold tight_apart in |- *.
162 unfold ap_fun in |- *.
163 unfold eq_fun in |- *.
180 set (H2 := eq_imp_not_ap B (f a) (g a) (H a) X) in *.
185 Lemma sym_apfun : forall A B : CSetoid, Csymmetric (ap_fun A B).
186 unfold Csymmetric in |- *.
187 unfold ap_fun in |- *.
193 apply ap_symmetric_unfolded.
197 Definition FS_is_CSetoid (A B : CSetoid) :=
198 Build_is_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
199 (irrefl_apfun A B) (sym_apfun A B) (cotrans_apfun A B) (ta_apfun A B).
201 Definition FS_as_CSetoid (A B : CSetoid) :=
202 Build_CSetoid (CSetoid_fun A B) (eq_fun A B) (ap_fun A B)
205 (** **Nullary and n-ary operations
208 Definition is_nullary_operation (S:CSetoid) (s:S):Prop := True.
210 Fixpoint n_ary_operation (n:nat)(V:CSetoid){struct n}:CSetoid:=
213 |(S m)=> (FS_as_CSetoid V (n_ary_operation m V))
216 Section unary_function_composition.
218 (** ** Composition of Setoid functions
220 Let [S1], [S2] and [S3] be setoids, [f] a
221 setoid function from [S1] to [S2], and [g] from [S2]
222 to [S3] in the following definition of composition. *)
224 Variables S1 S2 S3 : CSetoid.
225 Variable f : CSetoid_fun S1 S2.
226 Variable g : CSetoid_fun S2 S3.
228 Definition compose_CSetoid_fun : CSetoid_fun S1 S3.
229 apply (Build_CSetoid_fun _ _ (fun x : S1 => g (f x))).
231 unfold fun_strext in |- *; intros x y H.
232 apply (csf_strext _ _ f). apply (csf_strext _ _ g). assumption.
235 End unary_function_composition.
237 (** ***Composition as operation
239 Definition comp (A B C : CSetoid) :
240 FS_as_CSetoid A B -> FS_as_CSetoid B C -> FS_as_CSetoid A C.
242 set (H := compose_CSetoid_fun A B C f g) in *.
246 Definition comp_as_bin_op (A:CSetoid) : CSetoid_bin_op (FS_as_CSetoid A A).
248 unfold CSetoid_bin_op in |- *.
249 eapply Build_CSetoid_bin_fun with (comp A A A).
250 unfold bin_fun_strext in |- *.
254 unfold ap_fun in |- *.
255 unfold compose_CSetoid_fun in |- *.
258 unfold fun_strext in |- *.
262 unfold fun_strext in |- *.
266 unfold fun_strext in |- *.
270 unfold fun_strext in |- *.
278 set (H0 := ap_cotransitive A (g1 (f1 a)) (g2 (f2 a)) H (g2 (f1 a))) in *.
294 Lemma assoc_comp : forall A : CSetoid, associative (comp_as_bin_op A).
295 unfold associative in |- *.
296 unfold comp_as_bin_op in |- *.
299 unfold eq_fun in |- *.
304 Section unary_and_binary_function_composition.
306 Definition compose_CSetoid_bin_un_fun (A B C : CSetoid)
307 (f : CSetoid_bin_fun B B C) (g : CSetoid_fun A B) : CSetoid_bin_fun A A C.
309 apply (Build_CSetoid_bin_fun A A C (fun a0 a1 : A => f (g a0) (g a1))).
310 intros x1 x2 y1 y2 H0.
311 assert (H10:= csbf_strext B B C f).
313 assert (H40 := csf_strext A B g).
315 elim (H10 (g x1) (g x2) (g y1) (g y2) H0); [left | right]; auto.
318 Definition compose_CSetoid_bin_fun A B C (f g : CSetoid_fun A B)
319 (h : CSetoid_bin_fun B B C) : CSetoid_fun A C.
321 apply (Build_CSetoid_fun A C (fun a : A => h (f a) (g a))).
323 elim (csbf_strext _ _ _ _ _ _ _ _ H); apply csf_strext.
326 Definition compose_CSetoid_un_bin_fun A B C (f : CSetoid_bin_fun B B C)
327 (g : CSetoid_fun C A) : CSetoid_bin_fun B B A.
329 apply Build_CSetoid_bin_fun with (fun x y : B0 => g (f x y)).
333 unfold bin_fun_strext in |- *.
336 unfold fun_strext in |- *.
337 intros gu gstrext fu fstrext H.
343 End unary_and_binary_function_composition.
348 Section function_projection.
350 Lemma proj_bin_fun : forall A B C (f : CSetoid_bin_fun A B C) a, fun_strext (f a).
356 intros csbf_strext0 x y H.
357 elim (csbf_strext0 _ _ _ _ H); intro H0.
358 elim (ap_irreflexive_unfolded _ _ H0).
362 Definition projected_bin_fun A B C (f : CSetoid_bin_fun A B C) (a : A) :=
363 Build_CSetoid_fun B C (f a) (proj_bin_fun A B C f a).
365 End function_projection.
369 Variable S : CSetoid.
371 Definition binproj1 (x y:S) := x.
373 Lemma binproj1_strext : bin_fun_strext _ _ _ binproj1.
377 Definition cs_binproj1 : CSetoid_bin_op S.
378 red in |- *; apply Build_CSetoid_bin_op with binproj1.
379 apply binproj1_strext.
384 (** **Combining operations
385 %\begin{convention}% Let [S1], [S2] and [S3] be setoids.
389 Section CombiningOperations.
390 Variables S1 S2 S3 : CSetoid.
393 In the following definition, we assume [f] is a setoid function from
394 [S1] to [S2], and [op] is an unary operation on [S2].
395 Then [opOnFun] is the composition [op] after [f].
397 Section CombiningUnaryOperations.
398 Variable f : CSetoid_fun S1 S2.
399 Variable op : CSetoid_un_op S2.
401 Definition opOnFun : CSetoid_fun S1 S2.
402 apply (Build_CSetoid_fun S1 S2 (fun x : S1 => op (f x))).
404 unfold fun_strext in |- *; intros x y H.
405 apply (csf_strext _ _ f x y).
406 apply (csf_strext _ _ op _ _ H).
409 End CombiningUnaryOperations.
411 End CombiningOperations.
415 (** **The Free Setoid
416 %\begin{convention}% Let [A:CSetoid].
421 Definition Astar := (list A).
423 Definition empty_word := (nil A).
425 Definition appA:= (app A).
427 Fixpoint eq_fm (m:Astar)(k:Astar){struct m}:Prop:=
433 |cons b n => match k with
435 |cons a l => b[=]a /\ (eq_fm n l)
439 Fixpoint ap_fm (m:Astar)(k:Astar){struct m}: CProp :=
445 |cons b n => match k with
447 |cons a l => b[#]a or (ap_fm n l)
451 Lemma ap_fm_irreflexive: (irreflexive ap_fm).
465 generalize (ap_irreflexive A a).
473 Lemma ap_fm_symmetric: Csymmetric ap_fm.
493 generalize (ap_symmetric A a c).
502 Lemma ap_fm_cotransitive : (cotransitive ap_fm).
537 generalize (ap_cotransitive A a c H c0).
542 generalize (IHx l H l0).
546 Lemma ap_fm_tight : (tight_apart eq_fm ap_fm).
574 generalize (ap_tight A a c).
589 generalize (ap_tight A a c).
596 Definition free_csetoid_is_CSetoid:(is_CSetoid Astar eq_fm ap_fm):=
597 (Build_is_CSetoid Astar eq_fm ap_fm ap_fm_irreflexive ap_fm_symmetric
598 ap_fm_cotransitive ap_fm_tight).
600 Definition free_csetoid_as_csetoid:CSetoid:=
601 (Build_CSetoid Astar eq_fm ap_fm free_csetoid_is_CSetoid).
604 (bin_fun_strext free_csetoid_as_csetoid free_csetoid_as_csetoid
605 free_csetoid_as_csetoid appA).
606 unfold bin_fun_strext.
635 generalize (IHx1 l y1 (nil A)).
644 generalize (IHx1 l0 y1 (cons c l)).
648 Definition app_as_csb_fun:
649 (CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
650 free_csetoid_as_csetoid):=
651 (Build_CSetoid_bin_fun free_csetoid_as_csetoid free_csetoid_as_csetoid
652 free_csetoid_as_csetoid appA app_strext).
654 Lemma eq_fm_reflexive: forall (x:Astar), (eq_fm x x).
666 (** **Partial Functions
668 In this section we define a concept of partial function for an
669 arbitrary setoid. Essentially, a partial function is what would be
670 expected---a predicate on the setoid in question and a total function
671 from the set of points satisfying that predicate to the setoid. There
672 is one important limitations to this approach: first, the record we
673 obtain has type [Type], meaning that we can't use, for instance,
674 elimination of existential quantifiers.
676 Furthermore, for reasons we will explain ahead, partial functions will
677 not be defined via the [CSetoid_fun] record, but the whole structure
678 will be incorporated in a new record.
680 Finally, notice that to be completely general the domains of the
681 functions have to be characterized by a [CProp]-valued predicate;
682 otherwise, the use you can make of a function will be %\emph{%#<i>#a
683 priori#</i>#%}% restricted at the moment it is defined.
685 Before we state our definitions we need to do some work on domains.
688 Section SubSets_of_G.
690 (** ***Subsets of Setoids
692 Subsets of a setoid will be identified with predicates from the
693 carrier set of the setoid into [CProp]. At this stage, we do not make
694 any assumptions about these predicates.
696 We will begin by defining elementary operations on predicates, along
697 with their basic properties. In particular, we will work with well
698 defined predicates, so we will prove that these operations preserve
701 %\begin{convention}% Let [S:CSetoid] and [P,Q:S->CProp].
705 Variable S : CSetoid.
709 Variables P Q : S -> CProp.
711 Definition conjP (x : S) : CProp := P x and Q x.
713 Lemma prj1 : forall x : S, conjP x -> P x.
714 intros x H; inversion_clear H; assumption.
717 Lemma prj2 : forall x : S, conjP x -> Q x.
718 intros x H; inversion_clear H; assumption.
721 Lemma conj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ conjP.
723 red in |- *; intros x y H1 H2.
724 inversion_clear H1; split.
726 apply H with x; assumption.
728 apply H0 with x; assumption.
735 Variables P Q : S -> CProp.
738 Although at this stage we never use it, for completeness's sake we also treat disjunction (corresponding to union of subsets).
741 Definition disj (x : S) : CProp := P x or Q x.
743 Lemma inj1 : forall x : S, P x -> disj x.
744 intros; left; assumption.
747 Lemma inj2 : forall x : S, Q x -> disj x.
748 intros; right; assumption.
751 Lemma disj_wd : pred_wd _ P -> pred_wd _ Q -> pred_wd _ disj.
753 red in |- *; intros x y H1 H2.
756 left; apply H with x; assumption.
758 right; apply H0 with x; assumption.
766 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].
769 Variable P : S -> CProp.
770 Variable R : forall x : S, P x -> CProp.
772 Definition extend (x : S) : CProp := P x and (forall H : P x, R x H).
774 Lemma ext1 : forall x : S, extend x -> P x.
775 intros x H; inversion_clear H; assumption.
778 Lemma ext2_a : forall x : S, extend x -> {H : P x | R x H}.
779 intros x H; inversion_clear H.
783 Lemma ext2 : forall (x : S) (Hx : extend x), R x (ProjT1 (ext2_a x Hx)).
784 intros; apply projT2.
787 Lemma extension_wd : pred_wd _ P ->
788 (forall (x y : S) Hx Hy, x [=] y -> R x Hx -> R y Hy) -> pred_wd _ extend.
790 red in |- *; intros x y H1 H2.
791 elim H1; intros H3 H4; split.
793 apply H with x; assumption.
795 intro H5; apply H0 with x H3; [ apply H2 | apply H4 ].
802 Notation Conj := (conjP _).
803 Implicit Arguments disj [S].
805 Implicit Arguments extend [S].
806 Implicit Arguments ext1 [S P R x].
807 Implicit Arguments ext2 [S P R x].
811 We are now ready to define the concept of partial function between arbitrary setoids.
814 Record BinPartFunct (S1 S2 : CSetoid) : Type :=
815 {bpfdom : S1 -> CProp;
816 bdom_wd : pred_wd S1 bpfdom;
817 bpfpfun :> forall x : S1, bpfdom x -> S2;
818 bpfstrx : forall x y Hx Hy, bpfpfun x Hx [#] bpfpfun y Hy -> x [#] y}.
821 Notation BDom := (bpfdom _ _).
822 Implicit Arguments bpfpfun [S1 S2].
825 The next lemma states that every partial function is well defined.
828 Lemma bpfwdef : forall S1 S2 (F : BinPartFunct S1 S2) x y Hx Hy,
829 x [=] y -> F x Hx [=] F y Hy.
831 apply not_ap_imp_eq; intro H0.
832 generalize (bpfstrx _ _ _ _ _ _ _ H0).
833 exact (eq_imp_not_ap _ _ _ H).
836 (** Similar for automorphisms. *)
838 Record PartFunct (S : CSetoid) : Type :=
840 dom_wd : pred_wd S pfdom;
841 pfpfun :> forall x : S, pfdom x -> S;
842 pfstrx : forall x y Hx Hy, pfpfun x Hx [#] pfpfun y Hy -> x [#] y}.
844 Notation Dom := (pfdom _).
845 Notation Part := (pfpfun _).
846 Implicit Arguments pfpfun [S].
849 The next lemma states that every partial function is well defined.
852 Lemma pfwdef : forall S (F : PartFunct S) x y Hx Hy, x [=] y -> F x Hx [=] F y Hy.
854 apply not_ap_imp_eq; intro H0.
855 generalize (pfstrx _ _ _ _ _ _ H0).
856 exact (eq_imp_not_ap _ _ _ H).
860 A few characteristics of this definition should be explained:
861 - The domain of the partial function is characterized by a predicate
862 that is required to be well defined but not strongly extensional. The
863 motivation for this choice comes from two facts: first, one very
864 important subset of real numbers is the compact interval
865 [[a,b]]---characterized by the predicate [ fun x : IR => a [<=] x /\ x
866 [<=] b], which is not strongly extensional; on the other hand, if we
867 can apply a function to an element [s] of a setoid [S] it seems
868 reasonable (and at some point we do have to do it) to apply that same
869 function to any element [s'] which is equal to [s] from the point of
870 view of the setoid equality.
871 - The last two conditions state that [pfpfun] is really a subsetoid
872 function. The reason why we do not write it that way is the
873 following: when applying a partial function [f] to an element [s] of
874 [S] we also need a proof object [H]; with this definition the object
875 we get is [f(s,H)], where the proof is kept separate from the object.
876 Using subsetoid notation, we would get $f(\langle
877 s,H\rangle)$#f(⟨s,H⟩)#; from this we need to apply two
878 projections to get either the original object or the proof, and we
879 need to apply an extra constructor to get $f(\langle
880 s,H\rangle)$#f(⟨s,H⟩)# from [s] and [H]. This amounts
881 to spending more resources when actually working with these objects.
882 - This record has type [Type], which is very unfortunate, because it
883 means in particular that we cannot use the well behaved set
884 existential quantification over partial functions; however, later on
885 we will manage to avoid this problem in a way that also justifies that
886 we don't really need to use that kind of quantification. Another
887 approach to this definition that completely avoid this complication
888 would be to make [PartFunct] a dependent type, receiving the predicate
889 as an argument. This does work in that it allows us to give
890 [PartFunct] type [Set] and do some useful stuff with it; however, we
891 are not able to define something as simple as an operator that gets a
892 function and returns its domain (because of the restrictions in the
893 type elimination rules). This sounds very unnatural, and soon gets us
894 into strange problems that yield very unlikely definitions, which is
895 why we chose to altogether do away with this approach.
897 %\begin{convention}% All partial functions will henceforth be denoted by capital letters.
900 We now present some methods for defining partial functions.
903 Hint Resolve CI: core.
907 Variable S : CSetoid.
910 To begin with, we want to be able to ``see'' each total function as a partial function.
913 Definition total_eq_part : CSetoid_un_op S -> PartFunct S.
916 Build_PartFunct with (fun x : S => CTrue) (fun (x : S) (H : CTrue) => f x).
917 red in |- *; intros; auto.
919 exact (csf_strext_unfolded _ _ f _ _ H).
922 Section Part_Function_Const.
925 In any setoid we can also define constant functions (one for each element of the setoid) and an identity function:
927 %\begin{convention}% Let [c:S].
933 Definition Fconst := total_eq_part (Const_CSetoid_fun _ _ c).
935 End Part_Function_Const.
937 Section Part_Function_Id.
939 Definition Fid := total_eq_part (id_un_op S).
941 End Part_Function_Id.
944 (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.)
946 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.
948 %\begin{convention}% Let [G,F:(PartFunct S)] and denote by [Q] and [P], respectively, the predicates characterizing their domains.
952 Section Part_Function_Composition.
954 Variables G F : PartFunct S.
960 Let R x := {Hx : P x | Q (F x Hx)}.
962 Lemma part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
963 G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
965 exact (pfstrx _ _ _ _ _ _ (pfstrx _ _ _ _ _ _ H)).
968 Lemma part_function_comp_dom_wd : pred_wd S R.
969 red in |- *; intros x y H H0.
970 unfold R in |- *; inversion_clear H.
971 exists (dom_wd _ F x y x0 H0).
972 apply (dom_wd _ G) with (F x x0).
974 apply pfwdef; assumption.
977 Definition Fcomp := Build_PartFunct _ R part_function_comp_dom_wd
978 (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
979 part_function_comp_strext.
981 End Part_Function_Composition.
986 %\begin{convention}% Let [F:(BinPartFunct S1 S2)] and [G:(PartFunct S2 S3)], and denote by [Q] and [P], respectively, the predicates characterizing their domains.
990 Section BinPart_Function_Composition.
992 Variables S1 S2 S3 : CSetoid.
994 Variable G : BinPartFunct S2 S3.
995 Variable F : BinPartFunct S1 S2.
1001 Let R x := {Hx : P x | Q (F x Hx)}.
1003 Lemma bin_part_function_comp_strext : forall x y (Hx : R x) (Hy : R y),
1004 G (F x (ProjT1 Hx)) (ProjT2 Hx) [#] G (F y (ProjT1 Hy)) (ProjT2 Hy) -> x [#] y.
1006 exact (bpfstrx _ _ _ _ _ _ _ (bpfstrx _ _ _ _ _ _ _ H)).
1009 Lemma bin_part_function_comp_dom_wd : pred_wd S1 R.
1010 red in |- *; intros x y H H0.
1011 unfold R in |- *; inversion_clear H.
1012 exists (bdom_wd _ _ F x y x0 H0).
1013 apply (bdom_wd _ _ G) with (F x x0).
1015 apply bpfwdef; assumption.
1018 Definition BinFcomp := Build_BinPartFunct _ _ R bin_part_function_comp_dom_wd
1019 (fun x (Hx : R x) => G (F x (ProjT1 Hx)) (ProjT2 Hx))
1020 bin_part_function_comp_strext.
1022 End BinPart_Function_Composition.
1024 (* Different tokens for compatibility with coqdoc *)
1026 Implicit Arguments Fconst [S].
1027 Notation "[-C-] x" := (Fconst x) (at level 2, right associativity).
1029 Notation FId := (Fid _).
1031 Implicit Arguments Fcomp [S].
1032 Infix "[o]" := Fcomp (at level 65, no associativity).
1034 Hint Resolve pfwdef bpfwdef: algebra.
1039 Definition injective A B (f : CSetoid_fun A B) := (forall a0 a1 : A,
1040 a0 [#] a1 -> f a0 [#] f a1):CProp.
1042 Definition injective_weak A B (f : CSetoid_fun A B) := forall a0 a1 : A,
1043 f a0 [=] f a1 -> a0 [=] a1.
1045 Definition surjective A B (f : CSetoid_fun A B) := (forall b : B, {a : A | f a [=] b}):CProp.
1047 Implicit Arguments injective [A B].
1048 Implicit Arguments injective_weak [A B].
1049 Implicit Arguments surjective [A B].
1051 Lemma injective_imp_injective_weak : forall A B (f : CSetoid_fun A B),
1052 injective f -> injective_weak f.
1054 unfold injective in |- *.
1056 unfold injective_weak in |- *.
1058 apply not_ap_imp_eq.
1061 set (H2 := H a0 a1 H1) in *.
1062 set (H3 := ap_imp_neq B (f a0) (f a1) H2) in *.
1063 set (H4 := eq_imp_not_neq B (f a0) (f a1) H0) in *.
1068 Definition bijective A B (f:CSetoid_fun A B) := injective f and surjective f.
1070 Implicit Arguments bijective [A B].
1072 Lemma id_is_bij : forall A, bijective (id_un_op A).
1076 intro b; exists b; apply eq_reflexive.
1079 Lemma comp_resp_bij : forall A B C f g, bijective f -> bijective g ->
1080 bijective (compose_CSetoid_fun A B C f g).
1083 elim H0; clear H0; intros H00 H01.
1084 elim H1; clear H1; intros H10 H11.
1086 intros a0 a1; simpl; intro.
1087 apply H10; apply H00; auto.
1089 elim (H11 c); intros b H20.
1090 elim (H01 b); intros a H30.
1095 Lemma inv : forall A B (f:CSetoid_fun A B),
1096 bijective f -> forall b : B, {a : A | f a [=] b}.
1097 unfold bijective in |- *.
1098 unfold surjective in |- *.
1102 Implicit Arguments inv [A B].
1104 Definition invfun A B (f : CSetoid_fun A B) (H : bijective f) : B -> A.
1106 elim (inv f H H0); intros a H2.
1110 Implicit Arguments invfun [A B].
1112 Lemma inv1 : forall A B (f : CSetoid_fun A B) (H : bijective f) (b : B),
1113 f (invfun f H b) [=] b.
1115 unfold invfun in |- *; case inv.
1119 Lemma inv2 : forall A B (f : CSetoid_fun A B) (H : bijective f) (a : A),
1120 invfun f H (f a) [=] a.
1122 unfold invfun in |- *; case inv; simpl.
1123 elim H; clear H; intros H0 H1.
1125 apply injective_imp_injective_weak.
1129 Lemma inv_strext : forall A B (f : CSetoid_fun A B) (H : bijective f),
1130 fun_strext (invfun f H).
1133 elim H; intros H00 H01.
1134 elim (H01 x); intros a0 H2.
1135 elim (H01 y); intros a1 H3.
1139 astepl (invfun f H x).
1140 astepr (invfun f H y).
1142 astepl (invfun f H (f a1)).
1144 apply injective_imp_injective_weak with (f := f); auto.
1151 astepl (invfun f H (f a0)).
1154 apply injective_imp_injective_weak with (f := f); auto.
1157 apply eq_symmetric; apply inv1.
1158 apply eq_symmetric; apply inv1.
1161 Definition Inv A B f (H : bijective f) :=
1162 Build_CSetoid_fun B A (invfun f H) (inv_strext A B f H).
1164 Implicit Arguments Inv [A B].
1166 Definition Inv_bij : forall A B (f : CSetoid_fun A B) (H : bijective f),
1167 bijective (Inv f H).
1169 unfold bijective in |- *.
1171 unfold injective in |- *.
1172 unfold bijective in H.
1173 unfold surjective in H.
1181 astepl (Inv f (CAnd_intro _ _ H0 H1) (f a0)).
1182 astepr (Inv f (CAnd_intro _ _ H0 H1) (f a1)).
1184 unfold fun_strext in |- *.
1203 unfold surjective in |- *.
1213 Implicit Arguments bijective [A B].
1214 Implicit Arguments injective [A B].
1215 Implicit Arguments injective_weak [A B].
1216 Implicit Arguments surjective [A B].
1217 Implicit Arguments inv [A B].
1218 Implicit Arguments invfun [A B].
1219 Implicit Arguments Inv [A B].
1221 Implicit Arguments conj_wd [S P Q].
1223 Notation Prj1 := (prj1 _ _ _ _).
1224 Notation Prj2 := (prj2 _ _ _ _).