-- File: stack

-- Gives the example of the ADT of stacks.
-- This file is divided into two parts.
-- 1) Without existential types.
-- 2) With existential types.

Path "../lol"
Path "../lolExtra"
Load "lambdaLplus"
Load "logic2"
Load "list2"


------------------------------------------------------------
------------------------------------------------------------
--                                                        --
--  1. W I T H O U T   E X I S T E N T I A L   T Y P E S  --
--                                                        --
------------------------------------------------------------
------------------------------------------------------------

Def StackI := \Rep:*s. {| empty : Rep, 
                          push : Nat -> Rep -> Rep,
                          pop : Rep -> Rep,
                          top : Rep -> Nat,
                          isEmpty : Rep -> Bool |}

Def Rep1 := List Nat
Def ops1 := {empty = nil Nat,
              push = (;) Nat,
              pop = tail Nat,
              top = head O,
              isEmpty = null Nat} :
             StackI Rep1

Def Spec := \Rep:*s. \ops:StackI Rep.
                   ops`isEmpty ops`empty = true /\
                   (@s:Rep. @n:Nat. ops`isEmpty (ops`push n s) = false) /\
                   (@s:Rep. @n:Nat. ops`top (ops`push n s) = n) /\
                   (@s:Rep. @n:Nat. ops`pop (ops`push n s) = s) :
            @Rep:*s. StackI Rep -> *p

Prove Spec_ops1 : Spec Rep1 ops1
Unfold Spec
Repeat AndI
Unfold ops1
Apply null_nil
Intros
Unfold ops1
Apply null_cons
Intros
Unfold ops1
Apply head_cons
Intros
Unfold ops1
Apply tail_cons
Exit

-- 'wprinciple' is called 'principle' in my thesis
Prove wprinciple : @Rep1:*s. @ops1: StackI Rep1. Spec Rep1 ops1 ->
                   @A:*s. @body:(@X:*s.StackI X -> A). @Q:A->*p.
                 (@X:*s.@ops:StackI X. Spec X ops -> Q (body X ops)) ->
                 Q ((\X:*s.\ops:StackI X. body X ops) Rep1 ops1)
Intros
Simplify
Apply H1
Assumption
Exit

Def prog1 := (\X:*s.\ops : StackI X.
                  ops`isEmpty (ops`pop (ops`push O ops`empty))) Rep1 ops1

Prove prog1_is_true : prog1 = true
Convert (\b:Bool. b= true) ((\X:*s.\ops : StackI X.
                  ops`isEmpty (ops`pop (ops`push O ops`empty))) Rep1 ops1)
Apply wprinciple
Exact Spec_ops1
Intros
Unfold Spec In H
AndE H
AndE H2
AndE H4
Rewrite H6
Apply H1
Exit



------------------------------------------------------
------------------------------------------------------
--                                                  --
--  2. W I T H   E X I S T E N T I A L   T Y P E S  --
--                                                  --
------------------------------------------------------
------------------------------------------------------

Def imp1 := pack StackI Rep1 ops1 : Sig Rep:*s. StackI Rep

Def StackImp := Sig Rep:*s. StackI Rep

Def prog1' := unpack imp1 (\X:*s. \ops:StackI X.
                              ops`isEmpty (ops`pop (ops`push O ops`empty))) :
              Bool

Def Rep2 := List Nat
Def ops2 := {empty = nil Nat,
              push = snoc Nat,
              pop = init Nat,
              top = last O,
              isEmpty = null Nat} :
             StackI Rep2
Def imp2 := pack StackI Rep2 ops2 : StackImp

Def UserSpec := \imp:StackImp. ExK Rep:*s. Ex ops:StackI Rep.
                     imp = pack StackI Rep ops /\ Spec Rep ops :
                StackImp -> *p

Prove UserSpec_imp1 : UserSpec imp1
Unfold UserSpec
Unfold imp1
ExistsI Rep1
ExistsI ops1
AndI
Refl
Apply Spec_ops1
Exit

Prove principle : @imp:StackImp. UserSpec imp ->
                  @A:*s. @body:(@X:*s.StackI X -> A). @Q:A->*p.
                 (@X:*s.@ops:StackI X. Spec X ops -> Q (body X ops)) ->
                 Q (unpack imp (\X:*s.\ops:StackI X. body X ops))
Intros
Unfold UserSpec In H
ExistsE H
ExistsE H2
AndE H3
Rewrite H4
Rewrite beta_Sig
Apply H1
Assumption
Exit

Prove prog1'_is_true : prog1'=true
Unfold prog1'
Apply principle On \b:Bool. b=true
Exact UserSpec_imp1
Intros
Unfold Spec In H
AndE H
AndE H2
AndE H4
Rewrite H6
Apply H1
Exit