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

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

open import Agda.Builtin.Nat
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' = {!   !}

-- "(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

-- ex12 : (2 + 5) ≡ 6
-- ex12 = refl

-- "forall n ∈ N. n can be written as a sum of powers of two"

-- " ∀ n > 2. there are no a b c ∈ ℕ s.t. a^n + b^n = c^n"
-- " ∀ n ∈ ℕ. there are no a b c ∈ ℕ s.t. a^(n + 3) + b^(n + 3) = c^(n + 3)"
-- " ∀ n ∈ ℕ. (∃ a b c ∈ ℕ s.t. a^(n + 3) + b^(n + 3) = c^(n + 3)) ⇒ false
-- " ∀ n ∈ ℕ. ∀ a b c ∈ ℕ. a^(n + 3) + b^(n + 3) = c^(n + 3) ⇒ false""
-- " ∀ n a b c ∈ ℕ. a^(n + 3) + b^(n + 3) = c^(n + 3) ⇒ false"

_^_ : Nat → Nat → Nat
m ^ zero = 1
m ^ suc n = m * m ^ n

fermats-last-theorem : ∀ {n a b c} → (a ^ (n + 3) + b ^ (n + 3)) ≡ (c ^ (n + 3)) → ⊥
fermats-last-theorem = {!   !}

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

ex13 : ∀ x → (x + 0) ≡ x
-- ex13 _ = refl
ex13 zero = refl
ex13 (suc x') = cong suc (ex13 x')

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

-- Recursive proof
------------------

map : (String → String) → List String → List String
map _ [] = []
map f (x ∷ ss) = f x ∷ map f ss

ex14 : ∀ {f : String → String} x xs → x ∈ xs → f x ∈ map f xs
ex14 _ (s ∷ xs) here = here
ex14 _ (s ∷ xs) (there x∈xs) = there (ex14 _ _ x∈xs)