silly goal

Stream: general

[Reid Barton]

surely there should be a one-word tactic for this?
example {n : ℕ} (m : ℕ) : m.succ + n = 1 + (m + n) := sorry

[Reid Barton]

actually, no: what I really want is an induction principle for nat that uses m+1 rather than m.succ

[Kenny Lau]

PR?

[Kenny Lau]

I also find m+1 more useful at times

[Kenny Lau]

Reid Barton said:

surely there should be a one-word tactic for this?
example {n : ℕ} (m : ℕ) : m.succ + n = 1 + (m + n) := sorry

does omega work?

[Jalex Stark]

we should have that induction principle, and we should also make a tag for the induction tactic that lets you specify a default induction principle for each type

[Reid Barton]

omega did work, thanks

[Kenny Lau]

induction using?

[Jalex Stark]

right. I essentially always want induction n using nat.induction_on', where induction_on' is the version with +1 instead of .succ. The idea I'm proposing is an attribute @[induction] with priority k, so that induction n actually means induction n using h where h is the lemma with the highest priority induction attribute.

[Jalex Stark]

(maybe this "induction with the right default induction principle" is instead a new tactic induction' or by_induction)

[Simon Hudon]

@Jalex Stark I think that's a good idea. That would be pretty useful for my datatype project.