induction over-generalizing

Stream: general

[zbatt]

I'm trying to implement the basics of simply typed lambda calculus and I have an inductive type given as

inductive has_type : Context -> Term -> Typ -> Prop
| t_Var : ∀ (Γ : Context) (x : var) (τ : Typ), Dict.get Γ x = some τ -> has_type Γ (tm_Var x) τ
| t_Lam : ∀ (Γ : Context) (x : var) (τ₁ τ₂ : Typ) (t₁ : Term),
    has_type (Dict.add Γ x τ₁) t₁ τ₂ -> has_type Γ (tm_Lam x τ₁ t₁) (typ_Lam τ₁ τ₂)
| t_Ap : ∀ Γ τ₁ τ₂ e₁ e₂, has_type Γ e₁ (typ_Lam τ₁ τ₂) -> has_type Γ e₂ τ₁ -> has_type Γ (tm_Ap e₁ e₂) τ₂
| t_Unit : ∀ Γ, has_type Γ tm_Unit typ_Unit
| t_Nat : ∀ Γ n, has_type Γ (tm_Nat n) typ_Nat

based roughly off of https://softwarefoundations.cis.upenn.edu/plf-current/Stlc.html

With that in mind, I'm having a bit of trouble with induction. For example, I'm trying to prove that every term has a unique type with the followin theorem

theorem unique_type {Γ : Context} {τ₁ τ₂ : Typ} (e : Term) (h1 : has_type Γ e τ₁) (h2 : has_type Γ e τ₂) : τ₁ = τ₂

However, when I start with induction h1, it generalizes the Γ term into a h_Γ. It's important that the context is the same throughout the proofs, but I'm not sure how to fix this. Thank you so much for your help!

[Eric Wieser]

My reading is that the context can't be the same thoughout the proof though because t_Lam changes it; am I missing something?

[Eric Wieser]

My reading is that the context can't be the same thoughout the proof though because t_Lam changes it; am I missing something?

[zbatt]

It does, but for certain theorems it was important that the inductive step not generalize it from the outset (I believe). For example in trying to prove progress its important that when inducting over the typing judgement, the context stay empty. I got it to work using advice from @Wojciech Nawrocki via

theorem progress (e : Term) (τ : Typ) (h : has_type ctx_Empty e τ) : value e ∨ ∃ e', e ↦ e' :=
begin
  generalize_hyp hΓ : ctx_Empty = Γ at h,

Admittedly I'm pretty new to both programming language theory and Lean so I might be missing something obvious.

[Floris van Doorn]

The trick in the last code snippet is indeed useful if you want to do induction when the context (or the term or type) are not variables. You can also try induction' (available with import tactic.induction from mathlib), which will (hopefully) do this automatically for you.

On your earlier question: you clearly cannot have the context the same in all induction steps. However, induction h1 generalizing h2 is probably good enough: it will also replace the Γ by h_Γ in h2.

[Jannis Limperg]

zbatt said:

It does, but for certain theorems it was important that the inductive step not generalize it from the outset (I believe). For example in trying to prove progress its important that when inducting over the typing judgement, the context stay empty.

This sounds fishy to me. Over-generalisation should never be harmful; you can always recover the specialised induction hypothesis by applying the generalised one. Under-generalisation, on the other hand, where certain expressions remain fixed but should be variable, is a very common source of trouble. This is why induction' generalises everything by default; if you have an example where this is harmful, I'm very interested.

[Kevin Buzzard]

yeah mathematically there's never anything wrong with over-generalizing, but I can't comment on applications to CS/type theory.

[Mario Carneiro]

it is syntactically annoying since you have to pass a ton of arguments to the IH when you apply it

[Mario Carneiro]

Also, you can't generalize everything; the indices and parameters of the inductive type can't be generalized, as well as their dependencies

[Kevin Buzzard]

Mario Carneiro said:

it is syntactically annoying since you have to pass a ton of arguments to the IH when you apply it

I heard the apply bug was fixed in Lean 4 though :-)

[Mario Carneiro]

indeed it was, just yesterday

[Jannis Limperg]

Mario Carneiro said:

Also, you can't generalize everything; the indices and parameters of the inductive type can't be generalized, as well as their dependencies

Sure, induction' generalises everything that can be generalised. The syntactic overhead can indeed get annoying, but at least for teaching, we thought this was a better default than having people run into the under-generalisation issue all the time.

[Kevin Buzzard]

In NNG you essentially never need to over-generalise and people think they're getting good at the game, and then there's one level in advanced multiplication world where you do and loads of people get stuck there.

[Kevin Buzzard]

https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=9&level=4 In the end I just put in a big explainer about the phenomenon.

[Michael Stoll]

IIRC, I had a solution for that level without generalizing. :smile: