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
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
¬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 4
even4 = sucsuc (sucsuc zero)

{- show that 3 is not even. -}

¬even3 : ¬ (Even 3)
¬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 7 _∧_
infixr 6 _⇒_ 
infix 4 _⊢sk_
infix 4 _⊢_
infixl 5 _·_
infixl 7 _∨_

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