induction with abbreviations

Stream: new members

[?????]

I defined an inductive family f : nat -> Type, and an abbreviation abbreviation f0 := f 0. However, the induction tactic does not recognize f 0 and f0 are the same. So induction on the former works but not the latter. How can I fix this?

[Mario Carneiro]

Could you give an example?

[?????]

I got a bit further by generalizing the 0 and using nat.zero instead of 0. Now the problem is that in the type f nat.zero, nat.zero is not a variable, which makes the induction tactic throw an error. I want to generalize the 0 anyway, so is there a way of unfolding abbreviations?

inductive f : ℕ → Type
| c1 : ∀ n, f n

open f

abbreviation f0 := f nat.zero

example : ∀ (v : f0), v = c1 nat.zero :=
begin
intros,
set x := nat.zero with h,
induction v,
end

[Floris van Doorn]

The easy way to do this is to use the cases tactic. This tactic is a little smarter, and can do cases on terms which live in a specific instance of an inductive family:

inductive f : ℕ → Type
| c1 : ∀ n, f n

open f

abbreviation f0 := f nat.zero

example : ∀ (v : f0), v = c1 nat.zero :=
begin
  intros, cases v, refl
end

[Floris van Doorn]

The problem with the induction tactic is that the induction tactic requires v to have type f x where x is a variable in the local context (and not a local definition, i.e. not of the form x : nat := ...)

[?????]

Thanks for the tip. But from the spec it looks like cases doesn't generate the inductive hypothesis, which I would need sometimes.

[Floris van Doorn]

That is correct. But what do you expect your induction hypothesis to look like if you are only proving something about elements in f 0?
To get an induction hypothesis, you need to prove something for an element in f n for an arbitrary n.

[?????]

Ah that makes sense. Thanks!