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: Dec 20 2023 at 11:08 UTC