```{-
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
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))

{- 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 6 _⇒_

{- 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 4 _⊢sk_
infix 4 _⊢_
infixl 5 _·_

-- ⊢ = \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)
```