-- File: bag3

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

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

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

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 Rep3 := {| els : List Nat, mx : Nat |}

Def ops3 := {empty = {els = nil Nat, mx=O},
             add = \n:Nat. \r:Rep3.
                   {els= n;r`els, mx= max r`mx n},
             card = \n:Nat. \r:Rep3. count n r`els,
             bound = \r:Rep3. r`mx} : BagI Rep3
Def imp3 := pack BagI Rep3 ops3 : 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 Spec := \Rep:*s. \(~~) : Rep->Rep->*p. \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->Rep->*p) -> (Rep->*p) -> BagI Rep -> *p

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

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

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

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

Def Inv3 := \r:Rep3. @n:Nat. Elem n r`els -> n<=r`mx

Prove IsInvar_Inv3 : IsInvarBagI Rep3 Inv3 ops3
Unfold IsInvarBagI
Unfold ops3
Unfold Inv3
AndI
Intros
FalseE
Apply Elem_nil_ On H
Intros
Rewrite Elem_cons In H1
OrE H2
Rewrite H3
Apply Le_max2
Forward H On H3
Apply Le_trans On H4
Apply Le_max1
Exit

Def Sim3 := \r,r':Rep3. Perm r`els r'`els /\ 
                       r`mx = r'`mx 

Prove Bisim_Sim3 : BisimBagI Rep3 Sim3 ops3
Unfold BisimBagI
Unfold SimBagI
Unfold ops3
Repeat AndI
Unfold Sim3
AndI
Apply Perm_refl
Refl
Unfold Sim3
Intros
AndE H
AndI
Apply Perm_cons
Assumption
Rewrite H2
Refl
Unfold Sim3
Intros
AndE H
Apply Perm__count_equal
Assumption
Unfold Sim3
Intros
AndE H
Assumption
Exit

Prove IsERon_Sim3 : IsERon Sim3 Inv3
Apply IsER__IsERon
Unfold Sim3
Unfold IsER
Repeat AndI
Intros
AndI
Apply Perm_refl
Refl
Intros
AndE H
AndI
Apply Perm_sym
Assumption
Apply is_sym
Assumption
Intros
AndE H
AndE H1
AndI
Apply Perm_trans On H2
Assumption
Apply is_trans On H3
Assumption
Exit

Prove Spec_ops3 : Spec Rep3 Sim3 Inv3 ops3
Unfold Spec
Intros
Unfold ops3
Repeat AndI
Apply count_nil
Apply count_m_m_cons
Apply count_m_n_cons
Unfold Sim3
AndI
Apply Perm_cons_weak
Repeat Rewrite max_assoc
Rewrite 2 max_comm
Refl
Unfold Inv3 In H
Intro
Apply H
Apply SO_Le_count__Elem
Assumption
Exit

Prove ImplemSpec_ops3 : ImplemSpec Rep3 ops3
Unfold ImplemSpec
ExistsI Sim3
ExistsI Inv3
Repeat AndI
Exact Spec_ops3
Exact Bisim_Sim3
Exact IsInvar_Inv3
Exact IsERon_Sim3
Exit

Prove WeakUserSpec_imp3 : WeakUserSpec imp3
Unfold WeakUserSpec
ExistsI Rep3
ExistsI ops3
ExistsI Sim3
ExistsI Inv3
Repeat AndI
Refl
Exact Spec_ops3
Exact Bisim_Sim3
Exact IsERon_Sim3
Exact IsInvar_Inv3
Exit



-------------------------------------------------------------------------
--                                                                     --
--  4d. C O M B I N I N G   Q U O T I E N T S   A N D   S U B S E T S  --
--                                                                     --
-------------------------------------------------------------------------

Def IsQuotSubsetAlg := \R:*s. \opsR : BagI R. \(~~) : R->R->*p. \Inv:R->*p. 
               \Q:*s. \opsQ : BagI 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') /\
                     SimBagI R Q Rel opsR opsQ : 
              @R:*s. BagI R -> (R->R->*p) -> (R->*p) -> @Q:*s. BagI Q -> *p

Var exis_QuotSubsetAlg : 
                @R:*s. @opsR:BagI R. @(~~):R->R->*p. @Inv:R->*p.
                IsERon (~~) Inv -> 
                BisimBagI R (~~) opsR -> 
                IsInvarBagI R Inv opsR ->
                ExK Q:*s. Ex opsQ: BagI Q. 
                IsQuotSubsetAlg R opsR (~~) Inv Q opsQ

Prove pack_QuotSubset : 
               @R:*s. @opsR:BagI R. @(~~):R->R->*p.@Inv:R->*p.
               @Q:*s. @opsQ:BagI Q. IsQuotSubsetAlg R opsR (~~) Inv Q opsQ ->
               pack BagI R opsR = pack BagI Q opsQ
Intros
Unfold IsQuotSubsetAlg In H
ExistsE H
AndE H1
AndE H3
AndE H5
Apply parSigmaBagI On H7
Exit


Prove Spec_Sens :
                @R:*s. @opsR:BagI R. @(~~):R->R->*p. @Inv:R->*p.
                @Q:*s. @opsQ: BagI Q. 
                IsQuotSubsetAlg R opsR (~~) Inv Q opsQ -> 
                Spec R (~~) Inv opsR ->
                Spec Q ((=) Q) (\q:Q.True) opsQ
Intros
Unfold IsQuotSubsetAlg In H
ExistsE H
AndE H2
AndE H4
AndE H6
Unfold Spec In H1
Unfold Spec
Intro m,n,q
Intro
ExistsE H5 On q
AndE H1 On m, n, r
Rewrite H3
Unfold Dom
ExistsI q
Assumption
AndE H14
AndE H16
AndE H18
Hide H1
Unfold SimBagI In H8
AndE H8
AndE H22
AndE H24
First @q:Q.@r:R. Rel r q -> Inv r
Intros
Rewrite H3
Unfold Dom Then ExistsI q1 Then Assumption
Intro
Repeat AndI
Lewrite H13
Apply is_sym
Apply H25
Assumption
Apply is_trans On opsR`card m (opsR`add m r)
Apply is_sym
Apply H25
Apply H23
Assumption
Rewrite H15
Rewrite H25 On q
Assumption
Refl
Intro
Apply is_trans On opsR`card m (opsR`add n r)
Apply is_sym
Apply H25
Apply H23
Assumption
Rewrite H17
Assumption
Apply H25
Assumption
Forward H23 On n, H11
Forward H23 On m, H28
Forward H23 On m, H11
Forward H23 On n, H30
Lewrite H7 On H29, H31
Apply H19
Intros
Lewrite H26 On H11
Apply H20
Rewrite H25 On H11
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
ExistsE H1
AndE H2
AndE H4
AndE H6
ExistsE exis_QuotSubsetAlg On H5, H7 Then Try Assumption
ExistsE H10
ExistsI Q
ExistsI opsQ
AndI
Apply pack_QuotSubset On H11
Apply Spec_True__NaiveSpec
Apply Spec_Sens On H11
Assumption
Exit

Prove UserSpec_imp3 : UserSpec imp3
Apply Implem__UserSpec
Apply ImplemSpec_ops3
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 ((=) 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