{- amenities -}
--#include "amenities.agda"
{- THERE ARE SEVERE PROBLEMS HERE.
I am not sure how to begin sorting this out.
-}
package conway (A :: Set) (B :: Pow A)
where
{- we work in a universe closed under binary disjoint sum -}
mutual
U :: Set = data ground (a :: A)
| sum (a :: U) (b :: U)
T :: Pow U = \(u::U) -> case u of
(ground a) -> B a
(sum a b) -> or (T a) (T b)
sum (a, b :: U) :: U = sum@_ a b
fam (A :: Set) :: Set
= data fam (ix :: U) (if :: T ix -> A)
mk_fam (A :: Set) (a :: U) (b :: T a -> A) :: fam A
= fam@_ a b
ix (A :: Set) (f :: fam A) :: U
= case f of (fam ix if) -> ix
if (A :: Set) (f :: fam A) (i :: T (ix A f)) :: A
= case f of (fam ix if) -> if i
union (A :: Set) (f,g :: fam A) :: fam A
= fam@_ (sum (ix A f) (ix A g)) (copair (T (ix A f)) (T (ix A g)) A (if A f) (if A g))
-----------------------------------------------------------------------------------------------------
{- A first effort -}
game :: Set = data G (l :: U) (fl :: T l -> game)
(r :: U) (fr :: T r -> game)
li (g :: game) :: U = case g of { (G l fl r fr) -> l;}
ri (g :: game) :: U = case g of { (G l fl r fr) -> r;}
lf (g :: game) (m :: T (li g)) :: game = case g of { (G l fl r fr) -> fl m;}
rf (g :: game) (m :: T (ri g)) :: game = case g of { (G l fl r fr) -> fr m;}
minus (g :: game) :: game
= case g of
(G l fl r fr) ->
G@_ r (\(h::T r) -> minus (fr h))
l (\(h::T l) -> minus (fl h))
add (g :: game) (h :: game) :: game
= let
l :: U = li g
r :: U = ri g
l' :: U = li h
r' :: U = ri h
fl (i :: T l) :: game = lf g i
fr (i :: T r) :: game = rf g i
fl' (i :: T l') :: game = lf h i
fr' (i :: T r') :: game = rf h i
ll (x :: T (sum l l')) :: game
= case x of
(inl a) -> fl a `add` h
(inr b) -> g `add` (fl' b)
rr (x :: T (sum r r')) :: game
= case x of
(inl a) -> fr a `add` h
(inr b) -> g `add` (fr' b)
in G@_ (sum l l') ll (sum r r') rr
sub (g :: game) (h :: game) :: game
= g `add` minus h
{-
mutual
{- winning strategies for left, if second -}
S0 (g :: game) :: Set = Pi (T (ri g)) (\(h :: T (ri g))-> S1 (rf g h))
{- case g of
(G l fl r fr) ->
data S0 (resp :: (h::T r) -> S1 (fr h)) -}
{- winning strategies for left, if first -}
S1 (g :: game) :: Set = Sigma (T (li g)) (\(h :: T (li g))-> S0 (lf g h))
{- case g of
(G l fl r fr) ->
data S1 (move :: T l) (ready :: S0 (fl move)) -}
identity (A :: game) :: S0 (A `sub` A)
= \(a::T (ri (sub A A))) -> {! a!}
sum_lemma (A, B :: game) ( a :: S0 A) (b :: S0 B) :: S0 (A `add` B)
= case A of { (G l fl r fr) -> case B of { (G l' fl' r' fr') -> case A `add` B of { (G l0 fl0 r0 fr0) -> {! !};};};}
main_lemma (A, B :: game)
(u :: S0 A) (t :: S0 (B `sub` A)) :: S0 B
= {! !}
-}
-----------------------------------------------------------------------------------------
{- A second effort, to localise the constructors and case expansions,
in case that is what is causing the problem. -}
game' :: Set
= data G' (left :: fam game') (right :: fam game')
mk_game' (left,right :: fam game') :: game'
= G'@_ left right
left (g :: game') :: fam game'
= case g of { (G' left right) -> left;}
right (g :: game') :: fam game'
= case g of { (G' left right) -> right;}
li' (g :: game') :: U = ix game' (left g)
ri' (g :: game') :: U = ix game' (right g)
lf' (g :: game') (m :: T (li' g)) :: game' = if game' (left g) m
rf' (g :: game') (m :: T (ri' g)) :: game' = if game' (right g) m
minus' (g :: game') :: game'
= let l :: fam game' = left g
r :: fam game' = right g
in mk_game' (mk_fam game' (ix game' r) (\(h::T (ix game' r)) -> minus' (if game' r h)))
(mk_fam game' (ix game' l) (\(h::T (ix game' l)) -> minus' (if game' l h)))
add' (G,H :: game') :: game'
= let
leftG :: fam game' = left G
rightG :: fam game' = right G
leftH :: fam game' = left H
rightH :: fam game' = right H
leftGix :: U = ix game' leftG
rightGix :: U = ix game' rightG
leftHix :: U = ix game' leftH
rightHix :: U = ix game' rightH
left' :: fam game' = union game' (fam@_ leftGix (\(g::T leftGix) -> add' (if game' leftG g) H))
(fam@_ leftHix (\(h::T leftHix) -> add' G (if game' leftH h)))
right' :: fam game' = union game' (fam@_ rightGix (\(g::T rightGix) -> add' (if game' rightG g) H))
(fam@_ rightHix (\(h::T rightHix) -> add' G (if game' rightH h)))
in G'@_ left' right'
sub' (g :: game') (h :: game') :: game'
= g `add'` (minus' h)
mutual
{- winning strategies for left, if second -}
S0' (g :: game') :: Set =
{- loops
Pi (T (ix game' (right g)))
(\(h::T (ix game' (right g))) -> S1' (if game' (right g) h))
-}
{- loops
(h::T (ix game' (right g))) -> S1' (if game' (right g) h)
-}
{- loops
data S0' (resp :: (h::T (ix game' (right g))) -> S1' (if game' (right g) h))
-}
{! !}
{- winning strategies for left, if first -}
S1' (g :: game') :: Set = data S1' (move :: T (ix game' (left g)))
(ready :: S0' (if game' (left g) move))
Set2 :: Type = sig { A :: Set ; B :: Set }
FF (PQ :: game' -> Set2) (h :: game') :: Set2
= struct
A = (m::T (ix game' (right h))) -> (PQ (if game' (right h) m)).B
B = Sigma (T (ix game' (left h))) (\(m ::T (ix game' (left h))) -> (PQ (if game' (left h) m)).A)
-- S0S1 :: game' -> Set2 = data cons (x :: FF PairPow)
identity' (A :: game') :: S0' (A `sub'` A)
= {! !}
{- S0'@_
(\(a::T (ri' (sub' A A))) ->
copair (T (ix game' (fam@_ (ix game' (right A))
(\(g'::T (ix game' (right A))) ->
add' (if game' (right A) {! !}) (minus' A)))))
(T (ix game' (fam@_ (ix game' (left A))
(\(h'::T (ix game' (right (minus' A)))) ->
add' A (if game' (right (minus' A)) {! !})))))
(S1' (rf' (sub' A A) a))
(\(h::T (ix game' (fam@_ (ix game' (right A))
(\(g'::T (ix game' (right A))) ->
add' (if game' (right A) g') (minus' A))))) -> {! !})
(\(h::T (ix game' (fam@_ (ix game' (right (minus' A)))
(\(h'::T (ix game' (right (minus' A)))) ->
add' A (if game' (right (minus' A)) {! !}))))) -> {! !}) a
) -}
{-
sum_lemma' (A, B :: game') ( a :: S0' A) (b :: S0' B) :: S0' (A `add'` B)
= {! !}
main_lemma' (A, B :: game')
(u :: S0' A) (t :: S0' (B `sub'` A)) :: S0' B
= {! !}
-}
Bool :: Set = data ff | tt
inv (i :: Bool) :: Bool = case i of
(ff) -> tt@_
(tt) -> ff@_
S( i :: Bool) ( G :: game' ) :: Set = case i of
(ff) -> data Sff (x :: (h::T (ix game' (right G))) ->
S (inv i) (if game' (right G) h))
(tt) -> data Stt (x :: Sigma (T (ix game' (left G))) (\(h::T (ix game' (left G))) ->
S (inv i) (if game' (left G) h)))
identity'' (A :: game') :: S ff@_ (A `sub'` A)
= Sff@_ (
(h::T (ix game' (right (sub' A A))))->
copair
(T (ix game' (right A)))
(T (ix game' (left A)))
? -- (S tt@_ (if game' (right (sub' A A)) {! !}))
(\(a::T (ix game' (right A)))
-> Stt@_ (struct { fst = ? ; snd = identity'' (if game' (right A) a);}))
(\(b::T (ix game' (left A)))
-> Stt@_ (struct { fst = ? ; snd = identity'' (if game' (left A) b) ;}))
h
)