-- File: axiomatizing -- In this file we postulate only the axiom of choice and the existence of -- quotient and subset types, and show how to prove the existence of quotient -- and subset algebras from these axioms. -- This file is divided into three parts. -- 1. The axiom of choice and the axioms stating the existence of quotient -- and subset types. This corresponds to definition 6.8.1.3 on page 194. -- We also show that the existence of QuotSubset types follows from the -- last two axioms. -- 2. We prove the existence of quotient and subset algebras for all -- simply-typed interfaces (including higher-order ones). This corresponds -- to Conjectures 6.8.2.1, 6.8.2.2 and 6.8.2.6 -- 3. We prove the existence of quotient and subset algebras for first-order -- interfaces. This does not follow directly from part 2, since the -- theorems that state the existence are formulated quite differently. -- This corresponds to Theorem 6.8.1.4. Path "../lol" Path "../lolExtra" Load "lambdaLplus" Load "parametricity" ---------------------- ---------------------- -- -- -- 1. A X I O M S -- -- -- ---------------------- ---------------------- Var axiom_choice : @A,B:*s.@P:A->B->*p. (@x:A.Ex y:B. P x y) -> Ex f:A->B. @x:A. P x (f x) Def IsQuotType := \R:*s. \(~~):R->R->*p. \Q:*s. Ex surj:R->Q. (@r,r':R. r ~~ r' <=> surj r = surj r') /\ IsSurjection surj : @R:*s. (R->R->*p) -> *s -> *p Var exis_QuotType : @R:*s. @(~~):R->R->*p. IsER (~~) -> ExK Q:*s. IsQuotType R (~~) Q Def IsSubsetType := \R:*s. \Inv:R->*p. \S:*s. Ex inj:S->R. IsInjection inj /\ (Inv <==> Image inj) : @R:*s. (R->*p) -> *s -> *p Var exis_SubsetType : @R:*s. @Inv:R->*p. ExK S:*s. IsSubsetType R Inv S Def IsQuotSubsetType := \R:*s. \(~~):R->R->*p. \Inv:R->*p. \Q:*s. ExR rel:R->Q->*p. (Inv <==> Dom rel) /\ (@q:Q. Ex r:R. rel r q) /\ (@r,r':R. @q,q':Q. rel r q -> rel r' q' -> r~~r' <=> q=q') : @R:*s. (R->R->*p) -> (R->*p) -> *s -> *p Prove exis_QuotSubsetType : @R:*s. @(~~):R->R->*p. @Inv:R->*p. IsERon (~~) Inv -> ExK Q:*s. IsQuotSubsetType R (~~) Inv Q Intros ExistsE exis_SubsetType On Inv Unfold IsSubsetType In H2 ExistsE H2 AndE H3 First IsER (\s1,s2:S. inj s1 ~~ inj s2) Unfold IsER Unfold IsERon In H AndE H AndE H7 AndI Intro Apply H6 Rewrite H5 Apply Image_f_f_x AndI Intros 2 Apply H8 Rewrite H5 Apply Image_f_f_x Rewrite H5 Apply Image_f_f_x Intros 3 Apply H9 Rewrite H5 Then Apply Image_f_f_x Rewrite H5 Then Apply Image_f_f_x Rewrite H5 Then Apply Image_f_f_x Intro ExistsE exis_QuotType On H6 ExistsI Q Unfold IsQuotType In H8 ExistsE H8 AndE H9 Unfold IsQuotSubsetType ExistsI \r:R.\q:Q. Ex s:S. r = inj s /\ q = surj s Repeat AndI Rewrite H5 Apply equiv_predQ Intro x Unfold Image Unfold Dom Apply equiv_prop Then Intros ExistsE H12 ExistsI surj a ExistsI a AndI Apply is_sym Assumption Refl ExistsE H12 ExistsE H13 AndE H14 ExistsI s Apply is_sym Assumption Intro ExistsE H11 On q ExistsI inj a ExistsI a AndI Refl Apply is_sym Assumption Intros ExistsE H12 ExistsE H13 AndE H14 AndE H15 Rewrite H16 Then Rewrite H17 Then Rewrite H18 Then Rewrite H19 Apply H10 Exit ---------------------------------------------------- ---------------------------------------------------- -- -- -- 2. H I G H E R - O R D E R A L G E B R A S -- -- -- ---------------------------------------------------- ---------------------------------------------------- -- auxialary result Prove has_elem : @I:*s->*s. SimplyT I -> @R : *s. @S : *s. (Ex r:R. True) -> (Ex s:S. True) -> (Ex r:I R. True) -> (Ex s:I S. True) Intros 2 Pattern I Apply H Intros Assumption Intros Assumption Intros Cut Ex s:I1 S -> I2 S. @t:I1 S. (\a:I1 S.\b:I2 S. True) t (s t) Intro ExistsE H6 ExistsI s Exact true_True Apply axiom_choice Intro ExistsE H1 On H4, H3 ExistsI x Exact true_True ExistsE H5 ExistsE H2 On H3, H4 ExistsI r s Assumption Assumption Intros ExistsE H5 ExistsE H1 On H3, H4 ExistsI r`l Assumption ExistsE H2 On H3, H4 ExistsI r`r Then Assumption ExistsI {l=s,r=s1} Assumption Exit -- induction-step for Sim_LeftC for the case I = I1 -> I2 prove Sim_lemma : @I1,I2 : *s->*s. SimplyT I1 -> SimplyT I2 -> @Y,Z : *s. (Ex r:Y. True) -> (Ex s:Z. True) -> @(~) : Y->Z->*p. IsZclosed (Sim I2 Y Z (~)) -> LeftC (Sim I1 Y Z (~)) <===> Sim I1 Y Y (LeftC (~)) -> LeftC (Sim I2 Y Z (~)) <===> Sim I2 Y Y (LeftC (~)) -> LeftC (Sim (\X:*s. I1 X -> I2 X) Y Z (~)) <===> Sim (\X:*s. I1 X -> I2 X) Y Y (LeftC (~)) Intros Repeat Rewrite Sim_arrow Unfold 1 LeftC Apply equiv_predR Intro x,y Apply equiv_prop Intros 3 Lewrite H5 Intro ExistsE H7 AndE H9 Unfold LeftC In H8 ExistsE H8 AndE H12 Lewrite H6 Unfold LeftC Forward H10 On H13 Forward H11 On H14 ExistsI z1 z2 AndI Then Assumption Intros Cut Ex z:I1 Z -> I2 Z. @z1:I1 Z. (\a:I1 Z.\fa:I2 Z. (@y1:I1 Y. Sim I1 Y Z (~) y1 a -> Sim I2 Y Z (~) (x y1) fa) /\ (@y1:I1 Y. Sim I1 Y Z (~) y1 a -> Sim I2 Y Z (~) (y y1) fa)) z1 (z z1) Intro ExistsE H8 ExistsI z AndI Intros 2 AndEL H9 On z2 Apply H11 Intros 2 AndER H9 On z2 Apply H11 Apply axiom_choice Intro Apply exm On Ex y1:I1 Y. Sim I1 Y Z (~) y1 x1 Intro ExistsE H8 Forward H9 Let H11 := *p -- dummy Forward rel_LeftC On H10, H10 Rewrite H5 In H12 Forward H7 On H13 Lewrite H6 In H14 Unfold LeftC In H15 ExistsE H15 AndE H16 ExistsI z AndI Intros Forward rel_LeftC On H19, H10 Rewrite H5 In H20 Forward H7 On H21 Lewrite H6 In H22 Unfold LeftC In H23 ExistsE H23 AndE H24 Apply H4 On H26 Then Assumption Intros Forward rel_LeftC On H10, H19 Rewrite H5 In H20 Forward H7 On H21 Lewrite H6 In H22 Unfold LeftC In H23 ExistsE H23 AndE H24 Apply H4 On H25 Then Assumption Intro First Ex s:I1 Z. True ExistsI x1 Then Exact true_True Intro ExistsE has_elem On H2, H9 Assumption Assumption First Ex z:I2 Z. True Apply has_elem On H2 Assumption Assumption ExistsI x s Assumption Intro ExistsE H12 ExistsI z AndI Intros FalseE NotE H8 ExistsI y1 Assumption Intros FalseE NotE H8 ExistsI y2 Assumption Exit Prove Sim_LeftC : @I:*s->*s. SimplyT I -> @Y : *s. @Z : *s. (Ex r:Y.True) -> (Ex s:Z.True) -> @(~) : Y->Z->*p. IsZclosed (~) -> (Sim I Y Y (LeftC (~)) <===> LeftC (Sim I Y Z (~))) Intros 4 Then Intro Y_not_empty,Z_not_empty Then Intros 2 Pattern I Apply SimplyT_elim On H Repeat Rewrite Sim_id Refl Intro Repeat Rewrite Sim_const Unfold LeftC Apply equiv_predR Intros Apply equiv_prop Then Intros ExistsI b AndI Assumption Refl ExistsE H2 AndE H3 Rewrite H5 Assumption Intro I1,I2 Intros Apply BimplR_sym Apply Sim_lemma Then Try Assumption Apply IsZclosed_Sim Assumption Assumption Apply BimplR_sym Assumption Apply BimplR_sym Assumption Intro I1,I2 Intros Repeat Rewrite Sim_rec Apply equiv_predR Intros Unfold 3 LeftC Apply equiv_prop Intros AndE H6 Rewrite H4 In H7 Rewrite H5 In H8 Unfold LeftC In H9 Then ExistsE H9 Unfold LeftC In H10 Then ExistsE H10 AndE H11 AndE H12 ExistsI {l= z,r= z1} Repeat AndI Then Assumption Intros ExistsE H6 AndE H7 AndE H8 AndE H9 AndI Rewrite H4 Apply rel_LeftC On H10, H12 Apply rel_LeftC On H11, H13 Intros AndE H14 Rewrite H5 Apply rel_LeftC On H15, H16 Exit -- simple corollary of Sim_LeftC prove Sim_LeftC_weak : @I:*s->*s. SimplyT I -> @Y : *s. @Z : *s. (Ex r:Y.True) -> (Ex s:Z.True) -> @(~) : Y->Z->*p. IsZclosed (~) -> @opsY : I Y. Bisim I Y (LeftC (~)) opsY -> Ex opsZ : I Z. Sim I Y Z (~) opsY opsZ Intros Unfold Bisim In H4 Rewrite Sim_LeftC In H4 Then Try Assumption Unfold LeftC In H5 ExistsE H5 AndE H6 ExistsI z Assumption Exit -- Now we are ready to consider quotient/subset algebras. Def IsQuotAlg := \I:*s->*s. \R:*s. \opsR : I R. \(~~):R->R->*p. \Q:*s. \opsQ : I Q. Ex surj:R->Q. (@r,r':R. r ~~ r' <=> surj r = surj r') /\ IsSurjection surj /\ Sim I R Q (\r:R.\q:Q. q = surj r) opsR opsQ : @I:*s->*s.@R:*s. I R -> (R->R->*p) -> @Q:*s. I Q -> *p Def IsSubsetAlg := \I:*s->*s.\R:*s. \opsR : I R. \Inv:R->*p. \S:*s.\opsS : I S. Ex inj:S->R. IsInjection inj /\ (Inv <==> Image inj) /\ Sim I R S (\r:R.\s:S. r = inj s) opsR opsS : @I:*s->*s. @R:*s. I R -> (R->*p) -> @S:*s. I S -> *p Def IsQuotSubsetAlg := \I:*s->*s. \R:*s. \opsR : I R. \(~~) : R->R->*p. \Inv:R->*p. \Q:*s. \opsQ : I Q. ExR rel:R->Q->*p. (Inv <==> Dom rel) /\ (@q:Q. Ex r:R. rel r q) /\ (@r,r':R. @q,q':Q. rel r q -> rel r' q' -> r~~r' <=> q=q') /\ Sim I R Q rel opsR opsQ : @I:*s->*s.@R:*s. I R -> (R->R->*p) -> (R->*p) -> @Q:*s. I Q -> *p Prove exis_QuotSubsetAlgHO : @I:*s->*s. SimplyT I -> @R:*s. @opsR:I R. @(~~):R->R->*p. @Inv:R->*p. IsERon (~~) Inv -> (Ex r:R. Inv r) -> Bisim I R (Restr (~~) Inv) opsR -> ExK Q:*s. Ex opsQ: I Q. IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ Intros ExistsE exis_QuotSubsetType On Inv, H1 ExistsI Q Unfold IsQuotSubsetType In H5 ExistsE H5 AndE H6 AndE H8 First Restr (~~) Inv <===> LeftC rel Apply equiv_predR Intro x,y Apply equiv_prop Then Intro Unfold Restr In H11 AndE H11 AndE H13 Unfold LeftC Rewrite H7 In H12 Rewrite H7 In H15 Unfold Dom In H16 Then ExistsE H16 Unfold Dom In H17 Then ExistsE H17 ExistsI b AndI Assumption First b=b1 Lewrite H10 On H18, H19 Then Assumption Intro Rewrite H20 Assumption Unfold LeftC In H11 ExistsE H11 AndE H12 Unfold Restr Repeat AndI Rewrite H7 Unfold Dom Then ExistsI z Assumption Rewrite H10 On H13, H14 Refl Rewrite H7 Unfold Dom Then ExistsI z Assumption Intro Rewrite H11 In H3 First Ex r:R. True ExistsE H2 ExistsI r Exact true_True Intro R_not_empty First Ex q:Q. True ExistsE H2 Rewrite H7 In H13 Unfold Dom In H14 ExistsE H14 ExistsI b Exact true_True Intro Q_not_empty Forward Sim_LeftC_weak On H12 Then Try Assumption Unfold IsZclosed Intros First z1=z2 Lewrite H10 On H13, H14 Rewrite H10 On H13, H13 Refl Intro Rewrite H16 Assumption ExistsE H13 Unfold IsQuotSubsetAlg ExistsI opsZ ExistsI rel Repeat AndI Then Try Assumption Exit Prove exis_QuotAlgHO : @I:*s->*s. SimplyT I -> @R:*s. @opsR:I R. @(~~):R->R->*p. Bisim I R (~~) opsR -> IsER (~~) -> ExK Q:*s. Ex opsQ: I Q. IsQuotAlg I R opsR (~~) Q opsQ Intros 5 OrE exm (Ex r:R. True) Intros ExistsE exis_QuotType On H3 ExistsI Q Unfold IsQuotType In H5 ExistsE H5 AndE H6 Let (~) := \r:R.\q:Q. q = surj r First LeftC (~) <===> (~~) Unfold LeftC Unfold (~) Apply equiv_predR Intros Rewrite H7 Apply equiv_prop Then Intro ExistsE H9 AndE H10 Lewrite H11 Assumption ExistsI surj b AndI Apply is_sym Assumption Refl Intro Lewrite H9 In H2 Forward Sim_LeftC_weak On H10 Then Try Assumption ExistsE H1 ExistsI surj r Assumption Unfold IsZclosed Unfold (~) Intros Rewrite H11 Lewrite H12 Assumption Unfold LeftC In H11 ExistsE H11 Unfold IsQuotAlg ExistsI opsZ ExistsI surj Repeat AndI Then Assumption Intros ExistsI R ExistsI opsR Unfold IsQuotAlg ExistsI \r:R. r First @r:R. False Intro NotE H1 ExistsI r Exact true_True Intros Repeat AndI Intros FalseE Apply H4 Assumption Unfold IsSurjection Intro FalseE Apply H4 Assumption First (=) R <===> (\r,q:R. q=r) Apply equiv_predR Intro x,y Apply equiv_prop Then Intro Then Rewrite H5 Then Refl Intro Lewrite H5 Rewrite Sim_is Assumption Refl Exit Prove exis_SubsetAlgHO : @I:*s->*s. SimplyT I -> @R:*s. @opsR:I R. @Inv:R->*p. (Ex r:R. Inv r) -> Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR -> ExK S:*s. Ex opsS: I S. IsSubsetAlg I R opsR Inv S opsS Intros ExistsE exis_SubsetType On Inv ExistsI S Unfold IsSubsetType In H4 ExistsE H4 AndE H5 Let (~) := \r:R.\s:S. r = inj s First (\r1,r2:R. Inv r1 /\ r1=r2) <===> LeftC (~) Unfold (~) Unfold LeftC Apply equiv_predR Intros Apply equiv_prop Then Intro AndE H8 Rewrite H7 In H9 Unfold Image In H11 ExistsE H11 ExistsI a1 AndI Apply is_sym Assumption Lewrite H10 Apply is_sym Assumption ExistsE H8 AndE H9 AndI Rewrite H7 Rewrite H10 Apply Image_f_f_x Rewrite H11 Assumption Intro Rewrite H8 In H2 Forward Sim_LeftC_weak On H9 Then Try Assumption ExistsE H1 ExistsI r Exact true_True ExistsE H1 Rewrite H7 In H10 Unfold Image In H11 ExistsE H11 ExistsI a Exact true_True Unfold IsZclosed Unfold (~) Intros Lewrite H10 Rewrite H11 Assumption ExistsE H10 ExistsI opsZ Unfold IsSubsetAlg ExistsI inj Repeat AndI Then Try Assumption Exit -------------------------------------------------- -------------------------------------------------- -- -- -- 3. F I R S T - O R D E R A L G E B R A S -- -- -- -------------------------------------------------- -------------------------------------------------- -- We first consider quotients, then subsets, and then quotients of subsets. --------------- -- QUOTIENTS -- --------------- Prove exis_QuotAlg :@I:*s->*s. FirstO I -> @R:*s. @opsR:I R. @(~~):R->R->*p. Bisim I R (~~) opsR -> IsER (~~) -> ExK Q:*s. Ex opsQ: I Q. IsQuotAlg I R opsR (~~) Q opsQ Intros 2 Apply exis_QuotAlgHO Apply FirstO__SimplyT Assumption Exit ------------- -- SUBSETS -- ------------- -- Now first-order subset algebras. We do this in two steps. -- First we prove exis_SubsetAlg_Bisim, i.e. -- @I:*s->*s. FirstO I -> -- @R:*s. @Inv:R->*p. @opsR:I R. -- Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR -> -- ExK S:*s. Ex opsS: I S. -- IsSubsetAlg I R opsR Inv S opsS -- This requires three auxiliary results. -- Then it is easy to prove exis_SubsetAlg. -- Auxiliary result 1: Sim_LeftC for Basic interfaces, but with possibly -- empty types. prove Sim_Basic_LeftC_strong : @I:*s->*s. Basic I -> @Y : *s. @Z : *s. @(~) : Y->Z->*p. IsZclosed (~) -> Sim I Y Y (LeftC (~)) <===> LeftC (Sim I Y Z (~)) Intros Apply Basic_elim On H Repeat Rewrite Sim_id Refl Intros Repeat Rewrite Sim_const Apply equiv_predR Unfold LeftC Intros Apply equiv_prop Then Intro ExistsI b AndI Assumption Refl ExistsE H2 AndE H3 Rewrite H5 Assumption Intros Repeat Rewrite Sim_rec Apply equiv_predR Intros Rewrite H4 Rewrite H5 Apply equiv_prop Then Intro Unfold LeftC In H6 AndE H6 ExistsE H7 AndE H9 ExistsE H8 AndE H12 Unfold LeftC ExistsI {l= z,r= z1} Repeat AndI Then Assumption Unfold LeftC In H6 ExistsE H6 AndE H7 AndE H8 AndE H9 Unfold LeftC AndI ExistsI z`l AndI Then Assumption ExistsI z`r AndI Then Assumption Exit -- Auxiliary result 2 prove Sim_FirstO_LeftC_weak_lemma : @I:*s->*s. Basic I -> @Y : *s. @Z : *s. @(~) : Y->Z->*p. (@z:Z. Ex y:Y. y~z) -> (@opsZ:I Z. Ex opsY:I Y. Sim I Y Z (~) opsY opsZ ) Intros 6 Apply Basic_elim On H Rewrite Sim_id Assumption Intros Rewrite Sim_const ExistsI opsZ Refl Intros ExistsE H4 On opsZ`l ExistsE H5 On opsZ`r ExistsI {l= opsY,r= opsY1} Rewrite Sim_rec AndI Then Assumption Exit -- Auxiliary result 3 prove Sim_FirstO_LeftC_weak : @I:*s->*s. FirstO I -> @Y : *s. @Z : *s. @(~) : Y->Z->*p. IsZclosed (~) -> (@z:Z. Ex y:Y. y~z) -> @opsY,opsY':I Y. Sim I Y Y (LeftC (~)) opsY opsY' -> LeftC (Sim I Y Z (~)) opsY opsY' Intros 6 Intro prop_twig Apply FirstO_elim On H Intros Lewrite Sim_Basic_LeftC_strong Assumption Assumption Assumption Intros 4 Repeat Rewrite Sim_arrow Intro Then Intro x,y Then Intros Unfold LeftC Cut Ex z:I2 Z -> I3 Z. @z1:I2 Z. (\z1:I2 Z.\zz1:I3 Z. @y1:I2 Y. Sim I2 Y Z (~) y1 z1 -> Sim I3 Y Z (~) (x y1) zz1 /\ Sim I3 Y Z (~) (y y1) zz1) z1 (z z1) Simplify Intro ExistsE H6 ExistsI z AndI Intros AndE H7 On H8 Assumption Intros AndE H7 On H8 Assumption Apply axiom_choice Intro OrE exm On Ex y1:I2 Y. Sim I2 Y Z (~) y1 x1 ExistsE H7 Forward H4 On x y1, y y1 Unfold 2 LeftC In H9 ExistsE H9 Apply H5 Rewrite Sim_Basic_LeftC_strong Assumption Assumption Apply rel_LeftC On H8, H8 AndE H11 ExistsI z Intros AndI Forward rel_LeftC On H14, H8 Lewrite Sim_Basic_LeftC_strong In H15 Assumption Assumption Forward H5 On H16 Forward H4 On H17 Unfold LeftC In H18 ExistsE H18 AndE H19 Forward IsZclosed_Sim On I3, H1 Apply FirstO__SimplyT Assumption Apply H22 On H21 Then Assumption Forward rel_LeftC On H8, H14 Lewrite Sim_Basic_LeftC_strong In H15 Assumption Assumption Forward H5 On H16 Forward H4 On H17 Unfold LeftC In H18 ExistsE H18 AndE H19 Forward IsZclosed_Sim On I3, H1 Apply FirstO__SimplyT Assumption Apply H22 On H20 Then Assumption Cut Ex z:I3 Z. True Intro ExistsE H8 ExistsI z Intros FalseE NotE H7 ExistsI y2 Assumption Cut @z:Z. Ex y:Y. y~z Intro Cut @z:I2 Z. Ex y:I2 Y. Sim I2 Y Z (~) y z Intro ExistsE H9 On x1 Forward rel_LeftC On H11, H11 Lewrite Sim_Basic_LeftC_strong In H12 Assumption Assumption Forward H5 On H13 Forward H4 On H14 Unfold LeftC In H15 ExistsE H15 ExistsI z Exact true_True Apply Sim_FirstO_LeftC_weak_lemma Assumption Assumption Exact prop_twig Intros 6 Then Intro x,y Repeat Rewrite Sim_rec Intros AndE H6 Unfold LeftC Forward H4 On H7 Forward H5 On H8 Unfold LeftC In H9 ExistsE H9 AndE H11 Unfold LeftC In H10 ExistsE H10 Then AndE H14 ExistsI {l= z,r= z1} Repeat AndI Then Assumption Exit -- The next result is equal to exis_SubsetAlg, except that it has -- Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR -- instead of -- IsInvar I R Inv opsR Prove exis_SubsetAlg_Bisim : @I:*s->*s. FirstO I -> @R:*s. @Inv:R->*p. @opsR:I R. Bisim I R (\r1,r2:R. Inv r1 /\ r1=r2) opsR -> ExK S:*s. Ex opsS: I S. IsSubsetAlg I R opsR Inv S opsS Intros ExistsE exis_SubsetType On Inv ExistsI S Unfold IsSubsetType In H3 ExistsE H3 AndE H4 Let (~) := \r:R.\s:S. r = inj s First (\r1,r2:R. Inv r1 /\ r1=r2) <===> LeftC (~) Apply equiv_predR Unfold LeftC Unfold (~) Intros Apply equiv_prop Intros AndE H7 Rewrite H6 In H8 Unfold Image In H10 ExistsE H10 ExistsI a1 AndI Rewrite H11 Refl Rewrite H11 Rewrite H9 Refl Intros ExistsE H7 AndE H8 AndI Rewrite H9 Rewrite H6 Apply Image_f_f_x Rewrite H10 Assumption Intro Rewrite H7 In H1 Unfold Bisim In H8 Forward Sim_FirstO_LeftC_weak On H8 Assumption Unfold (~) Unfold IsZclosed Intros Rewrite H11 Lewrite H10 Assumption Unfold (~) Intros ExistsI inj z Refl Unfold LeftC In H9 ExistsE H9 AndE H10 ExistsI z Unfold IsSubsetAlg ExistsI inj Repeat AndI Then Try Assumption Exit Prove exis_SubsetAlg : @I:*s->*s. FirstO I -> @R:*s. @opsR:I R. @Inv:R->*p. IsInvar I R Inv opsR -> ExK S:*s. Ex opsS: I S. IsSubsetAlg I R opsR Inv S opsS Intros Apply exis_SubsetAlg_Bisim Assumption First (\r1,r2:R. Inv r1 /\ r1=r2) <===> Restr ((=) R) Inv Apply equiv_predR Unfold Restr Intros Apply equiv_prop Then Intros AndE H2 Lewrite 2 H4 Repeat AndI Then Assumption AndE H2 AndE H4 AndI Then Assumption Intro Rewrite H2 Unfold Bisim Apply Sim_FirstO_Restr Assumption Rewrite Sim_is Apply FirstO__SimplyT Assumption Unfold Restr Repeat AndI Then Try Assumption Refl Exit -------------------------- -- QUOTIENTS OF SUBSETS -- -------------------------- -- By combining exis_QuotAlg and exis_SubsetAlg prove exis_QuotSubsetAlg : @I:*s->*s. FirstO I -> @R:*s. @opsR:I R. @(~~):R->R->*p. @Inv:R->*p. IsERon (~~) Inv -> Bisim I R (~~) opsR -> IsInvar I R Inv opsR -> ExK Q:*s. Ex opsQ: I Q. IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ Intros ExistsE exis_SubsetAlg On H3 Assumption ExistsE H5 Unfold IsSubsetAlg In H6 ExistsE H6 AndE H7 AndE H9 Let (~) := \s1,s2:S. inj s1 ~~ inj s2 First Bisim I S (~) opsS First Sim I R R (Restr (~~) Inv) opsR opsR Apply Sim_FirstO_Restr Assumption Unfold Restr Repeat AndI Then Assumption Intro Forward SimFirstO_Trans On H12, H11 Assumption First Comp (Restr (~~) Inv) (\r:R.\s:S. r = inj s) <===> (\r:R.\s:S. Inv r /\ r ~~ inj s) Apply equiv_predR Intros Unfold Comp Apply equiv_prop Then Intro ExistsE H14 Unfold Restr In H15 AndE H15 AndE H16 AndE H19 AndI Assumption Lewrite H17 Assumption AndE H14 ExistsI inj b Unfold Restr Repeat AndI Then Try Assumption Rewrite H10 Apply Image_f_f_x Refl Intro Rewrite H14 In H13 Hide H13 Forward Sim_sym On H15 Apply FirstO__SimplyT Assumption Forward SimFirstO_Trans On H16, H15 Assumption First (Comp (Inverse (\r:R.\s:S. Inv r /\ r ~~ inj s)) (\r:R.\s:S. Inv r /\ r ~~ inj s)) <===> (~) Apply equiv_predR Intros Unfold Inverse Unfold Comp Unfold (~) Apply equiv_prop Then Intro ExistsE H18 AndE H19 AndE H20 AndE H21 Unfold IsERon In H1 AndE H1 AndE H27 Apply H29 On H25 Rewrite H10 Then Apply Image_f_f_x Assumption Rewrite H10 Then Apply Image_f_f_x Apply H28 Assumption Rewrite H10 Then Apply Image_f_f_x Assumption ExistsI inj a Repeat AndI Rewrite H10 Then Apply Image_f_f_x Unfold IsERon In H1 AndE H1 Apply H19 Rewrite H10 Then Apply Image_f_f_x Rewrite H10 Then Apply Image_f_f_x Assumption Intro Unfold Bisim Lewrite H18 Assumption First IsER (~) Unfold IsERon In H1 AndE H1 AndE H13 Unfold (~) Unfold IsER Repeat AndI Intro Apply H12 Rewrite H10 Then Apply Image_f_f_x Intros 2 Apply H14 Rewrite H10 Then Apply Image_f_f_x Rewrite H10 Then Apply Image_f_f_x Intros 3 Apply H15 Rewrite H10 Then Apply Image_f_f_x Rewrite H10 Then Apply Image_f_f_x Rewrite H10 Then Apply Image_f_f_x Intros ExistsE exis_QuotAlg On H13 Assumption Assumption ExistsI Q ExistsE H15 ExistsI opsQ Unfold IsQuotAlg In H16 ExistsE H16 AndE H17 AndE H19 Unfold IsQuotSubsetAlg Let Rel := \r:R.\q:Q. Ex s:S. r = inj s /\ q = surj s ExistsI Rel Repeat AndI Rewrite H10 Unfold Rel Apply equiv_predQ Intro Apply equiv_prop Then Intro Unfold Dom Unfold Image In H22 ExistsE H22 ExistsI surj a1 ExistsI a1 AndI Rewrite H23 Refl Refl Unfold Dom In H22 ExistsE H22 ExistsE H23 AndE H24 Rewrite H25 Apply Image_f_f_x Intro Unfold Rel ExistsE H20 On q ExistsI inj a ExistsI a AndI Refl Rewrite H23 Refl Unfold Rel Intros ExistsE H22 ExistsE H23 AndE H24 AndE H25 Rewrite H26 Rewrite H27 Rewrite H28 Rewrite H29 Lewrite H18 Unfold (~) Refl Forward SimFirstO_Trans On H11, H21 Assumption First Comp (\r:R.\s:S. r = inj s) (\r:S.\q:Q. q = surj r) <===> Rel Unfold Rel Unfold Comp Refl Intro Lewrite H23 Assumption Exit