Zulip Chat Archive

Stream: general

Topic: default recursor

Yury G. Kudryashov (May 13 2020 at 05:33):

Is it possible to change the default lemma for the induction tactic? E.g., I'd like induction s where s : finset α to use finset.induction_on.

Mario Carneiro (May 13 2020 at 05:43):

no

Mario Carneiro (May 13 2020 at 05:44):

PR?

Yury G. Kudryashov (May 13 2020 at 05:54):

Should it be a class with instances or an attribute?

Johan Commelin (May 13 2020 at 05:58):

I would guess attributes should work best here

Yury G. Kudryashov (May 13 2020 at 05:59):

attribute [default_recursor finset.induction_on] finset?

Johan Commelin (May 13 2020 at 05:59):

Or maybe the other way round?

Johan Commelin (May 13 2020 at 06:00):

attribute [default_recursor finset]
lemma finset.induction_on ...

Yury G. Kudryashov (May 13 2020 at 06:00):

If we go the other way around, then induction will have to go over all attributes and find the first with value finset.

Johan Commelin (May 13 2020 at 06:00):

And maybe the finset in [default_recursor finset] can even be figured out by staring at the namespace. I don't know

Johan Commelin (May 13 2020 at 06:01):

Yury G. Kudryashov said:

If we go the other way around, then induction will have to go over all attributes and find the first with value finset.

Hmm, that's true

Yury G. Kudryashov (May 13 2020 at 06:01):

Of course, we can have two attributes, one setting the other.

Last updated: Dec 20 2023 at 11:08 UTC