(********************************************************************** DOING SET THEORY IN TYPE THEORY USING A VIRTUAL CHOICE AXIOM Carlos Simpson March 2002 (minor changes in June 2002 for compatibility with Coq 7.3) Thanks to Marco Maggesi for many helpful suggestions and for fixing up many things in this file *********************************************************************) (********************************************************************** We suppose three axioms: (1) "extens" which is extensionality in its standard form; (2) the axiom "Prop_uni" that if P,Q : Prop and P <-> Q then P == Q. This axiom is a consequence of an axiom Ensembles.extensionality contained in the standard library Ensembles.v so instead of stating it as an axiom we deduce it from that axiom; and (3) "virtual_choice" giving a choice for X nonempty of a proposition X -> Prop singling out one element of X. The first axiom is standard. The second comes from Giles Kahn's Ensembles package. The third axiom has already appeared in at least two different places that I know of (and probably many others): (a) In a message to coq-club Ensembles and the Axiom of Choice From: David Nowak (David.Nowak@irisa.fr) Date: Wed Nov 25 1998 - 10:27:48 MET David Nowak asks if he can assume the axiom of choice in the context of the Ensembles library. This is roughly equivalent to the virtual_choice axiom. (b) In the user-contribution "Paradoxes in Set Theory and Type Theory" by Benjamin Werner (1997), in the second half of the file diaconescu.v he shows that a weak form of the axiom of choice (which is equivalent to virtual_choice) implies excluded middle. We do not assume the description axiom giving the element in question when one has such a proposition. In order to make virtual_choice useful, one thus has to assume, in addition to a type X : Type, an additional variable d : (description X) where (description X) is the type of functions which associate to each single-element property X -> Prop, the element singled out. In many cases one can get a d: (description X) for free, for example if X := Y -> Prop. The hope is that the above three axioms are consistent, even when one includes the sort Set. We require Classical_Type in order to have NNPP (excluded middle). This would not be strictly necessary because we could derive NNPP from virtual_choice using Werner's proof refered to in (b) above. Rather than doing this we just require Classical_Type. Another feature is that we use an equality EQ between terms of types which are not necessarily convertible (note however that if (EQ a b) then of course (type_of a) == (type_of b)). Although we introduce it in a different way, our EQ is the same as C. McBride's JMeqT (see the file Logic/JMeq.v of the standard library). Our virtual_choice axiom allows us to actually prove the statement JMeqT_eqT which was assumed as an axiom in the file JMeq.v. Also that file concerns only the sort Set (i.e. JMeq is defined instead of JMeqT). For these reasons we develop EQ on our own rather than requiring JMeq.v. *********************************************************************) Require Classical_Type. Require Ensembles. Require Berardi. (*************************************************************************) (****************** tactics ****************************************) (*************************************************************************) Tactic Definition Prolog3 := Prolog [] 3. Tactic Definition Prolog6 := Prolog [ ] 6. Tactic Definition Prolog9 := Prolog [ ] 9. Definition DepTrue := [X: Type; x:X]True. Implicits DepTrue [1]. Definition truth : True := I. Tactic Definition Poser u v := Assert truhyp : (DepTrue v); [Exact truth | Idtac]; (LetTac u := v in truhyp); (Clear truhyp). (*** subterfuge for generating a name ***) Definition SubterTrue := True. Tactic Definition Sel v := ((Assert SubterTrue); [Exact truth|Idtac]); (Match Context With [id1 : SubterTrue |- ? ] -> (Clear id1; (Poser id1 v))). Lemma False_implies_everything : (P:Prop)False->P. Intros. Elim H. Save. Tactic Definition Exact_fie := Match Context With [id1 : False |- ?1 ] -> First [Exact (False_implies_everything ?1 id1)]. (*************************************************************************) (****************** excluded middle ********************************) (*************************************************************************) Definition excluded_middle : (P: Prop)(not (not P))-> P := NNPP. Tactic Definition Exact_em := Match Context With [id1 : (not (not ?)) |- ? ] -> First [Exact (excluded_middle ? id1)]. (*************************************************************************) (***** the following parameter is our axiom of choice ********************) (*************************************************************************) Definition is_empty := [X: Type]X ->False. Definition is_nonempty := [X:Type]((X -> False)-> False). Definition doesnt_exist := [A: Type] [P: A->Prop] (a:A) (P a) -> False. Implicits doesnt_exist [1]. (*Definition exists := [A: Type] [P: A-> Prop] (not (doesnt_exist P)).*) Definition exists := [X:Type; P:X -> Prop](((w:X)((P w) -> False)) -> False). Implicits exists [1]. Lemma exists_th1 : (A: Type)(a:A)(P: A -> Prop)(P a) -> (exists P). Intros. Intro. Apply H0 with a. Assumption. Save. Implicits exists_th1 [1 2]. Tactic Definition UseExists v:= Match Context With [v : (exists ?1) |- ?] -> First [(Apply NNPP; Unfold not; Intro); Assert (doesnt_exist ?1); [Unfold doesnt_exist; Intros |Prolog [] 2 ] ]. Tactic Definition UseExists2 v:= Match Context With [id1 : (exists ?1) |- ?] -> First [(Assert dummy : (id1 == v);[Trivial|Clear dummy]); (Apply NNPP; Unfold not; Intro contra); Assert (doesnt_exist ?1); [Unfold doesnt_exist; Intros |Prolog [] 2 ]; EApply contra; Clear contra ]. Tactic Definition Exhibit v := Match Context With [ |- (exists ?1)] -> First [(EApply (!exists_th1 ? v ?1))]. Tactic Definition UseNonempty v := Match Context With [v:(is_nonempty ?1) |- ?] -> First [(Apply NNPP; Unfold not; Intro); Assert (is_empty ?1); [Unfold is_empty; Intros |Prolog [] 2 ] ]. Tactic Definition NonemptyPose v w := Match Context With [v:(is_nonempty ?1) |- ?] -> First [(Apply NNPP; Unfold not; Intro); Assert (is_empty ?1); [Unfold is_empty; Intro w |Prolog [] 2 ] ]. Lemma nonempty_th1 : (X:Type; x:X) (is_nonempty X). Intros. Unfold is_nonempty. Intros. Tauto. Save. Implicits nonempty_th1 [1]. Record virtual [X:Type] : Type :={ virtualP :> X -> Prop ; virtual_exists : (exists virtualP); virtual_unique : (x,y:X)(virtualP x) -> (virtualP y) -> (x == y) }. Syntactic Definition points := (virtualP ?). Tactic Definition Unvirtualize v := Match Context With [v : (virtual ?1) |- ?2 ] -> First [ (Poser exstat '(virtual_exists ?1 v)); (UseExists2 exstat); (Clear exstat) ]. Section virtual_map_def. Variables X,Y: Type. Variable f : X -> Y. Variable s : (virtual X). Local Q : Y -> Prop := [y:Y](exists [x:X](((f x) == y) /\ (points s x))). Remark rmk1 : (exists Q). Intro. Apply virtual_exists with v := s. Intros. Apply (H (f w)). Intro. Apply (H1 w). Tauto. Save. Remark rmk2 : (a,b:Y) (Q a) -> (Q b) -> (a == b). Intros. Apply NNPP. Intro. Apply H. Intros w (Hw, Sw). Apply H0. Intros u (Hu, Su). Apply H1. Rewrite <- Hw. Rewrite <- Hu. Apply congr_eqT with f := f. Apply virtual_unique with s; Assumption. Save. Definition virtual_map : (virtual Y) := (Build_virtual Y Q rmk1 rmk2). Lemma virtual_map_pr : (x:X)(points s x) -> (points virtual_map (f x)). Intros. Cut (Q (f x)). Intro. Exact H0. Unfold Q. Unfold exists. Intros. EApply (H0 x). Apply conj. Trivial. Exact H. Save. End virtual_map_def. Implicits virtual_map [1 2]. (***** here is the weak axiom of choice ****) Parameter virtual_choice : (X:Type)(is_nonempty X) -> (virtual X). Section extending_sections. Variable X:Type. Variable A : X -> Type. Hypothesis ne : (u:X)(is_nonempty (A u)). Variable x:X. Variable a:(A x). Hypothesis hyp : (sect : (y:X)(virtual (A y)))(points (sect x) a)-> False. Record extsectB [y:X] : Type :={ extsectBb : (A y); extsectBnot : (sect : (z:X)(virtual (A z)))(points (sect y) extsectBb) -> False }. Record extsectC [y:X] : Type := { extsectCc : (A y); extsectCmaybe : (is_nonempty (extsectB y)) -> (sect : (z:X)(virtual (A z)))(points (sect y) extsectCc) -> False }. Lemma lemma1 : (is_nonempty (extsectB x)). Intros. Unfold is_nonempty. Intros. Cut (extsectB x). Exact H. EApply (Build_extsectB x a). Trivial. Save. Lemma lemma2 : (z:X)(is_nonempty (extsectC z)). Intros. Unfold is_nonempty. Intro. Cut (is_nonempty (extsectB z)). Intro. Cut (extsectB z)->False. Intro. Exact (H0 H1). Intro. Cut (extsectC z). Exact H. EApply (Build_extsectC z (extsectBb z X0)). Intro. Exact (extsectBnot z X0). Unfold is_nonempty. Intro. Cut (A z)->False. Intro. Exact (ne z H1). Intro. Cut (extsectC z). Exact H. EApply (Build_extsectC z X0). Intro. Intros. Trivial. Exact (H1 H0). Save. Definition sectionC :(z:X)(virtual (extsectC z)):= [z:X](virtual_choice (extsectC z) (lemma2 z)). Definition sectionA : (z:X)(virtual (A z)) := [z:X](virtual_map (extsectCc z) (sectionC z)). Remark rmk3 : (c:(extsectC x))(points (sectionA x) (extsectCc x c)) -> False. Intros. EApply (extsectCmaybe x c lemma1 sectionA). Exact H. Save. Remark rmk4 : (c:(extsectC x))(points (sectionC x) c) -> False. Intros. EApply (rmk3 c). EApply (virtual_map_pr ? ? (extsectCc x) (sectionC x) c). Exact H. Save. Remark thm1 : False. Cut (c:(extsectC x))(points (sectionC x) c)->False. Intros. Cut (exists [c:(extsectC x)](points (sectionC x) c)). Unfold exists. Intros. Apply H0. Exact H. Exact (virtual_exists (extsectC x) (sectionC x)). Exact rmk4. Save. End extending_sections. Record section_extension [X: Type; A : X -> Type; x:X; a:(A x)] : Type :={ the_sect_extn : (u:X)(virtual (A u)); extn_property : (points (the_sect_extn x) a) }. Implicits the_sect_extn [1 2 3 4]. Theorem extension_theorem1 : (X:Type; A:X-> Type; x:X; a:(A x)) ((u:X)(is_nonempty (A u))) -> (is_nonempty (section_extension X A x a)). Intros. Unfold is_nonempty. Intros. Cut (sect:((z:X)(virtual (A z))))(points (sect x) a)->False. Intro. Exact (extending_sections.thm1 X A H x a H1). Intros. EApply H0. EApply (Build_section_extension X A x a sect). Exact H1. Save. Record property_extension [X:Type; A:X-> Type; x:X; P:(A x) -> Prop] : Type :={ the_prop_extn : (u:X)(A u) -> Prop; prop_extn_for : (a:(A x))(P a) -> (the_prop_extn x a); prop_extn_back : (a:(A x))(the_prop_extn x a) -> (P a) }. Implicits the_prop_extn [1 2 3 4]. Definition spp: (Y:Type)(virtual (Y -> Prop)) -> Y -> Prop := [Y:Type; s:(virtual (Y -> Prop));y:Y] (Q : Y -> Prop)(points s Q) -> (Q y). Section extending_properties. Variable X: Type. Variable A : X -> Type. Variable x:X. Variable P : (A x) -> Prop. Local R := [z:X](A z)-> Prop. Remark rmk1 : (z:X)(is_nonempty (R z)). Intros. Unfold is_nonempty. Intros. Cut (R z). Exact H. Unfold R. Intro. Exact False. Save. Section extpropA. Variable r : (section_extension X R x P). Local sectionr := (the_sect_extn r). Definition helpful_construction : (property_extension X A x P). EApply (Build_property_extension X A x P [u:X; a:(A u)] (spp (A u) (the_sect_extn r u) a) ). Intros. Unfold spp. Intros. Cut Q==P. Intros. Rewrite H1. Exact H. Cut (points (sectionr x) P). Intro. Exact (virtual_unique (R x) (sectionr x) Q P H0 H1). Exact (extn_property ? ? ? ? r). Intros. Unfold spp in H. EApply (H P). Exact (extn_property ? ? ? ? r). Defined. End extpropA. Theorem extension_theorem2 : (is_nonempty (property_extension X A x P)). Unfold is_nonempty. Intros. Cut (is_nonempty (section_extension X R x P)). Intros. Cut (section_extension X R x P)->False. Intros. Exact (H0 H1). Intro. Exact (H (helpful_construction X0)). EApply extension_theorem1. Exact rmk1. Save. End extending_properties. Definition spe : (X : Type; A : X -> Type ; x:X; P : (A x) -> Prop) (virtual (property_extension X A x P)) -> (property_extension X A x P). Intros X A x P s. EApply (Build_property_extension X A x P [u:X; a:(A u)](E : (property_extension X A x P))(points s E)-> (the_prop_extn E u a)). Intros. Prolog [prop_extn_for prop_extn_back] 5. Intros. EApply NNPP. Unfold not. Intro. Assert (doesnt_exist (virtualP (property_extension X A x P) s)). Unfold doesnt_exist. Intros. Sel '(H a0 H1). Apply H0. Apply prop_extn_back with X A x a0. Assumption. Assert (exists (virtualP (property_extension X A x P) s)). Exact (virtual_exists ? s). Exact (H2 H1). Defined. Section diagonal_property_extension. Variable X : Type. Variable A : X -> X -> Type. Variable P : (x:X)(A x x) -> Prop. Local dpe1 : (x:X)(property_extension X (A x) x (P x)). Intros. Cut (virtual (property_extension X (A x) x (P x))). Exact (spe ? ? ? ?). EApply virtual_choice. EApply extension_theorem2. Defined. Definition diag_prop_extn : (x,y:X)(A x y) -> Prop := [x,y:X] (the_prop_extn (dpe1 x) y). Lemma dpe_for : (x:X; a:(A x x))(P x a) -> (diag_prop_extn x x a). Intros. Unfold diag_prop_extn. Prolog [prop_extn_for] 5. Save. Lemma dpe_back : (x:X; a:(A x x))(diag_prop_extn x x a) -> (P x a). Intros. Unfold diag_prop_extn in H. Apply prop_extn_back with X (A x) x (dpe1 x). Assumption. Save. End diagonal_property_extension. (****************************************************************************) (*** now we define equality in a way which works for elements of any type ***) (****************************************************************************) (***** note that this is the same as C. McBride's JMeqT (the equivalence will be proven later on in the file) ***********************************) Record Term : Type := { the_type : Type; the_term : the_type }. Definition EQterm := [r,s: Term] (P : Term -> Prop) (P r) -> (P s). Syntactic Definition term := (Build_Term ?). (**** note that EQterm is Leibniz equality on terms ***************) Section EQterm_ref_proof. Variable r:Term. Section eqtermrefA. Variable P : Term -> Prop. Hypothesis hyp : (P r). Fact fact1 : (P r). Proof hyp. End eqtermrefA. Lemma EQterm_ref : (EQterm r r). Proof fact1. End EQterm_ref_proof. Section EQterm_sym_proof. Variables r,s: Term. Hypothesis hyp : (EQterm r s). Section eqtermsymA. Variable P : Term -> Prop. Hypothesis hr : (P s). Section eqtermsymB. Hypothesis contra : (not (P r)). Local Q : Term -> Prop := [u:Term] (not (P u)). Remark rmk1 : (Q r). Proof contra. Remark rmk2 : (Q s). Proof (hyp Q rmk1). Fact fact1 : False. Proof (rmk2 hr). End eqtermsymB. Remark rmk3 : (not (not (P r))). Proof fact1. Fact fact2 : (P r). Proof (excluded_middle (P r) rmk3). End eqtermsymA. Lemma EQterm_sym : (EQterm s r). Proof fact2. End EQterm_sym_proof. Section EQterm_trans_proof. Variables r,s,t: Term. Hypothesis hyp1 : (EQterm r s). Hypothesis hyp2 : (EQterm s t). Section eqtermtransA. Variable P : Term -> Prop. Hypothesis hr : (P r). Remark rmk1 : (P s). Proof (hyp1 P hr). Fact fact1 : (P t). Proof (hyp2 P rmk1). End eqtermtransA. Lemma EQterm_trans : (EQterm r t). Proof fact1. End EQterm_trans_proof. Definition EQ := [A,B: Type; a: A; b: B] (EQterm (term a) (term b)). Implicits EQ [1 2]. Lemma EQ_ref : (A: Type)(a: A)(EQ a a). Proof [A:Type; a:A] (EQterm_ref (term a)). Implicits EQ_ref [1]. Lemma EQ_sym : (A,B: Type)(a: A)(b:B)(EQ a b)-> (EQ b a). Proof [A,B: Type; a: A; b:B; hyp : (EQ a b)] (EQterm_sym (term a) (term b) hyp). Implicits EQ_sym [1 2 3 4]. Lemma EQ_trans : (A,B,C: Type) (a:A) (b:B) (c:C) (EQ a b) -> (EQ b c) -> (EQ a c). Proof [A,B,C: Type; a:A; b:B; c:C; hyp1 : (EQ a b); hyp2 : (EQ b c)] (EQterm_trans (term a) (term b) (term c) hyp1 hyp2). Implicits EQ_trans [1 2 3 4 5 6]. Lemma EQ_leib : (A : Type; a,b:A)(a == b) -> (EQ a b). Intros. Rewrite H. Exact (EQ_ref b). Save. Implicits EQ_leib [1 2 3]. (* Marco's Tactics for the reflexivity and symmetry property of [EQ]. *) Tactic Definition etRef := Apply EQ_ref. Tactic Definition etSym := Apply EQ_sym. (* Tactics for the transitivity property of [EQ]. *) Tactic Definition etTrans m := Match Context With [|- (!EQ ?1 ?2 ?3 ?4)] -> Apply (!EQ_trans ?1 ? ?2 ?3 m ?4). Tactic Definition Exact_EQ_ref := First [Exact (EQ_ref ?)]. Tactic Definition Exact_EQ_sym := Match Context With [id1 : (EQ ? ?) |- (EQ ? ?) ] -> First [Exact (EQ_sym id1)]. Tactic Definition Sym_EQ_trans u v := First [Exact (EQ_trans u v) | Exact (EQ_trans (EQ_sym u) v) | Exact (EQ_trans u (EQ_sym v)) | Exact (EQ_trans (EQ_sym u) v)]. Tactic Definition Exact_EQ_trans := Match Context With [id1 : (EQ ? ?); id2 : (EQ ? ?) |- (EQ ? ?) ] -> First [Sym_EQ_trans id1 id2]. Tactic Definition SymOne := Match Context With [id1 : (EQ ? ?) |- ?] -> First [Exact (EQ_sym id1)] | [id1 : (EQ ?1 ?2) |- ?] -> First [ (Assert (EQ ?2 ?1);First [Assumption|Idtac]); [Exact (EQ_sym id1)|Idtac] ]. Tactic Definition Transform_EQ := Match Context With [id1 : (?1 == ?2) |- ?] -> First [ (Assert (EQ ?1 ?2); First [Assumption |Idtac]); [Exact (EQ_leib id1) | Idtac] ]. Tactic Definition Sym9 := First[(Do 9 (Try Transform_EQ)); (Do 9 (Try SymOne))]. Tactic Definition Sym15 := First[ (Do 15 (Try Transform_EQ)); (Do 15 (Try SymOne))]. Definition pointEQ := EQ. Implicits pointEQ [1 2]. Tactic Definition TransStart := Match Context With [|-(EQ ?1 ?)] -> First [Assumption | Exact_EQ_ref | Assert (pointEQ ?1 ?1); [Exact (EQ_ref ?1) | Idtac] ]. Tactic Definition TransNext := Match Context With [id1 : (pointEQ ?1 ?2); id2 : (EQ ?2 ?3) |- ?] -> First [Exact (EQ_trans id1 id2) | (Assert (pointEQ ?1 ?3);First [ (Match Context With [id1 : (pointEQ ? ?)|- ?]-> First [Exact id1]) |Idtac]); [Exact (EQ_trans id1 id2)|Idtac] ] | [id1 : (pointEQ ?1 ?); id2 : (EQ ? ?2) |- ?]-> First [ Exact (EQ_trans id1 id2) | (Assert (EQ ?1 ?2);First [ (Match Context With [id1 : (pointEQ ? ?)|- ?]-> First [Exact id1]) |Idtac]); [Exact (EQ_trans id1 id2)|Idtac] ]. Tactic Definition Trans9 := Try Sym9; Try TransStart; Do 9 (Try TransNext). Tactic Definition Trans15 := Try Sym15; Try TransStart; Do 15 (Try TransNext). (* Section trans9_test. Variable X : Type. Variables x,y,z,w,a,b,c,d,e,f,g : X. Hypothesis h1 : (EQ x y). Hypothesis h2 : (EQ c b). Hypothesis h3 : (EQ a b). Hypothesis h4 : (EQ w a). Hypothesis h5 : (EQ w z). Hypothesis h6 : (EQ z y). Hypothesis h7 : (EQ d c). Hypothesis h8 : (EQ d e). Hypothesis h9 : (EQ f e). Hypothesis h10 : (EQ g f). Remark rmk0 : (EQ x b). Trans9. Save. Remark rmk1 : (EQ x f). Trans9. Save. (*** in 3.85 seconds nov 2001 Coq 7.1 on math4 at Nice ***) End trans9_test. *) (*** here is a different approach where we specify the sequence of objects ***) Tactic Definition SymTrans := First [Assumption | Exact_EQ_ref |Exact_EQ_sym | Exact_EQ_trans]. Tactic Definition TransBridge3 a b c:= (Assert span1 : (EQ a b);[SymTrans | Idtac]); (Assert span2 : (EQ b c) ; [SymTrans |Idtac]); First [Assert (EQ a c); [Exact (EQ_trans span1 span2)|Clear span1; Clear span2] | Exact (EQ_trans span1 span2)]; (Try Assumption). (**** note that this won't work if any of the span assertions are actually the goal ****) Tactic Definition TransBridge4 a b c d := (TransBridge3 a b c); (TransBridge3 a c d). Tactic Definition TransBridge5 a b c d e := (TransBridge3 a b c); (TransBridge3 c d e); (TransBridge3 a c e). Tactic Definition TransBridge6 a b c d e f := (TransBridge3 a b c); (TransBridge3 c d e); (TransBridge3 c e f); (TransBridge3 a c f). Tactic Definition TransBridge7 a b c d e f g := (TransBridge3 a b c); (TransBridge3 c d e); (TransBridge3 e f g); (TransBridge3 a e g). (********************************************************************** *** our EQ above is the same as the Type version of what is called *** JMeq in the file JMeq.v (in Logic). In that file, an axiom *** JMeq_eq was required. Here, using the axiom of choice, we prove *** that statement. **********************************************************************) Section term_prop_extension. Variable T: Type. Variable P : T -> Prop. Local A :Type -> Type := [X:Type]X. Local Extns := (property_extension Type A T P). Remark rmk1 : (is_nonempty Extns). Exact (extension_theorem2 Type A T P). Save. Section term_prop_extnA. Variable E : Extns. Definition term_prop_extn_out : Term -> Prop := [u:Term](the_prop_extn E (the_type u) (the_term u)). Local Q := term_prop_extn_out. Remark rmk2 : (t:T)(P t) -> (Q (term t)). Intros. Exact (prop_extn_for ? ? ? ? E t H). Save. Remark rmk3 : (t:T)(Q (term t)) -> (P t). Intros. Exact (prop_extn_back ? ? ? ? E t H). Save. End term_prop_extnA. Remark rmk4 : (exists [Q:Term -> Prop](t:T)(((P t) -> (Q (term t)))/\ ((Q (term t)) -> (P t)))). Unfold exists. Intros. Cut Extns->False. Intro. Sel rmk1. Exact (H1 H0). Intro. EApply (H (term_prop_extn_out X)). Intro. Apply conj. Exact (term_prop_extnA.rmk2 X t). Exact (term_prop_extnA.rmk3 X t). Save. End term_prop_extension. Lemma extend_prop_to_term : (T:Type; P:T -> Prop) (exists [Q:Term -> Prop](t:T)(((P t) -> (Q (term t)))/\ ((Q (term t)) -> (P t)))). Proof term_prop_extension.rmk4. Theorem EQ_subs : (A: Type) (a,b:A) (P: A -> Prop) (P a) -> (EQ a b) -> (P b). Intros. Sel '(extend_prop_to_term A P). UseExists H1. Apply H2. Sel '(H3 a). Unfold EQ in H0. Unfold EQterm in H0. Sel '(H0 a0). Assert (a0 (term a)). Exact (proj1 ? ? H4 H). Sel '(H5 H6). Sel '(H3 b). Exact (proj2 ? ? H8 H7). Save. Implicits EQ_subs [1 2 3]. Tactic Definition Exact_EQ_subs := Match Context With [id1 : ?; id2 : ? ; id3 : (EQ ? ?) |- ?]-> First [Exact (EQ_subs id1 id2 id3) | Exact (EQ_subs id1 id2 (EQ_sym id3))]. (********************************************************************** *** The other half of the statement that EQ restricts to Leibniz *** equality is provided by the following lemma. **********************************************************************) Section EQ_leibniz_proof. Variable A : Type. Variables a,b : A. Hypothesis hyp : ((P : A -> Prop) (P a) -> (P b)). Section eqliebA. Variable Q : Term -> Prop. Variable ha : (Q (term a)). Local P : A -> Prop := [x:A](Q (term x)). Remark rmk1 : (P a). Proof ha. Remark rmk2 : (P b). Proof (hyp P rmk1). Fact fact1 : (Q (term b)). Proof rmk2. End eqliebA. Lemma EQ_leibniz_out : (EQterm (term a) (term b)). Proof fact1. End EQ_leibniz_proof. Lemma EQ_leibniz : (A : Type; a,b: A) ((P : A -> Prop) (P a) -> (P b))-> (EQ a b). Proof EQ_leibniz_out. Implicits EQ_leibniz [1]. Lemma EQ_eq : (A:Type; a,b : A)(EQ a b) -> (a == b). Intros. Poser P '([x:A]a==x). Assert (P a). Unfold P. Tauto. Exact_EQ_subs. Save. Implicits EQ_eq [1 2 3]. Tactic Definition etRewrite v x y := (Assert rega : x == y ; [Exact (EQ_eq v)|Idtac]); First [ Rewrite -> rega ; Assumption | Rewrite <- rega ; Assumption ]; Clear rega. Tactic Definition etReRe := Match Context With [id1 : (EQ ?1 ?2) |- ? ]-> First [etRewrite id1 '(?1) '(?2)]. Tactic Definition etPlug := Match Context With [ |- (EQ ?1 ?2)] -> Assert (EQ ?1 ?1); [Exact_EQ_ref | etReRe]. Tactic Definition RewriteB v := First [(Rewrite v) | (Rewrite<- v)]. (********************************************************************** *** The most useful version of the substitution property is the *** following one. **********************************************************************) Section EQ_plug_proof. Variables A,B: Type. Variables x,y:A. Variable f:A -> B. Hypothesis hyp : (EQ x y). Lemma EQ_plug : (EQ (f x) (f y)). etPlug. Save. End EQ_plug_proof. Implicits EQ_plug [1 2 3 4]. (*************************************************************************) (****************** proof irrelevance ********************************) (*************************************************************************) Theorem proof_irrelevance : (P: Prop; p,q: P)(EQ p q). Intros. Assert p==q. EApply classical_proof_irrelevence. Intro. Apply classic. Elim H. Exact (EQ_ref ?). Save. Implicits proof_irrelevance [1]. Tactic Definition Exact_pi := First [Exact (proof_irrelevance ? ?)]. (*** the following "axiom" follows from some stuff in Ensembles.v; we rename it for convenience and emphasis *****) Lemma Prop_uni : (P,Q : Prop) (P-> Q) -> (Q -> P) -> (EQ P Q). Intros. Poser P1 '[t:UnitT]P. Poser Q1 '[t:UnitT]Q. Assert (Same_set UnitT P1 Q1). Unfold Same_set. Apply conj. Unfold Included. Unfold In. Unfold P1. Unfold Q1. Intro t. Exact H. Unfold Included. Unfold In. Unfold Q1. Unfold P1. Intro t. Exact H0. Assert P1==Q1. Apply (Extensionality_Ensembles UnitT). Trivial. Assert (P1 IT)==(Q1 IT). Elim H2. Trivial. Assert P==Q. Exact H3. Elim H4. Exact (EQ_ref ?). Save. Implicits Prop_uni [1 2]. Tactic Definition Exact_Prop_uni := Match Context With [id1 : ? ; id2 : ? |- ?] -> First [Exact (Prop_uni id1 id2)]. (********************************************************************** *** Extensionality (1) : we show that with Gilles Kahn's axiom *** we get extensionality for Prop *** this is optional since we will actually assume the full extensionality *** later. **********************************************************************) Lemma prop_extens : (A:Type; P,Q : A -> Prop)((a:A)(EQ (P a) (Q a))) -> (EQ P Q). Intros. Assert (Same_set A P Q). Unfold Same_set. Apply conj. Unfold Included. Unfold In. Intro. Sel '(H x). Assert (P x) -> (P x). Trivial. etReRe. Unfold Included. Unfold In. Intro. Sel '(H x). Assert (P x) -> (P x). Trivial. etReRe. Assert (P == Q). Apply (Extensionality_Ensembles A). Trivial. Rewrite H1. Apply EQ_ref. Save. Implicits prop_extens [1 2 3]. (*** unfortunately the following generates a universe inconsistency: Lemma virtual_extens : (A,B: Type)(f,g:A -> (virtual B)) ((a:A)(EQ (f a) (g a))) -> (EQ f g). *** this means that in the course of the above proofs we have constrained *** the type of virtual X to be bigger than the type allowed in EQ; *** in particular we shouldnt really use virtual. We could redefine it *** but this would require redefining at each universe level. Instead *** we use a notion of is_fibrant and then create a tactic which *** enables us to use that ... (???) ******) Inductive emptyT : Type := . Section empty_initial_def. Variable A : Type. Definition empty_initial : emptyT -> A := [x:emptyT] <[u:emptyT]A> Cases x of end. End empty_initial_def. Lemma empty_empty : (is_empty emptyT). Unfold is_empty. Intro x. Elim x. Save. Record has_one_element [X:Type]:Prop := { one_nonempty : (is_nonempty X); one_unique : (x,y:X)(EQ x y) }. Implicits one_nonempty [1]. Implicits one_unique [1]. Tactic Definition Use_has_one_element := Match Context With [id1 : (has_one_element ?) |- ?]-> First [Exact (one_nonempty id1) ] | [id1 : (has_one_element ?) |- (EQ ?1 ?2)] -> First [Exact (one_unique id1 ?1 ?2)]. Tactic Definition Show_has_one_element := Match Context With [ |- (has_one_element ?1)]-> Try (EApply (Build_has_one_element ?1)). Definition compose_functions := [A,B,C: Type; F: B-> C; G: A -> B]([a:A](F (G a))). Implicits compose_functions [1 2 3]. Tactic Definition Show_existsA := Match Context With [|- (exists ?)] -> First [Unfold exists; Unfold not; Unfold doesnt_exist; Intros]. Tactic Definition Show_exists := Match Context With [id1 : ? |- (exists ?1)] -> First [Exact (exists_th1 ?1 id1)] | [id1 : ?; id2 : ? |- (exists ?1)]-> First [Exact (!exists_th1 ? id1 ?1 id2)] | [|- (exists ?)] -> First [Unfold exists; Unfold not; Unfold doesnt_exist; Intros]. (*********** SetOf ***************************************) Record SetOf [A: Type; P : A -> Prop] : Type := { the_element : A; the_property : (P the_element) }. Implicits SetOf [1]. Syntactic Definition generalize := (the_element ? ?). Syntactic Definition specialize := (Build_SetOf ? ?). Syntactic Definition generalize_pr := (the_property ? ?). Lemma set_of_univ_spec : (X:Type; P:X->Prop)(EQ (SetOf P) (SetOf P)). Proof [X:Type; P:X->Prop](EQ_ref (SetOf P)). Tactic Definition Create_SetOf := Match Context With [id1 : ? ; id2 : ? |- ?] -> First [Exact (specialize id1 id2)]. Record BigSetOf [A: Type; P : A -> Prop] : Type := { the_element_big : A; the_property_big : (P the_element_big) }. Tactic Definition Create_BigSetOf := Match Context With [id1 : ? ; id2 : ? |- ?] -> First [Exact (Build_BigSetOf ? ? id1 id2)]. Lemma spec_gen_eq : (A:Type; P: A-> Prop; x:(SetOf P)) (EQ (specialize (generalize x) (generalize_pr x)) x). Intros. Elim x. Intros. EApply EQ_ref. Save. Implicits spec_gen_eq [1 2]. Lemma gen_spec_eq : (A:Type; P: A-> Prop; a:A; p: (P a)) (EQ (generalize (specialize a p)) a). Intros. EApply EQ_ref. Save. Implicits gen_spec_eq [1 2]. Theorem specialize_inj : (A: Type; P:A->Prop;x,y:A; p:(P x); q:(P y))(specialize x p) == (specialize y q) -> x == y. Intros. Assert (generalize (specialize x p)) == (generalize (specialize y q)). Rewrite H. Trivial. Exact H0. Save. Section generalize_inj_proof. Variable A:Type. Variable P:A -> Prop. Local S := (SetOf P). Local g : S -> A := [x:S](generalize x). Remark rmk1 : (x:S)(P (g x)). Intro. Exact (generalize_pr x). Save. Variables x,y:S. Hypothesis hyp : (g x) == (g y). Local QQ : A -> Prop := [a:A]((p:(P a))(specialize a p)== x). Remark rmk2 : (QQ (g x)). Unfold QQ. Intros. Assert (EQ (specialize (g x) (generalize_pr x)) x). Exact (spec_gen_eq x). Assert (p == (generalize_pr x)). EApply EQ_eq. EApply proof_irrelevance. Rewrite H0. EApply EQ_eq. Assumption. Save. Remark rmk3 : (QQ (g y)). Assert (QQ (g x)). Exact rmk2. Rewrite<- hyp. Assumption. Save. Remark rmk4 : (specialize (g y) (generalize_pr y)) == y. EApply EQ_eq. Exact (spec_gen_eq y). Save. Theorem generalize_inj_out : (x == y). Assert (QQ (g y)). Exact rmk3. Unfold QQ in H. Assert (specialize (g y) (generalize_pr y))== x. Exact (H (generalize_pr y)). Rewrite<- H0. Exact rmk4. Save. End generalize_inj_proof. Theorem generalize_inj : (A:Type; P:A-> Prop; x,y:(SetOf P)) (generalize x) == (generalize y) -> x == y. Exact generalize_inj_out. Save. (****** now we define description *******) Definition singleton : (X:Type)X-> (virtual X). Intros X x. EApply (Build_virtual X [y:X](y == x)). Exhibit x. Trivial. Intros. EApply EQ_eq. Trans9. Defined. Implicits singleton [1]. Theorem singleton_points : (X:Type; x:X)(points (singleton x) x). Intros. Unfold virtualP. Compute. Trivial. Save. Theorem singleton_points_only : (X:Type; x,y:X)(points (singleton x) y) -> (EQ x y). Intros. Assert (points (singleton x) x). EApply singleton_points. EApply EQ_leib. EApply virtual_unique with (singleton x). Assumption. Assumption. Save. Syntactic Definition upre_description := [X:Type](P:X-> Prop; e:(exists P);u:(x,y:X)(P x) -> (P y) -> (x ==y))X. Syntactic Definition pre_chfn := [X:Type](P:X->Prop) (exists P) -> X. Definition is_description := [X:Type; s:(upre_description X)] (P:X->Prop; e:(exists P);u:(x,y:X)(P x) -> (P y) -> (x ==y))(P (s P e u)). Definition is_chfn := [X:Type; s:(pre_chfn X)] (P:X->Prop; e:(exists P))(P (s P e)). Implicits is_description [1]. Implicits is_chfn [1]. Record >description [X:Type] : Type := { descrip_pre :> (upre_description X); descrip_descrip : (is_description descrip_pre) }. Implicits descrip_descrip [1]. Definition descrip_fun :(X:Type; s:(description X)) (virtual X) -> X. Intros X s v. Sel '(descrip_pre X s). EApply (H v). EApply virtual_exists. Intros. Exact (virtual_unique X v x y H0 H1). Defined. Implicits descrip_fun [1]. Theorem descrip_fun_points :(X:Type; s:(description X); v:(virtual X)) (points v (descrip_fun s v)). Intros. Assert (is_description s). EApply (descrip_descrip). Unfold is_description in H. Unfold descrip_fun. EApply (H v). Save. Definition Create_predescription : (X:Type; c : (pre_chfn X)) (upre_description X). Intros. Cbv Beta. Intros. EApply (c P). Assumption. Defined. Definition Create_description : (X: Type; c: (pre_chfn X); i: (is_chfn c))(description X). Intros. EApply (Build_description X (Create_predescription X c)). Unfold Create_predescription. Unfold is_description. Intros. Unfold is_chfn in i. EApply i. Defined. (***** the above was slightly twisted but it means that if we want to include a data type description in an object we can actually include s:(pre_description X) then h:(is_description s); now h is coerced to (description X); however the pair (s, h) has the same universe level as X rather than the fixed (much higher) universe level of the type description. ****) (**** we use the axiom virtual_choice to refine a property with existence, to one with existence and uniqueness ****) Section refine_def. Variable X : Type. Variable P : X -> Prop. Hypothesis e : (exists P). Remark rmk1 : (is_nonempty (SetOf P)). Unfold is_nonempty. Intros. UseExists2 e. EApply H. Exact (specialize a H0). Save. Local V : (virtual (SetOf P)). EApply virtual_choice. Exact rmk1. Defined. Definition refine_out : X -> Prop. Intro x. Exact (exists [pr:(P x)](points V (specialize x pr))). Defined. Theorem refine_ex_out : (exists (refine_out)). Unfold refine_out. Assert (exists [y:(SetOf P)](V y)). Exact (virtual_exists (SetOf P) V). UseExists2 H. Exhibit '(generalize a). Exhibit '(generalize_pr a). Assert (specialize (generalize a) (generalize_pr a)) == a. EApply EQ_eq. Exact (spec_gen_eq a). Rewrite H1. Assumption. Save. Theorem refine_pr_out : (x:X)(refine_out x) -> (P x). Intros. Unfold refine_out in H. UseExists2 H. Exact a. Save. Theorem refine_uni_out : (x,y:X)(refine_out x) -> (refine_out y) -> x == y. Intros. Unfold refine_out in H. Unfold refine_out in H0. UseExists2 H. UseExists2 H0. Assert (specialize x a) == (specialize y a0). EApply (virtual_unique (SetOf P) ? ? ? H1 H2). EApply (specialize_inj X P x y a a0). Assumption. Save. End refine_def. Definition refine : (X:Type; P:X->Prop; e:(exists P))X->Prop. Exact refine_out. Defined. Implicits refine [1]. Theorem refine_pr : (X:Type; P:X -> Prop; e:(exists P)) (x:X)(refine P e x) -> (P x). Proof refine_pr_out. Theorem refine_uni : (X:Type; P:X->Prop; e:(exists P)) (x,y:X)(refine P e x) -> (refine P e y) -> x == y. Proof refine_uni_out. Theorem refine_ex : (X:Type; P:X->Prop; e:(exists P)) (exists (refine P e)). Proof refine_ex_out. Section choice_def. Variable X:Type. Variable P : X -> Prop. Variable de : (description X). Hypothesis e : (exists P). Local pre:(upre_description X) := (descrip_pre X de). Local pre_des : (is_description pre) := (descrip_descrip de). Local RP := (refine P e). Remark rmk1 : (exists RP). Exact (refine_ex X P e). Save. Remark rmk2 : (x,y:X)(RP x) -> (RP y) -> x == y. Proof (refine_uni X P e). Definition choice_out : X. EApply (pre RP). Exact rmk1. Exact rmk2. Defined. Remark rmk3 : (P choice_out). Assert (RP choice_out). Unfold choice_out. EApply pre_des. Unfold choice_out. EApply (refine_pr X P e). Exact H. Save. End choice_def. (**** the object description A is essentially a choice function ****) Definition choice : (A: Type) (P: A -> Prop) (de:(description A)) (e: (exists P))A. Intros. Exact (choice_out A P de e). Defined. Implicits choice [1 2]. Lemma choice_pr1 : (A:Type)(P: A->Prop) (de:(description A))(e: (exists P)) (P (choice de e)). Intros. EApply (choice_def.rmk3 A P). Save. Implicits choice_pr1 [1 2]. Tactic Definition SoChoose u v := Match Context With [id1 : ? ; id2 : ? |- ? ] -> First [ Poser u '(!choice ? v id1); Assert (v u); [Exact (choice_pr1 id1 id2)|Idtac]]. Record exists_unique [X:Type; P: X -> Prop]: Prop :={ exists_unique_exists :> (exists P); exists_unique_unique : (u,v: X) (P u) -> (P v)-> (EQ u v) }. Implicits exists_unique [1]. Implicits exists_unique_exists [1 2]. Implicits exists_unique_unique [1 2 4 5]. Tactic Definition By_unicity := Match Context With [id1 : ?; id2: ?; id3 : ? |- (EQ ? ?) ] -> First [Exact (exists_unique_unique id1 id2 id3)]. Definition described_choice : (X:Type)(is_nonempty X)->(description X) -> X. Intros. EApply descrip_fun. Assumption. EApply virtual_choice. Assumption. Defined. Implicits described_choice [1]. Definition pre_described_choice : (X:Type)(is_nonempty X)-> (upre_description X) -> X. Intros X h sp. Assert v :(virtual X). EApply virtual_choice. Assumption. EApply (sp v). EApply virtual_exists. Intros. Exact (virtual_unique X v x y H H0). Defined. Tactic Definition Choose u v := Match Context With [id1 : ?; id2 : ? |- ? ] -> First [((Assert u : v);[Exact (described_choice id1 id2) | Idtac])] | [id1 : ?; id2 : ? |- ? ] -> First [((Assert u : v);[Exact (pre_described_choice id1 id2) | Idtac])]. Definition is_fibrant := [X:Type](is_nonempty (description X)). Tactic Definition DescribeFibrants_1 := Match Context With [id1 : (is_fibrant ?1) |- ?] -> First [(Unfold is_fibrant in id1); (UseNonempty id1)]. Tactic Definition DescribeFibrants := Do 15 (Try DescribeFibrants_1). (********************************************************************** *** Extensionality: the following axiom says that functions *** (or more generally elements of dependent products) *** are determined by their values. *** for now we assume this; otherwise we get into more complicated *** stuff where we need to use description to prove extensionality *** with values in the thing which is being specified. **********************************************************************) Axiom extensionality : (A:Type) (F:A-> Type) (x,y: (a:A)(F a)) ((a:A)(x a)== (y a)) -> x == y. Theorem extens : (A:Type) (F:A-> Type) (x,y: (a:A)(F a)) ((a:A)(EQ (x a) (y a))) -> (EQ x y). Intros. EApply EQ_leib. EApply extensionality. Intro. EApply EQ_eq. EApply H. Save. Implicits extens [1]. (** either A or F has to be in the context, as well as the hypothesis of course ***) Tactic Definition Exact_extensA := Match Context With [id1 : ? ; id2 : ? |- (EQ ?1 ?2)] -> First [Exact (extens id1 ?1 ?2 id2) | Exact (!extens id1 ? ?1 ?2 id2)]. (************************************************************************) (************************************************************************) (************************************************************************) (********** end of axioms and parameters : check that the words Axiom or Parameter don't occur below *********************************************) (************************************************************************) (************************************************************************) (************************************************************************) (************************************************************************) (**** using this we prove extensionality for mapping types which are special cases of dependent products ***********************************************) Section Extens_proof. Variable A : Type. Variables F,G : A -> Type. Variable f : (a:A)(F a). Variable g : (a:A)(G a). Hypothesis eq : (a:A)(EQ (f a) (g a)). Remark rmk1 : (a:A)(F a) == (G a). Intro. Assert (EQ (f a) (g a)). EApply eq. Unfold EQ in H. Unfold EQterm in H. Sel '(H [t:Term]( (F a)== (the_type t))). EApply H0. Trivial. Save. Remark rmk2 : F == G. EApply (!extensionality A [a:A]Type F G). Intro. Exact (rmk1 a). Save. Remark rmk3 : (F', G' : A -> Type; hyp : F' == G'; f':(a:A)(F' a); g' : (a : A)(G' a); eq' : (a:A)(EQ (f' a) (g' a))) (EQ f' g'). Intros F1 G1. Intro hyp. NewInduction hyp. Intros. EApply (!extens A F1 f' g'). Assumption. Save. Remark rmk4 : (EQ f g). EApply rmk3. Exact rmk2. Assumption. Save. End Extens_proof. Theorem Extens : (A: Type; F,G : A -> Type; f: (a:A)(F a); g: (a : A)(G a); hyp : (a:A)(EQ (f a) (g a)))(EQ f g). Proof Extens_proof.rmk4. Section extens_indep_proof. Variables A,B:Type. Variables f,g: A-> B. Hypothesis e : ((a:A)(EQ (f a) (g a))). Lemma extens_indep : (EQ f g). Sel '([x:A]B). Exact_extensA. Save. End extens_indep_proof. Implicits extens_indep [1 2]. Theorem extens_indep1 : (A,B: Type; f,g:A->B) ((a:A)(f a) == (g a)) -> f == g. Intros. EApply EQ_eq. EApply extens_indep. Intros. EApply EQ_leib. Exact (H a). Save. Implicits extens_indep1 [1 2]. Section Extens_indep_proof. Variables A,B,C:Type. Variable f : A -> B. Variable g : A -> C. Hypothesis e : ((a:A)(EQ (f a) (g a))). Lemma Extens_indep : (EQ f g). Exact (!Extens A [x:A]B [x:A]C f g e). Save. End Extens_indep_proof. Implicits Extens_indep [1 2 3]. Tactic Definition Exact_extens_indep := Match Context With [id1 : ? |- (EQ ?1 ?2)]-> First [Exact (extens_indep ?1 ?2 id1)] | [id1 : ? |- (?1 == ?2)]-> First [Exact (extens_indep1 ?1 ?2 id1)]. Tactic Definition Exact_extens := First [Exact_extens_indep | Exact_extensA]. Tactic Definition Exact_nonempty_th1 := Match Context With [id1 : ? |- ?] -> First [Exact (nonempty_th1 id1)]. Tactic Definition Show_nonempty := Match Context With [|- (is_nonempty ?)] -> First [Exact_nonempty_th1 | Unfold is_nonempty; Intros; Unfold not; Intros]. Record good_subtype : Type := { gst_container: Type ; gst_subtype : Type; gst_injection : gst_subtype -> gst_container; gst_retraction : (x:gst_container; e : (exists [y:gst_subtype]((gst_injection y) == x)))gst_subtype; gst_injection_inj : (x,y:gst_subtype) (gst_injection x) == (gst_injection y) -> (x == y); gst_retraction_retr : (x:gst_container; e : (exists [y:gst_subtype]((gst_injection y) == x))) (gst_injection (gst_retraction x e)) == x }. Section gst_description_def. Variable G : good_subtype. Local X := (gst_container G). Local S := (gst_subtype G). Local f := (gst_injection G). Local r := (gst_retraction G). Remark rmk1 : (x,y :S)(f x) == (f y) -> x == y. Intros. EApply (gst_injection_inj G). Assumption. Save. Remark rmk2 : (x:X; e:(exists [y:S](f y) == x)) (f (r x e)) == x. Intros. Unfold f. Unfold r. EApply (gst_retraction_retr G). Save. Variable de : (description X). Section gst_desc2. Variable P : S -> Prop. Hypothesis hyp : (exists P). Local QQ : X -> Prop := [x:X](exists [y:S]((P y)/\(f y)==x)). Remark rmk1 : (exists QQ). UseExists2 hyp. Exhibit '(f a). Unfold QQ. Exhibit 'a. EApply conj. Assumption. Trivial. Save. Local x : X := (choice de rmk1). Remark rmk2 : (QQ x). Exact (choice_pr1 de rmk1). Save. Remark rmk3 : (exists [y:S](f y)==x). Assert (QQ x). Exact rmk2. Unfold QQ in H. UseExists2 H. Exhibit 'a. EApply (proj2 ? ? H0). Save. Local z : S := (r x rmk3). Remark rmk4 : (P z). Assert (QQ x). Exact rmk2. Unfold QQ in H. UseExists2 H. Assert (z == a). EApply (gst_injection_inj G). Assert (f a) == x. EApply (proj2 ? ? H0). Assert (f z) == x. Unfold r in z. Exact (gst_retraction_retr G x rmk3). Transitivity x. Assumption. Trivial. Rewrite<- H1. Trivial. Rewrite H1. Exact (proj1 ? ? H0). Save. Definition gst_predescription := z. End gst_desc2. Definition gst_description_out : (description S). EApply (Create_description S gst_predescription). Unfold is_chfn. Intros. EApply (gst_desc2.rmk4 P e). Save. End gst_description_def. Definition gst_description : (G:good_subtype)(description (gst_container G))-> (description (gst_subtype G)). Exact gst_description_out. Defined. Section SetOf_good_subtype_def. Variable A:Type. Variable P : A -> Prop. Local S:= (SetOf P). Local f:= [y:S](generalize y). Section SOgst2. Variable a:A. Hypothesis hyp : (exists [y:S](f y) == a). Remark rmk1 : (P a). UseExists2 hyp. Rewrite<- H. Exact (generalize_pr a0). Save. Definition SOgst2_out : S := (specialize a rmk1). Remark rmk2 : (f SOgst2_out) == a. EApply EQ_eq. Exact (gen_spec_eq a rmk1). Save. End SOgst2. Definition SetOf_gst : good_subtype. EApply (Build_good_subtype A (SetOf P) [x:(SetOf P)](generalize x) [a:A; e : (exists [y:S](f y) == a)](SOgst2_out a e)). Intros. EApply generalize_inj. Assumption. Intros. EApply SOgst2.rmk2. Defined. End SetOf_good_subtype_def. Definition SetOf_good_subtype : (A:Type; P:A-> Prop)good_subtype. Exact SetOf_gst. Defined. Definition SetOf_description : (A:Type; P:A -> Prop; de : (description A)) (description (SetOf P)). Intros. Sel '(SetOf_good_subtype A P). EApply (gst_description H). Exact de. Defined. (******** a useful gadget ****************) Definition type_of := [A:Type; a:A]A. Implicits type_of [1]. (******** transporting between two types that are equal ********) (**** in this part, we leave the explicit proofs of the main results for clarity ********) Section transport_def. Variables X,Y: Type. Variable de : (description Y). Hypothesis hyp : (EQ X Y). Variable x : X. Local Q := [Z:Type](exists ([z:Z](EQ x z))). Remark rmk1 : (EQ x x). Proof (EQ_ref x). Remark rmk2 : (exists ([z:X](EQ x z))). Proof (exists_th1 ([z:X](EQ x z)) rmk1). Remark rmk3 : (Q X). Proof rmk2. Remark rmk4 : (Q Y). Proof (EQ_subs Q rmk3 hyp). Remark rmk5 : (exists ([y:Y](EQ x y))). Proof rmk4. Definition transport : Y := (choice de rmk5). Lemma transport_eq: (EQ x transport). Proof (choice_pr1 de rmk5). End transport_def. Implicits transport [1 2]. Implicits transport_eq [1 2]. (*** we need an equality that is above Term ****) Definition EQtype := [A,B: Type] (P : Type -> Prop) (P A) -> (P B). Section EQtype_ref_proof. Variable A:Type. Variable P: Type -> Prop. Hypothesis hyp : (P A). Lemma EQtype_ref_out : (P A). Proof hyp. End EQtype_ref_proof. Lemma EQtype_ref : (A:Type) (EQtype A A). Proof EQtype_ref_out. Section bigtransport_def. Variables X,Y: Type. Variable de : (description Y). Hypothesis hyp : (EQtype X Y). Variable x : X. Local Q := [Z:Type](exists ([z:Z](EQ x z))). Remark rmk1 : (EQ x x). Proof (EQ_ref x). Remark rmk2 : (exists ([z:X](EQ x z))). Proof (exists_th1 ([z:X](EQ x z)) rmk1). Remark rmk3 : (Q X). Proof rmk2. Remark rmk4 : (Q Y). Proof (hyp Q rmk3). Remark rmk5 : (exists ([y:Y](EQ x y))). Proof rmk4. Definition bigtransport : Y := (choice de rmk5). Lemma bigtransport_eq: (EQ x bigtransport). Proof (choice_pr1 de rmk5). End bigtransport_def. Implicits bigtransport [1 2]. Implicits bigtransport_eq [1 2]. Definition prop_upredescrip : (upre_description Prop). Cbv Beta. Intros. Exact (X:Prop)(P X) -> X. Defined. Definition prop_description : (description Prop). EApply (Build_description Prop prop_upredescrip). Unfold is_description. Intros. UseExists2 e. Apply NNPP. Unfold not. Intros. Assert (prop_upredescrip P e u) == a. EApply EQ_eq. EApply Prop_uni. Unfold prop_upredescrip. Intros. EApply H1. Assumption. Unfold prop_upredescrip. Intros. Assert a == X. EApply u. Assumption. Assumption. Rewrite<- H3. Assumption. EApply H0. Rewrite H1. Assumption. Defined. Definition proof_upredescrip : (P:Prop)(upre_description P). Intros. Cbv Beta. Intros. UseExists2 e. Exact a. Defined. Definition proof_description : (P:Prop)(description P). Intro. EApply (Build_description P (proof_upredescrip P)). Unfold is_description. Intros. UseExists2 e. Assert a == (proof_upredescrip P P0 e u). EApply EQ_eq. EApply proof_irrelevance. Rewrite<- H0. Assumption. Defined. Section proptransport_def. Variables X,Y: Prop. Hypothesis hyp : (EQ X Y). Variable x : X. Local Q := [Z:Prop](exists ([z:Z](EQ x z))). Local de : (description Y) := (proof_description Y). Remark rmk1 : (EQ x x). Proof (EQ_ref x). Remark rmk2 : (exists ([z:X](EQ x z))). Proof (exists_th1 ([z:X](EQ x z)) rmk1). Remark rmk3 : (Q X). Proof rmk2. Remark rmk4 : (Q Y). Proof (EQ_subs Q rmk3 hyp). Remark rmk5 : (exists ([y:Y](EQ x y))). Proof rmk4. Definition proptransport : Y := (choice de rmk5). Remark rmk6 : (EQ x proptransport). Proof (choice_pr1 de rmk5). End proptransport_def. Implicits proptransport [1 2]. Lemma proptransport_eq : (X,Y: Prop)(hyp : (EQ X Y))(x:X) (EQ x (proptransport hyp x)). Proof (proptransport_def.rmk6). Implicits proptransport_eq [1 2]. Definition prop_of := [P:Prop; p: P]P. Implicits prop_of [1]. Tactic Definition Transport u v w := Match Context With [id1 : (EQ ? ?); de : (description ?) |- ? ] -> First [ Poser v '(!transport (type_of u) w de id1 u); Assert (EQ u v); [Exact (transport_eq de id1 u)|Idtac] | Poser v '(!transport (type_of u) w de (EQ_sym id1) u); Assert (EQ u v); [Exact (transport_eq de (EQ_sym id1) u)|Idtac] ] | [id1 : (EQ ? ?) |- ? ] -> First [ Poser v '(!proptransport (prop_of u) w id1 u); Assert (EQ u v); [Exact (proptransport_eq id1 u)|Idtac] | Poser v '(!proptransport (prop_of u) w (EQ_sym id1) u); Assert (EQ u v); [Exact (proptransport_eq (EQ_sym id1) u)|Idtac] ] | [id1 : (EQtype ? ?) ; de : (description ?) |- ? ] -> First [ Poser v '(!bigtransport (type_of u) w de id1 u); Assert (EQ u v); [Exact (bigtransport_eq de id1 u)|Idtac] ]. Section Transport_example1. Variables A,B : Type. Variable de : (description B). Hypothesis h : (EQ B A). Variable a : A. Remark rmk1 : (is_nonempty B). Unfold is_nonempty. Unfold not. Intros. Transport a b B. Prolog3. Save. End Transport_example1. (***** uniqueness of proofs *****) Lemma proof_uni : (P,Q:Prop; p:P; q:Q) (EQ p q). Intros. Assert P->Q. Intro. Exact q. Assert Q->P. Intro. Exact p. Assert (EQ P Q). Exact_Prop_uni. Sel '(proof_description Q). Transport p r Q. Assert (EQ q r). Exact_pi. Exact_EQ_trans. Save. Implicits proof_uni [1 2]. Tactic Definition Exact_proof_uni := First [Exact (proof_uni ? ?)]. Section var_prop_descrip_def. (**** here we give a (description X-> Prop) ****) Variable X:Type. Local upre : (upre_description X-> Prop). Cbv Beta. Intros. Exact (a : X -> Prop)(P a) -> (a X0). Defined. Definition var_prop_description_out : (description X-> Prop). EApply (Build_description X-> Prop upre). Unfold is_description. Intros. UseExists2 e. Assert (upre P e u) == a. EApply EQ_eq. EApply extens_indep. Intros. Unfold upre. EApply Prop_uni. Intros. EApply H0. Assert a == [x:X](a x). EApply EQ_eq. EApply extens_indep. Intro. Exact (EQ_ref ?). Rewrite<- H1. Assumption. Intros. Assert a1 == a. EApply u. Assumption. Assumption. Rewrite H2. Assumption. Rewrite H0. Assumption. Defined. End var_prop_descrip_def. Definition var_prop_description : (X:Type)(description X -> Prop). Exact var_prop_description_out. Defined. Section mor_description_def. Variables A,B: Type. Variable de : (description B). Section mordesc1. Variable P : (A -> B) -> Prop. Hypothesis e : (exists P). Hypothesis u : (u,v: A -> B)(P u) -> (P v) -> u == v. Variable a : A. Local imP : B -> Prop := [b:B](f:A -> B)(P f) -> (f a) == b. Remark rmk1 : (exists imP). UseExists2 e. Exhibit '(a0 a). Unfold imP. Intros. Assert f == a0. EApply u. Assumption. Assumption. Rewrite H1. Trivial. Save. Remark rmk2 : (x,y:B)(imP x) -> (imP y) -> x == y. Intros. Unfold imP in H. Unfold imP in H0. UseExists2 e. Transitivity (a0 a). Apply sym_eqT. EApply H. Assumption. EApply H0. Assumption. Save. Definition mordesc_out :B. Sel '(de imP). EApply H. Exact rmk1. Intros. EApply rmk2. Assumption. Assumption. Defined. Remark rmk3 : (imP mordesc_out). Intros. Assert (is_description de). Exact (descrip_descrip de). Unfold mordesc_out. EApply (H imP). Save. Remark rmk4 : (f: A->B)(P f) -> (f a) == mordesc_out. Exact rmk3. Save. End mordesc1. Definition mor_desc_out : (description A -> B). EApply (Build_description A -> B mordesc_out). Unfold is_description. Intros. UseExists2 e. Assert (a == (mordesc_out P e u)). EApply EQ_eq. EApply extens_indep. Intros. EApply EQ_leib. EApply mordesc1.rmk4. Assumption. RewriteB H0. Assumption. Defined. End mor_description_def. Definition mor_description : (A,B: Type; de : (description B)) (description A-> B). Exact mor_desc_out. Defined. Theorem eq_EQtype : (A,B: Type)A== B -> (EQtype A B). Intros. Unfold EQtype. Intros. Rewrite<- H. Assumption. Save. Implicits eq_EQtype [1 2]. (*s John Major's Equality as proposed by C. Mc Bride *) (*** see the file JMeq.v but we do it with Type instead ***) (*** this definition is equivalent to EQ but the inductive version is better for proving application_plug ***) Inductive JMeqT [A:Type;x:A] : (B:Type)B->Prop := JMeqT_refl : (JMeqT A x A x). Implicits JMeqT [1 3]. Implicits JMeqT_refl [1]. Theorem JMeqT_EQ : (A,B: Type; a:A; b:B)(JMeqT a b) -> (EQ a b). Intros. Elim H. Exact (EQ_ref ?). Save. Theorem JMeqT_eqT : (A:Type; a,b:A)(JMeqT a b) -> a == b. Intros. EApply EQ_eq. EApply JMeqT_EQ. Assumption. Save. (***** a parenthesis : we don't need this but we show that we also get the theorem JMeq_eq for sets; the def of JMeq is identical to that from JMeq.v *********) Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop := JMeq_refl : (JMeq A x A x). Implicits JMeq [1 3]. Lemma JMeq_JMeqT : (A,B: Set; a:A; b:B)(JMeq a b) -> (JMeqT a b). Intros. NewInduction H. EApply JMeqT_refl. Save. Theorem JMeq_eq : (A: Set; a,b:A)(JMeq a b) -> a = b. Intros. Assert a == b. Assert (JMeqT a b). EApply JMeq_JMeqT. Assumption. EApply JMeqT_eqT. Assumption. Rewrite H0. Reflexivity. Save. (********* end of parenthesis *******) Definition JMeqT_on_term := [t1,t2 : Term] (JMeqT (the_term t1) (the_term t2)). Theorem JMeqT_thru_term : (A,B: Type; a:A; b:B) (JMeqT_on_term (term a) (term b)) -> (JMeqT a b). Intros. Exact H. Save. Theorem EQ_JMeqT : (A,B: Type; a:A; b:B)(EQ a b) -> (JMeqT a b). Intros. Unfold EQ in H. EApply JMeqT_thru_term. Unfold EQterm in H. Sel '(H [t:Term](JMeqT_on_term (term a) t)). EApply H0. Clear H0. Clear H. Unfold JMeqT_on_term. Exact (JMeqT_refl ?). Save. Theorem JMeqT_app : (A,B, X : Type; F: A -> X; G : B -> X; a:A; b:B)(JMeqT F G) -> (JMeqT a b) -> (JMeqT (F a) (G b)). Intros. NewInduction H0. Assert (EQ F G). Exact (JMeqT_EQ ? ? ? ? H). Assert F==G. EApply EQ_eq. Assumption. Rewrite H1. Exact (JMeqT_refl ?). Save. Section dependent_plug_proof. Variable X : Type. Variable M : X -> Type. Variable F : (x:X)(M x). Variables a,b : X. Hypothesis hyp : (EQ a b). Section dppA. Variable P : Term -> Prop. Hypothesis p : (P (term (F a))). Local Q : X -> Prop := [x:X](P (term (F x))). Remark rmk1 : (Q a). Proof p. Remark rmk2 : (Q b). Proof (EQ_subs Q rmk1 hyp). Remark rmk3 : (P (term (F b))). Proof rmk2. End dppA. Remark rmk4 : (EQterm (term (F a)) (term (F b))). Proof (dppA.rmk3). Remark rmk5 : (EQ (F a) (F b)). Proof rmk4. End dependent_plug_proof. Lemma dependent_plug : (X:Type; M : X -> Type; F : (x:X)(M x); a,b:X; hyp:(EQ a b)) (EQ (F a) (F b)). Proof (dependent_plug_proof.rmk4). Implicits dependent_plug [1 4 5]. (***** using JMeqT we get a great proof of the following theorem **** which would have been a real pain to prove using only EQ ****) Theorem application_plug : (A,B,X: Type; F : A->X; G:B->X; a:A; b:B; h:(EQ F G); k:(EQ a b)) (EQ (F a) (G b)). Intros. EApply JMeqT_EQ. EApply (JMeqT_app A B X F G a b). EApply EQ_JMeqT. Assumption. EApply EQ_JMeqT. Assumption. Save. Implicits application_plug [1 2 3 4 5 6 7]. Section application_plug2_proof. Variables A,B,X,Y: Type. Variable a : A. Variable b : B. Hypothesis k : (EQ a b). Hypothesis m : (EQ X Y). Theorem app2bis : (F: A-> X; G : B -> Y)(EQ F G)->(EQ (F a) (G b)). Assert X == Y. EApply EQ_eq. Assumption. NewInduction H. Intros. EApply (!application_plug A B X F G a b). Assumption. Assumption. Save. End application_plug2_proof. Lemma application_plug2 : (A,B,X,Y: Type; F:A->X; G:B->Y;a:A;b:B) (m:(EQ X Y); h:(EQ F G); k:(EQ a b)) (EQ (F a) (G b)). Intros. EApply (app2bis A B X Y a b k m F G). Assumption. Save. Implicits application_plug2 [1 2 3 4 5 6 7 8]. Section compose_transport_proof. Variables A, X, Y : Type. Variable F : A -> X. Variable deY : (description Y). Hypothesis e : (EQ X Y). Local deAY : (description A-> Y) := (mor_description A Y deY). Section ajskA1. Variable P : Type -> Prop. Hypothesis hp : (P (A -> X)). Remark rmk0 : (P (A -> Y)). Proof (EQ_subs [U:Type](P (A -> U)) hp e). End ajskA1. Remark rmk1 : (EQtype (A -> X) (A -> Y)). Proof (ajskA1.rmk0). (* Remark rmk1 : (EQ (A -> X) (A-> Y)). Proof (EQ_plug [U:Type](A->U) e). --- this produced an anomaly *) Local G : A-> Y := (bigtransport deAY rmk1 F). Local H : A -> Y := [a:A](transport deY e (F a)). Remark rmk2 : (EQ F G). Proof (bigtransport_eq deAY rmk1 F). Section ajskA. Variable a : A. Section ajskB. Variable P : Term -> Prop. Hypothesis hp : (P (term (F a))). Local W : (A-> X) -> Prop := [f:A->X](P (term (f a))). Local U : (A ->Y) -> Prop := [g:A->Y](P (term (g a))). Remark rmk3 : (EQ W U). Proof (dependent_plug [V:Type]((A->V)->Prop) [V:Type]([v:A->V](P (term (v a)))) e). Remark rmk4 : (EQ (W F) (U G)). Proof (application_plug rmk3 rmk2). Remark rmk5 : (EQ (P (term (F a))) (P (term (G a)))). Proof rmk4. Remark rmk6 : (P (term (G a))). Proof (proptransport rmk5 hp). End ajskB. Remark rmk7 : (EQ (F a) (G a)). Proof (ajskB.rmk6). Remark rmk8 : (EQ (F a) (H a)). Proof (transport_eq deY e (F a)). Remark rmk9 : (EQ (G a) (H a)). Proof (EQ_trans (EQ_sym rmk7) rmk8). End ajskA. Remark rmk10 : (EQ G H). Proof (extens_indep G H ajskA.rmk9). Remark rmk11 : (EQ F H). Proof (EQ_trans rmk2 rmk10). Definition compose_transport := H. End compose_transport_proof. Implicits compose_transport [1 2 3]. Lemma compose_transport_eq : (A,X,Y: Type; F:A->X; deY : (description Y); e:(EQ X Y)) (EQ F (compose_transport F deY e)). Proof (compose_transport_proof.rmk11). Implicits compose_transport_eq [1 2 3]. Theorem description_destruct : (X:Type; de: (description X)) de == (Build_description X (descrip_pre X de) (descrip_descrip de)). Intros. NewInduction de. Trivial. Save. Section description_uni_proof. Variable X : Type. Variables de1, de2 : (description X). Local pre1 :(P:(X->Prop)) (exists P)->((x,y:X)(P x)->(P y)->x==y)->X := (descrip_pre X de1). Local pre2:(P:(X->Prop)) (exists P)->((x,y:X)(P x)->(P y)->x==y)->X := (descrip_pre X de2). Remark rmk1 : (P : X -> Prop; e : (exists P))(pre1 P e) == (pre2 P e). Intros. EApply EQ_eq. EApply extens_indep. Intros. EApply EQ_leib. EApply a. Assert (is_description pre1). Exact (descrip_descrip de1). EApply H. Assert (is_description pre2). Exact (descrip_descrip de2). EApply H. Save. Remark rmk2 : (P: X -> Prop) (EQ (pre1 P) (pre2 P)). Intros. EApply extens_indep. Intros. EApply EQ_leib. EApply rmk1. Save. Local FF : (X-> Prop) -> Type := [P : (X -> Prop)] (exists P)->((x,y:X)(P x)->(P y)->x==y)->X . Remark rmk3 : pre1 == pre2. EApply EQ_eq. Exact (extens FF pre1 pre2 rmk2). Save. Local dpre1 : (is_description pre1) := (descrip_descrip de1). Local dpre2 : (is_description pre2) := (descrip_descrip de2). Remark rmk4 : (EQ dpre1 dpre2). Exact_proof_uni. Save. Local A1 := (Build_description X pre1). Local A2 := (Build_description X pre2). Remark rmk5 : (EQ A1 A2). Unfold A1. Unfold A2. Assert (pre1 == pre2). Exact rmk3. RewriteB H. EApply EQ_ref. Save. Remark rmk6 : (EQ (A1 dpre1) (A2 dpre2)). Exact (application_plug rmk5 rmk4). Save. Remark rmk7 : de1 == de2. Assert (de1 == (A1 dpre1)). Exact (description_destruct X de1). RewriteB H. Assert (A1 dpre1) == (A2 dpre2). EApply EQ_eq. Exact rmk6. Rewrite H0. Symmetry. Exact (description_destruct X de2). Save. End description_uni_proof. Theorem description_uni : (X:Type; de1, de2 : (description X))de1 == de2. Exact description_uni_proof.rmk7. Save. (********************************************************************** *** we construct a function by glueing from functions on two pieces *** of a type. This more or less says that we can do case-analysis *** on a P : Prop to construct a term y : Y, under the condition *** that we have de : (description Y). **********************************************************************) Section dichot_construction. Variable Y : Type. Variable P : Prop. Variable f : P -> Y. Variable g : (not P) -> Y. Variable de : (description Y). Local is_good : Y -> Prop := [y:Y]((p:P)(EQ y (f p))) /\ ((n:(not P))(EQ y (g n))). Section dc_x. Hypothesis contra : (not (exists is_good)). Section dc_1. Hypothesis p:P. Local y := (f p). Section dc_1a. Variable p' : P. Remark rmk1 : (EQ p p'). Proof (proof_irrelevance p p'). Fact fact1 : (EQ y (f p')). Proof (EQ_plug f rmk1). End dc_1a. Remark rmk2 : (p':P)(EQ y (f p')). Proof fact1. Section dc_1b. Variable n:(not P). Remark rmk3 : False. Proof (n p). Fact fact2 : (EQ y (g n)). Proof (False_implies_everything (EQ y (g n)) rmk3). End dc_1b. Remark rmk5 : (is_good y). Proof. Split. Apply rmk2. Apply fact2. Qed. Remark rmk6 : (exists is_good). Proof (exists_th1 is_good rmk5). Fact fact3 : False. Proof (contra rmk6). End dc_1. Remark rmk7 : (not P). Proof fact3. Local y:= (g rmk7). Section dc_2a. Variable n:(not P). Remark rmk8 : (EQ rmk7 n). Proof (proof_irrelevance rmk7 n). Fact fact4:(EQ y (g n)). Proof (EQ_plug g rmk8). End dc_2a. Remark rmk9 : (n:(not P))(EQ y (g n)). Proof fact4. Section dc_2b. Variable p:P. Remark rmk10 : False . Proof (rmk7 p). Fact fact5 : (EQ y (f p)). Proof (False_implies_everything (EQ y (f p)) rmk10). End dc_2b. Remark rmk12 : (is_good y). Proof. Split. Apply fact5. Apply rmk9. Qed. Remark rmk13 : (exists is_good). Proof (exists_th1 is_good rmk12). Fact fact6 : False. Proof (contra rmk13). End dc_x. Remark rmk14 : (not (not (exists is_good))). Proof fact6. Remark rmk15 : (exists is_good). Proof (excluded_middle (exists is_good) rmk14). Definition glueing0' := (choice de rmk15). Remark rmk16 : (is_good glueing0'). Proof (choice_pr1 de rmk15). Lemma glueing0_pr1' : (p:P)(EQ glueing0' (f p)). Proof (proj1 ? ? rmk16). Lemma glueing0_pr2' : (n: (not P))(EQ glueing0' (g n)). Proof (proj2 ? ? rmk16). End dichot_construction. Definition glueing0 : (Y:Type; P: Prop; f: P-> Y; g: (not P) ->Y ; de : (description Y)) Y := glueing0'. Implicits glueing0 [1 2]. Lemma glueing0_pr1 : (Y:Type; P: Prop; f: P-> Y; g: (not P) ->Y; de : (description Y); p:P) (EQ (glueing0 f g de) (f p)). Proof glueing0_pr1'. Implicits glueing0_pr1 [1 2]. Lemma glueing0_pr2 : (Y:Type; P: Prop; f: P-> Y; g: (not P) ->Y; de : (description Y); n:(not P)) (EQ (glueing0 f g de) (g n)). Proof glueing0_pr2'. Implicits glueing0_pr2 [1 2]. (************************************************************************) (******************** injectivity, surjectivity and bijections **********) (************************************************************************) (*** in the present version we replace EQ by eqT ***) (*** define EQ' as == to facilitate rewriting the file ***) Definition EQ1 := [A:Type; a,b:A](a == b). Implicits EQ1 [1]. Theorem EQ1_sym : (A: Type; a,b:A)(EQ1 a b) -> (EQ1 b a). Intros. Unfold EQ1 in H. Unfold EQ1. Symmetry. Assumption. Save. Implicits EQ1_sym [1 2 3]. Theorem EQ1_trans : (A: Type; a,b,c: A) (EQ1 a b) -> (EQ1 b c) -> (EQ1 a c). Intros. Unfold EQ1 in H H0. Unfold EQ1. Transitivity b. Assumption. Assumption. Save. Implicits EQ1_trans [1 2 3 4]. Definition is_injective := [A,B: Type; F:A-> B] (x,y:A)(F x)== (F y) -> x == y. Implicits is_injective [1 2]. Definition is_surjective := [A,B: Type; F: A-> B] (y:B)(exists ([x:A](F x) == y)). Implicits is_surjective [1 2]. Section surj_description_def. Variables A,B : Type. Variable F : A -> B. Variable deA : (description A). Hypothesis hyp : (is_surjective F). Section surjdesc1. Variable P : B -> Prop. Hypothesis e : (exists P). Local PA : A -> Prop := [a:A](P (F a)). Remark rmk1 : (exists PA). UseExists2 e. Assert (exists [x:A](F x) == a). EApply hyp. UseExists2 H0. Exhibit a0. Unfold PA. RewriteB H1. Assumption. Save. Definition surjdesc_pre : B := (F (choice deA rmk1)). Remark rmk2 : (P surjdesc_pre). Unfold surjdesc_pre. Change (PA (choice deA rmk1)). Exact (choice_pr1 deA rmk1). Save. End surjdesc1. Definition surjdesc_out : (description B). EApply (Create_description B surjdesc_pre). Unfold is_chfn. Intros. EApply (surjdesc1.rmk2 P e). Defined. End surj_description_def. Definition surj_description : (A,B: Type; F:A->B; de : (description A)) (is_surjective F) -> (description B). Exact surjdesc_out. Defined. Definition section := [A,B: Type; de : (description A);F:A->B; hyp : (is_surjective F); y:B] (choice de (hyp y)). Implicits section [1 2]. Definition section_pr := [A,B: Type; de : (description A);F:A->B; hyp : (is_surjective F); y:B] (choice_pr1 de (hyp y)). Implicits section_pr [1 2]. Record is_bijective [A,B: Type; f: A -> B] : Prop := { bijective_inj : (is_injective f); bijective_surj : (is_surjective f) }. Implicits is_bijective [1 2]. Implicits bijective_inj [1 2 3]. Implicits bijective_surj [1 2 3]. Record bijection [A,B: Type]: Type :={ the_bijection :> A->B; bij_injective : (is_injective the_bijection); bij_surjective : (is_surjective the_bijection) }. Implicits the_bijection [1 2]. Implicits bij_injective [1 2]. Implicits bij_surjective [1 2]. Section bijection_bijective_def. Variables A,B: Type. Variable b : (bijection A B). Lemma bijection_bijective : (is_bijective (the_bijection b)). Proof (Build_is_bijective A B (the_bijection b) (bij_injective b) (bij_surjective b)). End bijection_bijective_def. Implicits bijection_bijective [1 2]. Section bijective_bijection_def. Variables A,B: Type. Variable f: A -> B. Hypothesis hyp: (is_bijective f). Definition bijective_bijection := (Build_bijection A B f (bijective_inj hyp) (bijective_surj hyp)). End bijective_bijection_def. Implicits bijective_bijection [1 2]. (*** (bijective_bijection f hyp) : (bijection A B). ***) Section bijection_inverse_def. Variables A,B: Type. Variable de : (description A). Variable F : (bijection A B). Local G := (section de (the_bijection F) (bij_surjective F)). Section bijinvA. Variable b : B. Lemma bijection_th1 : (EQ1 b (F (G b))). Unfold EQ1. Symmetry. Exact (section_pr de (the_bijection F) (bij_surjective F) b). Save. End bijinvA. Section bijinvB. Variable a : A. Local b := (F a). Remark rmk1 : (EQ1 (F a) (F (G b))). Proof (bijection_th1 b). Remark rmk2 : (is_injective F). Proof (bij_injective F). Remark rmk3 : (EQ1 a (G b)). Proof (rmk2 a (G b) rmk1). Lemma bijection_th2 : (EQ1 a (G (F a))). Proof rmk3. End bijinvB. Section bijinvC. Variables x,y:B. Hypothesis hyp : (EQ1 (G x) (G y)). Remark rmk4 : (EQ1 x (F (G x))). Proof (bijection_th1 x). Remark rmk5 : (EQ1 y (F (G y))). Proof (bijection_th1 y). Remark rmk6 : (EQ1 (F (G x)) (F (G y))). Unfold EQ1. Unfold EQ1 in hyp. RewriteB hyp. Trivial. Save. Fact fact1 : (EQ1 x y). Unfold EQ1. Exact (EQ1_trans (EQ1_trans rmk4 rmk6) (EQ1_sym rmk5)). Save. End bijinvC. Remark rmk7 : (is_injective G). Proof fact1. Section bijinvD. Hypothesis z : A. Local y := (F z). Remark rmk8 : (EQ1 z (G y)). Proof (bijection_th2 z). Remark rmk9 : (EQ1 (G y) z). EApply (EQ1_sym). Exact rmk8. Save. Fact fact2 : (exists [x:B](EQ1 (G x) z)). Proof (exists_th1 [x:B](EQ1 (G x) z) rmk9). End bijinvD. Remark rmk9 : (is_surjective G). Proof fact2. Definition inverse_bijection := (Build_bijection B A G rmk7 rmk9). End bijection_inverse_def. Implicits inverse_bijection [1 2]. Implicits bijection_th1 [1 2]. Implicits bijection_th2 [1 2]. Section bijection_example. Variables A,B: Type. Variable de : (description A). Variable F : (bijection A B). Local G:= (inverse_bijection de F). Variable a : A. Variable b : B. Remark rmk1 : (EQ1 a (G (F a))). Proof (bijection_th2 de F a). Remark rmk2 : (EQ1 b (F (G b))). Proof (bijection_th1 de F b). End bijection_example. (**** other things to do: prove (EQ (id A) (compose_functions G F)) etc??? prove that (EQ F (inverse_bijection G)) etc ??? *****) Record bijection2 [A,B: Type] : Type :={ bij_forward :> A -> B; bij_backward : B -> A; bij_eqA : (a:A)((bij_backward (bij_forward a))== a); bij_eqB : (b:B)((bij_forward (bij_backward b)) == b) }. Implicits bij_forward [1 2]. Implicits bij_backward [1 2]. Implicits bij_eqA [1 2]. Implicits bij_eqB [1 2]. Section bijection2_proofs. Variables A,B: Type. Variable f:(bijection2 A B). Local for := (bij_forward f). Local back := (bij_backward f). Local for_back := [b:B](for (back b)). Local back_for := [a:A](back (for a)). Local idA := [a:A]a. Local idB := [b:B]b. Remark rmk1 : (a:A)(EQ1 (back_for a) a). Proof (bij_eqA f). Remark rmk2 : (b:B)(EQ1 (for_back b) b). Proof (bij_eqB f). Lemma bijection2_thA :(EQ1 back_for idA). Proof (extens_indep1 back_for idA rmk1). Lemma bijection2_thB : (EQ1 for_back idB). Proof (extens_indep1 for_back idB rmk2). Section bijection2inj_proof. Variables x,y: A. Hypothesis hyp: (EQ1 (for x) (for y)). Local x' := (back (for x)). Local y' := (back (for y)). Remark rmk3 : (EQ1 x' y'). Unfold EQ1. EApply EQ_eq. Assert hyp1 : (EQ (for x) (for y)). EApply EQ_leib. Exact hyp. Exact (EQ_plug back hyp1). Save. Remark rmk4 : (EQ1 x' x). Proof (bij_eqA f x). Remark rmk5 : (EQ1 y' y). Proof (bij_eqA f y). Fact fact1 : (EQ1 x y). Exact (EQ1_trans (EQ1_sym rmk4) (EQ1_trans rmk3 rmk5)). Save. End bijection2inj_proof. Lemma bijection2_inj : (is_injective for). Proof fact1. Section bijection2surj_proof. Variable z : B. Local x := (back z). Remark rmk6 : (EQ1 (for x) z). Proof (bij_eqB f z). Fact fact2 : (exists [a:A](EQ1 (for a) z)). Proof (exists_th1 [a:A](EQ1 (for a) z) rmk6). End bijection2surj_proof. Lemma bijection2_surj : (is_surjective for). Proof fact2. Lemma bijection2_bijective : (is_bijective for). Proof (Build_is_bijective A B for bijection2_inj bijection2_surj). End bijection2_proofs. Implicits bijection2_thA [1 2]. (*** (bijection2_thA f) : (EQ (compose_functions (bij_forward f) (bij_backward f)) [a:A]a) ***) Implicits bijection2_thB [1 2]. (*** (bijection2_thB f) : (EQ (compose_functions (bij_forward f) (bij_backward f)) [b:B]b) ***) Implicits bijection2_inj [1 2]. (*** (bijection2_inj f) : (is_injective (bij_forward f)) **) Implicits bijection2_surj [1 2]. (*** (bijection2_surj f) : (is_surjective (bij_forward f)) **) Implicits bijection2_bijective [1 2]. (*** (bijection2_bijective f) : (is_bijective (bij_forward f)) **) Section bijective_bijection2_def. Variables A,B: Type. Variable de : (description A). Variable f:A-> B. Hypothesis hyp:(is_bijective f). Local bijF := (bijective_bijection f hyp). Local bijB := (inverse_bijection de bijF). Local g :B-> A:= (the_bijection bijB). Remark rmk1 : (x:A)(EQ1 (g (f x)) x). Proof [x:A](EQ1_sym (bijection_th2 de bijF x)). Remark rmk2 : (y:B)(EQ1 (f (g y)) y). Proof [y:B](EQ1_sym (bijection_th1 de bijF y)). Definition bijective_bijection2 : (bijection2 A B) := (Build_bijection2 A B f g rmk1 rmk2). End bijective_bijection2_def. Implicits bijective_bijection2 [1 2]. (*** (bijective_bijection2 de f hyp) : (bijection2 A B) ***) Definition are_bijective := [X,Y: Type](is_nonempty (bijection X Y)). (************************************************************************) (********************** subsets and operations thereon ******************) (************************************************************************) (**** actually it would be better to input all of this directly from the Ensembles.v library ******) Definition Subset := [A: Type](A-> Prop). Definition IN := [A: Type; a:A; B: (Subset A)](B a). Implicits IN [1]. Definition SUB := [A: Type; B,C: (Subset A)] (a:A)(IN a B) -> (IN a C). Implicits SUB [1]. Section SUB_ref_proof. Variable X:Type. Variable A: (Subset X). Lemma SUB_ref : (SUB A A). Proof [x:X; h:(IN x A)]h. End SUB_ref_proof. Implicits SUB_ref [1]. Section SUB_trans_proof. Variable X:Type. Variables A,B,C: (Subset X). Hypothesis hyp1 : (SUB A B). Hypothesis hyp2 : (SUB B C). Section subtransA. Variable x:X. Hypothesis i: (IN x A). Remark rmk1 : (IN x B). Proof (hyp1 x i). Fact fact1 : (IN x C). Proof (hyp2 x rmk1). End subtransA. Lemma SUB_trans : (SUB A C). Proof fact1. End SUB_trans_proof. Implicits SUB_trans [1 2 3 4]. Definition intersection := [X:Type; A,B: (Subset X)] ([x:X](IN x A) /\ (IN x B)). Implicits intersection [1]. Definition union := [X:Type; A,B: (Subset X)] ([x:X](IN x A) \/ (IN x B)). Implicits union [1]. Definition complement := [X:Type; A:(Subset X)] ([x:X](not (IN x A))). (**** we should prove intersection_sym, intersection_ref, intersection_assoc union_sym union_ref union_assoc complement_invol complement_disjoint complement_intersection_union complement_union_intersection etc etc *****) Definition empty_subset :=[X:Type]([x:X]False). Definition full_subset := [X:Type]([x:X]True). Definition is_a_nonempty_subset := [X:Type; A:(Subset X)] (exists [x:X](IN x A)). Implicits is_a_nonempty_subset [1]. Section nonempty_subset_th1_proof. Variable X: Type. Variable x : X. Variable A:(Subset X). Hypothesis hyp : (IN x A). Remark rmk1 : (exists [u:X](IN u A)). Proof (exists_th1 [u:X](IN u A) hyp). Lemma nonempty_subset_th1 : (is_a_nonempty_subset A). Proof rmk1. End nonempty_subset_th1_proof. Implicits nonempty_subset_th1 [1 2 3]. Definition is_an_empty_subset := [X:Type; A:(Subset X)] (doesnt_exist [x:X](IN x A)). Implicits is_an_empty_subset [1]. Section empty_nonempty_subsets_proof. Variable X : Type. Variable A : (Subset X). Hypothesis hyp1 : (is_an_empty_subset A). Hypothesis hyp2 : (is_a_nonempty_subset A). Lemma empty_nonempty_subsets: False. Proof (hyp2 hyp1). End empty_nonempty_subsets_proof. Implicits empty_nonempty_subsets [1 2]. Section empty_subset_th1_proof. Variable X : Type. Variable x:X. Variable A : (Subset X). Hypothesis hyp : (is_an_empty_subset A). Hypothesis i : (IN x A). Remark rmk1 : (is_a_nonempty_subset A). Proof (nonempty_subset_th1 i). Lemma empty_subset_th1 : False. Proof (empty_nonempty_subsets hyp rmk1). End empty_subset_th1_proof. Implicits empty_subset_th1 [1 2 3]. Section subset_extens_proof. Variable X: Type. Variables A,B: (Subset X). Hypothesis ab : (SUB A B). Hypothesis ba : (SUB B A). Section sub_exA. Variable x:X. Remark rmk1 : (A x) -> (B x). Proof (ab x). Remark rmk2 : (B x) -> (A x). Proof (ba x). Fact fact1 : (EQ (A x) (B x)). Proof (Prop_uni rmk1 rmk2). End sub_exA. Remark rmk3 : (EQ A B). Proof (extens_indep A B fact1). End subset_extens_proof. Lemma subset_extens : (X:Type; A,B: (Subset X)) (SUB A B) -> (SUB B A) -> (EQ A B). Proof (subset_extens_proof.rmk3). Implicits subset_extens [1 2 3]. Definition are_disjoint2 :=[X:Type; A,B: (Subset X)](is_an_empty_subset (intersection A B)). Implicits are_disjoint2 [1]. Section are_disjoint2_pr_proof. Variable X:Type. Variable x : X. Variables A,B: (Subset X). Hypothesis inA : (IN x A). Hypothesis inB : (IN x B). Hypothesis hyp : (are_disjoint2 A B). Remark rmk1 : (IN x A) /\ (IN x B). Proof. Split; Assumption. Qed. Remark rmk2 : (IN x (intersection A B)). Proof rmk1. Remark rmk3 : (is_a_nonempty_subset (intersection A B)). Proof (nonempty_subset_th1 rmk2). Remark rmk4 : (is_an_empty_subset (intersection A B)). Proof hyp. Lemma are_disjoint2_pr : False. Proof (empty_nonempty_subsets rmk4 rmk3). End are_disjoint2_pr_proof. Implicits are_disjoint2_pr [1 2 3 4]. Record are_disjoint3 [X:Type; A,B,C:(Subset X)]:Prop := { disjoint3_ab : (are_disjoint2 A B); disjoint3_bc : (are_disjoint2 B C); disjoint3_ac : (are_disjoint2 A C) }. Implicits are_disjoint3 [1]. Implicits disjoint3_ab [1 2 3 4]. Implicits disjoint3_bc [1 2 3 4]. Implicits disjoint3_ac [1 2 3 4]. Record are_disjoint4 [X:Type; A,B,C,D : (Subset X)] : Prop :={ disjoint4_abc : (are_disjoint3 A B C); disjoint4_ad : (are_disjoint2 A D); disjoint4_bd : (are_disjoint2 B D); disjoint4_cd : (are_disjoint2 C D) }. Implicits are_disjoint4 [1]. Implicits disjoint4_abc [1 2 3 4 5]. Implicits disjoint4_ad [1 2 3 4 5]. Implicits disjoint4_bd [1 2 3 4 5]. Implicits disjoint4_cd [1 2 3 4 5]. Section disjoint4_properties. Variable X:Type. Variables A,B,C,D: (Subset X). Hypothesis hyp:(are_disjoint4 A B C D). Remark rmk1 : (are_disjoint3 A B C). Proof (disjoint4_abc hyp). Lemma disjoint4_ab : (are_disjoint2 A B). Proof (disjoint3_ab rmk1). Lemma disjoint4_ac : (are_disjoint2 A C). Proof (disjoint3_ac rmk1). Lemma disjoint4_bc : (are_disjoint2 B C). Proof (disjoint3_bc rmk1). End disjoint4_properties. Implicits disjoint4_ab [1 2 3 4 5]. Implicits disjoint4_bc [1 2 3 4 5]. Implicits disjoint4_ac [1 2 3 4 5]. (************************************************************************) (******* now we discuss equivalence relations and quotients *************) (************************************************************************) (*** the construction of the quotient of an equivalence relation proceeds as in usual classical math; however sometimes we need to assume a de : (description Z) for some Z : Type entering into the argument. **************************************************************) Record Equivalence_Relation [X:Type]:Type :={ the_relation :> X -> X -> Prop; equiv_ref : (x: X) (the_relation x x); equiv_trans : (x,y,z: X) (the_relation x y) -> (the_relation y z) -> (the_relation x z); equiv_sym : (x,y: X) (the_relation x y) -> (the_relation y x) }. Implicits equiv_ref [1]. Implicits equiv_trans [1 2 3 4 5]. Implicits equiv_sym [1 2 3 4]. Record is_a_coset [X:Type; R:(Equivalence_Relation X); C:(Subset X)] : Prop := { coset_nonempty : (is_a_nonempty_subset C); coset_related : (x,y:X)(IN x C) -> (IN y C) -> (R x y); coset_trans : (x,y:X)(IN x C) -> (R x y) -> (IN y C) }. Implicits is_a_coset [1]. Implicits coset_nonempty [1 2 3]. Implicits coset_related [1 2 3 5 6]. Implicits coset_trans [1 2 3 5 6]. Section coset_of_def. Variable X: Type. Variable R:(Equivalence_Relation X). Variable x:X. Local C := [y:X](R x y). Remark rmk1 : (exists [y:X](C y)). Proof (exists_th1 [y:X](C y) (equiv_ref R x)). Section coset_ofA. Variables u,v: X. Hypothesis cu : (C u). Hypothesis cv : (C v). Remark rmk2 : (R u x). Proof (equiv_sym cu). Remark rmk3 : (R x v). Proof cv. Fact fact1 : (R u v). Proof (equiv_trans rmk2 rmk3). End coset_ofA. Section coset_ofB. Variables u,v:X. Hypothesis cu : (C u). Hypothesis ruv : (R u v). Fact fact2 : (C v). Proof (equiv_trans cu ruv). End coset_ofB. Lemma coset_of_coset : (is_a_coset R C). Proof (Build_is_a_coset X R C rmk1 fact1 fact2). Lemma coset_of_pr : (IN x C). Proof (equiv_ref R x). Lemma coset_of_rel : (y:X)(IN y C) -> (R x y). Proof [y:X][hyp : (C y)]hyp. Definition coset_of := C. End coset_of_def. Implicits coset_of [1]. Implicits coset_of_coset [1]. Implicits coset_of_pr [1]. Implicits coset_of_rel [1]. Section coset_of_uni_proof. Variable X : Type. Variable R : (Equivalence_Relation X). Variable C : (Subset X). Variable x : X. Hypothesis hc : (is_a_coset R C). Hypothesis hx : (IN x C). Local D := (coset_of R x). Remark rmk1 : (IN x D). Proof (coset_of_pr R x). Remark rmk2 : (is_a_coset R D). Proof (coset_of_coset R x). Section coupA. Variable y : X. Hypothesis hy : (IN y C). Remark rmk3 : (R x y). Proof (coset_related hc hx hy). Remark rmk4 : (IN y D). Proof (coset_trans rmk2 rmk1 rmk3). End coupA. Remark rmk5 : (SUB C D). Proof (coupA.rmk4). Section coupB. Variable y:X. Hypothesis hy : (IN y D). Remark rmk6 : (R x y). Proof (coset_related rmk2 rmk1 hy). Remark rmk7 : (IN y C). Proof (coset_trans hc hx rmk6). End coupB. Remark rmk8 : (SUB D C). Proof (coupB.rmk7). Remark rmk9 : (EQ C D). Proof (subset_extens rmk5 rmk8). End coset_of_uni_proof. Lemma coset_of_uni : (X:Type; R:(Equivalence_Relation X); C: (Subset X);x:X) (is_a_coset R C) -> (IN x C) -> (EQ C (coset_of R x)). Proof (coset_of_uni_proof.rmk9). Implicits coset_of_uni [1 2 3 4]. Section quotient_def. Variable X: Type. Variable R:(Equivalence_Relation X). Local P := [C : (Subset X)] (is_a_coset R C). Definition Quotient := (SetOf P). End quotient_def. Implicits Quotient [1]. Section quotient_map. Variable X: Type. Variable R:(Equivalence_Relation X). Local P := [C : (Subset X)] (is_a_coset R C). Section qmA. Variable x:X. Local C := (coset_of R x). Remark rmk1 : (is_a_coset R C). Proof (coset_of_coset R x). Remark rmk2 : (P C). Proof rmk1. Definition quotient_map_out : (Quotient R) := (specialize C rmk2). Remark rmk3 : (EQ (generalize quotient_map_out) C). Proof (EQ_ref C). End qmA. Definition Quotient_Map : X -> (Quotient R) := quotient_map_out. End quotient_map. Implicits Quotient_Map [1]. Lemma Quotient_Map_eq : (X:Type; R:(Equivalence_Relation X)) (x:X)(EQ (generalize (Quotient_Map R x)) (coset_of R x)). Proof (quotient_map.qmA.rmk3). Implicits Quotient_Map_eq [1]. Section quotient_lift. Variable X: Type. Variable de : (description X). Variable R:(Equivalence_Relation X). Local P := [C : (Subset X)] (is_a_coset R C). Variable q : (Quotient R). Local p := (generalize q). Remark rmk1 : (is_a_coset R p). Proof (generalize_pr q). Remark rmk2 : (EQ (generalize q) p). Proof (EQ_ref p). Remark rmk3 : (exists [z:X](p z)). Proof (coset_nonempty rmk1). Local lift :X:= (choice de rmk3). Remark rmk4 : (p lift). Proof (choice_pr1 de rmk3). Local back := (coset_of R lift). Remark rmk8 : (EQ (generalize (Quotient_Map R lift)) back). Proof (Quotient_Map_eq R lift). Section quotient_liftA. Variable x:X. Hypothesis b : (back x). Remark rmk9 : (R lift x). Proof b. Fact fact1 : (p x). Proof (coset_trans rmk1 rmk4 rmk9). End quotient_liftA. Remark rmk10 : (x:X)(back x) -> (p x). Proof fact1. Section quotient_liftB. Variable x:X. Hypothesis hyp: (p x). Remark rmk11 : (R lift x). Proof (coset_related rmk1 rmk4 hyp). Fact fact2 : (back x). Proof rmk11. End quotient_liftB. Remark rmk12 : (x:X)(p x) -> (back x). Proof fact2. Remark rmk13 : (EQ p back). EApply (!extens_indep X Prop p back). Intros. EApply Prop_uni. Exact (rmk12 a). Exact (rmk10 a). Save. Remark rmk14 : (EQ p (generalize (Quotient_Map R lift))). Proof (EQ_trans rmk13 (EQ_sym rmk8)). Remark rmk14bis : (EQ (generalize q) (generalize (Quotient_Map R lift))). Proof (EQ_trans rmk2 rmk14). Remark rmk15 : (EQ q (Quotient_Map R lift)). EApply EQ_leib. Assert (generalize q) == (generalize (Quotient_Map R lift)). EApply EQ_eq. Exact rmk14bis. Exact (generalize_inj ? ? ? ? H). Save. Definition Quotient_Lift := lift. End quotient_lift. Implicits Quotient_Lift [1]. Lemma Quotient_Lift_eq : (X:Type; de : (description X); R:(Equivalence_Relation X);q:(Quotient R)) (EQ q (Quotient_Map R (Quotient_Lift de R q))). Proof (quotient_lift.rmk15). Implicits Quotient_Lift_eq [1]. Section quotient_relation. Variable X: Type. Variable R: (Equivalence_Relation X). Variables x, y: X. Local Q := (Quotient R). Local M := (Quotient_Map R). Hypothesis hyp:(EQ (M x) (M y)). Local P := [C:X -> Prop] (is_a_coset R C). Local cx := (coset_of R x). Local cy := (coset_of R y). Remark rmk0 : (EQ (generalize (M x)) (generalize (M y))). Proof (EQ_plug [u : Q](generalize u) hyp). Remark rmk1 : (EQ (generalize (M x)) cx). Proof (Quotient_Map_eq R x). Remark rmk2 : (EQ (generalize (M y)) cy). Proof (Quotient_Map_eq R y). Remark rmk3 : (EQ cx cy). Proof (EQ_trans (EQ_trans (EQ_sym rmk1) rmk0) rmk2). Remark rmk4 : (cx x). Proof (coset_of_pr R x). Remark rmk5 : (cy x). Proof (EQ_subs [C:X->Prop](C x) rmk4 rmk3). Remark rmk6 : (R y x). Proof (coset_of_rel R y x rmk5). Remark rmk7 : (R x y). Proof (equiv_sym rmk6). End quotient_relation. Lemma Quotient_Map_rel : (X:Type; R:(Equivalence_Relation X)) (x,y: X) (EQ (Quotient_Map R x) (Quotient_Map R y))-> (R x y). Proof (quotient_relation.rmk7). Implicits Quotient_Map_rel [1 3 4]. Lemma Quotient_Map_surj : (X : Type; R: (Equivalence_Relation X)) (is_surjective (Quotient_Map R)). Intros. Unfold is_surjective. Intros. Poser c '(generalize y). Assert (is_a_coset R c). Exact (generalize_pr y). Assert (exists c). Change (is_a_nonempty_subset c). Exact (coset_nonempty H). UseExists2 H0. Exhibit a. Assert (EQ (generalize (Quotient_Map R a)) (coset_of R a)). EApply Quotient_Map_eq. Assert (EQ c (coset_of R a)). EApply coset_of_uni. Assumption. Assumption. Assert (generalize (Quotient_Map R a)) == (generalize y). EApply EQ_eq. Trans9. Exact (generalize_inj ? ? ? ? H4). Save. Section quotient_lift_rel. Variable X:Type. Variable de : (description X). Variable R: (Equivalence_Relation X). Variable x : X. Local Q := (Quotient R). Local M := (Quotient_Map R). Local L := (Quotient_Lift de R). Local y := (L (M x)). Remark rmk1 : (EQ (M x) (M y)). Proof (Quotient_Lift_eq de R (M x)). Remark rmk2 : (R x y). Proof (Quotient_Map_rel R rmk1). Remark rmk3 : (R x (L (M x))). Proof rmk2. End quotient_lift_rel. Lemma Quotient_Lift_rel : (X:Type; de : (description X); R:(Equivalence_Relation X); x:X) (R x (Quotient_Lift de R (Quotient_Map R x))). Proof (quotient_lift_rel.rmk3). Implicits Quotient_Lift_rel [1]. Section quotient_pr. Variable X : Type. Variable R : (Equivalence_Relation X). Variables x,y: X. Hypothesis hyp : (R x y). Local Q := (Quotient R). Local M:= (Quotient_Map R). Local c := (coset_of R x). Local d := (coset_of R y). Remark rmk1 : (is_a_coset R c). Proof (coset_of_coset R x). Remark rmk2 : (is_a_coset R d). Proof (coset_of_coset R y). Remark rmk3 : (IN x c). Proof (coset_of_pr R x). Remark rmk4 : (IN y c). Proof (coset_trans rmk1 rmk3 hyp). Remark rmk5 : (EQ c d). Proof (coset_of_uni rmk1 rmk4). Remark rmk6 : (EQ (generalize (M x)) c). Proof (Quotient_Map_eq R x). Remark rmk7 : (EQ (generalize (M y)) d). Proof (Quotient_Map_eq R y). Remark rmk8 : (EQ (generalize (M x)) (generalize (M y))). Proof (EQ_trans rmk6 (EQ_trans rmk5 (EQ_sym rmk7))). Remark rmk9 : (EQ (M x) (M y)). EApply EQ_leib. EApply (generalize_inj ? ? (M x) (M y)). EApply EQ_eq. Exact rmk8. Save. End quotient_pr. Lemma Quotient_Map_pr : (X:Type; R:(Equivalence_Relation X); x,y: X) (R x y) -> (EQ (Quotient_Map R x) (Quotient_Map R y)). Proof (quotient_pr.rmk9). Implicits Quotient_Map_pr [1 2 3 4]. Theorem Quotient_Map_ap : (X:Type; R: (Equivalence_Relation X); x:X) ((generalize (Quotient_Map R x)) x). Intros. Unfold Quotient_Map. Unfold quotient_map_out. Change ((coset_of R x) x). Exact (coset_of_pr R x). Save. Section quotient_factor. Variables X,Y : Type. Variable de : (description X). Variable R : (Equivalence_Relation X). Variable F : X -> Y. Hypothesis hyp : (a,b: X) (R a b) -> (EQ (F a) (F b)). Local Q := (Quotient R). Local M := (Quotient_Map R). Local L := (Quotient_Lift de R). Local K := [q:Q](F (L q)). Section qfactA. Variable x: X. Remark rmk1 : (R x (L (M x))). Proof (Quotient_Lift_rel de R x). Remark rmk2 : (EQ (F x) (F (L (M x)))). Proof (hyp x (L (M x)) rmk1). Fact fact1 : (EQ (F x) (K (M x))). Proof (EQ_trans rmk2 (EQ_ref (F (L (M x))))). End qfactA. Remark rmk3 : (EQ F ([x:X](K (M x)))). Proof (extens_indep F ([x:X](K (M x))) fact1). Definition Quotient_Factor := K. Remark rmk4 : (EQ F (compose_functions K M)). Proof rmk3. End quotient_factor. Implicits Quotient_Factor [1 2]. (*** note that the hypothesis hyp isnt used in the definition of Quotient_Factor ***) Lemma Quotient_Factor_eq : (X,Y: Type; de : (description X); R:(Equivalence_Relation X)) (F:X->Y; hyp:(a,b:X)(R a b) -> (EQ (F a) (F b))) (EQ F (compose_functions (Quotient_Factor de R F) (Quotient_Map R))). Proof (quotient_factor.rmk4). Implicits Quotient_Factor_eq [1 2]. Definition mplug := EQ_plug. Implicits mplug [1 2 3 4 5]. Section quotient_factor_uni. Variables X,Y : Type. Variable de : (description X). Variable R : (Equivalence_Relation X). Variable F : X -> Y. Local Q := (Quotient R). Local M := (Quotient_Map R). Variable G : Q -> Y. Hypothesis hyp : (EQ F (compose_functions G M)). Local L := (Quotient_Lift de R). Local H := (Quotient_Factor de R F). Section qfuA. Variable q : Q. Local x : X := (L q). Remark rmk1 : (EQ (H q) (F x)). Proof (EQ_ref (F x)). Remark rmk2 : (EQ (F x) (G (M x))). Proof (EQ_plug [U:X -> Y](U x) hyp). Remark rmk3 : (EQ q (M (L q))). Proof (Quotient_Lift_eq de R q). Remark rmk4 : (EQ (G q) (G (M x))). Proof (mplug rmk3). Remark rmk5 : (EQ (G q) (H q)). Proof (EQ_trans rmk4 (EQ_trans (EQ_sym rmk2) (EQ_sym rmk1))). End qfuA. Remark rmk6 : (EQ G H). Proof (extens_indep G H (qfuA.rmk5)). Remark rmk7 : (EQ H G). Proof (EQ_sym rmk6). End quotient_factor_uni. Lemma Quotient_Factor_uni : (X,Y: Type; de : (description X); R : (Equivalence_Relation X)) (F:X->Y; G : (Quotient R) -> Y) (EQ F (compose_functions G (Quotient_Map R))) -> (EQ (Quotient_Factor de R F) G). Proof (quotient_factor_uni.rmk7). Implicits Quotient_Factor_uni [1 2 3 4 5]. Theorem Quotient_factorization_uni : (X,Y: Type; R:(Equivalence_Relation X); F : X-> Y; G1, G2 : (Quotient R)-> Y) (F== (compose_functions G1 (Quotient_Map R))) -> (F== (compose_functions G2 (Quotient_Map R))) -> (G1 == G2). Proof. Intros. EApply EQ_eq. EApply extens_indep. Intro q. Assert (exists [x:X]((Quotient_Map R x) == q)). Assert (is_surjective (Quotient_Map R)). EApply Quotient_Map_surj. Sel '(H1 q). UseExists2 H2. Exhibit a. Assumption. UseExists2 H1. Assert ((F a) == (G1 q)). RewriteB H. Unfold compose_functions. Rewrite H2. Trivial. Assert (F a) == (G2 q). RewriteB H0. Unfold compose_functions. Rewrite H2. Trivial. Trans9. Save. Section quotient_factor2. Variables X,Y : Type. Variable de : (description Y). Variable R : (Equivalence_Relation X). Variable F : X -> Y. Hypothesis hyp : (a,b: X) (R a b) -> (EQ (F a) (F b)). Local Q := (Quotient R). Local M := (Quotient_Map R). Section qfact2A. Variable q : Q. Definition qfact2_virt : Y -> Prop := [y:Y](x:X)((generalize q) x) -> (EQ (F x) y). Remark rmk1 : (exists qfact2_virt). Poser c '(generalize q). Assert (is_a_coset R c). Exact (generalize_pr q). Assert (exists [x:X](c x)). Change (is_a_nonempty_subset c). EApply coset_nonempty with R. EApply H. UseExists2 H0. Exhibit '(F a). Unfold qfact2_virt. Change (x:X)(c x) -> (EQ (F x) (F a)). Intros. Assert (R x a). EApply (coset_related H). Assumption. Assumption. EApply hyp. Assumption. Save. Remark rmk2 : (y,z: Y)(qfact2_virt y) -> (qfact2_virt z) -> y == z. Intros. Poser c '(generalize q). Assert (is_a_coset R c). Exact (generalize_pr q). Assert (exists c). Exact (coset_nonempty H1). UseExists2 H2. Assert (EQ (F a) y). EApply H. Assumption. Assert (EQ (F a) z). EApply H0. Assumption. EApply EQ_eq. Trans9. Save. Definition qfact2_out : Y := (choice de rmk1). Remark rmk3 : (x:X)((generalize q) x) -> (EQ (F x) qfact2_out). Intros. Assert (qfact2_virt qfact2_out). Exact (choice_pr1 de rmk1). EApply H0. Assumption. Save. End qfact2A. Definition quotient_factor2_out : Q -> Y := qfact2_out. Remark rmk4 : (x:X)(EQ (F x) (quotient_factor2_out (Quotient_Map R x))). Intros. Poser q '(Quotient_Map R x). Change (EQ (F x) (qfact2_out q)). EApply qfact2A.rmk3. EApply (Quotient_Map_ap X R x). Save. Remark rmk5 : (EQ F (compose_functions quotient_factor2_out (Quotient_Map R))). EApply extens_indep. Intro x. Exact (rmk4 x). Save. End quotient_factor2. Definition Quotient_Factor2 : (X, Y: Type; de : (description Y); R : (Equivalence_Relation X); F : X -> Y; hyp : (x,y: X)(R x y) -> (EQ (F x) (F y)))(Quotient R)-> Y := quotient_factor2_out. Theorem Quotient_Factor2_eq :(X, Y: Type; de : (description Y); R : (Equivalence_Relation X); F : X -> Y; hyp : (x,y: X)(R x y) -> (EQ (F x) (F y))) (F == (compose_functions (Quotient_Factor2 X Y de R F hyp) (Quotient_Map R))). Proof. Intros. EApply EQ_eq. Exact (quotient_factor2.rmk5 X Y de R F hyp). Save. Theorem Quotient_Factor2_uni : (X, Y: Type; de : (description Y); R : (Equivalence_Relation X); F : X -> Y; hyp : (x,y: X)(R x y) -> (EQ (F x) (F y))) (G : (Quotient R) -> Y)(F == (compose_functions G (Quotient_Map R)))-> (G == (Quotient_Factor2 X Y de R F hyp)). Proof. Intros. EApply EQ_eq. EApply extens_indep. Intro q. Assert (exists [x:X](Quotient_Map R x) == q). Assert (is_surjective (Quotient_Map R)). EApply Quotient_Map_surj. EApply H0. UseExists2 H0. Sel '(Quotient_Factor2_eq X Y de R F hyp). Assert (EQ (F a) (Quotient_Factor2 X Y de R F hyp q)). RewriteB H1. Poser F1 '(compose_functions (Quotient_Factor2 X Y de R F hyp) (Quotient_Map R)). Change (EQ (F a) (F1 a)). Assert F == F1. Exact H2. Rewrite H3. Exact (EQ_ref ?). Assert (F a) == (G q). Rewrite H. RewriteB H1. Trivial. Trans9. Save. (********************************************************************* ********************************************************************** ********************************************************************** ********************************************************************** ********************************************************************** *********************************************************************)