How to control generated sizeof_spec for inductive types?

Stream: new members

[Rui Liu]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Rui Liu]

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

[Rui Liu]

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

[Mario Carneiro]

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

[Mario Carneiro]

the instance using sizeof is low priority

[Rui Liu]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Rui Liu]

OK cool will try this!

[Rui Liu]

Succeeded!