-- 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


----------------------------------------------------
----------------------------------------------------
--                                                --
--  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)

-- 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 (~))

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 (~)))

-- 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


-- 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

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

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


--------------------------------------------------
--------------------------------------------------
--                                              --
--  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

-------------
-- 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 (~))

-- 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 )

-- 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'

-- 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

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


--------------------------
-- 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