-- File: bag1

-- This file treats implementation 1 of the example of bags. It follows exactly
-- the structure of Section 6.5.1, and is hence divided in the following parts.
-- 0.  Preliminaries (not in thesis)
-- 1.  Interface
-- 2.  Specification
-- 3.  Implementation
-- 4b. Finding another implementation
-- 4c. Using a weaker specification
-- 4d. Quotient algebras

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

------------------------------------
--                                --
--  0. P R E L I M I N A R I E S  --
--                                --
------------------------------------

Prove IsER_Perm : @A:*s. IsER (Perm A)


----------------------------
--                        --
--  1. I N T E R F A C E  --
--                        --
----------------------------

Def BagI := \X:*s. {| empty : X,
                        add : Nat -> X -> X,
                        card : Nat -> X -> Nat |}

Def BagImp := Sig X:*s. BagI X


-- We introduce Sim, Bisim, and the parametricity axiom just for BagI;
-- the general scheme cannot be formalized in Yarrow (see the discussion
-- at the end of Section 6.7.6, on pages 190,191).

Def SimBagI := \Rep1,Rep2:*s. \(~):Rep1 ->Rep2->*p.
            \ops1:BagI Rep1. \ops2:BagI Rep2. 
                ops1`empty ~ ops2`empty /\
                (@x:Rep1.@y:Rep2. @m:Nat. x ~ y -> 
                                          ops1`add m x ~ ops2`add m y) /\
                (@x:Rep1.@y:Rep2. @m:Nat.  x ~ y -> 
                                          ops1`card m x = ops2`card m y) :
            @Rep1,Rep2:*s. (Rep1->Rep2->*p) -> BagI Rep1 -> BagI Rep2 -> *p

Def BisimBagI := \Bag:*s.\(~): Bag->Bag->*p.\ops:BagI Bag. 
                    SimBagI Bag Bag (~) ops ops : 
             @Bag:*s. (Bag->Bag->*p) -> BagI Bag -> *p

Var parSigmaBagI : @X1:*s.@X2:*s.@x1:BagI X1. @x2:BagI X2.
                       @(~) : X1->X2->*p.
                       SimBagI X1 X2 (~) x1 x2 ->
                       pack BagI X1 x1 = pack BagI X2 x2

------------------------------------
--                                --
--  2. S P E C I F I C A T I O N  --
--                                --
------------------------------------

Def NaiveSpec := \Bag:*s. \ops:BagI Bag.
                 @m,n:Nat. @b:Bag.
                    ops`card m ops`empty = O /\
                    ops`card m (ops`add m b) = S (ops`card m b) /\
                    (Not (m=n) -> ops`card m (ops`add n b) = 
                                                ops`card m b) /\
                    ops`add m (ops`add n b) =
                                   ops`add n (ops`add m b) :
              @Bag:*s. BagI Bag -> *p

Def UserSpec := \imp:BagImp. ExK Rep:*s. Ex ops:BagI Rep.
                      imp = pack BagI Rep ops /\ NaiveSpec Rep ops

Prove NaiveSpec__UserSpec : @Rep:*s. @ops:BagI Rep.
                            NaiveSpec Rep ops -> UserSpec (pack BagI Rep ops)


--------------------------------------
--                                  --
--  3. I M P L E M E N T A T I O N  --
--                                  --
--------------------------------------

Def Rep1 := List Nat

Def ops1 := {empty = nil Nat,
             add = (;) Nat,
             card = count} : BagI Rep1
Def imp1 := pack BagI Rep1 ops1 : BagImp

-----------------------------------------------------------------------
--                                                                   --
--  4b. F I N D I N G   A N O T H E R   I M P L E M E N T A T I O N  --
--                                                                   --
-----------------------------------------------------------------------

Def RepSort := List Nat

Def opsSort := {empty = nil Nat,
                add = insert,
                card = count} : BagI RepSort

Def impSort := pack BagI RepSort opsSort : BagImp


Prove NaiveSpec_opsSort : NaiveSpec RepSort opsSort


Prove UserSpec_impSort : UserSpec impSort

Prove imp1_is_impSort : imp1 = impSort

Prove clumsy_UserSpec_imp1 : UserSpec imp1


-------------------------------------------------------------------
--                                                               --
--  4c. U S I N G   A   W E A K E R   S P E C I F I C A T I O N  --
--                                                               --
-------------------------------------------------------------------

Prove Bisim_Perm_ops1 : BisimBagI Rep1 (Perm Nat) ops1

Def Spec := \Rep:*s. \(~~) : Rep->Rep->*p. \ops:BagI Rep.
               @m,n:Nat. @r:Rep.
                ops`card m ops`empty = O /\
                ops`card m (ops`add m r) = S (ops`card m r) /\
                (Not (m=n) -> ops`card m (ops`add n r) = 
                                                ops`card m r) /\
                ops`add m (ops`add n r) ~~
                                   ops`add n (ops`add m r) :
              @Rep:*s. (Rep->Rep->*p) -> BagI Rep -> *p


Def ImplemSpec := \Rep:*s. \ops:BagI Rep.
                  ExR (~~) : Rep->Rep->*p. Spec Rep (~~) ops /\ 
                                           BisimBagI Rep (~~) ops /\
                                           IsER (~~)

Def WeakUserSpec := \bagImp : BagImp. 
                    ExK Rep:*s. Ex ops:BagI Rep. ExR (~~) : Rep->Rep->*p.
                    bagImp = pack BagI Rep ops /\ Spec Rep (~~) ops /\ 
                     BisimBagI Rep (~~) ops /\ IsER (~~)

Prove Spec_Perm_ops1 : Spec Rep1 (Perm Nat) ops1

Prove ImplemSpec_ops1 : ImplemSpec Rep1 ops1

Prove Implem__WeakUserSpec : @Rep:*s. @ops:BagI Rep.
                                 ImplemSpec Rep ops -> 
                                 WeakUserSpec (pack BagI Rep ops)

Prove WeakUserSpec_imp1 : WeakUserSpec imp1


---------------------------------------------
--                                         --
--  4d. Q U O T I E N T   A L G E B R A S  --
--                                         --
---------------------------------------------

Def IsQuotAlg := \R:*s. \opsR : BagI R. \(~~):R->R->*p. \Q:*s. \opsQ : BagI Q.
              Ex surj:R->Q.
                (@r,r':R. r ~~ r' <=> surj r = surj r') /\
                IsSurjection surj /\
                SimBagI R Q (\r:R.\q:Q. q = surj r) opsR opsQ  :
              @R:*s. BagI R -> (R->R->*p) -> @Q:*s. BagI Q -> *p

Var exis_QuotAlg : @R:*s. @opsR:BagI R. @(~~):R->R->*p. 
                BisimBagI R (~~) opsR -> IsER (~~) ->
                ExK Q:*s. Ex opsQ: BagI Q. 
                IsQuotAlg R opsR (~~) Q opsQ


-- (i)
Prove pack_Quot : @R:*s. @opsR:BagI R. @(~~):R->R->*p.
                  @Q:*s. @opsQ: BagI Q. IsQuotAlg R opsR (~~) Q opsQ ->
                  (=) BagImp (pack BagI R opsR) (pack BagI Q opsQ)


-- (ii)
Prove Spec_Sens :
                @R:*s. @opsR:BagI R. @(~~):R->R->*p. @Q:*s. @opsQ: BagI Q. 
                IsQuotAlg R opsR (~~) Q opsQ -> Spec R (~~) opsR ->
                Spec Q ((=) Q) opsQ


Prove Implem__UserSpec : @Rep:*s. @ops:BagI Rep.
                             ImplemSpec Rep ops -> 
                             UserSpec (pack BagI Rep ops)

Prove UserSpec_imp1 : UserSpec imp1

Prove principle : @imp:BagImp. UserSpec imp ->
                  @A:*s.@Q:A->*p.@body:@X:*s. BagI X -> A.
                  (@X:*s.@ops:BagI X. Spec X ((=) X) ops -> Q (body X ops)) -> 
                  Q (unpack imp (\X:*s.\ops:BagI X. body X ops))