Zulip Chat Archive

Stream: new members

Topic: How to control generated sizeof_spec for inductive types?


view this post on Zulip Rui Liu (Dec 12 2020 at 17:32):

I have this inductive type T:

inductive T
  | a:   T  T

#check T.a.sizeof_spec

However, this is not the sizeof_spec that I wanted. I don't want sizeof to take into account, which will block me to prove some well-foundedness properties when I use T, according to docs here https://leanprover-community.github.io/extras/well_founded_recursion.html

view this post on Zulip Kevin Buzzard (Dec 12 2020 at 17:33):

It won't block you, it's just that you'll have to use your own well-founded function. See for example this recent question.

view this post on Zulip Kevin Buzzard (Dec 12 2020 at 17:36):

NB there are no terms of that type:

inductive T
  | a:   T  T

theorem no_T : T  false
| (T.a n t) := no_T t

view this post on Zulip Rui Liu (Dec 12 2020 at 17:38):

Yep there're more inductive cases that I didn't post here

view this post on Zulip Rui Liu (Dec 12 2020 at 17:39):

Is there a way to change the well founded relation for an inductive type globally?

view this post on Zulip Mario Carneiro (Dec 12 2020 at 17:39):

yes, you just give an instance of has_well_founded for your type

view this post on Zulip Mario Carneiro (Dec 12 2020 at 17:40):

the instance using sizeof is low priority

view this post on Zulip Rui Liu (Dec 12 2020 at 17:40):

Is there an example on how to do this? @Mario Carneiro

view this post on Zulip Mario Carneiro (Dec 12 2020 at 17:41):

instance : has_well_founded T := \<my_relation, proof_it_is_well_founded\>

view this post on Zulip Kevin Buzzard (Dec 12 2020 at 17:42):

Searching for instance : has_well_founded in mathlib gives five examples, for example here

view this post on Zulip Rui Liu (Dec 12 2020 at 17:47):

OK cool will try this!

view this post on Zulip Rui Liu (Dec 12 2020 at 18:54):

Succeeded!


Last updated: May 15 2021 at 02:11 UTC