Agda-2.3.2.2: examples/AIM4/bag/Bag.agda
{-# 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