-- File: library

-- This file gives our general theory of ADTs, leading to the main theorems.
-- It follows the structure of Sections 6.7.4, 6.7.5, and 6.7.6, and is hence
-- divided in the following parts.
--  4. Quotients and Subsets (Section 6.7.4)
--  5. Sensible and well-behaved (Section 6.7.5)
--  6. Main results (Section 6.7.6)


Path "../lol"
Path "../lolExtra"
Load "lambdaLplus"
Load "parametricity"


----------------------------------------------------
----------------------------------------------------
--                                                --
--  4. Q U O T I E N T S   A N D   S U B S E T S  --
--                                                --
----------------------------------------------------
----------------------------------------------------

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

var 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


var 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

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

Prove pack_QuotSubset : @I:*s->*s. SimplyT I ->
                 @R:*s. @opsR:I R. @(~~):R->R->*p.
                 @Inv: R->*p.
                 @Q:*s. @opsQ:I Q. IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ ->
                 (=) (Sig X:*s. I X) (pack I R opsR) (pack I Q opsQ)


------------------------------------------------------------
------------------------------------------------------------
--                                                        --
--  5. S E N S I B L E   A N D   W E L L - B E H A V E D  --
--                                                        --
------------------------------------------------------------
------------------------------------------------------------

Def Sensible := \I:*s->*s. \Spec : @R:*s.(R->R->*p) -> (R->*p) -> I R -> *p.
                 @R:*s.@opsR:I R.@(~~):R->R->*p. @Inv:R->*p.@Q:*s.@opsQ:I Q.
                 IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ ->
                 Spec R (~~) Inv opsR -> Spec Q ((=) Q) (\q:Q.True) opsQ
LatexVar 1 Sensible

Def WB := \I:*s->*s.
     \Spec: (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p).
     @Y,Z:*s. 
     @RelY:Y->Y->*p.  @RelZ:Z->Z->*p.
     @InvY:Y->*p. @InvZ:Z->*p. IsERon RelY InvY -> IsERon RelZ InvZ ->
     @opsY:I Y. @opsZ : I Z.
     (ExR (~):Y->Z->*p.
       Sim I Y Z (~) opsY opsZ /\
       (Restr RelY InvY <===> LeftC (~)) /\
       (Restr RelZ InvZ <===> RightC (~)) /\
       IsZclosed (~)) ->
     Spec Y RelY InvY opsY -> Spec Z RelZ InvZ opsZ
Implicit 1 WB
LatexVar 1 WB

-- For proving properties about WB, it is easier to use the following,
-- equivalent formulation.
Def WB' := \I:*s->*s.
     \Spec: (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p).
     @Y,Z:*s.
     @RelY:Y->Y->*p. @RelZ:Z->Z->*p.
     @InvY:Y->*p. @InvZ:Z->*p.
     @opsY:I Y. @opsZ : I Z.
     @(~):Y->Z->*p.
       Sim I Y Z (~) opsY opsZ ->
       IsZclosed (~) ->
       (Restr RelY InvY) <===> LeftC (~) ->
       (Restr RelZ InvZ) <===> RightC (~) ->
       IsERon RelY InvY ->
       IsERon RelZ InvZ ->
       Spec Y RelY InvY opsY -> Spec Z RelZ InvZ opsZ
Implicit 1 WB'
LatexVar 1 WB'

-- WB and WB' are really equivalent:
Prove WB__WB' : @I:*s->*s. @Spec : (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p).
                WB' I Spec <=> WB I Spec

Prove WB__Sensible : @I:*s->*s. SimplyT I -> 
            @Spec: (@R:*s. (R->R->*p)->(R->*p)->I R->*p).
            WB' I Spec -> Sensible I Spec

Prove WB_Prop: @I:*s->*s. @P:*p.
   WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p.\ops:I R.  P)

Prove WB_Impl : @I:*s->*s. SimplyT I ->
   @P,Q:(@R:*s. (R->R->*p)->(R->*p)->I R->*p).
   WB' P -> WB' Q ->
   WB' (\R:*s.\(~~):R->R->*p.\Inv:R->*p.\ops:I R. 
                     P R (~~) Inv ops -> Q R (~~) Inv ops)

Prove WB_Pred : @I:*s->*s. SimplyT I ->
    @A:*s. @f: @R:*s. I R -> A. @P:A->*p.
    WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p.\ops:I R. 
                              P (f R ops))

Prove WB_Univ : @I:*s->*s.
  @A:*s. @P:A->(@R:*s. (R->R->*p)->(R->*p)->I R->*p).
  (@a:A. WB' (P a)) -> 
  WB' (\R:*s.\(~~):R->R->*p.\Inv:R->*p.\ops:I R. 
                    @a:A. P a R (~~) Inv ops)

Prove WB_Tw : @I:*s->*s. SimplyT I ->
    @f,g: @R:*s. I R -> R.
    WB I (\R:*s.\(~~):R->R->*p. \Inv:R->*p. \ops:I R.
    f R ops ~~ g R ops)

Prove WB_UnivRep : @I:*s->*s. SimplyT I ->
     @P:(@R:*s. (R->R->*p)->(R->*p)->I R-> R->*p).
     WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p.
                       \ops: {|l:I R, r: R|}. 
                               P R (~~) Inv ops`l ops`r) ->
     WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p.\ops:I R. 
                        @r:R. Inv r -> P R (~~) Inv ops r)


----------------------------------
----------------------------------
--                              --
--  6. M A I N   R E S U L T S  --
--                              --
----------------------------------
----------------------------------

Def MkUserSpec := \I:*s->*s.
           \Spec:(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p).
           \imp : (Sig X:*s. I X).
                ExK R:*s. Ex ops:I R.
                    imp = pack I R ops /\
                    Spec R ((=) R) (\r:R.True) ops :
           @I:*s->*s.(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p) ->
           (Sig X:*s. I X) -> *p
LatexVar 1 MkUserSpec

Def MkImplemSpec := \I:*s->*s.
           \Spec:(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p).
           \R:*s. \ops:I R.
                           ExR (~~) : R->R->*p. ExQ Inv:R->*p.
                                Spec R (~~) Inv ops /\ 
                                Bisim I R (~~) ops /\
                                IsInvar I R Inv ops /\
                                IsERon (~~) Inv  : 
           @I:*s->*s.(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p) ->
           @R:*s. I R -> *p
LatexVar 1 MkImplemSpec

Prove Implem__UserSpec :
     @I:*s->*s. FirstO I ->
     @Spec: (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p). WB' I Spec ->
     @Rep:*s.@ops:I Rep.
     MkImplemSpec I Spec Rep ops ->
     MkUserSpec I Spec (pack I Rep ops)

Prove principle : @I:*s->*s.
                  @Spec:(@Rep:*s. (Rep->Rep->*p) -> (Rep->*p) -> I Rep -> *p).
                  @imp: (Sig X:*s. I X). MkUserSpec I Spec imp ->
                  @A:*s. @Q:A->*p. @body:(@X:*s.I X -> A). 
                  (@X:*s.@ops:I X. Spec X ((=) X) (\r:X. True) ops ->
                                       Q (body X ops)) ->
                 Q (unpack imp (\X:*s.\ops:I X. body X ops))