-- Demo code from 3rd AFP Agda lecture
module Demo4 where

-- From previous lectures
-------------------------

open import Data.Nat renaming (ℕ to Nat; suc to succ)
open import Data.Bool using (Bool; if_then_else_; true ; false; _∧_)
open import Data.Unit using (⊤ ; tt)
open import Agda.Builtin.List
open import Agda.Builtin.String

data _∈_ (s : String) : List String → Set where
  here : ∀{ss} → s ∈ (s ∷ ss)
  there : ∀{s' ss} → s ∈ ss → s ∈ (s' ∷ ss)

-- Types to propositions
------------------------

ex1 : "helo" ∈ ("helo" ∷ "world" ∷ [])
ex1 = here

-- "the type ("helo" ∈ ("helo" ∷ "world" ∷ [])) is inhabited"
-- "the string "helo" is in the list ("helo" ∷ "world" ∷ [])"

-- ex2 : "helo" ∈ []
-- ex2 = {!   !}

-- "the type ("helo" ∈[]) is inhabited"
-- "the string "helo" is in the list []"

data ⊥ : Set where -- (empty)

ex3 : "helo" ∈ [] → ⊥
ex3 () -- 'absurd pattern'

ex4 : Nat
ex4 = 3 + 6

-- "the type Nat is inhabited"
-- "there exist some ℕ"

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

ex5 : Nat × ("helo" ∈ ("helo" ∷ "world" ∷ []))
ex5 = 7 , ex1

-- "the type (Nat × ("helo" ∈ ("helo" ∷ "world" ∷ []))) is inhabited"
-- "the type Nat is inhabited and the type ("helo" ∈ ("helo" ∷ "world" ∷ [])) is inhabited"
-- "the type Nat is inhabited ∧ the type ("helo" ∈ ("helo" ∷ "world" ∷ [])) is inhabited"
-- "there exist some ℕ ∧ the string "helo" is in the list ("helo" ∷ "world" ∷ [])"

ex6 : Nat → ("helo" ∈ ("helo" ∷ "world" ∷ []))
ex6 x = ex1

-- "the type (Nat → ("helo" ∈ ("helo" ∷ "world" ∷ []))) is inhabited"
-- "given that the type Nat is inhabited, the type ("helo" ∈ ("helo" ∷ "world" ∷ [])) is inhabited"
-- "given that the type Nat is inhabited ⇒ the type ("helo" ∈ ("helo" ∷ "world" ∷ [])) is inhabited"
-- "there exist some   ⇒ the string "helo" is in the list ("helo" ∷ "world" ∷ [])"

-- Curry-Howard correspondence
------------------------------

-- | Agda type T        |  Theorem that holds if T has values  |
-- | ------------------ | ------------------------------------ |
-- | A × B              | A' ∧ B'                              |
-- | A + B              | A' ∨ B'                              |
-- | A → B              | A' ⇒ B'                              |
-- | Nat                | there exists a natural number        |
-- | ⊥                  | false                                |
-- | (x ∈ xs)           | x is in the list xs                  |
-- | (A : Set) → B      | ∀ A. B'                              |
-- |                    | A' ⇔ B'                              |
-- | (A → B) × (B → A)  | (A' ⇒ B') ∧ (B' ⇒ A')                |

-- Propositions to types
------------------------

-- "∀ A . ∀ B . A ∧ B ⇒ B ∧ A"

ex7 : ∀{A B : Set} → A × B → B × A
ex7 (a , b) = b , a

data _＋_ (A B : Set) : Set where
  inl : A → A ＋ B
  inr : B → A ＋ B

-- ex8 : ∀{A B : Set} → A ＋ B → A × B
-- ex8 (inl a) = a , {!   !}
-- ex8 (inr b) = {!   !} , b

-- "∀ A B C. (A ∧ (B ∨ C)) ⇒ (A ∧ B) ∨ (A ∧ C)"

ex9 : ∀{A B C : Set} → A × (B ＋ C) → (A × B) ＋ (A × C)
ex9 (a , inl b) = inl (a , b)
ex9 (a , inr c) = inr (a , c)

-- "∀ A B C. (A ∧ (B ∨ C)) ⇐ (A ∧ B) ∨ (A ∧ C)"

ex9' : ∀{A B C : Set} → (A × B) ＋ (A × C) → A × (B ＋ C)
ex9' (inl (x , x₁)) = x , inl x₁
ex9' (inr (x , x₁)) = x , inr x₁

-- "(A × (B ＋ C)) ⇔ ((A × B) ＋ (A × C))"

_↔_ : Set → Set → Set
A ↔ B = (A → B) × (B → A)

ex10 : ∀{A B C : Set} → (A × (B ＋ C)) ↔ ((A × B) ＋ (A × C))
ex10 {A} {B} {C} = ex9 , ex9'

-- Equality
-----------

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a



ex11 : (2 + 4) ≡ 6
ex11 = refl

data Vec (A : Set) : Nat → Set where
  nil : Vec A zero
  cons : {n : Nat} → A → Vec A n → Vec A (succ n)

vappend : {A : Set} {m n : Nat} → Vec A n → Vec A m → Vec A (n + m)
vappend nil ys = ys
vappend (cons x xs) ys = cons x (vappend xs ys)

ℕ : Set
ℕ = Nat


variable
  A : Set
  xs ys zs acc : List A
  x : A

reverse : List A → List A → List A
reverse [] acc = acc
reverse (x ∷ xs) acc = reverse xs (x ∷ acc)

data Rev {A : Set} : List A → List A → List A → Set where
  rev-base : Rev [] acc acc
  rev-step : Rev xs (x ∷ acc) zs → Rev (x ∷ xs) acc zs

rev-complexity : {xs ys zs : List A} → Rev xs ys zs → ℕ
rev-complexity rev-base = 1
rev-complexity (rev-step rev) = 1 + rev-complexity rev

length : List A → ℕ
length [] = 0
length (x ∷ xs) = 1 + length xs

cong : ∀ {A B : Set} {a1 a2} (f : A → B)
      →   a1 ≡   a2
      → f a1 ≡ f a2
cong _ refl = refl


rev-lineair : {xs ys zs : List A} → (r : Rev xs ys zs) → (rev-complexity r) ≡ (1 + length xs)
rev-lineair rev-base = refl
rev-lineair (rev-step r) = cong succ (rev-lineair r)

data Sorted (b : ℕ) : List Nat → Set where
  base : Sorted b []
  step : b ≤ x → Sorted x xs → Sorted b (x ∷ xs)

insert : ℕ → List ℕ → List ℕ
insert y []       = y ∷ []
insert y (x ∷ xs) = if y ≤ᵇ x then (y ∷ x ∷ xs) else (x ∷ insert y xs)

postulate
  insert-correct : {b : ℕ} (x : ℕ) → (xs : List ℕ) → Sorted b xs → Sorted b (insert x xs)

insertion-sort : List ℕ → List ℕ
insertion-sort [] = []
insertion-sort (x ∷ xs) = insert x (insertion-sort xs)

insertion-sort-correct : {xs : List ℕ} → Sorted 0 (insertion-sort xs)
insertion-sort-correct {[]} = base
insertion-sort-correct {x ∷ xs} = let ih = insertion-sort-correct {xs} in
                                  insert-correct x (insertion-sort xs) ih

snoc : List A → A → List A
snoc [] x = x ∷ []
snoc (y ∷ ys) x = y ∷ (snoc ys x)

slow-reverse : (xs : List A) → List A
slow-reverse [] = []
slow-reverse (x ∷ xs) = snoc (slow-reverse xs) x 

_++_ : List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

trans : ∀ {A : Set} {a1 a2 a3 : A}
      →   a1 ≡ a2
      →        a2 ≡ a3
      →   a1 ≡      a3
trans p refl = p

sym : ∀ {A : Set} {a1 a2 : A}
      →   a1 ≡ a2
      →   a2 ≡ a1
sym refl = refl

infixr 2 _⟨_⟩_
_⟨_⟩_ : {a : Set} -> (x : a) -> {y z : a} -> (x ≡ y) -> (y ≡ z) -> x ≡ z
x ⟨ p ⟩ q = trans p q

_∎ : forall {a : Set} (x : a) -> x ≡ x
_∎ x = refl

lemma : (x : A) (xs ys : List A) → (xs ++ (x ∷ ys)) ≡ (snoc xs x ++ ys)
lemma x [] ys = refl
lemma x (a ∷ as) ys =
  let ih = lemma x as ys in
  ((a ∷ as) ++ (x ∷ ys))
    ⟨ refl ⟩
  (a ∷ (as ++ (x ∷ ys)))
    ⟨ cong (a ∷_) ih ⟩
  (a ∷ (snoc as x ++ ys))
    ⟨ refl  ⟩    
  (snoc (a ∷ as) x ++ ys) ∎


reverse-c : (xs : List A) (acc : List A) → reverse xs acc ≡ (slow-reverse xs ++ acc)
reverse-c [] acc = refl
reverse-c (x ∷ xs) acc = let ih = reverse-c xs (x ∷ acc) in trans ih (lemma x (slow-reverse xs) acc)


data U : Set where
  BOOL : U
  NAT : U
  PAIR : U → U → U

eqBool : Bool → Bool → Bool
eqBool Bool.false Bool.false = true
eqBool Bool.false Bool.true = false
eqBool true false = false
eqBool true true = true

eqNat : ℕ → ℕ → Bool
eqNat zero zero = true
eqNat (succ n) (succ m) = eqNat n m
eqNat _ _  = false

eqPair : {A B : Set} → (A → A → Bool) → (B → B → Bool) → A × B → A × B → Bool
eqPair eqA eqB (x , y) (x' , y') = eqA x x' ∧ eqB y y'

⟦_⟧ : U → Set
⟦ BOOL ⟧     = Bool
⟦ NAT ⟧      = Nat
⟦ PAIR u v ⟧ = ⟦ u ⟧ × ⟦ v ⟧

geq : {u : U} → ⟦ u ⟧ → ⟦ u ⟧ → Bool
geq {BOOL} x y     = eqBool x y
geq {NAT} x y      = eqNat x y
geq {PAIR u v} x y = eqPair geq geq x y

_ : geq (true , 3) (true , 3) ≡ true
_ = refl

data R : Set where
  TIMES : R → R → R
  PLUS : R → R → R
  I : R
  UNIT : R
  K : U → R

p-id : ∀ {a} {A : Set a} → A → A
p-id x = x

⟦_⟧R : R → Set → Set
⟦ TIMES r₀ r₁ ⟧R X = ⟦ r₀ ⟧R X × ⟦ r₁ ⟧R X
⟦ PLUS r₀  r₁ ⟧R X = ⟦ r₀ ⟧R X ＋ ⟦ r₁ ⟧R X
⟦ I ⟧R X           = X
⟦ UNIT ⟧R X        = ⊤
⟦ K x ⟧R X         = ⟦ x ⟧

data Fix (r : R) : Set where
  In : ⟦ r ⟧R (Fix r) → Fix r

-- fmap : (A → B) → ⟦ r ⟧R A → ⟦ r ⟧R B
-- cata : Fix r → (⟦ r ⟧R A → A) → A 
-- genericEq : (r : R) → Fix r → Fix r → Bool

variable
  n : ℕ

data Even : ℕ → Set where
  base : Even zero
  step : Even n → Even (succ (succ n))


_ : Even 2
_ = step base

_ : Even 24
_ = step
     (step
      (step
       (step
        (step (step (step (step (step (step (step (step base)))))))))))

even? : ℕ → Bool
even? zero = true
even? (succ zero) = false
even? (succ (succ n)) = even? n

So : Bool → Set
So true  = ⊤
So false = ⊥

even-sound : (n : ℕ) → So (even? n) → Even n
even-sound zero tt = base
even-sound (succ (succ n)) p = step (even-sound n p)

1022-even : Even 1022
1022-even = even-sound 1022 tt

-- Impossible to complete goal
-- _ : Even 1023
-- _ = even-sound 1023 {!!}

not-succ : {n : Nat} → Even n → (Even (succ n) → ⊥)
not-succ base ()
not-succ (step e) (step p) = not-succ e p

1023-not-even : Even 1023 → ⊥
1023-not-even = not-succ (1022-even)

+-even : {n m : ℕ} → Even n → Even m → Even (n + m)
+-even {n} {m} base e' = e'
+-even {n} {m} (step e) e' = step (+-even e e')