# Zulip Chat Archive

## Stream: new members

### Topic: induction with abbreviations

#### ????? (Feb 26 2020 at 19:03):

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 (Feb 26 2020 at 19:05):

Could you give an example?

#### ????? (Feb 26 2020 at 19:26):

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 (Feb 26 2020 at 19:39):

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 (Feb 26 2020 at 19:44):

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 := ...`

)

#### ????? (Feb 26 2020 at 19:47):

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 (Feb 26 2020 at 19:53):

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`

.

#### ????? (Feb 26 2020 at 19:57):

Ah that makes sense. Thanks!

Last updated: May 14 2021 at 03:27 UTC