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
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
To get an induction hypothesis, you need to prove something for an element in
f n for an arbitrary
????? (Feb 26 2020 at 19:57):
Ah that makes sense. Thanks!
Last updated: May 14 2021 at 03:27 UTC