module Live2 where

{- 

A : Set
Prime : Nat → Set
Equals : Nat → Nat → Set
_<_ : Nat → Nat → Set

A → B 
(x : A) → P x

-}

I : {P : Set} → P → P
I p = p

K : {P Q : Set} → P → Q → P
K p q = p

S : {P Q R : Set} → (P → Q → R) → (P → Q) → P → R
S = λ x → λ y → λ z → x z (y z)

data _∧_ (A B : Set) : Set where
  _,_ : A → B → A ∧ B

fst : {A B : Set} → A ∧ B → A
fst (a , b) = a

snd : {A B : Set} → A ∧ B → B
snd (a , b) = b

comm∧ : {A B : Set} → A ∧ B → B ∧ A
comm∧ (a , b) = (b , a)

uncurry : {A B C : Set} → (A → B → C) → A ∧ B → C
uncurry f (a , b) = f a b

curry : {A B C : Set} → (A ∧ B → C) → A → B → C
curry f a b = f (a , b)

data _∨_ (A B : Set) : Set where
  left  : A → A ∨ B
  right : B → A ∨ B

∨elim : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C
∨elim f g (left  a) = f a
∨elim f g (right b) = g b

distrib : {A B C : Set} → A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)
distrib (a , left  b) = left (a , b)
distrib (a , right c) = right (a , c)

distrib' : {A B C : Set} → A ∨ (B ∧ C) → (A ∨ B) ∧ (A ∨ C)
distrib' (left a)  = left a , left a
distrib' (right (b , c)) = right b , right c

data ⊤ : Set where
  tt : ⊤

data ⊥ : Set where

magic : {A : Set} → ⊥ → A
magic ()

¬_ : Set → Set
¬ A = A → ⊥

contradict : {A : Set} → ¬ (A ∧ ¬ A)
contradict = λ x → snd x (fst x)

contrapos : {A B : Set} → (A → B) → ¬ B → ¬ A
contrapos = λ x y z → y (x z)

not1 : {A B : Set} → A → ¬ A → B
not1 = λ x y → magic (y x)

not2 : {A B : Set} → (A → B) → (A → ¬ B) → ¬ A
not2 = λ x y z → y z (x z)

--de Morgan

deMorgan1 : {A B : Set} → ¬ (A ∨ B) → ¬ A ∧ ¬ B
deMorgan1 p = (λ x → p (left x)) , λ x → p (right x)

deMorgan2 : {A B : Set} → (¬ A) ∧ (¬ B) → ¬ (A ∨ B)
deMorgan2 (f , g) (left a)  = f a
deMorgan2 (f , g) (right b) = g b

deMorgan3 : {A B : Set} → (¬ A) ∨ (¬ B) → ¬ (A ∧ B)
deMorgan3 (left y) (y' , y0) = y y'
deMorgan3 (right y) (y' , y0) = y y0

deMorgan4 : {A B : Set} → ¬ (A ∧ B) → (¬ A) ∨ (¬ B)
deMorgan4 = λ x → left (λ x' → x (x' , {!!}))

dndeMorgan4 : {A B : Set} → ¬ (A ∧ B) → ¬ ¬ ((¬ A) ∨ (¬ B))
dndeMorgan4 = λ x x' → x' (left (λ a → x' (right (λ b → x (a , b)))))

lem1 : ∀{A}{B C : A → Set} → ((a : A) → B a ∧ C a) → ((a : A) → B a) ∧ ((a : A) → C a)
lem1 {A} f = (λ (a : A) → fst (f a)) , λ (a : A) → snd (f a)

lem2 : ∀{A}{B C : A → Set} → ((a : A) → B a) ∧ ((a : A) → C a) → (a : A) → B a ∧ C a
lem2 (f , g) a = f a , g a

data ∃ (A : Set)(B : A → Set) : Set where
  _,_ : (a : A) → B a → ∃ A B

And : Set → Set → Set
And A B = ∃ A (λ _ → B)

lem3 : {A : Set}{B : A → Set}{C : Set} → ((a : A) → B a → C) → ∃ A (λ a → B a) → C
lem3 f (a , b) = f a b

lem4 : {A : Set}{B : A → Set}{C : Set} → (∃ A (λ a → B a) → C) → (a : A) → B a → C
lem4 f a b = f (a , b)

data Nat : Set where
  z : Nat
  s : Nat → Nat

data Even : Nat → Set where
  zEven : Even z
  ssEven : ∀{n} → Even n → Even (s (s n))

data Odd : Nat → Set where
  zOdd  : Odd (s z)
  ssOdd : ∀{n} → Odd n → Odd (s (s n))

oddtheneven : {n : Nat} → Odd n → Even (s n)
oddtheneven zOdd      = ssEven zEven
oddtheneven (ssOdd p) = ssEven (oddtheneven p)

eventhenodd : {n : Nat} → Even n → Odd (s n)
eventhenodd zEven      = zOdd
eventhenodd (ssEven p) = ssOdd (eventhenodd p)

oddeven : (n : Nat) → Odd n ∨ Even n
oddeven z     = right zEven
oddeven (s n) with oddeven n
... | left  p = right (oddtheneven p)
... | right p = left (eventhenodd p)

mutual
  data even : Set where
    ez : even
    es : odd → even

  data odd : Set where
    os : even → odd

nat2oddeven : Nat → odd ∨ even
nat2oddeven z     = right ez
nat2oddeven (s n) with nat2oddeven n
... | left  n' = right (es n')
... | right n' = left (os n')

mutual
  odd2nat : odd → Nat
  odd2nat (os n) = s (even2nat n)

  even2nat : even → Nat
  even2nat ez     = z
  even2nat (es n) = s (odd2nat n)

oddeven2nat : odd ∨ even → Nat
oddeven2nat (left  n) = odd2nat n
oddeven2nat (right n) = even2nat n

data _≅_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≅ a

subst : (A : Set)(P : A → Set)(a a' : A) → a ≅ a' → P a → P a'
subst A P a .a refl p = p

resp : ∀{A B : Set}(f : A → B){a a'} → a ≅ a' → f a ≅ f a'
resp f refl = refl

ir : {A : Set}{a a' : A}(p q : a ≅ a') → p ≅ q
ir refl refl = refl

data _≤_ : Nat → Nat → Set where
  z≤ : ∀{n} → z ≤ n
  s≤ : ∀{m n} → m ≤ n → s m ≤ s n

1≤3 : s z ≤ s (s (s z))
1≤3 = s≤ z≤

¬3≤1 : ¬ (s (s (s z)) ≤ s z)
¬3≤1 (s≤ ())

refl≤ : ∀ n → n ≤ n
refl≤ z     = z≤
refl≤ (s n) = s≤ (refl≤ n)

asym : ∀{m n} → m ≤ n → n ≤ m → m ≅ n
asym z≤     z≤ = refl
asym (s≤ p) (s≤ q) = resp s (asym p q)

data List (A : Set) : Set where
  [] : List A
  _::_ : A → List A → List A

length : ∀{A} → List A → Nat
length []        = z
length (a :: as) = s (length as)

safehead : ∀{A} → (as : List A) → ∃ Nat (λ n → s n ≤ length as) → A
safehead [] (a , ())
safehead (a :: as) p = a

safetail : ∀{A} → (as : List A) → ∃ Nat (λ n → s n ≤ length as) → List A
safetail [] (a , ())
safetail (a :: as) p = as