inductive definition of well-foundedness

Stream: new members

[Chris M]

I'm still in the process of trying to understand induction and recursion in Lean.
I came accross this definition of well-foundedness:

inductive well_founded {α : Sort u} (r : α → α → Prop) : Prop
| intro (h : ∀ a, acc r a) : well_founded

I would have guessed that instead, this would be defined as:

def well_founded {α : Sort u} (r : α → α → Prop) : Prop : =  ∀ a, acc r a

Why is the first one chosen rather than the second one, and how are they different ?

[Mario Carneiro]

I don't think there is a good reason for this definition. The one constructor inductive is pretty similar to a structure with one field, which is sometimes used when you want to avoid accidental definitional reduction from well_founded r to ∀ a, acc r a, but other than that it is basically the same thing

[Mario Carneiro]

The structure has the advantage that you get the projection for free; in this case it was defined manually using well_founded.apply

[Mario Carneiro]

One reason it might have been written that way is that well_founded occurs very early in lean core, before the tactic framework and parts of the equation compiler are working properly because many of the required definitions (like well_founded!) don't exist yet. So it's possible that structure doesn't actually work at this part of the prelude

[Chris M]

I see. that clarifies, thanks :)

[Mario Carneiro]

lean#408