-- 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
LatexVar 1 IsQuotAlg

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
LatexVar 1 IsSubsetAlg

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
LatexVar 1 IsQuotSubsetAlg

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