unfold creating new hypothesis and induction failing

Stream: new members

[Pedro Minicz]

Why does tactic#unfold created a new hypothesis in the example below? Also, why does induction fail? Sorry if the example is a bit too long, I tried to make it as small as possible.

import data.vector

structure Language :=
(functions : ℕ → Type)

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

def term := preterm L 0

namespace term

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

end term

structure Structure (L : Language) :=
(carrier : Type)

instance (L : Language) : has_coe_to_sort (Structure L) Type :=
⟨λ A, A.carrier⟩

variables {L} {A : Structure L}

def realize_preterm (s : ℕ → A) : ∀ {l : ℕ}, vector A l → preterm L l → A := sorry
def realize_term (s : ℕ → A) : term L → A := realize_preterm s vector.nil

set_option trace.check true

example (s₁ s₂ : ℕ → A) (t : term L) (h : ∀ x ∈ term.fv t, s₁ x = s₂ x) :
  realize_term s₁ t = realize_term s₂ t :=
begin
  -- Created a new `t`.
  unfold term at t,
  -- Clear newly created `t`.
  clear t,
  -- Induction fails.
  induction t,
end

[Kyle Miller]

unfold is a flavor of simp and dunfold is a flavor of dsimp. If you do dunfold it doesn't create a new hypothesis.

[Kyle Miller]

I think what's going on is that since t appears in other terms and unfold likes to rewrite rather than change, it just creates a new hypothesis.

[Kyle Miller]

As for why induction fails, I have no idea, but you can get around it by using the recursor directly with refine:

example (s₁ s₂ : ℕ → A) (t : term L) (h : ∀ x ∈ term.fv t, s₁ x = s₂ x) :
  realize_term s₁ t = realize_term s₂ t :=
begin
  dunfold term at t,
  revert h,
  refine preterm.rec_on t (λ n, _) (λ l f, _) (λ l tl t0, _); intro h,

end