module deduction where

{-

 A. Turing     1944 The Reform of Mathematical Notation and Phraseology

 "The deduction theorem should therefore be as well known as integration by parts"

-}

{-

 The deduction theorem tells us that in order to prove A => B from a list of hypotheses G
 it is enough to add A to the list G and then prove B from this extended list

 We need first to define what it means to prove a sentence from a list of hypotheses

    -either the sentence is in the list
    -or the sentence is an instance of an axiom (here two axioms S and K)
    -or the sentence can be deduced from modus-ponens: we have deduced A => B and we have deduced A
    and we deduce B by modus-ponens

 This definition is inductive:
       we define G |- A read "A is deduced from the hypotheses G" by induction

 We show then -by induction- that if G, A |- B then we have G |- A => B

 We have a lot of cases

 One key case is that we have G, A |- C => B and G, A |- C
 By -induction- we have G |- A => (C => B) and G |- A => C
 We want G |- A => B
 This is exactly where the axiom S plays a role

-}

data Nat : Set where
 zero : Nat
 suc  : Nat -> Nat

data list (A : Set) : Set where
 nil : list A
 cons : A -> list A -> list A


-- ============================================================
-- PART 0.  Warm-up: indexed inductive types
--
-- An inductive definition
--
--    data D (P : ...) : I -> Set where ...
--
-- has PARAMETERS P, written LEFT of the colon, and INDICES,
-- written RIGHT of the colon.
--
--   * a parameter is fixed once and for all: every constructor
--     produces an element of  D P ...  for the SAME P;
--   * an index may VARY from constructor to constructor, and a
--     constructor may choose which index it lands on.
--
-- Pattern matching on an element of  D P i  therefore tells us
-- something about i: this is why indexed families are the way we
-- express "the elements of this type satisfying ..." and, in
-- particular, the way we express derivations G |- X below.
-- ============================================================

-- addition, used below
infixl 20 _+_
_+_ : Nat -> Nat -> Nat
zero  + n = n
suc m + n = suc (m + n)

-- two small types, used further down
data ⊥ : Set where

efq : {A : Set} -> ⊥ -> A
efq ()

record ⊤ : Set where
 constructor tt

-- ------------------------------------------------------------
-- Vectors: the length is an index
-- ------------------------------------------------------------

infixr 5 _::_

data Vec (A : Set) : Nat -> Set where
 []   : Vec A zero
 _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

-- A is a parameter (the same for [] and _::_)
-- the length is an index ([] lands on zero, _::_ on suc n)

-- head is total: the type says the vector is non empty,
-- and Agda sees that the case [] is impossible
head : {A : Set} -> {n : Nat} -> Vec A (suc n) -> A
head (a :: as) = a

tail : {A : Set} -> {n : Nat} -> Vec A (suc n) -> Vec A n
tail (a :: as) = as

map : {A B : Set} -> {n : Nat} -> (A -> B) -> Vec A n -> Vec B n
map f []        = []
map f (a :: as) = f a :: map f as

-- two vectors of the SAME length: only two cases have to be written,
-- since once the first argument is [] the length is zero, and then the
-- second argument can only be [] as well
vadd : {n : Nat} -> Vec Nat n -> Vec Nat n -> Vec Nat n
vadd []        []        = []
vadd (a :: as) (b :: bs) = (a + b) :: vadd as bs

-- the elimination rule of Vec: the motive C now depends on the
-- length AND on the vector
VecRec : {A : Set} -> (C : (n : Nat) -> Vec A n -> Set) ->
         C zero [] ->
         ((n : Nat) -> (a : A) -> (as : Vec A n) -> C n as -> C (suc n) (a :: as)) ->
         (n : Nat) -> (as : Vec A n) -> C n as
VecRec C base step  zero     []       = base
VecRec C base step (suc n) (a :: as)  = step n a as (VecRec C base step n as)

-- ------------------------------------------------------------
-- Finite types: Fin n has exactly n elements
-- ------------------------------------------------------------

data Fin : Nat -> Set where
 zero : {n : Nat} ->          Fin (suc n)
 suc  : {n : Nat} -> Fin n -> Fin (suc n)

-- Fin zero is empty: no constructor can produce Fin zero

-- lookup is total: the index cannot be out of bounds
lookup : {A : Set} -> {n : Nat} -> Vec A n -> Fin n -> A
lookup (a :: as)  zero    = a
lookup (a :: as) (suc i)  = lookup as i

-- ------------------------------------------------------------
-- An inductively defined relation: m <= n
-- ------------------------------------------------------------

data _<=_ : Nat -> Nat -> Set where
 leZero : {n : Nat} ->              zero  <= n
 leSuc  : {m n : Nat} -> m <= n -> suc m <= suc n

-- here BOTH arguments are indices, and there is no parameter
-- a proposition (about two numbers) given by an inductive definition

leRefl : (n : Nat) -> n <= n
leRefl  zero   = leZero
leRefl (suc n) = leSuc (leRefl n)

leTrans : {l m n : Nat} -> l <= m -> m <= n -> l <= n
leTrans  leZero      q         = leZero
leTrans (leSuc p)   (leSuc q)  = leSuc (leTrans p q)

-- the case  leSuc p , leZero  does not have to be written:
-- leZero proves zero <= n, and  suc m  is not  zero

-- this was the FIRST derivation of transitivity: induction on the
-- derivation, written as pattern matching on both arguments
-- note that matching the SECOND argument with leSuc q uses that a
-- derivation of  suc m <= n  can only be a leSuc, so that n is a
-- successor: this is an INVERSION, and Agda does it for us

-- ------------------------------------------------------------
-- The elimination rule of _<=_, and a second derivation
-- ------------------------------------------------------------

-- the eliminator: one premise per constructor, and a MOTIVE R
leRec : (R : Nat -> Nat -> Set) ->
        ((n : Nat) -> R zero n) ->
        ((x y : Nat) -> R x y -> R (suc x) (suc y)) ->
        (x y : Nat) -> x <= y -> R x y
leRec R base step  zero    y       leZero    = base y
leRec R base step (suc x) (suc y) (leSuc p)  = step x y (leRec R base step x y p)

-- to prove transitivity with leRec we must choose a motive: the
-- statement we prove by induction on the derivation of x <= y is
--        R x y  =  for all z, if y <= z then x <= z
R : Nat -> Nat -> Set
R x y = (z : Nat) -> y <= z -> x <= z

Rbase : (n : Nat) -> R zero n
Rbase n z q = leZero

-- the step case is where the inversion is needed: from  suc y <= z
-- we must learn that z is a successor.  The eliminator does not give
-- this, but the SAME relation defined by recursion does -- see le below

-- the same relation, defined by RECURSION on the two numbers
le : Nat -> Nat -> Set
le  zero    y       = ⊤
le (suc x)  zero    = ⊥
le (suc x) (suc y)  = le x y

-- the two definitions agree
toLe : (x y : Nat) -> x <= y -> le x y
toLe  zero    y       leZero    = tt
toLe (suc x) (suc y) (leSuc p)  = toLe x y p

fromLe : (x y : Nat) -> le x y -> x <= y
fromLe  zero    y       h = leZero
fromLe (suc x)  zero    h = efq h
fromLe (suc x) (suc y)  h = leSuc (fromLe x y h)

-- now the step case goes through: we do induction on the NUMBER z,
-- which is a plain natural number, not a derivation
Rstep : (x y : Nat) -> R x y -> R (suc x) (suc y)
Rstep x y h  zero    q = efq (toLe (suc y) zero q)
Rstep x y h (suc z)  q = leSuc (h z (fromLe y z (toLe (suc y) (suc z) q)))

-- SECOND derivation of transitivity: the eliminator, with the motive R
leTrans2 : (x y z : Nat) -> x <= y -> y <= z -> x <= z
leTrans2 x y z p q = leRec R Rbase Rstep x y p z q

-- and, since le computes, transitivity for le is plain recursion
leTransRec : (x y z : Nat) -> le x y -> le y z -> le x z
leTransRec  zero    y        z       p q = tt
leTransRec (suc x)  zero     z       p q = efq p
leTransRec (suc x) (suc y)   zero    p q = efq q
leTransRec (suc x) (suc y)  (suc z)  p q = leTransRec x y z p q

leTrans3 : (x y z : Nat) -> x <= y -> y <= z -> x <= z
leTrans3 x y z p q = fromLe x z (leTransRec x y z (toLe x y p) (toLe y z q))

-- ------------------------------------------------------------
-- Two mutually defined families
-- ------------------------------------------------------------

data Even : Nat -> Set
data Odd  : Nat -> Set

data Even where
 evenZero :                Even  zero
 evenSuc  : {n : Nat} -> Odd n -> Even (suc n)

data Odd where
 oddSuc   : {n : Nat} -> Even n -> Odd (suc n)

-- ------------------------------------------------------------
-- The identity type is itself an indexed inductive type:
-- A is a parameter, the two endpoints are indices
-- (the formulation of Martin-Lof: refl a chooses both to be a)
-- ------------------------------------------------------------

data Id (A : Set) : A -> A -> Set where
 refl : (a : A) -> Id A a a

subst : {A : Set} -> (C : A -> Set) -> {a b : A} -> Id A a b -> C a -> C b
subst C (refl a) c = c

cong : {A B : Set} -> (f : A -> B) -> {a b : A} -> Id A a b -> Id B (f a) (f b)
cong f (refl a) = refl (f a)

-- the general eliminator: the motive sees both endpoints AND the proof
J : {A : Set} -> (C : (x y : A) -> Id A x y -> Set) ->
    ((x : A) -> C x x (refl x)) ->
    (a b : A) -> (p : Id A a b) -> C a b p
J C d a a (refl a) = d a

-- ------------------------------------------------------------
-- Where an index forces a transport
-- ------------------------------------------------------------

infixr 5 _++_
_++_ : {A : Set} -> {m n : Nat} -> Vec A m -> Vec A n -> Vec A (m + n)
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

-- zero + n computes to n, but n + zero does not compute:
-- it needs a proof by induction
addZero : (n : Nat) -> Id Nat (n + zero) n
addZero  zero   = refl zero
addZero (suc n) = cong suc (addZero n)

-- so xs ++ [] has type Vec A (n + zero), and we must transport
appendNil : {A : Set} -> {n : Nat} -> Vec A n -> Vec A n
appendNil {A} {n} xs = subst (Vec A) (addZero n) (xs ++ [])

-- ------------------------------------------------------------
-- Well-typed syntax: the type of an expression is an index
-- ------------------------------------------------------------

data Bool : Set where
 true false : Bool

data Typ : Set where
 nat bool : Typ

-- what each object-level type means
El : Typ -> Set
El nat  = Nat
El bool = Bool

data Exp : Typ -> Set where
 lit    : Nat -> Exp nat
 blit   : Bool -> Exp bool
 plus   : Exp nat -> Exp nat -> Exp nat
 isZero : Exp nat -> Exp bool
 ifte   : {a : Typ} -> Exp bool -> Exp a -> Exp a -> Exp a

-- only well-typed expressions can be written down:
--   plus (blit true) (lit zero)   is rejected by the type checker
-- and the two branches of ifte must have the SAME type a

If : {A : Set} -> Bool -> A -> A -> A
If true  x y = x
If false x y = y

-- the evaluator is total, and its RESULT TYPE depends on the index
eval : {a : Typ} -> Exp a -> El a
eval (lit n)        = n
eval (blit b)       = b
eval (plus e1 e2)   = eval e1 + eval e2
eval (isZero e)     = isZeroNat (eval e)
  where isZeroNat : Nat -> Bool
        isZeroNat  zero   = true
        isZeroNat (suc _) = false
eval (ifte b e1 e2) = If (eval b) (eval e1) (eval e2)

-- ============================================================
-- PART 1.  Formulae, contexts, derivations
--
-- The same pattern, one step further: a derivation G |- X is an
-- element of an inductive family indexed by a context G and a
-- formula X.
-- ============================================================
-- Form is the data type of "formulae", built only from atoms and implication
data Form : Set  where
 imply : Form -> Form -> Form
 atom  : Nat -> Form

-- context is the type of list of formulae
-- the terminology "context" comes from the system AUTOMATH
context : Set
context = list Form

-- nicer notation for implication
infixr 10 _=>_
_=>_ : Form -> Form -> Form
X => Y = imply X Y

-- nicer notation for contexts
infixr 10 _,_
_,_ : context -> Form -> context
G , X = cons X G

-- a formulae is in a context
-- this is the same family as Fin above, but indexed by a context:
-- an element of  isIn G X  is a POSITION in the list G holding X
-- (a de Bruijn index that remembers which formula it points at)
data isIn : context -> Form -> Set where
 zero : {X : Form} -> {G : context} ->
             isIn (G , X) X
 suc : {X Y : Form} -> {G : context} ->
             isIn G X ->
             isIn (G , Y) X 

infixr 6 _⊢_

-- defines when a formula is a consequence of a list of hypotheses
--
-- this is the main example of an indexed inductive type in this lecture:
-- G ⊢ X is indexed by BOTH the context G and the formula X, and each
-- constructor chooses its own index
--   var : reads a hypothesis out of the context
--   axK, axS : any instance of the two axiom schemes, in any context
--   mp : the only rule with two premises; the index Y of the premises
--        does NOT appear in the conclusion (it is "cut away")
-- an element of G ⊢ X is a derivation TREE, and induction on it is
-- exactly induction on derivations, as in a proof-theory textbook
data _⊢_ : context -> Form -> Set where
 var : {X : Form} -> {G : context} -> isIn G X -> G ⊢ X
 axK : {X Y : Form} -> {G : context} -> G ⊢ X => (Y => X)
 axS : {X Y Z : Form} -> {G : context} -> G ⊢ (X => (Y => Z)) => ((X => Y) => (X => Z))
 mp : {Y X : Form} -> {G : context} ->
      G ⊢ Y => X ->
      G ⊢ Y ->
      -------------
      G ⊢ X

-- 3 general lemmas used for proving the deduction theorem

dedlem1 : {G : context} -> {X : Form} -> G ⊢ X => X
dedlem1 {G} {X} = mp (mp axS axK) (axK {Y = X => X})

dedlem2 : {G : context} -> {X Y : Form} -> G ⊢ Y -> G ⊢ X => Y
dedlem2 d = mp axK d

dedlem3 : {G : context} -> {X Y : Form} -> isIn (G , X) Y -> G ⊢ X => Y
dedlem3 zero = dedlem1
dedlem3 (suc h) = mp axK (var h)

dedthm : {G : context} -> {X Y : Form} ->
         G , X ⊢ Y ->
         --------------
         G ⊢ X => Y

dedthm (var x) = dedlem3 x
dedthm axK = dedlem2 axK
dedthm axS = dedlem2 axS
dedthm (mp h h1) = mp (mp axS (dedthm h)) (dedthm h1)

dedcor1 : {G : context} -> {X : Form} -> G ⊢ X => X
dedcor1 {G} {X} = dedthm (var zero)

dedcor2 : {G : context} -> {X Y Z : Form} -> G ⊢ (X => (Y => Z)) => (Y => (X => Z))
dedcor2 {G} {X} {Y} {Z} =
 dedthm (dedthm (dedthm (mp (mp (var (suc (suc zero))) (var zero)) (var (suc zero)))))

dedcor3 : {G : context} -> {X Y Z : Form} -> G ⊢ (X => (Y => Z)) => ((X => Y) => X => Z)
dedcor3 {G} {X} {Y} {Z} =
 dedthm (dedthm (dedthm (mp (mp (var (suc (suc zero))) (var zero))
                        (mp (var (suc zero)) (var zero)))))

-- Composition / transitivity of implication, as an object-level theorem.
-- In context  G , (A => B) , (B => C) , A  we prove C by applying
-- (A => B) to A to get B, then (B => C) to B; discharging the three
-- hypotheses with dedthm yields the implication chain.
dedcor4 : {G : context} -> {A B C : Form} -> G ⊢ (A => B) => ((B => C) => (A => C))
dedcor4 {G} {A} {B} {C} =
 dedthm (dedthm (dedthm (mp (var (suc zero)) (mp (var (suc (suc zero))) (var zero)))))

-- The K-like combinator  A => (B => (C => A)).
-- In context  G , A , B , C  the goal A is simply the hypothesis A,
-- sitting two slots back; the three dedthm wrap it in the implications.
dedcor5 : {G : context} -> {A B C : Form} -> G ⊢ A => (B => (C => A))
dedcor5 {G} {A} {B} {C} =
 dedthm (dedthm (dedthm (var (suc (suc zero)))))




-- What is the normal form of decor?


-- ============================================================
-- The Carneiro derivation of the flip combinator.
--
-- This obtains the SAME result as dedcor2, but WITHOUT the
-- deduction theorem: it is point-free, using only mp / axS / axK
-- through a few combinators (the "Carneiro lift").
-- ============================================================

-- K-lift: carry an extra hypothesis R in front of a derived Q.
liftP : {G : context} -> {Q : Form} -> (R : Form) -> G ⊢ Q -> G ⊢ R => Q
liftP R D = mp axK D

-- One-level S: apply under a hypothesis X.
bComb : {G : context} -> {X Y Z : Form} ->
        G ⊢ X => (Y => Z) -> G ⊢ X => Y -> G ⊢ X => Z
bComb D1 D2 = mp (mp axS D1) D2

-- Two-level S: apply under two hypotheses X1 , X2.
bCombTwo : {G : context} -> {X1 X2 Y Z : Form} ->
           G ⊢ X1 => (X2 => (Y => Z)) ->
           G ⊢ X1 => (X2 => Y) ->
           G ⊢ X1 => (X2 => Z)
bCombTwo {X1 = X1} D1 D2 = bComb (bComb (liftP X1 axS) D1) D2

-- Transitivity of implication as a derivation.
impTransD : {G : context} -> {X Y Z : Form} ->
            G ⊢ X => Y -> G ⊢ Y => Z -> G ⊢ X => Z
impTransD pq qr = mp (mp axS (mp axK qr)) pq

-- The flip / C-combinator, derived a la Carneiro (cf. T4/mario.agda).
flipImp : {G : context} -> {X Y Z : Form} ->
          G ⊢ (X => (Y => Z)) => (Y => (X => Z))
flipImp {G} {X} {Y} {Z} =
  let Y' : Form
      Y' = (X => Y) => (X => Z)

      dYZ : G ⊢ Y' => (Y => (X => Z))
      dYZ = bCombTwo {X1 = Y'} {X2 = Y} {Y = X => Y} {Z = X => Z}
              (axK {X = Y'} {Y = Y})
              (liftP Y' (axK {X = Y} {Y = X}))
  in impTransD axS dYZ

-- ============================================================
-- Normal-form comparison of the two flip derivations.
--
-- Both dedcor2 (via the deduction theorem) and flipImp (direct,
-- Carneiro lift) are closed terms of the SAME inductive type _⊢_,
-- so each has a genuine normal form: a finite tree of
-- var / axK / axS / mp.  Computed at X,Y,Z := atom 0,1,2 and G := nil
-- (the structure is independent of these choices):
--
--   * Both reduce to pure axS / axK / mp trees, with NO var -- the
--     hypotheses are fully discharged in each case.
--   * They are NOT the same normal form (not definitionally equal).
--
--   derivation   route                       nodes
--   ----------   -------------------------   -----
--   flipImp      direct (Carneiro lift)         19
--   dedcor2      deduction theorem             161
--
-- The normal form of flipImp (compact: S/K placed by hand exactly
-- where needed) is
--
--   mp (mp axS
--          (mp axK (mp (mp axS (mp (mp axS (mp axK axS)) axK))
--                      (mp axK axK))))
--      axS
--
-- dedcor2 normalises to a 161-node tree of the same vocabulary.
--
-- Why the blow-up: dedthm is a structural recursion that rewrites
-- the WHOLE proof tree --
--   dedthm (mp h h1) = mp (mp axS (dedthm h)) (dedthm h1)
-- replaces every mp by an mp-of-mp-of-axS AND recurses into both
-- subtrees; every leaf axiom becomes mp axK _ (a K-lift); and
-- var zero unfolds to dedlem1 = mp (mp axS axK) axK (5 nodes).
-- dedcor2 nests dedthm THREE times, so this expansion compounds
-- multiplicatively -- hence 161 vs 19.
--
-- This answers "What is the normal form of decor?" above: the
-- deduction theorem is a convenient meta-level tactic, but
-- normalising its output yields a far larger object-level S/K term
-- than a direct derivation of the same theorem.
-- ============================================================


-- ============================================================
-- A second example: the W (contraction) combinator.
--
-- W "diagonalises" a hypothesis:  (X => (X => Y)) => (X => Y),
-- i.e. given a proof of X => X => Y, one copy of X suffices.
-- As with flip, we derive it two ways and compare normal forms.
-- ============================================================

-- Route 1: via the deduction theorem.
-- In context  G , (X => X => Y) , X  we prove Y by feeding the
-- single hypothesis X twice, then discharge X and (X => X => Y).
dedW : {G : context} -> {X Y : Form} -> G ⊢ (X => (X => Y)) => (X => Y)
dedW = dedthm (dedthm (mp (mp (var (suc zero)) (var zero)) (var zero)))

-- Route 2: direct, point-free (Carneiro lift).
-- axS at (X,X,Y) gives  (X=>X=>Y) => (X=>X) => (X=>Y);
-- bComb applies it under the hypothesis (X=>X=>Y) to the lifted
-- identity dedlem1 : X => X, contracting (X=>X) away.
wImp : {G : context} -> {X Y : Form} -> G ⊢ (X => (X => Y)) => (X => Y)
wImp {G} {X} {Y} =
  bComb (axS {X = X} {Y = X} {Z = Y}) (liftP (X => (X => Y)) dedlem1)

-- ============================================================
-- Normal-form comparison (computed at X,Y := atom 0,1, G := nil;
-- the structure is independent of these choices).  As with flip,
-- both are closed terms of _⊢_ and reduce to pure axS/axK/mp
-- trees with NO var, but they are not the same normal form.
--
--   derivation   route                       nodes
--   ----------   -------------------------   -----
--   wImp         direct (Carneiro lift)         11
--   dedW         deduction theorem              59
--
-- Normal form of wImp (compact: one S to split the application,
-- one K-lift of the identity dedlem1):
--
--   mp (mp axS axS) (mp axK (mp (mp axS axK) axK))
--
-- Normal form of dedW (59 nodes):
--
--   mp (mp axS
--          (mp (mp axS (mp axK axS))
--              (mp (mp axS
--                      (mp (mp axS (mp axK axS))
--                          (mp (mp axS (mp axK axK)) (mp (mp axS axK) axK))))
--                  (mp (mp axS (mp (mp axS (mp axK axS)) (mp axK axK)))
--                      (mp axK axK)))))
--      (mp (mp axS (mp (mp axS (mp axK axS)) (mp axK axK))) (mp axK axK))
--
-- Same moral as flip, and same cause: dedW nests dedthm twice, and
-- each nesting rewrites the whole proof tree (every mp becomes an
-- mp-of-mp-of-axS and recurses into both subtrees; every leaf axiom
-- becomes a K-lift; var zero unfolds to dedlem1 = mp (mp axS axK) axK,
-- 5 nodes).  Hence 59 via the theorem vs 11 placing S/K by hand.
-- (Flip needed three dedthm nestings -> 161 vs 19; W needs two,
-- a milder but identical blow-up.)
-- ============================================================


-- ============================================================
-- A third example: composition / transitivity of implication.
--   (A => B) => ((B => C) => (A => C))
-- The deduction-theorem route is dedcor4 above; here is the
-- direct, point-free derivation (Carneiro lift).
-- ============================================================

-- The natural B-combinator  (B => C) => ((A => B) => (A => C)) is
-- axS specialised at X := A, fed a K-lifted hypothesis: axK gives
--   (B=>C) => (A => (B=>C))
-- which impTransD chains into
--   axS : (A => (B=>C)) => ((A=>B) => (A=>C)).
-- compImp then just flips the first two arguments with flipImp.
compImp : {G : context} -> {A B C : Form} -> G ⊢ (A => B) => ((B => C) => (A => C))
compImp {G} {A} {B} {C} =
  mp (flipImp {X = B => C} {Y = A => B} {Z = A => C})
     (impTransD (axK {X = B => C} {Y = A}) (axS {X = A} {Y = B} {Z = C}))

-- Normal-form comparison (computed at A,B,C := atom 0,1,2, G := nil;
-- the structure is independent of these choices).  Both are closed
-- terms of _⊢_ reducing to pure axS/axK/mp trees with NO var.
--
--   derivation   route                       nodes
--   ----------   -------------------------   -----
--   compImp      direct (Carneiro lift)         27
--   dedcor4      deduction theorem             161
--
-- Normal form of compImp: the 19-node flip core (flipImp) applied to
-- a 7-node composition (impTransD axK axS), i.e. mp <flip> <comp>:
--
--   mp (mp (mp axS (mp axK (mp (mp axS (mp (mp axS (mp axK axS)) axK))
--                              (mp axK axK)))) axS)
--      (mp (mp axS (mp axK axS)) axK)
--
-- dedcor4 nests dedthm THREE times (like flip), so its output
-- normalises to a 161-node tree -- the very same size as dedcor2.
-- The per-mp expansion of the deduction theorem (every mp becomes
-- mp-of-mp-of-axS and recurses into both subtrees; every leaf axiom
-- becomes a K-lift) compounds multiplicatively over the three
-- nestings, hence 161 vs 27.
-- ============================================================


-- ============================================================
-- A fourth example: the nested-K (constant) combinator.
--   A => (B => (C => A))
-- The deduction-theorem route is dedcor5 above; here is the
-- direct, point-free derivation (Carneiro lift).
-- ============================================================

-- Two K's chained:  axK : A => (C => A)  is composed (impTransD)
-- with  axK : (C => A) => (B => (C => A)).
constImp : {G : context} -> {A B C : Form} -> G ⊢ A => (B => (C => A))
constImp {G} {A} {B} {C} =
  impTransD (axK {X = A} {Y = C}) (axK {X = C => A} {Y = B})

-- Normal-form comparison (A,B,C := atom 0,1,2, G := nil).
--
--   derivation   route                       nodes
--   ----------   -------------------------   -----
--   constImp     direct (Carneiro lift)          7
--   dedcor5      deduction theorem              29
--
-- Normal form of constImp (impTransD of two axK):
--
--   mp (mp axS (mp axK axK)) axK
--
-- Normal form of dedcor5 (29 nodes):
--
--   mp (mp axS (mp (mp axS (mp axK axS))
--                  (mp (mp axS (mp axK axK)) (mp axK axK))))
--      (mp (mp axS (mp axK axK)) (mp (mp axS axK) axK))
--
-- Same moral once more.  Here the meta-proof is maximally trivial --
-- "A is the hypothesis sitting two slots back" -- yet three dedthm
-- nestings still rewrite it into a 29-node S/K term, versus 7 nodes
-- placing the two K's by hand.  The deduction theorem trades brevity
-- of the meta-proof for size of the object-proof.
-- ============================================================


-- ============================================================
-- A fifth example: the "apply" combinator (modus ponens as a
-- formula).
--   A => ((A => B) => B)
-- Given A and a proof of A => B, modus ponens yields B; this
-- internalises that as an object-level theorem.
-- ============================================================

-- Deduction-theorem route.  In context  G , A , (A => B)  we prove
-- B by applying (A => B) to A, then discharge both hypotheses.
dedcor6 : {G : context} -> {A B : Form} -> G ⊢ A => ((A => B) => B)
dedcor6 {G} {A} {B} = dedthm (dedthm (mp (var zero) (var (suc zero))))

-- Direct route (Carneiro lift).  apply is just flip of the identity:
-- dedlem1 : (A=>B) => (A=>B)  is  (A=>B) => (A => B), and flipImp
-- swaps its first two arguments into  A => ((A=>B) => B).
applyImp : {G : context} -> {A B : Form} -> G ⊢ A => ((A => B) => B)
applyImp {G} {A} {B} = mp (flipImp {X = A => B} {Y = A} {Z = B}) (dedlem1 {X = A => B})

-- Normal-form comparison (A,B := atom 0,1, G := nil).  Both reduce
-- to pure axS/axK/mp trees with NO var.
--
--   derivation   route                       nodes
--   ----------   -------------------------   -----
--   applyImp     direct (Carneiro lift)         25
--   dedcor6      deduction theorem              35
--
-- Normal form of applyImp: the 19-node flip core (flipImp) applied
-- to the 5-node identity dedlem1 = mp (mp axS axK) axK:
--
--   mp (mp (mp axS (mp axK (mp (mp axS (mp (mp axS (mp axK axS)) axK))
--                              (mp axK axK)))) axS)
--      (mp (mp axS axK) axK)
--
-- Normal form of dedcor6 (35 nodes):
--
--   mp (mp axS (mp (mp axS (mp axK axS))
--                  (mp (mp axS (mp (mp axS (mp axK axS)) (mp axK axK)))
--                      (mp axK axK))))
--      (mp (mp axS (mp axK axK)) (mp (mp axS axK) axK))
--
-- This example nests dedthm only TWICE (like W), so the blow-up is
-- mild: 35 vs 25.  The deduction-theorem proof is the most natural
-- one to write -- "apply the hypothesis A => B to A" -- but the
-- direct derivation, reading apply as flip of the identity, is still
-- the smaller object-level term.
-- ============================================================