Substitution lemma

Stream: new members

[Pedro Minicz]

In Typed Lambda Calculi, the first lemma Henk Barendregt proposes is the following:

Proposition 2.1.6 (Substitution lemma). Let $M, N, L \in \Lambda$. Suppose $x \not\equiv y$ and $x \notin FV(L)$. Then

$M[x := N][y := L] = M[y := L][x := N[y := L]]$.

Proof. By induction on the structure of $M$. $\blacksquare$

A while ago I tried to formalize it in Lean, but it felt like it was taking way too much work to formalize a one-line proof. Well, not only once I've proved something just to find a much shorter proof on here or mathlib. Lean magicians know a simple proof for this proposition?

import tactic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

@[simp] def FV : term → set ℕ
| (app M N) := FV M ∪ FV N
| (lam M)   := {x | x + 1 ∈ FV M}
| (var x)   := {x}

instance (x : ℕ) (M : term) : decidable (x ∈ FV M) :=
begin
  induction M with M N ih₁ ih₂ M ih y generalizing x,
  { cases ih₁ x with ih₁ ih₁; cases ih₂ x with ih₂ ih₂,
    { exact is_false (λ h, h.cases_on ih₁ ih₂) },
    all_goals { exact is_true (by exact or.inl ih₁ <|> exact or.inr ih₂) } },
  { exact decidable.cases_on (ih (x + 1)) is_false is_true },
  { exact dite (x = y) is_true is_false }
end

@[simp] def rename_ext (ρ : ℕ → ℕ) : ℕ → ℕ
| 0       := 0
| (x + 1) := ρ x + 1

@[simp] def rename : (ℕ → ℕ) → term → term
| ρ (app M N) := app (rename ρ M) (rename ρ N)
| ρ (lam M)   := lam (rename (rename_ext ρ) M)
| ρ (var x)   := var (ρ x)

abbreviation shift := rename nat.succ

@[simp] def subst_ext (σ : ℕ → term) : ℕ → term
| 0       := var 0
| (x + 1) := shift (σ x)

@[simp] def subst : (ℕ → term) → term → term
| σ (app M N) := app (subst σ M) (subst σ N)
| σ (lam M)   := lam (subst (subst_ext σ) M)
| σ (var x)   := σ x

abbreviation σ (x : ℕ) (L : term) (y : ℕ) : term :=
if x = y then L else var y

-- This changes the precedence of `[`. Let's hope this doesn't become an issue.
notation M `[`:std.prec.max_plus x ` := ` L `]` := subst (σ x L) M

variables {x y : ℕ} {M N L : term}

example (h : x ≠ y) (hx : x ∉ FV L) :
  M[x := N][y := L] = M[y := L][x := N[y := L]] :=
sorry

[Mario Carneiro]

it was taking way too much work to formalize a one-line proof.

Ha! Type theory papers are famous for shuffling these "trivial" proof obligations under the rug. (Including mine!)

[Mario Carneiro]

I should point out though that your formalization differs significantly from Barendregt's

[Mario Carneiro]

Here's a more faithful translation of Barendregt:

-- import tactic.localized
import tactic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (x : ℕ) (M : term) : term
| var (x : ℕ) : term

open term

@[simp] def FV : term → finset ℕ
| (app M N) := FV M ∪ FV N
| (lam x M) := FV M \ {x}
| (var x)   := {x}

@[simp] def subst (x : ℕ) (L : term) : term → term
| (app M N) := app (subst M) (subst N)
| (lam y M) := if x = y then lam y M else lam y (subst M)
| (var y)   := if x = y then L else var y

-- This changes the precedence of `[`. Let's hope this doesn't become an issue.
notation M `[`:std.prec.max_plus x ` := ` L `]` := subst x L M

variables {x y : ℕ} {M N L : term}

theorem subst_none (hx : x ∉ FV M) : M[x := L] = M :=
begin
  induction M generalizing hx; simp [not_or_distrib] at hx; simp *,
  split_ifs; simp, exact M_ih (mt hx h)
end

example (h : x ≠ y) (hx : x ∉ FV L) :
  M[x := N][y := L] = M[y := L][x := N[y := L]] :=
begin
  induction M; simp *,
  { split_ifs; simp *,
    subst M_x, sorry },
  { split_ifs; simp *,
    { subst M, rw subst_none hx, sorry },
    { subst M, rw subst_none hx } }
end

As you can see, the proof is actually a straightforward induction, except for the sorry's

[Mario Carneiro]

and the reason I didn't finish the proof is because it's false!

#eval -- ff
  let x := 0, y := 1, z := 2,
      L := var z, N := var y, M := lam y (var x) in
  to_bool (∀ (h : x ≠ y) (hx : x ∉ FV L),
    M[x := N][y := L] = M[y := L][x := N[y := L]])

[Mario Carneiro]

@Simon Hudon I was hoping I could use slim_check out of the box for this but it seems like I have to write a testable instance for term. Are there any plans for @[derive testable]?

[Simon Hudon]

What you need is an instance of sampleable. I'd like to generate it

[Simon Hudon]

I've been considering doing some of what QuickChick does in Coq and creating generators for inductive relations too. It needs some thought

[Mario Carneiro]

For inductive relations, you can mostly get by using decidable

[Mario Carneiro]

It seems like Barendregt has some line about a "so-called variable convention" (his words) that may allow him to get out of this error, but I don't really understand what his intent is

[Reid Barton]

wow it's really called QuickChick

[Pedro Minicz]

Mario Carneiro said:

and the reason I didn't finish the proof is because it's false!

#eval -- ff
  let x := 0, y := 1, z := 2,
      L := var z, N := var y, M := lam y (var x) in
  to_bool (∀ (h : x ≠ y) (hx : x ∉ FV L),
    M[x := N][y := L] = M[y := L][x := N[y := L]])

Yes, it is false because you have to consider terms up to alpha equivalence.

[Pedro Minicz]

That is reason for using De Bruijn indices. But it may have made the proofs harder.

[Pedro Minicz]

There doesn't seem to be a straight forward way of defining alpha equivalence. The simplest thing I can think of is $M \equiv N$ if there is a bijective renaming $\rho : \mathbb{N} \to \mathbb{N}$ such that $rename \, \rho \, M = N$.

[Pedro Minicz]

@[simp] def rename (ρ : ℕ → ℕ) : term → term
| (app M N) := app (rename M) (rename N)
| (lam x M) := lam (ρ x) (rename M)
| (var x)   := var (ρ x)

@[simp] def α (M N : term) : Prop := ∃ ρ, function.bijective ρ ∧ rename ρ M = N

This seems correct. I may to make this relation into a setoid tomorrow if I have time.

[Mario Carneiro]

That doesn't actually solve the problem, as there is no guard in the case (lam y P)[x := N] == lam y (P [x := N]), provided x != y that prevents occurences of y in N from being captured. It simply makes the equation fail to hold sometimes

[Mario Carneiro]

If you want to use de bruijn indices, I would suggest using a book that deals with terms that way, as the proofs of all the basic properties is very different

[Mario Carneiro]

Here's the way I would suggest setting up de bruijn terms:

import tactic

@[derive decidable_eq]
inductive term : Type
| app (M N : term) : term
| lam (M : term) : term
| var (x : ℕ) : term

open term

@[simp] def shiftn : ℕ → term → term
| k (app M N) := app (shiftn k M) (shiftn k N)
| k (lam M)   := lam (shiftn (k+1) M)
| k (var x)   := if x < k then var x else var (x + 1)

abbreviation shift := shiftn 0

@[simp] def substn : ℕ → term → term → term
| k L (app M N) := app (substn k L M) (substn k L N)
| k L (lam M)   := lam (substn (k+1) (shift L) M)
| k L (var x)   := if x < k then var x else if x = k then L else var (x - 1)

abbreviation subst := substn 0

notation M `[0` ` := ` L `]` := subst L M

You can't really state Barendregt's theorem with this version though, as subst has to be used in restricted ways, basically only the operations that are needed to define beta reduction and typing

[Mario Carneiro]

your definition of alpha equivalence is not correct, as it fails to prove lam x (lam x (var x)) =ₐ lam x (lam y (var y))

[Mario Carneiro]

There is an elegant inductive definition using a context:

inductive alpha : list (ℕ × ℕ) → term → term → Prop
| app {Γ M M' N N'} : alpha Γ M M' → alpha Γ N N' → alpha Γ (app M N) (app M' N')
| lam {Γ x x' M M'} : alpha ((x, x') :: Γ) M M' → alpha Γ (lam x M) (lam x' M')
| var {Γ x x'} : (x, x') ∈ Γ → alpha Γ (var x) (var x')

but unfortunately it also fails in the case of shadowed variables

[Mario Carneiro]

You can define it by closing the relation lam x (M [x := y]) =ₐ lam y M under the term formers and refl/symm/trans, but this requires a previous definition of substitution (you can get around the BV capture problem here by just not having the result be defined, since it's only one case in the inductive relation)

[Simon Hudon]

On the subject of inductive relations @Mario Carneiro, I've been considering creating generators for Lean's expr type and in that situation, generating type correct terms is useful but most terms that you'll generate will not by type correct. I'd like to formalize the Lean typing relation (or a subset thereof) so that we could use slim_check to test tactics in a useful way. Is this something you've thought about?

[Mario Carneiro]

can't you use type_check if you want to test the result of a tactic?

[Mario Carneiro]

reimplementing lean in lean would be a huge project and the result wouldn't be particularly fast

[Simon Hudon]

type_check would be the right thing to do if you want to use type correctness as a guard. What I want to do is a generator that creates type correct expression. I don't want to evaluate a decision procedure about type correctness. I want to use the relation guide the construction of examples