Induction on RT-closures

Stream: general

[Patrick Johnson]

In the following lemma

import logic.relation
open relation

inductive T (F : ℕ → ℕ → Prop) : ℕ → Prop
| mk₁ : T 0
| mk₂ (n n₁ : ℕ) : F n n₁ → T n₁ → T n

def T₁ (F : ℕ → ℕ → Prop) (n : ℕ) :=
refl_trans_gen F n 0

lemma T_eq_T₁ : T = T₁ :=
begin
  ext F n, rw T₁, split; intro h,
  { induction h with n₁ n₂ h₁ h₂ h₃,
    { triv, },
    { exact refl_trans_gen.head h₁ h₃ }},
  { apply h.head_induction_on,
    { apply T.mk₁, },
    { rintro n₁ n₂ h₁ h₂ h₃, apply T.mk₂,
      { exact h₁ },
      { exact h₃ }}},
end

if I replace apply h.head_induction_on with induction h, then I get a dead-end:

lemma T_eq_T₁ : T = T₁ :=
begin
  ext F n, rw T₁, split; intro h,
  { induction h with n₁ n₂ h₁ h₂ h₃,
    { triv, },
    { exact refl_trans_gen.head h₁ h₃ }},
  {
    induction h,
  },
end

The first subgoal after the induction cannot be proved, because the induction tactic did not replace n with 0. Is this the expected behavior?

[Yaël Dillies]

Have you tried induction h with ... generalizing ...?

[Patrick Johnson]

There is nothing to be generalized. The goal is

F: ℕ → ℕ → Prop
n: ℕ
h: refl_trans_gen F n 0
⊢ T F n

After induction h, the first subgoal becomes:

F: ℕ → ℕ → Prop
n: ℕ
⊢ T F n

but the goal statement should be T F 0, because it's the refl case, so n must be unified with 0. What am I missing?

[Yaël Dillies]

If you look at the definition of refl_trans_gen, you see that it's 0 that gets replaced by n, not the other way around.

inductive refl_trans_gen (r : α → α → Prop) (a : α) : α → Prop
| refl : refl_trans_gen a
| tail {b c} : refl_trans_gen b → r b c → refl_trans_gen c

which makes sense, but is rather unexpected indeed.