-- File: bag2

-- This file treats implementation 2 of the example of bags. It follows the 
-- structure of Section 6.5.2, and is hence divided in the following parts.
-- 1.  Interface
-- 2.  Specification
-- 3.  Implementation
-- 4c. Using a weaker specification
-- 4d. Subset algebras

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

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

Def BagI := \X:*s. {| empty : X,
                      add : Nat -> X -> X,
                      card : Nat -> X -> Nat,
                      bound : 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) /\ 
                (@x:Rep1.@y:Rep2. x ~ y -> ops1`bound x = ops2`bound 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) /\
                   (S O <= ops`card m b -> m <= ops`bound 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

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

Def Rep2 := List Nat

Def ops2 := {empty = nil Nat,
             add = insert,
             card = count,
             bound = last O} : BagI Rep2
Def imp2 := pack BagI Rep2 ops2 : BagImp

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

Def IsInvarBagI := \Rep:*s.\Inv:Rep->*p.\ops:BagI Rep.
                       Inv (ops`empty) /\
                       @m:Nat. @r:Rep. Inv r -> Inv (ops`add m r)

Prove IsInvar_Ordered_ops2 : IsInvarBagI Rep2 Ordered ops2
Unfold IsInvarBagI
Unfold ops2
AndI
Exact Ordered_nil
Intros
Apply Ordered_insert
Assumption
Exit

Def Spec := \Rep:*s. \Inv : Rep->*p. \ops:BagI Rep.
      @m,n:Nat. @r:Rep. Inv r ->
           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) /\
           (S O <= ops`card m r -> m <= ops`bound r) :
            @Rep:*s. (Rep->*p) -> BagI Rep -> *p


Def ImplemSpec := \Rep:*s. \ops:BagI Rep.
                  ExQ Inv : Rep->*p. Spec Rep Inv ops /\ 
                    IsInvarBagI Rep Inv ops

Prove Spec_True__NaiveSpec : @R:*s.@opsR:BagI R. Spec R (\r:R. True) opsR ->
                                                 NaiveSpec R opsR
Intros
Unfold NaiveSpec
Intros
Apply H
Exact true_True
Exit

Prove NaiveSpec__Spec_True : @Rep:*s. @ops:BagI Rep. NaiveSpec Rep ops ->
                                                    Spec Rep (\r:Rep. True) ops
Intros
Unfold Spec
Intros
Apply H
Exit

Def WeakUserSpec := \bagImp : BagImp. 
                    ExK Rep:*s. Ex ops:BagI Rep. ExQ Inv : Rep->*p.
                    bagImp = pack BagI Rep ops /\ Spec Rep Inv ops /\ 
                    IsInvarBagI Rep Inv ops


Prove Spec_Ordered_ops2 : Spec Rep2 Ordered ops2
Unfold Spec
Intros
Unfold ops2
Repeat AndI
Apply count_nil
Apply count_m_insert_m
Intro
Apply count_m_insert_n
Assumption
Apply insert_m_n_is_insert_n_m
Intro
Apply Elem_Le_last
Apply SO_Le_count__Elem
Assumption
Assumption
Exit

Prove ImplemSpec_ops2 : ImplemSpec Rep2 ops2
Unfold ImplemSpec
ExistsI Ordered
AndI
Exact Spec_Ordered_ops2
Exact IsInvar_Ordered_ops2
Exit

Prove Implem__WeakUserSpec : @Rep:*s. @ops:BagI Rep.
                                 ImplemSpec Rep ops -> 
                                 WeakUserSpec (pack BagI Rep ops)
Intros
Unfold WeakUserSpec
Unfold ImplemSpec In H
ExistsI Rep
ExistsI ops
ExistsE H
ExistsI Inv
AndI
Refl
Assumption
Exit

Prove WeakUserSpec_imp2 : WeakUserSpec imp2
Apply Implem__WeakUserSpec
Exact ImplemSpec_ops2
Exit


-----------------------------------------
--                                     --
--  4d. S U B S E T   A L G E B R A S  --
--                                     --
-----------------------------------------

Def IsSubsetAlg :=\R:*s. \opsR : BagI R. \Inv:R->*p. \S:*s. \opsS : BagI S.
               Ex inj:S->R.
                IsInjection inj /\
                (Inv <==> Image inj) /\
                SimBagI R S (\r:R.\s:S. r = inj s) opsR opsS  :
              @R:*s. BagI R -> (R->*p) -> @S:*s. BagI S -> *p

Var exis_SubsetAlg : @R:*s. @opsR:BagI R. @Inv:R->*p.
                     IsInvarBagI R Inv opsR ->
                     ExK S:*s. Ex opsS: BagI S. 
                     IsSubsetAlg R opsR Inv S opsS

-- (i)
prove pack_Subset : @R:*s. @opsR:BagI R. @Inv:R->*p.
                    @S:*s. @opsS: BagI S. IsSubsetAlg R opsR Inv S opsS ->
                    (=) BagImp (pack BagI R opsR) (pack BagI S opsS)
Intros
Unfold IsSubsetAlg In H
ExistsE H
AndE H1
AndE H3
Apply parSigmaBagI On H5
Exit

-- (ii)
Prove Spec_Sens :
                @R:*s. @opsR:BagI R. @Inv:R->*p. @S:*s. @opsS: BagI S. 
                IsSubsetAlg R opsR Inv S opsS -> Spec R Inv opsR ->
                Spec S (\s:S. True) opsS
Intros
Unfold IsSubsetAlg In H
ExistsE H
AndE H2
AndE H4
Unfold SimBagI In H6
AndE H6
AndE H8
AndE H10
First @y:S1.@m:Nat. opsR`add m (inj y) = inj (opsS`add m y)
Intros
Apply H9
Refl
First @y:S1.@m:Nat. opsR`card m (inj y) = opsS`card m y
Intros
Apply H11
Refl
Intros
Hide H11,H12
Unfold Spec
Intro m,n,s,H15
AndE H1 On m, n, inj s
Rewrite H5
Apply Image_f_f_x
AndE H18
AndE H20
AndE H22
Repeat AndI
Lewrite H13
Lewrite H7
Assumption
Repeat Lewrite H13
Lewrite H14
Assumption
Repeat Lewrite H13
Lewrite H14
Assumption
Apply H3
Repeat Lewrite H14
Assumption
Unhide H11
Unhide H12
Hide H9,H11
Lewrite H12 On inj s
Refl
Lewrite H13
Assumption
Exit

Prove Implem__UserSpec : @Rep:*s. @ops:BagI Rep.
                             ImplemSpec Rep ops -> 
                             UserSpec (pack BagI Rep ops)
Intros
Unfold UserSpec
Unfold ImplemSpec In H
ExistsE H
AndE H1
Forward exis_SubsetAlg On H3
ExistsE H4
ExistsE H5
ExistsI S1
ExistsI opsS
AndI
Apply pack_Subset On H6
Apply Spec_True__NaiveSpec
Apply Spec_Sens On H6
Assumption
Exit

Prove UserSpec_imp2 : UserSpec imp2
Apply Implem__UserSpec
Apply ImplemSpec_ops2
Exit



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