Zulip Chat Archive

Stream: new members

Topic: Substitution lemma


view this post on Zulip 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ΛM, N, L \in \Lambda. Suppose x≢yx \not\equiv y and xFV(L)x \notin FV(L). Then

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

Proof. By induction on the structure of MM. \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

view this post on Zulip 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!)

view this post on Zulip Mario Carneiro (Oct 01 2020 at 00:21):

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

view this post on Zulip 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

view this post on Zulip 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]])

view this post on Zulip 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]?

view this post on Zulip Simon Hudon (Oct 01 2020 at 01:01):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 01 2020 at 01:07):

For inductive relations, you can mostly get by using decidable

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 01 2020 at 01:45):

wow it's really called QuickChick :coq:

view this post on Zulip 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.

view this post on Zulip Pedro Minicz (Oct 01 2020 at 02:17):

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

view this post on Zulip 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 MNM \equiv N if there is a bijective renaming ρ:NN\rho : \mathbb{N} \to \mathbb{N} such that renameρM=Nrename \, \rho \, M = N.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 03 2020 at 17:36):

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

view this post on Zulip 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

view this post on Zulip 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