equivalent definitions of substitution in lambda calculus

Stream: new members

[Patrick Thomas]

Are these two examples provable? I'm struggling with the first, and now I'm not certain if it actually holds.

import tactic

def var := ℕ

inductive term : Type
| var : var → term
| app : term → term → term
-- term.abs y P = λ y . P
| abs : var → term → term


def FV : term → set var
| (term.var x) := {x}
| (term.app P Q) := (FV P) ∪ (FV Q)
| (term.abs x P) := (FV P) \ {x}


-- sub_is_def M x N means M [ x := N ] is defined
inductive sub_is_def : term → var → term → Prop

-- y [ x := N ] is defined
| var (y : var) (x : var) (N : term) :
  sub_is_def (term.var y) x N

-- P [ x := N ] is defined → Q [ x := N ] is defined → (P Q) [ x := N ] is defined
| app (P : term) (Q : term) (x : var) (N : term) :
  sub_is_def P x N → sub_is_def Q x N → sub_is_def (term.app P Q) x N

-- x = y → ( λ y . P ) [ x := N ] is defined
| abs_same (y : var) (P : term) (x : var) (N : term) :
  x = y → sub_is_def (term.abs y P) x N

-- x ≠ y → x ∉ FV ( λ y . P ) → ( λ y . P ) [ x := N ] is defined
| abs_diff_nel (y : var) (P : term) (x : var) (N : term) :
  x ≠ y → x ∉ FV (term.abs y P) → sub_is_def (term.abs y P) x N

-- x ≠ y → y ∉ FV ( N ) → P [ x := N ] is defined → ( λ y . P ) [ x := N ] is defined
| abs_diff (y : var) (P : term) (x : var) (N : term) :
  x ≠ y → y ∉ FV N → sub_is_def P x N → sub_is_def (term.abs y P) x N

notation M `[` x `:=` N `]` `is_def` := sub_is_def M x N


-- M [ x := N ]
def sub : term → var → term → term
-- if x = y then y [ x := N ] = N else y [ x := N ] = y
| (term.var y) x N := if x = y then N else term.var y

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| (term.app P Q) x N := term.app (sub P x N) (sub Q x N)

-- if x = y then ( λ y . P ) [ x := N ] = ( λ y . P ) else ( λ y . P ) [ x := N ] = ( λ y . P [ x := N ] )
| (term.abs y P) x N := if x = y then term.abs y P else term.abs y (sub P x N)

notation M `[` x `:=` N `]` := sub M x N


-- is_sub M x N L means M [ x := N ] = L
inductive is_sub : term → var → term → term → Prop

-- if x = y then y [ x := N ] = N
| var_same (y : var) (x : var) (N : term) :
  x = y → is_sub (term.var y) x N N

-- if x ≠ y then y [ x := N ] = y
| var_diff (y : var) (x : var) (N : term) :
  x ≠ y → is_sub (term.var y) x N (term.var y)

-- (P Q) [ x := N ] = (P [ x := N ] Q [ x := N ])
| app (P : term) (Q : term) (x : var) (N : term) (P' : term) (Q' : term) :
  is_sub P x N P' → is_sub Q x N Q' → is_sub (term.app P Q) x N (term.app P' Q')

-- if x = y then ( λ y . P ) [ x := N ] = ( λ y . P )
| abs_same (y : var) (P : term) (x : var) (N : term) :
  x = y → is_sub (term.abs y P) x N (term.abs y P)

-- if x ≠ y then ( λ y . P ) [ x := N ] = ( λ y . P [ x := N ] )

| abs_diff_nel (y : var) (P : term) (x : var) (N : term) (P' : term) :
  x ≠ y → x ∉ FV (term.abs y P) → is_sub P x N P' → is_sub (term.abs y P) x N (term.abs y P')

| abs_diff (y : var) (P : term) (x : var) (N : term) (P' : term) :
  x ≠ y → y ∉ FV N → is_sub P x N P' → is_sub (term.abs y P) x N (term.abs y P')


example (M : term) (x : var) (N : term) (L : term)
(H1 : is_sub M x N L) : M [ x := N ] is_def := sorry

example (M : term) (x : var) (N : term) (L : term)
(H1 : is_sub M x N L) : M [ x := N ] = L := sorry

[Reid Barton]

The first one is just induction on the is_sub value

example (M : term) (x : var) (N : term) (L : term)
(H1 : is_sub M x N L) : M [ x := N ] is_def := begin
  induction H1,
  apply sub_is_def.var,
  apply sub_is_def.var,
  apply sub_is_def.app; assumption,
  apply sub_is_def.abs_same; assumption,
  apply sub_is_def.abs_diff_nel; assumption,
  apply sub_is_def.abs_diff; assumption,
end

[Reid Barton]

because the two inductive propositions have nearly the same structure

[Patrick Thomas]

Huh. I thought I had tried that, but I guess not. Thank you.