-- File: library -- This file gives our general theory of ADTs, leading to the main theorems. -- It follows the structure of Sections 6.7.4, 6.7.5, and 6.7.6, and is hence -- divided in the following parts. -- 4. Quotients and Subsets (Section 6.7.4) -- 5. Sensible and well-behaved (Section 6.7.5) -- 6. Main results (Section 6.7.6) Path "../lol" Path "../lolExtra" Load "lambdaLplus" Load "parametricity" ---------------------------------------------------- ---------------------------------------------------- -- -- -- 4. Q U O T I E N T S A N D S U B S E T S -- -- -- ---------------------------------------------------- ---------------------------------------------------- Def IsQuotAlg := \I:*s->*s. \R:*s. \opsR : I R. \(~~):R->R->*p. \Q:*s. \opsQ : I Q. Ex surj:R->Q. (@r,r':R. r ~~ r' <=> surj r = surj r') /\ IsSurjection surj /\ Sim I R Q (\r:R.\q:Q. q = surj r) opsR opsQ : @I:*s->*s.@R:*s. I R -> (R->R->*p) -> @Q:*s. I Q -> *p Def IsSubsetAlg := \I:*s->*s.\R:*s. \opsR : I R. \Inv:R->*p. \S:*s.\opsS : I S. Ex inj:S->R. IsInjection inj /\ (Inv <==> Image inj) /\ Sim I R S (\r:R.\s:S. r = inj s) opsR opsS : @I:*s->*s. @R:*s. I R -> (R->*p) -> @S:*s. I S -> *p Def IsQuotSubsetAlg := \I:*s->*s. \R:*s. \opsR : I R. \(~~) : R->R->*p. \Inv:R->*p. \Q:*s. \opsQ : I 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') /\ Sim I R Q Rel opsR opsQ : @I:*s->*s.@R:*s. I R -> (R->R->*p) -> (R->*p) -> @Q:*s. I Q -> *p var exis_QuotAlg :@I:*s->*s. FirstO I -> @R:*s. @opsR:I R. @(~~):R->R->*p. Bisim I R (~~) opsR -> IsER (~~) -> ExK Q:*s. Ex opsQ: I Q. IsQuotAlg I R opsR (~~) Q opsQ var exis_SubsetAlg : @I:*s->*s. FirstO I -> @R:*s. @opsR:I R. @Inv:R->*p. IsInvar I R Inv opsR -> ExK S:*s. Ex opsS: I S. IsSubsetAlg I R opsR Inv S opsS Prove exis_QuotSubsetAlg : @I:*s->*s. FirstO I -> @R:*s. @opsR:I R. @(~~):R->R->*p. @Inv:R->*p. IsERon (~~) Inv -> Bisim I R (~~) opsR -> IsInvar I R Inv opsR -> ExK Q:*s. Ex opsQ: I Q. IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ Prove pack_QuotSubset : @I:*s->*s. SimplyT I -> @R:*s. @opsR:I R. @(~~):R->R->*p. @Inv: R->*p. @Q:*s. @opsQ:I Q. IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ -> (=) (Sig X:*s. I X) (pack I R opsR) (pack I Q opsQ) ------------------------------------------------------------ ------------------------------------------------------------ -- -- -- 5. S E N S I B L E A N D W E L L - B E H A V E D -- -- -- ------------------------------------------------------------ ------------------------------------------------------------ Def Sensible := \I:*s->*s. \Spec : @R:*s.(R->R->*p) -> (R->*p) -> I R -> *p. @R:*s.@opsR:I R.@(~~):R->R->*p. @Inv:R->*p.@Q:*s.@opsQ:I Q. IsQuotSubsetAlg I R opsR (~~) Inv Q opsQ -> Spec R (~~) Inv opsR -> Spec Q ((=) Q) (\q:Q.True) opsQ Def WB := \I:*s->*s. \Spec: (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p). @Y,Z:*s. @RelY:Y->Y->*p. @RelZ:Z->Z->*p. @InvY:Y->*p. @InvZ:Z->*p. IsERon RelY InvY -> IsERon RelZ InvZ -> @opsY:I Y. @opsZ : I Z. (ExR (~):Y->Z->*p. Sim I Y Z (~) opsY opsZ /\ (Restr RelY InvY <===> LeftC (~)) /\ (Restr RelZ InvZ <===> RightC (~)) /\ IsZclosed (~)) -> Spec Y RelY InvY opsY -> Spec Z RelZ InvZ opsZ Implicit 1 WB -- For proving properties about WB, it is easier to use the following, -- equivalent formulation. Def WB' := \I:*s->*s. \Spec: (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p). @Y,Z:*s. @RelY:Y->Y->*p. @RelZ:Z->Z->*p. @InvY:Y->*p. @InvZ:Z->*p. @opsY:I Y. @opsZ : I Z. @(~):Y->Z->*p. Sim I Y Z (~) opsY opsZ -> IsZclosed (~) -> (Restr RelY InvY) <===> LeftC (~) -> (Restr RelZ InvZ) <===> RightC (~) -> IsERon RelY InvY -> IsERon RelZ InvZ -> Spec Y RelY InvY opsY -> Spec Z RelZ InvZ opsZ Implicit 1 WB' -- WB and WB' are really equivalent: Prove WB__WB' : @I:*s->*s. @Spec : (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p). WB' I Spec <=> WB I Spec Prove WB__Sensible : @I:*s->*s. SimplyT I -> @Spec: (@R:*s. (R->R->*p)->(R->*p)->I R->*p). WB' I Spec -> Sensible I Spec Prove WB_Prop: @I:*s->*s. @P:*p. WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p.\ops:I R. P) Prove WB_Impl : @I:*s->*s. SimplyT I -> @P,Q:(@R:*s. (R->R->*p)->(R->*p)->I R->*p). WB' P -> WB' Q -> WB' (\R:*s.\(~~):R->R->*p.\Inv:R->*p.\ops:I R. P R (~~) Inv ops -> Q R (~~) Inv ops) Prove WB_Pred : @I:*s->*s. SimplyT I -> @A:*s. @f: @R:*s. I R -> A. @P:A->*p. WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p.\ops:I R. P (f R ops)) Prove WB_Univ : @I:*s->*s. @A:*s. @P:A->(@R:*s. (R->R->*p)->(R->*p)->I R->*p). (@a:A. WB' (P a)) -> WB' (\R:*s.\(~~):R->R->*p.\Inv:R->*p.\ops:I R. @a:A. P a R (~~) Inv ops) Prove WB_Tw : @I:*s->*s. SimplyT I -> @f,g: @R:*s. I R -> R. WB I (\R:*s.\(~~):R->R->*p. \Inv:R->*p. \ops:I R. f R ops ~~ g R ops) Prove WB_UnivRep : @I:*s->*s. SimplyT I -> @P:(@R:*s. (R->R->*p)->(R->*p)->I R-> R->*p). WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p. \ops: {|l:I R, r: R|}. P R (~~) Inv ops`l ops`r) -> WB' (\R:*s.\(~~):R->R->*p. \Inv:R->*p.\ops:I R. @r:R. Inv r -> P R (~~) Inv ops r) ---------------------------------- ---------------------------------- -- -- -- 6. M A I N R E S U L T S -- -- -- ---------------------------------- ---------------------------------- Def MkUserSpec := \I:*s->*s. \Spec:(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p). \imp : (Sig X:*s. I X). ExK R:*s. Ex ops:I R. imp = pack I R ops /\ Spec R ((=) R) (\r:R.True) ops : @I:*s->*s.(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p) -> (Sig X:*s. I X) -> *p Def MkImplemSpec := \I:*s->*s. \Spec:(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p). \R:*s. \ops:I R. ExR (~~) : R->R->*p. ExQ Inv:R->*p. Spec R (~~) Inv ops /\ Bisim I R (~~) ops /\ IsInvar I R Inv ops /\ IsERon (~~) Inv : @I:*s->*s.(@R:*s. (R->R->*p) -> (R->*p) -> I R -> *p) -> @R:*s. I R -> *p Prove Implem__UserSpec : @I:*s->*s. FirstO I -> @Spec: (@R:*s.(R->R->*p) -> (R->*p) -> I R -> *p). WB' I Spec -> @Rep:*s.@ops:I Rep. MkImplemSpec I Spec Rep ops -> MkUserSpec I Spec (pack I Rep ops) Prove principle : @I:*s->*s. @Spec:(@Rep:*s. (Rep->Rep->*p) -> (Rep->*p) -> I Rep -> *p). @imp: (Sig X:*s. I X). MkUserSpec I Spec imp -> @A:*s. @Q:A->*p. @body:(@X:*s.I X -> A). (@X:*s.@ops:I X. Spec X ((=) X) (\r:X. True) ops -> Q (body X ops)) -> Q (unpack imp (\X:*s.\ops:I X. body X ops))