{- 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 )