Stream: new members

Topic: Substitution lemma

Pedro Minicz (Sep 30 2020 at 23:58):

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 (Oct 01 2020 at 00:00):

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 (Oct 01 2020 at 00:21):

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

Mario Carneiro (Oct 01 2020 at 00:54):

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 (Oct 01 2020 at 00:54):

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 (Oct 01 2020 at 00:57):

@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 (Oct 01 2020 at 01:01):

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

Simon Hudon (Oct 01 2020 at 01:02):

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 (Oct 01 2020 at 01:07):

For inductive relations, you can mostly get by using decidable

Mario Carneiro (Oct 01 2020 at 01:09):

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 (Oct 01 2020 at 01:45):

wow it's really called QuickChick

Pedro Minicz (Oct 01 2020 at 02:16):

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 (Oct 01 2020 at 02:17):

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

Pedro Minicz (Oct 01 2020 at 02:21):

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 (Oct 01 2020 at 02:24):

@[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 (Oct 01 2020 at 02:33):

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 (Oct 01 2020 at 02:34):

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 (Oct 01 2020 at 02:49):

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 (Oct 01 2020 at 03:04):

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 (Oct 01 2020 at 03:06):

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 (Oct 01 2020 at 03:11):

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 (Oct 03 2020 at 16:35):

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 (Oct 03 2020 at 17:36):

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

Mario Carneiro (Oct 03 2020 at 17:38):

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

Simon Hudon (Oct 03 2020 at 18:11):

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

Last updated: May 15 2021 at 00:39 UTC