{-# OPTIONS --guardedness #-}
{-
MGS 23 : Type Theory

Thursday
-}

open import tue-lib

infixr 5 _∷_

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

l123 : List ℕ
l123 = 1 ∷ 2 ∷ 3 ∷ []

{-
zeros : ℕ → List ℕ
zeros zero = []
zeros (suc n) = 0 ∷ zeros n
-}
----------------------------------------------------------------------




data Vec (A : Set) : ℕ → Set where
  [] : Vec A 0
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

v123 : Vec ℕ 3
v123 = 1 ∷ 2 ∷ 3 ∷ []

zeros : (n : ℕ) → Vec ℕ n
zeros zero = []
zeros (suc n) = 0 ∷ zeros n



----------------------------------------------------------------------

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

variable m n : ℕ

_++v_ : Vec A m → Vec A n → Vec A (m + n)
[] ++v ys = ys
(x ∷ xs) ++v ys = x ∷ (xs ++v ys)

{-
_!!_ : List A → ℕ → Maybe A
[] !! n = nothing
(x ∷ xs) !! zero = just x
(x ∷ xs) !! suc n = xs !! n
-}

----------------------------------------------------------------------

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc : {n : ℕ} → Fin n → Fin (suc n)

_!!_ : {n : ℕ} → Vec A n → Fin n → A
(x ∷ xs) !! zero = x
(x ∷ xs) !! suc i = xs !! i



----------------------------------------------------------------------

Π : (A : Set)(B : A → Set) → Set
Π A B = (x : A) → B x
syntax Π A (λ x → B) = Π[ x ∈ A ] B


record Σ( A : Set)(B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁ 
  
open Σ
syntax Σ A (λ x → B) = Σ[ x ∈ A ] B

List' : Set → Set
List' A = Σ[ n ∈ ℕ ] (Vec A n)



----------------------------------------------------------------------

variable PP QQ : A → prop

All : (A : Set)(P : A → prop) → prop
All A P = (x : A) → P x
Ex : (A : Set)(P : A → prop) → prop
Ex A P = Σ[ x ∈ A ] P x

syntax All A (λ x → P)  = ∀[ x ∈ A ] P  
infix 0 All
syntax Ex A (λ x → P) = ∃[ x ∈ A ] P
infix 0 Ex

taut : (∃[ x ∈ A ] (PP x)) ⇒ R
      ⇔ (∀[ x ∈ A ] (PP x ⇒ R))
proj₁ taut f a pa = f (a , pa)
proj₂ taut f (a , pa) = f a pa


----------------------------------------------------------------------

-- equality types

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

infix 4 _≡_


sym : {a b : A} → a ≡ b → b ≡ a
sym refl = refl
{-
trans : {a b c : A} → a ≡ b → b ≡ c → a ≡ c
trans p q = {!!}
-}

cong : (f : A → B){a b : A} → a ≡ b → f a ≡ f b
cong f refl = refl





assoc : (l m n : ℕ) → (l + (m + n)) ≡ ((l + m) + n) 
assoc zero m n = refl
assoc (suc l) m n = cong suc (assoc l m n)



----------------------------------------------------------------------
--variable l m n : ℕ

data _≤_ : ℕ → ℕ → Set where
  le-0 : 0 ≤ m
  le-S : m ≤ n → suc m ≤ suc n

variable l : ℕ

ex1 : 1 ≤ 3
ex1 = le-S le-0

ex2 : ¬ (3 ≤ 1)
ex2 (le-S ())

--reflexive≤ = {!!}

transitive≤ : l ≤ m → m ≤ n → l ≤ n
transitive≤ le-0 q = le-0
transitive≤ (le-S p) (le-S q) = le-S (transitive≤ p q)

antisym≤ : m ≤ n → n ≤ m → m ≡ n
antisym≤ = {!!}



----------------------------------------------------------------------


data Form : Set where
  _[⇒]_ : Form → Form → Form
  PVar : String → Form

infixr 10 _[⇒]_  

data Con : Set where
  • : Con -- \bu
  _,_ : Con → Form → Con

variable Γ Δ : Con
variable FP FQ FR : Form

data _⊢_ : Con → Form → Set where -- \vdash, \|-
  zero : (Γ , FP) ⊢ FP
  suc : Γ ⊢ FP → (Γ , FQ) ⊢ FP
  lam : (Γ , FP) ⊢ FQ → Γ ⊢ (FP [⇒] FQ)
  app : Γ ⊢ (FP [⇒] FQ) → Γ ⊢ FP → Γ ⊢ FQ


-- ¬ ⊢ (P ⇒ Q) ⇒ P
no-pqp : ¬ (• ⊢ (((PVar "P") [⇒] (PVar "Q")) [⇒] (PVar "P")))
no-pqp = {!!}

-- ¬ ⊢ ((P ⇒ Q) ⇒ P) ⇒ P
no-Pierce-deriv :
  ¬ (• ⊢ (((PVar "P" [⇒] PVar "Q") [⇒] PVar "P") [⇒] PVar "P"))
no-Pierce-deriv p = {!!}