failed to unfold definition

Stream: new members

[Pedro Minicz]

In the code below, tactic#simp, tactic#unfold and tactic#change fail to unfold the definition of the function fv, despite it being applied to enough arguments. Why is that the case and how can I unfold the definition?

structure language : Type 1 :=
(functions : ℕ → Type)
(relations : ℕ → Type)

def language.constants (L : language) := L.functions 0

variable (L : language)

inductive preterm : ℕ → Type
| var : ℕ → preterm 0
| func {l : ℕ} : L.functions l → preterm l
| app {l : ℕ} : preterm (l + 1) → preterm 0 → preterm l

@[reducible] def term := preterm L 0

namespace term

def fv {L : language} : ∀ {l : ℕ}, preterm L l → set ℕ
| 0 (preterm.var x) := {x}
| l (preterm.func f) := ∅
| l (preterm.app t s) := fv t ∪ fv s

instance (l x : ℕ) (t : preterm L l) : decidable (x ∈ fv t) :=
begin
  induction t with y l' f l' t s ht hs,
  { change decidable (x = y),
    apply_instance },
  { clear l,
    rename l' l,
    refine is_false _,
    intro h,
    --simp [fv] at h,
    --unfold fv at h,
    --change x ∈ ∅ at h,
    sorry },
  { clear l,
    rename l' l,
    --simp [fv],
    --unfold fv,
    --change decidable (x ∈ fv t ∪ fv s),
    sorry }
end

end term

[Kevin Buzzard]

#print prefix term.fv

shows you that Lean has decided to internally implement your fv definition by doing a case split on the natural number l and defining it to be the empty set on both occasions. So you need to make your own simp lemma to fix this up.

[Kevin Buzzard]

If you add

@[simp] lemma fv_func {l : ℕ} (f : L.functions l) : fv (preterm.func f) = ∅ :=
begin
  cases l;
  simp [fv],
end

then simp now works.

Lean's equation compiler does not always do the case splits that one would expect. Sometimes it is more eager, so you have to pick up the pieces by hand afterwards.

[Reid Barton]

Can also just change 0 to _ in the first line of fv.

[Kevin Buzzard]

Nice!

[Pedro Minicz]

Very cool. Thanks!

Why does changing 0 to _ fixes the problem? I find it really weird that it works in the first place, since the following doesn't work:

def fv {L : language} {l : ℕ} : preterm L l → set ℕ
| (preterm.var x) := {x}
| (preterm.func f) := ∅
| (preterm.app t s) := sorry

[Kevin Buzzard]

It fixes the problem because Lean can infer that l=0 in the first case. Edit: Yeah, I guess I see your point though. It's the magic of the equation compiler.

[Reid Barton]

To be honest, I wasn't really sure whether it would work either. But if you try defining fv manually using preterm.rec, you'll find that it's easy (but you won't get the useful equational lemmas autogenerated for you). So it is just a matter of cajoling the equation compiler into generating that. Putting a 0 pattern for the first variable is going to cause it to try to use nat.rec instead.