Chuangjie Xu, December 2016

We present a few simple examples and compare the terms extracted from
different proofs of a theorem.

\begin{code}

module Examples where

open import Preliminaries
open import DataTypes
open import H
open import Dialectica
open import Simp

\end{code}

We firstly prove a very simple theorem

  if n is standard, then so is n+1.

And then we extract an Agda term from the proof.

\begin{code}

Lmᴴ[st-succ] : {Γ : Cxt} {Ξ : Asmpt Γ}
             → Prf Ξ (∀ˢᵗ (st (Succ ν₀))) -- ∀ˢᵗn st(n+1)
Lmᴴ[st-succ] = ∀ˢᵗ-I (∀-intro (⇒-intro (st-succ κ₀)))

Φ₀ : Fml ε
Φ₀ = ∀ˢᵗ (st (Succ ν₀)) -- ∀ˢᵗn st(n+1)

Ex₀ : Prf ε Φ₀
Ex₀ = Lmᴴ[st-succ]

t₀ : List (ℕ → List ℕ)
t₀ = extract Ex₀

-- t₀ contains exactly one realiser - r₀
length-of-t₀ : length t₀ ≡ 
length-of-t₀ = refl

r₀ : ℕ → List ℕ
r₀ = head t₀ (≤-succ ≤-zero)

normal-form-of-r₀ : r₀ ≡ (λ x → ε ₊ succ x)
normal-form-of-r₀ = refl

\end{code}

We prove that

  any natural number which is smaller than or equal to a standard one is standard.

Then we extract its realiser (an Agda term), simplify it and have a few tests.

Ther realiser is a function computing a list of natural numbers that
are smaller than or equal to n for any given natural number n.

\begin{code}

Lmᴴ[st-≤] : {Γ : Cxt} {Ξ : Asmpt Γ}
          → Prf Ξ (∀ˢᵗ (∀ᴴ (ν₀ ≤ᴴ ν₁ ⇒ᴴ st ν₀))) -- ∀ˢᵗn ∀m (m ≤ n ⇒ st m)
Lmᴴ[st-≤] = IRˢᵗ base step
         -- Proved using external induction on n
 where
  base : Prf _ (∀ᴴ (ν₀ ≤ᴴ Zero ⇒ᴴ st ν₀))
  base = ∀-intro (⇒-intro (st-eq (st-cl Zero) (Sym (Lmᴴ[n≤0→n=0] κ₀))))
  step : Prf _ (∀ˢᵗ (∀ᴴ (ν₀ ≤ᴴ ν₁ ⇒ᴴ st ν₀) ⇒ᴴ (∀ᴴ (ν₀ ≤ᴴ Succ ν₁ ⇒ᴴ st ν₀))))
  step = ∀ˢᵗ-I (∀-intro (⇒-intro (⇒-intro (∀-intro (⇒-intro (∨-elim cL cR (Lmᴴ[≤-Succ-∨] κ₀)))))))
   where
    cL : Prf _ (ν₀ =ᴴ Succ ν₁ ⇒ᴴ st ν₀)
    cL = ⇒-intro (st-eq (st-succ κ₃) (Sym κ₀))
    cR : Prf _ (ν₀ ≤ᴴ ν₁ ⇒ᴴ st ν₀)
    cR = ⇒-intro (⇒-elim (∀-elim κ₂ ν₀) κ₀)

Φ₁ : Fml ε
Φ₁ = ∀ˢᵗ (∀ᴴ (ν₀ ≤ᴴ ν₁ ⇒ᴴ st ν₀))

Ex₁ : Prf ε Φ₁
Ex₁ = Lmᴴ[st-≤]

t₁ : List (ℕ → List ((List 𝟙 → List ℕ) × (List 𝟙 → 𝟙 → List 𝟙)))
t₁ = extract Ex₁

length-of-t₁ : length t₁ ≡ 
length-of-t₁ = refl

r₁ : ℕ → List ((List 𝟙 → List ℕ) × (List 𝟙 → 𝟙 → List 𝟙))
r₁ = head t₁ (≤-succ ≤-zero)

-- r₁ obviously contains too much useless information because of the
-- noncomputational part of the proof.  So we simplify it to sr₁.

sr₁ : ℕ → List (List ℕ)
sr₁ = simpᴹ _ r₁

-- The normal form of sr₁ (or r₁) is too complicated.  But, as
-- expected, it is defined using recursors rec and recᴸ.
-- One can let Agda to compute its normal form by pressing
--
--                 " Ctrl-c Ctrl-n "
--
-- and then entering " sr₁ " (or " r₁ ").

-- We here only test it with a few (small) inputs:

sr₁[0] : sr₁  ≡ ⟨ ε ₊  ⟩ -- a list containing a list containing 0
sr₁[0] = refl

sr₁[7] : sr₁  ≡ ⟨ ε ₊  ₊  ₊  ₊  ₊  ₊  ₊  ₊  ⟩
sr₁[7] = refl

sr₁[12] : sr₁  ≡ ⟨ ε ₊  ₊  ₊  ₊  ₊  ₊  ₊  ₊  ₊  ₊  ₊  ₊  ₊  ⟩
sr₁[12] = refl

-- For more tests, one can again use Agda to normalise " sr₁ X " for any numeral X.

\end{code}

We extract terms from some (simple) internal proofs.

\begin{code}

Ex₂ : {Γ : Cxt} {Ξ : Asmpt Γ}
    → Prf Ξ (∀ᴴ (∃ᴴ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀))) -- ∀n ∃m (m≤n ∧ even m)
Ex₂ = ∀-intro (∃-intro Zero (∧-intro ≤-Zero EvenZ)) -- choose m=0.

t₂ : List (𝟙 × 𝟙)
t₂ = extract (Ex₂ {ε} {ε})

normal-form-of-t₂ : t₂ ≡ ⟨ (⋆ , ⋆) ⟩
normal-form-of-t₂ = refl


Ex₂' : {Γ : Cxt} {Ξ : Asmpt Γ}
     → Prf Ξ (∀ᴴ (∃ᴴ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀)))    -- ∀n ∃m (m≤n ∧ even m)
Ex₂' = IR (int-∃ (int-∧ int-≤ int-E))           -- use internal induction
          (∃-intro Zero (∧-intro ≤-Zero EvenZ)) -- base case: choose m=0
          (∀-intro (⇒-intro (∃-intro Zero (∧-intro ≤-Zero EvenZ)))) -- inductive step: choose m=0

t₂' : List (𝟙 × 𝟙)
t₂' = extract (Ex₂' {ε} {ε})

normal-form-of-t₂' : t₂' ≡ ⟨ (⋆ , ⋆) ⟩
normal-form-of-t₂' = refl

-- Both t₂ and t₂' are ⟨ (⋆ , ⋆) ⟩
-- Internal proofs have no computational contents, no matter how they are constructed.

\end{code}

We prove the corresponding external theorem using Lmᴴ[st-≤], extract a
term, and then compare it to those extracted from direct proofs.

\begin{code}

--
-- Direct proof 1
--
Ex₃ : {Γ : Cxt} {Ξ : Asmpt Γ}
    → Prf Ξ (∀ˢᵗ (∃ˢᵗ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀))) -- ∀ˢᵗn ∃ˢᵗm (m≤n ∧ even m)
Ex₃ = ∀ˢᵗ-I (∀-intro (⇒-intro (∃ˢᵗ-I (∃-intro Zero (∧-intro (st-cl Zero) (∧-intro ≤-Zero EvenZ))))))
   -- choose m=0 and st(0)

t₃ : List (ℕ → List ℕ)
t₃ = simpExtract Ex₃

length-of-t₃ : length t₃ ≡ 
length-of-t₃ = refl

r₃ : ℕ → List ℕ
r₃ = head t₃ (≤-succ ≤-zero)

normal-form-of-r₃ : r₃ ≡ (λ _ → ⟨  ⟩)
normal-form-of-r₃ = refl

--
-- Direct proof 2
--
Ex₃' : {Γ : Cxt} {Ξ : Asmpt Γ}
     → Prf Ξ (∀ˢᵗ (∃ˢᵗ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀))) -- ∀ˢᵗn ∃ˢᵗm (m≤n ∧ even m)
                                               -- use external induction
Ex₃' = IRˢᵗ (∃ˢᵗ-I (∃-intro Zero (∧-intro (st-cl Zero) (∧-intro ≤-Zero EvenZ))))
            -- base case: choose m=0 and st(0)
            (∀ˢᵗ-I (∀-intro (⇒-intro (⇒-intro (∃ˢᵗ-I (∃-intro Zero (∧-intro (st-cl Zero) (∧-intro ≤-Zero EvenZ))))))))
            -- inductive step: choose m=0 and st(0)

t₃' : List (ℕ → List ℕ)
t₃' = simpExtract Ex₃'

length-of-t₃' : length t₃' ≡ 
length-of-t₃' = refl

r₃' : ℕ → List ℕ
r₃' = head t₃' (≤-succ ≤-zero)

-- Agda spends a long time to type-check the following.
--
--   normal-form-of-r₃' : r₃' ≡ (λ n → recᴸ ε (λ w ys → ys ₊ pr₁ w) (rec (ε ₊ (0 , ⋆)) (λ _ _ → ε ₊ (0 , ⋆)) n))
--   normal-form-of-r₃' = refl
--
-- The realiser r₃' of Ex₃' is defined using rec and recᴸ.

-- We can prove that it is constant with value ⟨ 0 ⟩.
r₃'[n]=⟨0⟩ : (n : ℕ) → r₃' n ≡ ⟨  ⟩
r₃'[n]=⟨0⟩         = refl
r₃'[n]=⟨0⟩ (succ n) = refl


--
-- Proof using the internal proof Ex₂ and the lemma Lmᴴ[st-≤]
--
Ex₃'' : {Γ : Cxt} {Ξ : Asmpt Γ}
      → Prf Ξ (∀ˢᵗ (∃ˢᵗ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀))) -- ∀ˢᵗn ∃ˢᵗm (m≤n ∧ even m)
Ex₃'' {Γ} {Ξ} = ∀ˢᵗ-I (∀-intro (⇒-intro goal))
 where
  claim₀ : Prf (wknᵃ (wknᵃ Ξ) ₊ st ν₁ ₊ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀)) (st ν₀)
  claim₀ = ⇒-elim (∀-elim (⇒-elim (∀-elim (∀ˢᵗ-E Lmᴴ[st-≤]) ν₁) κ₁) ν₀) (∧-elim₁ κ₀)
                                                -----------
  claim₁ : Prf (wknᵃ Ξ ₊ st ν₀) (∀ᴴ ((ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀) ⇒ᴴ ∃ˢᵗ (ν₀ ≤ᴴ ν₂ ∧ᴴ Even ν₀)))
  claim₁ = ∀-intro (⇒-intro (∃ˢᵗ-I (∃-intro ν₀ (∧-intro claim₀ κ₀))))
  claim₂ : Prf (wknᵃ Ξ ₊ st ν₀) (∃ᴴ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀) ⇒ᴴ ∃ˢᵗ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀))
  claim₂ = ∃-elim claim₁
  claim₃ : Prf (wknᵃ Ξ ₊ st ν₀) (∃ᴴ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀))
  claim₃ = ∀-elim Ex₂ ν₀
                 -----
  goal   : Prf (wknᵃ Ξ ₊ st ν₀) (∃ˢᵗ (ν₀ ≤ᴴ ν₁ ∧ᴴ Even ν₀))
  goal   = ⇒-elim claim₂ claim₃

t₃'' : List (ℕ → List ℕ)
t₃'' = simpExtract Ex₃''

length-of-t₃'' : length t₃'' ≡ 
length-of-t₃'' = refl

r₃'' : ℕ → List ℕ
r₃'' = head t₃'' (≤-succ ≤-zero)

-- The normal form of r₃'' is too complicated, since it is defined
-- using r₁ (the realiser of Lmᴴ[st-≤]).  So we directly test it and
-- compare the result with r₃ and r₃':

r₃''[0] : r₃''  ≡ ⟨  ⟩
r₃''[0] = refl

r₃[0]   :   r₃  ≡ ⟨  ⟩
r₃[0]   = refl

r₃'[0]  :  r₃'  ≡ ⟨  ⟩
r₃'[0]  = refl

-- 1 is not even and hence cannot be a realiser of "∃ˢᵗm (m≤2 ∧ even m)".
r₃''[2] : r₃''  ≡ ε ₊  ₊  ₊ 
                         -----
r₃''[2] = refl

r₃[2]   :   r₃  ≡ ⟨  ⟩
r₃[2]   = refl

r₃'[2]  :  r₃'  ≡ ⟨  ⟩
r₃'[2]  = refl

\end{code}

Therefore, to have simpler and more precise realisers, it seems better
to have a direct external proof (e.g. using external induction) rather
than using the lemma Lmᴴ[st-≤].