Help with induction on `Lex (Nat × Nat)`

Stream: new members

[Graham Leach-Krouse]

I'm trying to prove a theorem of the form

lindenbaumSequenceMonotone { t : Th } { Δ : Ctx } : Monotone (lindenbaumSequence t Δ)

where

lindenbaumSequence (t : Th) (Δ : Ctx) : Lex (Nat × Nat) → Ctx

[Graham Leach-Krouse]

Monotone unfolds as

∀ ⦃a b : Lex (ℕ × ℕ)⦄, a ≤ b → lindenbaumSequence t Δ a ≤ lindenbaumSequence t Δ b

so I start by introducing a and b. But I'm going to need to appeal inductively to statements

a ≤ c → lindenbaumSequence t Δ a ≤ lindenbaumSequence t Δ c

for c < b.

[Graham Leach-Krouse]

I don't seem to be able to get these by just calling lindenbaumSequenceMonotone (the termination checker objects...)

[Graham Leach-Krouse]

Could anyone help me figure out the right way to go about this? Maybe I need some kind of termination_by magic, or maybe there's a correct way to introduce the inductive hypothesis I need here?

[Graham Leach-Krouse]

OK, got it I think:

termination_by lindenbaumSequenceMonotone t Δ a b h => (b.fst, b.snd)

[Eric Wieser]

Can you give a #mwe?

[Eric Wieser]

I would hope you can use => b instead of => (b.fst, b.snd)

[Graham Leach-Krouse]

Here's an attempt. The following passes, modulo a sorry warning:

import Mathlib.Data.Prod.Lex

lemma mwe : ∀a : Lex (Nat × Nat), (0,0) ≤ a := by
  intros a
  match a with
    | ⟨0, 0⟩ => exact le_rfl
    | ⟨i + 1, 0⟩ =>
      have l₁ := mwe (i,0)
      sorry
    | ⟨i, j + 1⟩ => sorry
    termination_by mwe a => (a.fst, a.snd)

But fails to prove termination when I use => a instead of => (a.fst, a.snd).

[Graham Leach-Krouse]

It's perhaps a Lex quirk? It's OK when I try it with plain Nat × Nat

[Eric Wieser]

Thanks, I'll try that tomorrow. I would hope it is possible to teach lean to handle Lex automatically

[Eric Wieser]

docs4#ofLex b is a bit shorter than (b.fst, b.snd), but I haven't tried it

[Graham Leach-Krouse]

ofLex a Seems to produce the same behavior as a plain a

[Eric Wieser]

I think we need to add a docs4#WellFoundedRelation instance for lex

[Yaël Dillies]

Also, you can use the notation for Lex instead of writing it out.

[Graham Leach-Krouse]

What's the notation?

[Yaël Dillies]

ℕ ×ₗ ℕ is notation for Lex (Nat × Nat)