Bound variable not as bound as one would think about idris-dev HOT 3 CLOSED

> module TestBound

> soFalseElim : so False -> a
> soFalseElim x = FalseElim (believe_me x)

> X : Set
> X = (n : Nat ** so (n < 3))

> (==) : X -> X -> Bool
> (==) x x' = (getWitness x == getWitness x')

> data Move = L | R 

> adm : X -> Move -> Bool
> adm (n ** _) L = n <= 1
> adm (n ** _) R = n >= 1

> Y : X -> Set
> Y x = (a : Move ** so (adm x a))

> step : (x : X) -> Y x -> X
> step (O ** _) (L ** _) = (2 ** oh)
> step ((S n) ** _) (L ** _) = (n ** believe_me oh) -- trivial
> step (n ** _) (R ** _) = 
>   if n == 2 then (O ** oh) else (S n ** believe_me oh)

> pred : X -> X -> Bool
> pred x x' = (adm x L && x' == step x (L ** believe_me oh)) ||
>             (adm x R && x' == step x (R ** believe_me oh))

> succs : X -> (n : Nat ** Vect X n)
> succs x = filter (pred x) [(0 ** oh),(1 ** oh),(2 ** oh)]

> preds : X -> (n : Nat ** Vect X n)
> preds x' = filter ((flip pred) x') [(0 ** oh),(1 ** oh),(2 ** oh)]

> emptyC : (n : Nat ** Vect X n) -> Bool
> emptyC (_ ** Nil) = True
> emptyC (_ ** (x :: xs)) = False

> inC : X -> (n : Nat ** Vect X n) -> Bool
> inC _ (_ ** Nil) = False
> inC x (_ ** (x' :: xs')) = x == x' || inC x (_ ** xs')

> someC : (X -> Bool) -> (n : Nat ** Vect X n) -> Bool
> someC _ (_ ** Nil) = False
> someC p (_ ** (x :: xs)) = p x || someC p (_ ** xs)

> lemmaC2 : (xs : (n : Nat ** Vect X n)) ->
>           so (not (emptyC xs)) ->
>           (x : X ** so (x `inC` xs))
> lemmaC2 (_ ** Nil) soF = soFalseElim soF
> lemmaC2 (_ ** (x :: xs)) _ = (x ** believe_me oh)

> lemmaC3 : (x : X) ->
>           (p : X -> Bool) ->
>           (xs : (n : Nat ** Vect X n)) ->
>           so (p x) ->
>           so (inC x xs) ->
>           so (someC p xs)
> lemmaC3 _ _ (_ ** Nil) _ soF = soFalseElim soF
> lemmaC3 _ _ (_ ** (x :: xs)) _ _ = ?lemmaC3_2

> succsTh : (x : X) -> so (not (emptyC (succs x)))
> succsTh x = ?lala

> reachable : (m : Nat) -> X -> Bool
> reachable O _ = True
> reachable (S m) x' = someC (reachable m) (preds x')

> viable : (n : Nat) -> X -> Bool
> viable O _ = True
> viable (S n) x = someC (viable n) (succs x)

> viableTh : (n : Nat) -> (x : X) -> so (viable n x)
> viableTh O _ = oh
> viableTh (S n) k = step2 where  
>   step0 : so (not (emptyC (succs k)))
>   step0 = succsTh k
>   step1 : (x' : X ** so (x' `inC` (succs k)))
>   step1 = lemmaC2 (succs k) step0
>   step2 : so (someC (viable n) (succs k))
>   step2 = lemmaC3 x' (viable n) (succs k) vnx' x'inCsuccsx where
>     x' : X
>     x' = getWitness step1
>     vnx' : so (viable n x')
>     vnx' = viableTh n x' -- induction step
>     x'inCsuccsx : so (x' `inC` (succs k))
>     x'inCsuccsx = getProof step1