{-# OPTIONS --allow-unsolved-metas --no-termination-check #-} module Bag where import Prelude import Equiv import Datoid import Eq import Nat import List import Pos open Prelude open Equiv open Datoid open Eq open Nat open List abstract ---------------------------------------------------------------------- -- Bag type private -- If this were Coq then the invariant should be a Prop. Similar -- remarks apply to some definitions below. Since I have to write -- the supporting library myself I can't be bothered to -- distinguish Set and Prop right now though. data BagType (a : Datoid) : Set where bt : (pairs : List (Pair Pos.Pos (El a))) -> NoDuplicates a (map snd pairs) -> BagType a list : {a : Datoid} -> BagType a -> List (Pair Pos.Pos (El a)) list (bt l _) = l contents : {a : Datoid} -> BagType a -> List (El a) contents b = map snd (list b) invariant : {a : Datoid} -> (b : BagType a) -> NoDuplicates a (contents b) invariant (bt _ i) = i private elemDatoid : Datoid -> Datoid elemDatoid a = pairDatoid Pos.posDatoid a BagEq : (a : Datoid) -> BagType a -> BagType a -> Set BagEq a b1 b2 = rel' (Permutation (elemDatoid a)) (list b1) (list b2) eqRefl : {a : Datoid} -> (x : BagType a) -> BagEq a x x eqRefl {a} x = refl (Permutation (elemDatoid a)) {list x} eqSym : {a : Datoid} -> (x y : BagType a) -> BagEq a x y -> BagEq a y x eqSym {a} x y = sym (Permutation (elemDatoid a)) {list x} {list y} eqTrans : {a : Datoid} -> (x y z : BagType a) -> BagEq a x y -> BagEq a y z -> BagEq a x z eqTrans {a} x y z = trans (Permutation (elemDatoid a)) {list x} {list y} {list z} eqDec : {a : Datoid} -> (x y : BagType a) -> Either (BagEq a x y) _ eqDec {a} x y = decRel (Permutation (elemDatoid a)) (list x) (list y) BagEquiv : (a : Datoid) -> DecidableEquiv (BagType a) BagEquiv a = decEquiv (equiv (BagEq a) eqRefl eqSym eqTrans) (dec eqDec) Bag : Datoid -> Datoid Bag a = datoid (BagType a) (BagEquiv a) ---------------------------------------------------------------------- -- Bag primitives empty : {a : Datoid} -> El (Bag a) empty = bt nil unit private data LookupResult (a : Datoid) (x : El a) (b : El (Bag a)) : Set where lr : Nat -> (b' : El (Bag a)) -> Not (member a x (contents b')) -> ({y : El a} -> Not (member a y (contents b)) -> Not (member a y (contents b'))) -> LookupResult a x b lookup1 : {a : Datoid} -> (n : Pos.Pos) -> (y : El a) -> (b' : El (Bag a)) -> (nyb' : Not (member a y (contents b'))) -> (x : El a) -> Either (datoidRel a x y) _ -> LookupResult a x b' -> LookupResult a x (bt (pair n y :: list b') (pair nyb' (invariant b'))) lookup1 n y b' nyb' x (left xy) _ = lr (Pos.toNat n) b' (contrapositive (memberPreservesEq xy (contents b')) nyb') (\{y'} ny'b -> snd (notDistribIn ny'b)) lookup1 {a} n y b' nyb' x (right nxy) (lr n' (bt b'' ndb'') nxb'' nmPres) = lr n' (bt (pair n y :: b'') (pair (nmPres nyb') ndb'')) (notDistribOut {datoidRel a x y} nxy nxb'') (\{y'} ny'b -> notDistribOut (fst (notDistribIn ny'b)) (nmPres (snd (notDistribIn ny'b)))) lookup2 : {a : Datoid} -> (x : El a) -> (b : El (Bag a)) -> LookupResult a x b lookup2 x (bt nil nd) = lr zero (bt nil nd) (not id) (\{_} _ -> not id) lookup2 {a} x (bt (pair n y :: b) (pair nyb ndb)) = lookup1 n y (bt b ndb) nyb x (decRel (datoidEq a) x y) (lookup2 x (bt b ndb)) lookup3 : {a : Datoid} -> {x : El a} -> {b : El (Bag a)} -> LookupResult a x b -> Pair Nat (El (Bag a)) lookup3 (lr n b _ _) = pair n b lookup : {a : Datoid} -> El a -> El (Bag a) -> Pair Nat (El (Bag a)) lookup x b = lookup3 (lookup2 x b) private insert' : {a : Datoid} -> (x : El a) -> {b : El (Bag a)} -> LookupResult a x b -> El (Bag a) insert' x (lr n (bt b ndb) nxb _) = bt (pair (Pos.suc' n) x :: b) (pair nxb ndb) insert : {a : Datoid} -> El a -> El (Bag a) -> El (Bag a) insert x b = insert' x (lookup2 x b) private postulate insertLemma1 : {a : Datoid} -> (x : El a) -> (b : El (Bag a)) -> (nxb : Not (member a x (contents b))) -> datoidRel (Bag a) (insert x b) (bt (pair Pos.one x :: list b) (pair nxb (invariant b))) insertLemma2 : {a : Datoid} -> (n : Pos.Pos) -> (x : El a) -> (b : El (Bag a)) -> (nxb : Not (member a x (contents b))) -> datoidRel (Bag a) (insert x (bt (pair n x :: list b) (pair nxb (invariant b)))) (bt (pair (Pos.suc n) x :: list b) (pair nxb (invariant b))) ---------------------------------------------------------------------- -- Bag traversals data Traverse (a : Datoid) : Set where Empty : Traverse a Insert : (x : El a) -> (b : El (Bag a)) -> Traverse a run : {a : Datoid} -> Traverse a -> El (Bag a) run Empty = empty run (Insert x b) = insert x b abstract traverse : {a : Datoid} -> El (Bag a) -> Traverse a traverse (bt nil _) = Empty traverse {a} (bt (pair n x :: b) (pair nxb ndb)) = traverse' (Pos.pred n) where private traverse' : Maybe Pos.Pos -> Traverse a traverse' Nothing = Insert x (bt b ndb) traverse' (Just n) = Insert x (bt (pair n x :: b) (pair nxb ndb)) traverseTraverses : {a : Datoid} -> (b : El (Bag a)) -> datoidRel (Bag a) (run (traverse b)) b traverseTraverses {a} (bt nil unit) = dRefl (Bag a) {empty} traverseTraverses {a} (bt (pair n x :: b) (pair nxb ndb)) = tT (Pos.pred n) (Pos.predOK n) where private postulate subst' : {a : Datoid} -> (P : El a -> Set) -> (x y : El a) -> datoidRel a x y -> P x -> P y tT : (predN : Maybe Pos.Pos) -> Pos.Pred n predN -> datoidRel (Bag a) (run (traverse (bt (pair n x :: b) (pair nxb ndb)))) (bt (pair n x :: b) (pair nxb ndb)) tT Nothing (Pos.ok eq) = ? -- subst' (\p -> datoidRel (Bag a) -- (run (traverse (bt (pair p x :: b) (pair nxb ndb)))) -- (bt (pair p x :: b) (pair nxb ndb))) -- Pos.one n eq (insertLemma1 x (bt b ndb) nxb) -- eq : one == n -- data Pred (p : Pos) (mP : Maybe Pos) : Set where -- ok : datoidRel posDatoid (sucPred mP) p -> Pred p mP -- insert x (bt b ndb) == bt (pair n x :: b) (pair nxb ndb) tT (Just n) (Pos.ok eq) = ? -- insertLemma2 n x (bt b ndb) nxb -- insert x (bt (pair n x :: b) (pair nxb btb) == -- bt (pair (suc n) x :: b) (pair nxb btb) bagElim : {a : Datoid} -> (P : El (Bag a) -> Set) -> Respects (Bag a) P -> P empty -> ((x : El a) -> (b : El (Bag a)) -> P b -> P (insert x b)) -> (b : El (Bag a)) -> P b bagElim {a} P Prespects e i b = bagElim' b (traverse b) (traverseTraverses b) where private bagElim' : (b : El (Bag a)) -> (t : Traverse a) -> datoidRel (Bag a) (run t) b -> P b bagElim' b Empty eq = subst Prespects empty b eq e bagElim' b (Insert x b') eq = subst Prespects (insert x b') b eq (i x b' (bagElim' b' (traverse b') (traverseTraverses b'))) ---------------------------------------------------------------------- -- Respect and equality preservation lemmas postulate insertPreservesRespect : {a : Datoid} -> (P : El (Bag a) -> Set) -> (x : El a) -> Respects (Bag a) P -> Respects (Bag a) (\b -> P (insert x b)) lookupPreservesRespect : {a : Datoid} -> (P : El (Bag a) -> Set) -> (x : El a) -> Respects (Bag a) P -> Respects (Bag a) (\b -> P (snd $ lookup x b)) -- This doesn't type check without John Major equality or some -- ugly substitutions... -- bagElimPreservesEquality -- : {a : Datoid} -- -> (P : El (Bag a) -> Set) -- -> (r : Respects (Bag a) P) -- -> (e : P empty) -- -> (i : (x : El a) -> (b : El (Bag a)) -> P b -> P (insert x b)) -- -> ( (x1 x2 : El a) -> (b1 b2 : El (Bag a)) -- -> (p1 : P b1) -> (p2 : P b2) -- -> (eqX : datoidRel a x1 x2) -> (eqB : datoidRel (Bag a) b1 b2) -- -> i x1 b1 p1 =^= i x2 b2 p2 -- ) -- -> (b1 b2 : El (Bag a)) -- -> datoidRel (Bag a) b1 b2 -- -> bagElim P r e i b1 =^= bagElim P r e i b2