module Demo where

data Bool : Set where
  True : Bool
  False : Bool

not : Bool -> Bool
not True = False
not False = True

if_then_else_ : Bool -> Bool -> Bool -> Bool
if True then t else e = t
if False then t else e = e

data Nat : Set where
  Zero : Nat
  Succ : Nat → Nat

_+_ : Nat → Nat → Nat
Zero + y = y
Succ x + y = Succ (x + y)

{-# BUILTIN NATURAL Nat #-}

cond : ∀ {a : Set} -> Bool -> a -> a -> a
cond True t e = t
cond False t e = e

test : Nat
test = cond True  

id : ∀ {a : Set} -> a -> a 
id x = x

data List (a : Set) : Set where
  Nil : List a 
  Cons : a -> List a -> List a

_++_ : {a : Set} -> List a -> List a -> List a
Nil ++ ys = ys
Cons x xs ++ ys = Cons x (xs ++ ys)

xs : List Nat
xs = Cons  (Cons  (Cons  Nil))


map : {a b : Set} -> (a -> b) -> List a -> List b
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

data Maybe (a : Set) : Set where
  Nothing : Maybe a
  Just : a -> Maybe a

_!!_ : {a : Set} -> List a -> Nat -> Maybe a
Nil !! Zero = Nothing
Cons x xs !! Zero = Just x
Nil !! Succ i = Nothing
Cons x xs !! Succ i = xs !! i

length : {a : Set} -> List a -> Nat
length Nil = Zero
length (Cons x xs) = Succ (length xs)

data _<_ : Nat -> Nat -> Set where
  Base : forall {n} -> Zero < Succ n
  Step : ∀ {n m} -> n < m -> Succ n < Succ m

lemma :  < 
lemma = Step (Step (Step Base))

impossible : {a : Set} -> (n : Nat) -> n < Zero -> a
impossible n ()

lookup : {a : Set} -> (n : Nat) -> (xs : List a) -> n < length xs -> a
lookup n Nil ()
lookup Zero (Cons x xs) p = x
lookup (Succ n) (Cons x xs) (Step p) = lookup n xs p

data Vec (a : Set) : Nat -> Set where
  Nil : Vec a Zero
  Cons : {n : Nat} -> a -> Vec a n -> Vec a (Succ n)

head : {a : Set} -> (xs : List a) ->  < length xs -> a
head Nil ()
head (Cons x xs) p = x

vhead : {a : Set} {n : Nat} -> Vec a (Succ n) -> a
vhead (Cons x xs) = x

vlookup : {a : Set} {n : Nat} -> Vec a n -> (m : Nat) -> m < n -> a
vlookup Nil m ()
vlookup (Cons x xs) Zero p = x
vlookup (Cons x xs) (Succ n) (Step p) = vlookup xs n p

data Fin : Nat -> Set where
  FZero : {n : Nat} -> Fin (Succ n)
  FSucc : {n : Nat} -> Fin n -> Fin (Succ n)

vlookup' : {a : Set} {n : Nat} -> Vec a n -> Fin n -> a
vlookup' (Cons x xs) FZero = x
vlookup' (Cons x xs) (FSucc i) = vlookup' xs i

vappend : (a : Set) (n m : Nat) -> Vec a n -> Vec a m -> Vec a (n + m)
vappend a .Zero m Nil ys = {!!}
vappend a .(Succ k) m (Cons {k} x xs) ys = {!!}


data _==_ : Nat -> Nat -> Set where
  Refl : {n : Nat} -> n == n

q :  == 
q = Refl 

r : ( + ( + )) == ( + )
r = Refl

q' : (n : Nat) -> (Zero + n) == n
q' n = Refl

sym : (x y : Nat) -> x == y -> y == x
sym x .x Refl = Refl

trans : {x y z : Nat} -> x == y -> y == z -> x == z
trans Refl q = q

cong : {x y : Nat} -> (f : Nat -> Nat) -> x == y -> f x == f y
cong f Refl = Refl

plus-zero : (n : Nat) -> (n + Zero) == n
plus-zero Zero = Refl
plus-zero (Succ n) = let ih = plus-zero n in cong Succ ih

infixr  _⟨_⟩_
_⟨_⟩_ : (x : Nat) -> { y z : Nat} -> x == y -> y == z -> x == z
_⟨_⟩_ x = trans

_■ : forall x -> x == x
_■ x = Refl

plus-zero' : (n : Nat) -> (n + Zero) == n
plus-zero' Zero = Refl
plus-zero' (Succ n) = 
  (Succ n) + Zero
    ⟨ Refl ⟩
  Succ (n + Zero)
    ⟨ cong Succ (plus-zero' n) ⟩
  Succ n ■

foo : (x y : Nat) -> x == (y + ) -> (y + ) == x
foo .(y + ) y Refl = Refl

data Either (a b : Set) : Set where
  Inl : a -> Either a b
  Inr : b -> Either a b

data Empty : Set where

Not : Set -> Set
Not a  = a -> Empty

bar : Not ( == )
bar ()

zs-lemma : (y : Nat) -> (Not (Zero == Succ y))
zs-lemma y ()

eq : (x y : Nat) -> Either (x == y) (Not (x == y))
eq Zero Zero = Inl Refl
eq Zero (Succ y) = Inr (λ () )
eq (Succ x) Zero = Inr (λ ())
eq (Succ x) (Succ y) with eq x y
eq (Succ .y) (Succ y)| Inl Refl = {!!}
... | Inr q = Inr (\sxy -> q (h sxy))
  where
  h : {x y : Nat} -> Succ x == Succ y -> x == y
  h Refl = Refl

filter : {a : Set} -> (a -> Bool) -> List a -> List a
filter p Nil = Nil
filter p (Cons x xs) with p x
filter p (Cons x xs) | True = Cons x (filter p xs)
filter p (Cons x xs) | False = filter p xs

data SubList {a : Set} : List a -> List a -> Set where
  Base : {xs : List a} -> SubList Nil xs
  Keep : forall {x xs ys} -> SubList xs ys -> SubList (Cons x xs) (Cons x ys)
  Drop : forall {y xs ys} -> SubList xs ys -> SubList xs (Cons y ys)

exampleSL : SubList (Cons  Nil) (Cons  (Cons  (Cons  Nil)))
exampleSL = Drop (Keep Base)

filter-lemma : {a : Set} -> (p : a -> Bool) -> (xs : List a) -> SubList (filter p xs) xs
filter-lemma p Nil = Base
filter-lemma p (Cons x xs) with p x
filter-lemma p (Cons x xs) | True = Keep (filter-lemma p xs)
filter-lemma p (Cons x xs) | False = Drop (filter-lemma p xs)

baz : (x y : Nat) -> (y + ) == (x + ) -> x == y
baz x y p with y +  | x + 
baz x y Refl | xp | .xp = {!!}