module Jueves where

open import Data.Nat hiding (_≤_ ; module _≤_ ; _≤?_ ; _<_)
open import Relation.Binary.PropositionalEquality -- defines ≡ 
open import Relation.Nullary
open import Data.String

{- inductive defn of ≤ - there are two ways to show m ≤ n:
    z≤n : zero is less-or-equal any number.
    s≤s : if m is less-or equal n them suc m is less-or-equal suc n.
    These are the only ways to show m ≤ n.
 -}

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

{- examples -}

2≤4 :  ≤ 
2≤4 = s≤s (s≤s z≤n)

{- Note that there wasn't much choice deriving 2≤4. Indeed we just
   have to type C-c C-r three times. -}

{- How to prove a negative result? 
   We use pattern matching until we obtain an obviously impossible
   pattern. 
-}

¬4≤2 : ¬  ≤ 
¬4≤2 (s≤s (s≤s ()))

{- We want to show that ≤ is a partial order, i.e. it is reflexive,
   transitive and antisymmetric. -}  

{- we prove reflexivity by a simple induction over the natural
   numbers. -}

≤-refl : ∀ {n} → n ≤ n
≤-refl {zero} = z≤n
≤-refl {suc n} = s≤s (≤-refl {n})

{- transitivity and antisymmetry both require an analysis of the input
   derivation using pattern matching. -}

≤-trans : ∀ {l m n} → l ≤ m → m ≤ n → l ≤ n
≤-trans z≤n m≤n = z≤n
≤-trans (s≤s m≤n) (s≤s n≤n') = s≤s (≤-trans m≤n n≤n')

≤-asym : ∀ {m n} → m ≤ n → n ≤ m → m ≡ n
≤-asym z≤n z≤n = refl
≤-asym (s≤s m≤n) (s≤s m≤n') = cong suc (≤-asym m≤n m≤n')

{- Additionally we can prove something about the proofs of ≤, namely
   that they contain no information. We can show that any two proof of
   m ≤ n are the same. Note that this similar to the uniqueness of
   identy proofs we showed in the last lecture. -}

≤-unique : {m n : ℕ} → (p q : m ≤ n) → p ≡ q
≤-unique z≤n z≤n = refl
≤-unique (s≤s m≤n) (s≤s m≤n') = cong s≤s (≤-unique m≤n m≤n')

{- Finally we establish that ≤ is decidable: -}

{- To deal with the negative successor case we need to invert the s≤s
   constructor, which is easy using pattern matching. -}
s≤s-inv : ∀ {m n} → suc m ≤ suc n → m ≤ n
s≤s-inv (s≤s m≤n) = m≤n

{- decidablity can be derived by analyzing the numbers. The structure
   is similar to the decidability of equality for natural numbers we
   did last week. -}

_≤?_ : (m n : ℕ) → Dec (m ≤ n)
zero ≤? n = yes z≤n
suc n ≤? zero = no (λ ())
suc n ≤? suc n' with n ≤? n'
suc n ≤? suc n' | yes p = yes (s≤s p)
suc n ≤? suc n' | no ¬p = no (λ x → ¬p (s≤s-inv x))

{- an alternative definition of ≤ -}

data _≤'_ : ℕ → ℕ → Set where
  n≤'n : ∀ {n}                 → n  ≤' n
  m≤'s : ∀ {m n} (m≤n : m ≤' n) → m ≤' suc n

m≤s : ∀ {m n} (m≤n : m ≤ n) → m ≤ suc n
m≤s z≤n = z≤n
m≤s (s≤s m≤n) = s≤s (m≤s m≤n)

≤'→≤ : ∀ {m}{n} → m ≤' n → m ≤ n
≤'→≤ n≤'n = ≤-refl
≤'→≤ (m≤'s m≤n) = m≤s (≤'→≤ m≤n)

z≤'n : ∀ {n}                 → zero  ≤' n
z≤'n {zero} = n≤'n
z≤'n {suc n} = m≤'s (z≤'n {n}) 
 
s≤'s : ∀ {m n} (m≤n : m ≤' n) → suc m ≤' suc n
s≤'s n≤'n = n≤'n
s≤'s (m≤'s m≤n) = m≤'s (s≤'s m≤n)

≤→≤' : ∀ {m}{n} → m ≤ n → m ≤' n
≤→≤' z≤n = z≤'n
≤→≤' (s≤s m≤n) = s≤'s (≤→≤' m≤n)

{- A simpler example: Even -}

data Even : ℕ → Set where
  zero : Even zero
  sucsuc : ∀ {n} → Even n → Even (suc (suc n))

{- show that 4 is even. -}

even4 : Even 
even4 = sucsuc (sucsuc zero)

{- show that 3 is not even. -}

¬even3 : ¬ (Even )
¬even3 (sucsuc ())

{- show that sucsuc is invertible -}

inv-sucsuc : ∀ {n} → Even (suc (suc n)) → Even n 
inv-sucsuc (sucsuc evenn) = evenn

{- show that there is at most one proof of even. -}

even-unique : ∀ {m} → (p q : Even m) → p ≡ q
even-unique zero zero = refl
even-unique (sucsuc p) (sucsuc q) = cong sucsuc (even-unique p q)

{- show that even is decidable. -}

even? : (n : ℕ) → Dec (Even n)
even? zero = yes zero
even? (suc zero) = no (λ ())
even? (suc (suc n)) with even? n
even? (suc (suc n)) | yes p = yes (sucsuc p)
even? (suc (suc n)) | no ¬p = no (λ x → ¬p (inv-sucsuc x))

{- Combinatoric logic: we extend propositional logic by conjunction:  -}

data Formula : Set where
  Atom : String → Formula
  _⇒_ : (A B : Formula) → Formula
  _∧_ :  (A B : Formula) → Formula
  _∨_ :  (A B : Formula) → Formula

{- Here is an example formula - the translation of (P -> Q) -> P -}
example : Formula
example = ((Atom "P") ⇒ (Atom "Q")) ⇒ Atom "P"

data Context : Set where
  ε : Context
  _·_ : (Γ : Context) → (A : Formula) → Context

infixl  _∧_
infixr  _⇒_ 
infix  _⊢sk_
infix  _⊢_
infixl  _·_
infixl  _∨_

data _⊢_ : Context → Formula → Set where
  ass : ∀ {Γ A} → Γ · A ⊢ A
  weak : ∀ {Γ A B} → Γ ⊢ A → Γ · B ⊢ A
  app : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
  abs : ∀ {Γ A B} → Γ · A ⊢ B → Γ ⊢ A ⇒ B
  {- To prove a conjuction we prove both components -}
  pair : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ B → Γ ⊢ A ∧ B
  {- To use a conjunction is the same as assuming both components -}
  elim : ∀ {Γ A B C} → Γ · A · B ⊢ C → Γ · A ∧ B ⊢ C
  {- There are two ways to prove a disjunction. -}
  left : ∀ {Γ A B} → Γ ⊢ A → Γ ⊢ A ∨ B
  right : ∀ {Γ A B} → Γ ⊢ B → Γ ⊢ A ∨ B
  {- The eliminator for disjunction is proof by cases -}
  case : ∀ {Γ A B C} → Γ · A ⊢ C → Γ · B ⊢ C → Γ · A ∨ B ⊢ C


{- In combinatory logic we add three combinators pair, fst and snd -}

data _⊢sk_ : Context → Formula → Set where
  ass : ∀ {Γ A} → Γ · A ⊢sk A
  weak : ∀ {Γ A B} → Γ ⊢sk A → Γ · B ⊢sk A
  app : ∀ {Γ A B} → Γ ⊢sk A ⇒ B → Γ ⊢sk A → Γ ⊢sk B
  K : ∀ {Γ A B} → Γ ⊢sk A ⇒ B ⇒ A
  S : ∀ {Γ A B C} → Γ ⊢sk (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
  pair : ∀ {Γ A B} → Γ ⊢sk A ⇒ B ⇒ A ∧ B
  fst : ∀ {Γ A B} → Γ ⊢sk A ∧ B ⇒ A
  snd : ∀ {Γ A B} → Γ ⊢sk A ∧ B ⇒ B
  left : ∀ {Γ A B} → Γ ⊢sk A ⇒ A ∨ B
  right : ∀ {Γ A B} → Γ ⊢sk B ⇒ A ∨ B
  case : ∀ {Γ A B C} → Γ ⊢sk (A ⇒ C) ⇒ (B ⇒ C) ⇒ A ∨ B ⇒ C


{- Show that the two derivation relations are equivalent.

  Hint: You are welcome to reuse (and extend) proofs from l11.agda 
-}

pair' : ∀ {Γ A B} → Γ ⊢ A ⇒ B ⇒ A ∧ B
pair' = abs (abs (pair (weak ass) ass))

fst' : ∀ {Γ A B} → Γ ⊢ A ∧ B ⇒ A
fst' = abs (elim (weak ass))

snd' : ∀ {Γ A B} → Γ ⊢ A ∧ B ⇒ B
snd' = abs (elim ass)

I : ∀ {Γ A} → Γ ⊢sk A ⇒ A
I {Γ} {A} = app (app S K) (K {B = A})

K' : ∀ {Γ A B} → Γ ⊢ A ⇒ B ⇒ A
K' = abs (abs (weak ass))

S' : ∀ {Γ A B C} → Γ ⊢ (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C
S' = abs (abs (abs (app (app (weak (weak ass)) ass)
         (app (weak ass) ass))))

abs' : ∀ {Γ A B} → Γ · A ⊢sk B → Γ ⊢sk A ⇒ B
abs' ass = I
abs' (weak d) = app K d
abs' (app d d') = app (app S (abs' d)) (abs' d')
abs' K = app K K
abs' S = app K S
abs' pair = app K pair
abs' fst = app K fst
abs' snd = app K snd
abs' left = app K left
abs' right = app K right
abs' case = app K case

left' : ∀ {Γ A B} → Γ ⊢sk A → Γ ⊢sk A ∨ B 
left' d = app left d

right' : ∀ {Γ A B} → Γ ⊢sk B → Γ ⊢sk A ∨ B
right' d = app right d

case' : ∀ {Γ A B C} → Γ · A ⊢sk C → Γ · B ⊢sk C → Γ · A ∨ B ⊢sk C 
case' d d' =  app (app (app case (weak (abs' d))) (weak (abs' d'))) ass

elim' :  ∀ {Γ A B C} → Γ · A · B ⊢sk C → Γ · A ∧ B ⊢sk C
elim' d = app (app (weak (abs' (abs' d))) (app fst ass)) (app snd ass)

⊢sk→⊢ : ∀ {Γ A} → Γ ⊢sk A → Γ ⊢ A
⊢sk→⊢ ass = ass
⊢sk→⊢ (weak d) = weak (⊢sk→⊢ d)
⊢sk→⊢ (app d d') = app (⊢sk→⊢ d) (⊢sk→⊢ d')
⊢sk→⊢ K = K'
⊢sk→⊢ S = S'
⊢sk→⊢ pair = pair'
⊢sk→⊢ fst = fst'
⊢sk→⊢ snd = snd'
⊢sk→⊢ left = abs (left ass)
⊢sk→⊢ right = abs (right ass)
⊢sk→⊢ case = abs (abs (abs (case (app (weak (weak ass)) ass) (app (weak ass) ass)) ))

⊢→⊢sk : ∀ {Γ A} → Γ ⊢ A → Γ ⊢sk A
⊢→⊢sk ass = ass
⊢→⊢sk (weak d) = weak (⊢→⊢sk d)
⊢→⊢sk (app d d') = app (⊢→⊢sk d) (⊢→⊢sk d')
⊢→⊢sk (abs d) = abs' (⊢→⊢sk d)
⊢→⊢sk (pair d d') = app (app pair (⊢→⊢sk d)) (⊢→⊢sk d')
⊢→⊢sk (elim d) = elim' (⊢→⊢sk d)
⊢→⊢sk (left d) = left' (⊢→⊢sk d)
⊢→⊢sk (right d) = right' (⊢→⊢sk d)
⊢→⊢sk (case d d') = case' (⊢→⊢sk d) (⊢→⊢sk d')

{- Use this to solve the exercise from Tuesday! -}

{-
B : {P Q R : prop} → (P → Q) → (Q → R) → P → R
B = λ pq qr p → qr (pq p)
-}
B : ∀ {Γ P Q R} → Γ ⊢ (P ⇒ Q) ⇒ (Q ⇒ R) ⇒ (P ⇒ R)
B = abs (abs (abs (app (weak ass) (app (weak (weak ass)) ass)))) 

B' : ∀ {Γ P Q R} → Γ ⊢sk (P ⇒ Q) ⇒ (Q ⇒ R) ⇒ (P ⇒ R)
B' = ⊢→⊢sk B

{-
C : {P Q R : prop} → (P → Q → R) → Q → P → R
C = λ x x' x0 → x x0 x'
-}

C : ∀ {Γ P Q R} → Γ ⊢ (P ⇒ Q ⇒ R) ⇒ Q ⇒ P ⇒ R
C = abs (abs (abs (app (app (weak (weak ass)) ass) (weak ass))))

C' : ∀ {Γ P Q R} → Γ ⊢sk (P ⇒ Q ⇒ R) ⇒ Q ⇒ P ⇒ R
C' = ⊢→⊢sk C

{- challenge: reprove distrib only with combinators. -}

{-
distribC : {P Q R : prop} → P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)
distribC = {!!}
-}
{-
distrib→ : {P Q R : prop} → P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)
distrib→ (p , left q) = left (p , q)
distrib→ (p , right r) = right (p , r)
-}

distrib : ∀ {Γ P Q R} → Γ ⊢ P ∧ (Q ∨ R) ⇒ (P ∧ Q) ∨ (P ∧ R)
distrib = abs (elim (case (left (pair (weak ass) ass)) (right (pair (weak ass) ass))))

distrib' : ∀ {Γ P Q R} → Γ ⊢sk P ∧ (Q ∨ R) ⇒ (P ∧ Q) ∨ (P ∧ R)
distrib' = ⊢→⊢sk distrib