## Stream: general

### Topic: Induction on RT-closures

#### Patrick Johnson (Dec 30 2021 at 09:30):

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 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 (Dec 30 2021 at 09:31):

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

#### Patrick Johnson (Dec 30 2021 at 09:42):

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 (Dec 30 2021 at 09:47):

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.

Last updated: Aug 03 2023 at 10:10 UTC