Formalising Church numerals in Agda

Beginer here. I'm trying to show that the closed $$\beta$$-nf's of type $$(\iota \to \iota) \to (\iota \to \iota)$$ are the Church numerals ($$\iota$$ the base type, using the simply-typed lambda calculus).

In Hindley's Basic Simple Type Theory, the lemma 8A5 states that every $$\beta$$-nf can be expressed uniquely in the following form (types omitted): $$M \equiv \lambda x_1 . .. x_m \cdot (\nu M_1... M_n)$$ Where $$m \ge 0$$, $$n \ge 0$$, and the type $$\tau$$ of $$M$$ is $$\tau \equiv \tau_1 \to ... \to \tau_m \to \tau^*$$. And each $$M_j$$ is a $$\beta$$-nf, too. And if $$M$$ is closed then $$m \ge 1$$ and $$\nu$$ is one of the $$x_i$$'s.

Now, it is easy to show (informally) that the (long) normal inhabitants of the type $$(\iota \to \iota) \to (\iota \to \iota)$$ are exactly the Church numerals, but I'm struggling to formalise that in Agda.

I follow the common definition of normal terms found in the literature, something like:

mutual
data Nf : Context → Type → Set where
ne  : {Γ : Context} → Ne Γ ι → Nf Γ ι
abs : {Γ : Context} {σ τ : Type} → Nf (Γ ∷ σ) τ → Nf Γ (σ ⇒ τ)

data Ne : Context → Type → Set where
var : {Γ : Context} {σ : Type} → Γ ∋ σ → Ne Γ σ
app : {Γ : Context} {σ τ : Type} → Ne Γ (σ ⇒ τ) → Nf Γ σ → Ne Γ τ


Where the Context is a list of Type's, and we use de Bruijn indices for variables.

I get stuck when I case split on the head of the term (it is a Ne), because app introduces a term of a new type which I don't know how to relate to any of the types in the context. Here's a naive function to clarify what I mean:

naive : Nf ∅ ((ι ⇒ ι) ⇒ (ι ⇒ ι)) → ℕ
naive (abs abs (ne (var Z))) = zero
naive (abs abs (ne (var S S () )))
naive (abs abs (ne (app (var S Z) N))) = suc ? -- This is the case I'm interested in
naive (abs abs (ne (app (app _ _) N))) = ? -- This is what I mean, think it's nonsense


I believe what I'm missing is a proof that if $$M$$ is closed then [...] $$\nu$$ is one of the $$x_i$$'s, so I'm trying to prove that a neutral term of a type not present in the context is not well-defined. Here's one attempt:

neutral-bad : {Γ : Context} {σ : Type} → Ne Γ σ → σ ∉ Γ → ⊥
neutral-bad (var x)   not-there = ? -- Easy
neutral-bad (app r M) not-there = ? -- Stuck again


The proposition σ ∉ Γ above is defined with Data.List.Relation.Unary.Any and negation (maybe not relevant, but would rather make it clear anyway).

Can someone provide advise on how to solve this? or maybe point me to related works? All help is much appreciated!

I think your neutral-bad lemma is too general. For instance:

$$f : τ ⇒ σ, x : τ ⊢ f\ x : σ$$

$$σ$$ does not occur in the context, but there is a neutral term with its type.

However, that is not the situation you're going to end up in. I believe where you'll end up is:

$$s : ι ⇒ ι, z : ι ⊢ F\ X \ Y : ι$$

where $$F$$ must be a neutral term with type $$σ ⇒ τ ⇒ ι$$. But now you can prove there are no neutral terms in that context whose type is of the form $$σ ⇒ τ ⇒ ε$$.

• Right, I thought of defining that lemma on the context restricted to the term, but then I may still find issues because my contexts, being lists, have order. I'll try to use the type's length to show it's not in the context. Thank you!
– lfrg
Apr 18 at 12:46
• I'm not sure what a general version of the lemma you need is. But, I was able to define a version of your $\mathsf{Ne} → ℕ$ myself, and what I wrote was part of my argument. Any neutral function that isn't a reference to the context can only come from the application of a function with a larger type. So if you are larger than any type in the context, that leads to an infinite regress. Apr 18 at 21:54