-- File: parametricity

-- This file introduces parametricity and the notion of first-order interfaces.
-- It follows the structure of Sections 6.7.2 through 6.7.3, and is hence
-- divided in the following parts.
--  2. Parametricity (Section 6.7.2)
--  3. First-order interfaces (Section 6.7.3)

Path "../lol"
Path "../lolExtra"
Load "lambdaLplus"
Load "prelims"
Load "LOLP_Axioms"

------------------------------------
------------------------------------
--                                --
--  2. P A R A M E T R I C I T Y  --
--                                --
------------------------------------
------------------------------------

Var Sim : @I:*s->*s. @Y:*s.@Z:*s. (Y->Z->*p) -> (I Y -> I Z -> *p)
LatexVar 1 Sim

Var Sim_id : @Y,Z:*s.@(~):Y->Z->*p.
                    Sim (\X:*s.X) Y Z (~) <===> (~)
Var Sim_const : @T:*s.@Y,Z:*s.@(~):Y->Z->*p.
                    Sim (\X:*s.T) Y Z (~) <===> ((=) T)
Var Sim_arrow : @I1,I2:*s->*s.@Y,Z:*s.@(~):Y->Z->*p.
                    Sim (\X:*s. I1 X -> I2 X) Y Z (~) <===>
                    \opsY:I1 Y -> I2 Y.\opsZ:I1 Z -> I2 Z.            
                    (@y:I1 Y.@z:I1 Z. Sim I1 Y Z (~) y z ->
                                      Sim I2 Y Z (~) (opsY y) (opsZ z))
Var Sim_rec : @I1,I2:*s->*s.@Y,Z:*s.@(~):Y->Z->*p.
                    Sim (\X:*s. {|l:I1 X,r:I2 X|}) Y Z (~) <===>
                \opsY:{|l:I1 Y,r:I2 Y|}.\opsZ:{|l:I1 Z,r:I2 Z|}.
                    (Sim I1 Y Z (~) opsY`l opsZ`l /\
                     Sim I2 Y Z (~) opsY`r opsZ`r)

Def SimplyT := \I:*s->*s. @P:(*s->*s)->*p.
              P (\X:*s.X) ->
              (@T:*s. P (\X:*s. T)) ->
              (@I1,I2:*s->*s. P I1 -> P I2 -> P (\X:*s. I1 X -> I2 X)) ->
              (@I1,I2:*s->*s. P I1 -> P I2 -> P (\X:*s. {|l:I1 X,r:I2 X|}))->
              P I

Prove SimplyT_id : SimplyT (\X:*s.X)

Prove SimplyT_const : @T:*s. SimplyT (\X:*s.T)

Prove SimplyT_arrow : @I1,I2:*s->*s. SimplyT I1 -> SimplyT I2 -> 
                     SimplyT (\X:*s.I1 X -> I2 X)

Prove SimplyT_rec : @I1,I2:*s->*s. SimplyT I1 -> SimplyT I2 -> 
                     SimplyT (\X:*s.{|l:I1 X,r: I2 X|})

Prove SimplyT_elim : @I:*s->*s. SimplyT I ->
              @P:(*s->*s)->*p.
              P (\X:*s.X) ->
              (@T:*s. P (\X:*s. T)) ->
              (@I1,I2:*s->*s. SimplyT I1 -> SimplyT I2 -> 
                              P I1 -> P I2 -> P (\X:*s. I1 X -> I2 X)) ->
              (@I1,I2:*s->*s. SimplyT I1 -> SimplyT I2 -> 
                              P I1 -> P I2 -> P (\X:*s. {|l:I1 X,r:I2 X|}))->
              P I

Var parPi : @I:*s->*s. SimplyT I ->
            @f:(@X:*s.I X). @Y,Z:*s. @(~):Y->Z->*p. Sim I Y Z (~) (f Y) (f Z)

-- Parametricity for Sigma-types.
Prove parSigma : @I:*s->*s. SimplyT I ->
                   @Y,Z:*s.@(~):Y->Z->*p. @y:I Y. @z:I Z.
                     Sim I Y Z (~) y z -> 
                     (=) (Sig X:*s. I X) (pack I Y y) (pack I Z z)

Def Bisim := \I:*s->*s. \R:*s.\(~):R->R->*p.\opsR:I R. 
             Sim I R R (~) opsR opsR
LatexVar 1 Bisim

Prove Sim_sym : @I:*s->*s.SimplyT I ->
                @Y,Z:*s. @(~):Y->Z->*p. @opsY:I Y. @opsZ:I Z.
                                 Sim I Y Z (~) opsY opsZ -> 
                                 Sim I Z Y (Inverse (~)) opsZ opsY

Prove Sim_is : @I:*s->*s. SimplyT I ->
                  @R:*s.
                  Sim I R R ((=) R) <===> ((=) (I R))

Prove IsZclosed_Sim : @I:*s->*s. SimplyT I ->
            @R,Q : *s.
            @rel : R->Q->*p.
            IsZclosed rel ->
            IsZclosed (Sim I R Q rel)

Var IsInvar : @I:*s->*s. @Rep:*s. (Rep->*p) -> I Rep -> *p
LatexVar 1 IsInvar

Var IsInvar_id : @Rep:*s.@Inv:Rep->*p. IsInvar (\X:*s.X) Rep Inv <==> Inv

Var IsInvar_const : @T:*s.@Rep:*s.@Inv:Rep->*p. 
                    IsInvar (\X:*s.T) Rep Inv <==> \t:T. True

Var IsInvar_arrow : @I1,I2:*s->*s. @Rep:*s.@Inv:Rep->*p. 
                    IsInvar (\X:*s.I1 X -> I2 X) Rep Inv <==> 
                    (\f:I1 Rep->I2 Rep. @x:I1 Rep. IsInvar I1 Rep Inv x ->
                                                   IsInvar I2 Rep Inv (f x))

Var IsInvar_rec : @I1,I2:*s->*s. @Rep:*s.@Inv:Rep->*p. 
                    IsInvar (\X:*s.{|l:I1 X, r:I2 X|}) Rep Inv <==> 
                    (\f:{|l:I1 Rep,r:I2 Rep|}. IsInvar I1 Rep Inv f`l /\
                                                 IsInvar I2 Rep Inv f`r)


------------------------------------------------------
------------------------------------------------------
--                                                  --
--  3. F I R S T - O R D E R   I N T E R F A C E S  --
--                                                  --
------------------------------------------------------
------------------------------------------------------

-- Defines the first-order interfaces, and gives some properties about Sim and 
-- IsInvar for these interfaces, namely those properties we need for
-- developing general theory for ADTs


-- Basic

Def Basic := \I:*s->*s. @P:(*s->*s)->*p.
              P (\X:*s.X) ->
              (@T:*s. P (\X:*s. T)) ->
              (@I1,I2:*s->*s. P I1 -> P I2 -> P (\X:*s. {|l:I1 X,r:I2 X|}))->
              P I

Prove Basic_id : Basic (\X:*s.X)

Prove Basic_const : @T:*s. Basic (\X:*s.T)

Prove Basic_rec : @I1,I2:*s->*s. Basic I1 -> Basic I2 -> 
                     Basic (\X:*s.{|l:I1 X,r: I2 X|})

Prove Basic_elim : @I:*s->*s. Basic I ->
              @P:(*s->*s)->*p.
              P (\X:*s.X) ->
              (@T:*s. P (\X:*s. T)) ->
              (@I1,I2:*s->*s. Basic I1 -> Basic I2 -> 
                              P I1 -> P I2 -> P (\X:*s. {|l:I1 X,r:I2 X|}))->
              P I


-- FirstO

Def FirstO := \I:*s->*s. @P:(*s->*s)->*p.
              (@I:*s->*s. Basic I -> P I) ->
              (@I1,I2:*s->*s. Basic I1 -> P I2 -> P (\X:*s. I1 X -> I2 X)) ->
              (@I1,I2:*s->*s. P I1 -> P I2 -> P (\X:*s. {|l:I1 X,r:I2 X|}))->
              P I

Prove FirstO_Basic : @I:*s->*s. Basic I -> FirstO I

Prove FirstO_arrow : @I1,I2:*s->*s. Basic I1 -> FirstO I2 -> 
                     FirstO (\X:*s.I1 X->I2 X)

Prove FirstO_rec : @I1,I2:*s->*s. FirstO I1 -> FirstO I2 -> 
                     FirstO (\X:*s.{|l:I1 X,r: I2 X|})

Prove FirstO_elim : @I:*s->*s. FirstO I ->
              @P:(*s->*s)->*p.
              (@I:*s->*s. Basic I -> P I) ->
              (@I1,I2:*s->*s. FirstO I2 -> 
                              Basic I1 -> P I2 -> P (\X:*s. I1 X -> I2 X)) ->
              (@I1,I2:*s->*s. FirstO I1 -> FirstO I2 ->
                              P I1 -> P I2 -> P (\X:*s. {|l:I1 X,r:I2 X|}))->
              P I


-- The next two lemmas are not stated in my thesis

Prove Basic__SimplyT : @I:*s->*s. Basic I -> SimplyT I

Prove FirstO__SimplyT : @I:*s->*s. FirstO I -> SimplyT I



-- Properties Sim for FirstOrder interfaces. For each property, we need
-- a similar (but often stronger) property for Basic interfaces.

Prove SimBasic_Comp : @I:*s->*s. Basic I ->
                       @X,Y,Z:*s. @(~):X->Y->*p.@(~~):Y->Z->*p.
                       Comp (Sim I X Y (~)) (Sim I Y Z (~~))  <===>
                       Sim I X Z (Comp (~) (~~))

Prove SimFirstO_Trans : @I:*s->*s. FirstO I ->
                       @X,Y,Z:*s. @(~):X->Y->*p.@(~~):Y->Z->*p.
                       @opsX:I X. @opsY: I Y. @opsZ: I Z.
                       Sim I X Y (~) opsX opsY ->
                       Sim I Y Z (~~) opsY opsZ  ->
                       Sim I X Z (Comp (~) (~~)) opsX opsZ

Prove Sim_Basic_Restr : @I:*s->*s. Basic I ->
       @Y:*s. @(~):Y->Y->*p. @P:Y->*p.
       Restr (Sim I Y Y (~)) (IsInvar I Y P) <===>
       Sim I Y Y (Restr (~) P)

Prove Sim_FirstO_Restr : @I:*s->*s. FirstO I ->
       @Y:*s. @(~):Y->Y->*p. @P:Y->*p.
       @opsY,opsY': I Y.
       Restr (Sim I Y Y (~)) (IsInvar I Y P) opsY opsY' ->
       Sim I Y Y (Restr (~) P) opsY opsY'