Need help dealing with orders

Stream: new members

[Egor Morozov]

Here is a toy version of the difficulty that I encountered. Suppose I have something like this

import Mathlib

variable (p q : ℕ → ℕ → Prop)

structure str where
  a : ℕ
  b : ℕ
  h : p a b

theorem str_nonempty (hq : ∃ (a b : ℕ), q a b) : Nonempty (str q) := by
  rcases hq with ⟨a, b, h⟩
  exact Nonempty.intro { a := a, b := b, h := h }

Now how to take the least element in str w.r.t. lexicographical order on ℕ x ℕ? I guess I should transfer somehow the lexicographical order on ℕ x ℕ to str and use that it is well-founded but I don't see any direct way to do this.

[Kenny Lau]

@Egor Morozov two ideas:

1. if i just address your question, you use RelEmbedding.isWellOrder to prove that str is well-ordered
2. if i go above your question, a wise man once said every new definition is a burden, so maybe you can avoid str and just use Subtype

[Matt Diamond]

going to bed so I can't stay and chat but why would RelEmbedding.isWellOrder be necessary if he uses a subtype on ℕ ×ₗ ℕ? that should synthesize a well-order automatically

[Matt Diamond]

unless you were only referring to his current approach with point 1, with the implication that using a subtype would avoid the need for RelEmbedding.isWellOrder

[Kenny Lau]

indeed, 1 and 2 are separate, 2 is a better alternative to 1

[Egor Morozov]

@Kenny Lau , @Matt Diamond, thank you both for the answers, I see your point. I thought about Subtype but these structures just look so nice! In fact, In my project I have a triple Lex product and three Prop fields so combining everything into a single Subtype is a bit ugly... But maybe you're right and it is still better than constantly jumping between the structure and the product type.

[Kenny Lau]

every new definition is a burden

[Matt Diamond]

@Egor Morozov perhaps you can do something like this:

import Mathlib

variable (p q : ℕ → ℕ → Prop)

structure str where
  a : ℕ
  b : ℕ
  h : p a b

def strToProd (s : str p) : ℕ ×ₗ ℕ := (s.a, s.b)

lemma strToProd_injective : (strToProd p).Injective := by
  intro ⟨a, b, h⟩ ⟨a', b', h'⟩ h_eq
  simp_all [strToProd, Lex]

instance : LinearOrder (str p) := LinearOrder.lift' _ (strToProd_injective p)

[Matt Diamond]

actually the RelEmbedding.isWellOrder approach is probably a better idea, defining a RelEmbedding by mapping the structure to ℕ ×ₗ ℕ (or ℕ ×ₗ ℕ ×ₗ ℕ or whatever it is)

[Kenny Lau]

well, you'll use your lift' to define an order, and then use my thing to make it a well order (since my thing requires an order to being with)

[Matt Diamond]

though weirdly I'm not seeing any lemmas that characterize the order generated by lift', but maybe it'll just automatically work

[Aaron Liu]

there's the definitional equality (a ≤ b) = (f a ≤ f b)

[Matt Diamond]

ah yeah, that makes sense... though it feels like maybe there should be some API lemmas that say that? then again, it's so obvious (what else would lift do?) that perhaps it would be unnecessary

[Kenny Lau]

there's no use to have an API lemma because every time you use it you'll need to write your own API (because of the f) and you'll prove it by Iff.rfl each time

[Aaron Liu]

you're expected to characterize it yourself if you define an instance with lift'

[Matt Diamond]

oh right, since you're dealing with ≤ via the instance rather than directly outputting a comparison function that you can talk about

[Egor Morozov]

@Matt Diamond, yes, that is exactly what I tried but the problem is that it gives only LinearOrder instance while to take the least element I need WellOrder or WellFoundedLT, I don't know.

[Egor Morozov]

And another problem is that I've just realized that in my structure there are some Prop fields depending on the others so I cannot implement it as a Subtype.

[Aaron Liu]

import Mathlib

variable (p q : ℕ → ℕ → Prop)

structure str where
  a : ℕ
  b : ℕ
  h : p a b

def strToProd (s : str p) : ℕ ×ₗ ℕ := (s.a, s.b)

lemma strToProd_injective : (strToProd p).Injective := by
  intro ⟨a, b, h⟩ ⟨a', b', h'⟩ h_eq
  simp_all [strToProd, Lex]

instance : LinearOrder (str p) := LinearOrder.lift' _ (strToProd_injective p)

instance : WellFoundedLT (str p) where
  wf := InvImage.wf (strToProd p) wellFounded_lt

[Aaron Liu]

Egor Morozov said:

And another problem is that I've just realized that in my structure there are some Prop fields depending on the others so I cannot implement it as a Subtype.

I think you still can you'll just need something a bit more complicated

[Aaron Liu]

p.s. why does core get to have _root_.invImage that seems like a very generic name

[Kenny Lau]

it's capital, so it's a namespace

[Aaron Liu]

docs#invImage is not a namespace and also docs#InvImage exists too

[Kenny Lau]

oh wow

[Kenny Lau]

yeah ok we should pr to core :upside_down:

[Egor Morozov]

@Aaron Liu, wow, thank you! So InvImage.wf is what I was looking for.

[Egor Morozov]

Aaron Liu said:

I think you still can you'll just need something a bit more complicated

Yes, actually it is an auxiliary structure, I need it only for for proof, not for the statement. So I'm free to choose the most convenient way to formalize it.

[Egor Morozov]

Okay, now I'm stuck on how to use the lifted order. If I have (s t : str p) and s < t, then how can I get strToProd s < strToProd t?

[Aaron Liu]

if you have h : s < t then you should have (show strToProd s < strToProd t from h) : strToProd s < strToProd t

[Egor Morozov]

And in the opposite direction?

[Aaron Liu]

if you have h : strToProd s < strToProd t then you should have (show s < t from h) : s < t

[Aaron Liu]

this works because s < t and strToProd s < strToProd t should be defeq

[Egor Morozov]

Ah, I see. Actually, I have s < t in the goal so I can just use the change tactic! Thank you again!