using instWellFoundedLTNat for RelHomClass.wellFounded

Stream: Is there code for X?

[Malvin Gattinger]

It feels like there must be a better / more canonical way to show that my own relation is wellfounded via an embedding to Nat.lt. Should I use something else than docs#RelEmbedding.isWellFounded ?

import Mathlib

-- Suppose I have this:
def X : Type := sorry
def myrel : X → X → Prop := sorry
def myrel_embed_nat : RelEmbedding myrel Nat.lt := sorry

-- How to show that myrel must be wellfounded?
theorem edge.wellFounded_via_length : WellFounded myrel := by
  have := @RelEmbedding.isWellFounded _ Nat myrel LT.lt myrel_embed_nat ?_
  · cases this
    assumption
  · have := instWellFoundedLTNat
    rcases this with ⟨nat_wf⟩
    constructor
    convert nat_wf

[Malvin Gattinger]

I also think that in my non-mwe code I don't actually have an embedding. So maybe I want to use something like docs#RelHomClass.wellFounded though that seems overkill - is there a version for one specific function instead of a class F?

I would guess it should be called RelHom.wf but that does not exist. :thinking:

[Malvin Gattinger]

Ah, the class can be a singleton I guess. The following works, but I would still happily take any style advice :-)

import Mathlib

def X : Type := sorry
def myrel : X → X → Prop := sorry
def mymeasure : X → Nat := sorry
theorem myrel_then_mymeasure_lt {s t : X} (s_t : myrel s t) : mymeasure s < mymeasure t := sorry

-- What is the elegant / usual way to now show that `myrel` is wellfounded?

def edge_natLT_relHom : RelHom myrel Nat.lt := ⟨mymeasure, myrel_then_mymeasure_lt⟩

theorem edge.wellFounded_via_RelHom : WellFounded myrel := by
  apply @RelHomClass.wellFounded _ Nat myrel Nat.lt _ _ _ edge_natLT_relHom
  have := instWellFoundedLTNat
  rcases this with ⟨nat_wf⟩
  convert nat_wf