WellFoundedRelation '<' for Bool outside mathlib

Stream: general

[cmlsharp]

Does

def Bool.lt_wfRel : WellFoundedRelation Bool where
  rel := (· < ·)
  wf := ...

Analogous to Nat.lt_wfRel exist outside of Mathlib? I found myself wanting to use it in a PR to Batteries.

[Robin Arnez]

You can also just use Bool.toNat as a termination measure

[cmlsharp]

Thanks, that will suffice

[Kim Morrison]

cmlsharp said:

Does

def Bool.lt_wfRel : WellFoundedRelation Bool where
  rel := (· < ·)
  wf := ...

Analogous to Nat.lt_wfRel exist outside of Mathlib? I found myself wanting to use it in a PR to Batteries.

I think this should be okay to PR upwards if you'd like.

[cmlsharp]

batteries#1639

[Kim Morrison]

Ugh, WellFoundedRelation is ugly, with the bundled relation... I guess it can't be helped immediately. WellFoundedLT and WellFoundedGT seem much nicer to expose to the world.

[cmlsharp]

Is there interest in a larger project to try and upstream WellFoundedLT/WellFoundedGT? I haven't looked into it too deeply. For my purposes WellFoundedRelation would have been sufficient (it just made for a convenient way to write the Finiteness relation for the scan iterator combinator )

[cmlsharp]

In the short term, I think upstreaming at least this makes sense

[Kim Morrison]

Could you add a comment in the module doc-string along the lines of "These are not instances, despite WellFoundedRelation being a class, as we provide versions for both < and >. If you need instances, you may use the WellFoundedLT and WellFoundedGT classes available in Mathlib."

[cmlsharp]

done

[Kim Morrison]

Oh, module doc, not the individual doc-strings.

[cmlsharp]

oop sorry, done