{- 
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Thorsten Altenkirch

  Lecture 11: Inductive relations

  In this lecture we show how relations can be defined
  inductively. The idea is that we give constructors for derivations
  defining a dependent type like Vec or Fin.

  We look at two examples: the ≤-relation (less-or-equal) on the
  natural numbers and two different definitions of derivations for
  propositional logic with implication only. We show that ≤ is an
  partial order and that the combinatory version of propositional
  logic (with the combinators S and K) is equivalent to one with an
  introduction rule for implication.

-}
module l11 where

open import Data.Nat hiding (_≤_ ; _≤?_ ; _<_)
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))

{- We shall now use inductively defined relations to develop some
   basic metatheory, i.e. we are going to prove something *about* a
   logic (instead of within). As an example we use a very small logic:
   Propositional Logic with implication only. -}

{- First we formalize the syntax of formulas: -}
data Formula : Set where
  Atom : String → Formula
  _⇒_ : (A B : Formula) → Formula

infixr  _⇒_ 

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

{- We also need to define contexts of assumptions which are basically
   lists of formulas. However, we are not using Lists since the
   convention is that contexts are written backwards. -}
data Context : Set where
  ε : Context
  _·_ : (Γ : Context) → (A : Formula) → Context

infix  _⊢sk_
infix  _⊢_
infixl  _·_

-- ⊢ = \vdash (pronounced turnstyle)

{- We define the relation ⊢ , where Γ ⊢ A means that the formular A is
   derivable from the assumptions Γ. 
   What are the basic proof rules for propositional logic?-}

data _⊢_ : Context → Formula → Set where
  ass : ∀ {Γ A} → Γ · A ⊢ A
  {- we can prove a formula is we have assumed it. -}
  weak : ∀ {Γ A B} → Γ ⊢ A → Γ · B ⊢ A
  {- we can ignore an assumption. -}
  app : ∀ {Γ A B} → Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
  {- this is also called the modus ponens. -}
  abs : ∀ {Γ A B} → Γ · A ⊢ B → Γ ⊢ A ⇒ B
  {- To prove A implies B, we assume A and prove B. -}

{- As two examples we derive the basic combinators S and K. -}
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))))

{- The main theorem we are going to prove is that K and S can be used
   as replacement for the abstraction rule.
   Formally we define an alternative derivation relation ⊢sk where 
   the abstraction rule is replaced by axioms for S and K. -}

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
 
{- It is easy to show that provability ising ⊢sk implies ⊢ since
   we have already established S and K.
   We prove this by induction over the derivation of ⊢sk.
-}
⊢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'

{- To show the other direction we need to show that the abstraction
   rule is derivable for ⊢sk.
   As a first step we show that A → A is provable.
-}
I : ∀ {Γ A} → Γ ⊢sk A ⇒ A
I {Γ} {A} = app (app S K) (K {B = A})

{- To show the abstraction rule for SK we analyze the possible proofs
   of the proof with the added assumption.
   The combinators I, K , S are precisely what is needed for the
   assumption, weakeneing and application rule. This explains the
   choice especially of the S combinator.
   The last two lines mean that we can prove S and K with an extra
   assumption using K.
-}
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

{- We are now ready to prove the other direction 
   by induction over the derivation. -}
⊢→⊢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)