Zulip Chat Archive

Stream: new members

Topic: induction with abbreviations


view this post on Zulip ????? (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?

view this post on Zulip Mario Carneiro (Feb 26 2020 at 19:05):

Could you give an example?

view this post on Zulip ????? (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

view this post on Zulip 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

view this post on Zulip 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 := ...)

view this post on Zulip ????? (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.

view this post on Zulip 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.

view this post on Zulip ????? (Feb 26 2020 at 19:57):

Ah that makes sense. Thanks!


Last updated: May 14 2021 at 03:27 UTC