Lean fails to prove linear order has transitive LE

Stream: general

[Bhavik Mehta]

Here's my example:

import Mathlib

example (β : Type*) [Infinite β] [LinearOrder β] [NoMaxOrder β]
    (g : ℕ ↪ β) :
    ∃ f : ℕ → β, StrictMono f := by
  -- have : IsTrans β (· ≤ ·) := inferInstance
  have hf := exists_increasing_or_nonincreasing_subseq (· ≤ ·) g

without the inferInstance, the hf line fails. What's going on here?

[Aaron Liu]

Try bumping the synth pending depth?
no that doesn't work

[Bhavik Mehta]

No luck. Here's the synthInstance trace:

[Meta.synthInstance] ❌️ IsTrans β fun x1 x2 => x1 ≤ x2 ▼
  [] new goal IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @SetRel.instIsTransSetOfProdMatch_1PropOfIsTrans to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instIsTransGt to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instIsTransGe to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @IsTrans.decide to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsWellOrder.toIsTrans to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @isWellOrder_gt to IsWellOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @instIsWellOrderOfIsEmpty to IsWellOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsStrictOrder.toIsTrans to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @Set.IsStrictOrder.subset to IsStrictOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instIsStrictOrderGt to IsStrictOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsStrictTotalOrder.toIsStrictOrder to IsStrictOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @instIsStrictTotalOrderOfIsWellOrder to IsStrictTotalOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsStrictWeakOrder.toIsStrictOrder to IsStrictOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsPreorder.toIsTrans to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instIsPreorderGe to IsPreorder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsEquiv.toIsPreorder to IsPreorder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsPartialOrder.toIsPreorder to IsPreorder β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instIsPartialOrderGe to IsPartialOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @IsLinearOrder.toIsPartialOrder to IsPartialOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instIsLinearOrderGe to IsLinearOrder β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @instIsTransOfIsWellOrder to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @instIsTransOfTrans to IsTrans β fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instTransGeGt_mathlib to Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instTransGtGe_mathlib to Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instTransGt_mathlib to Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @instTransGe_mathlib to Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2 ▶
  [] ❌️ apply @Std.instTransNotLtOfLawfulOrderLTOfTotalOfLe to Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2)
        fun x1 x2 => x1 ≤ x2 ▶
  [] ✅️ apply @instTransOfIsTrans to Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2 ▶
  [] result <not-available>
[Meta.synthInstance] ❌️ IsTrans β fun x1 x2 => x1 ≤ x2 ▼
  [] result <not-available> (cached)

[Bhavik Mehta]

So this explains why adding hf makes the second one work, but not why the first one breaks or why hf works.

[Aaron Liu]

It might be because you're not beta-reduced eta-reduced

[Aaron Liu]

it works when you do

import Mathlib

example (β : Type*) [Infinite β] [LinearOrder β] [NoMaxOrder β]
    (g : ℕ ↪ β) :
    ∃ f : ℕ → β, StrictMono f := by
  -- have : IsTrans β (· ≤ ·) := inferInstance
  have hf := exists_increasing_or_nonincreasing_subseq LE.le g

[Aaron Liu]

probably something with the discr tree keys

[Aaron Liu]

interacting with the metavariables in a weird way

[Bhavik Mehta]

I think it might be a metavariable thing, since

import Mathlib

example (β : Type*) [Infinite β] [LinearOrder β] [NoMaxOrder β]
    (g : ℕ ↪ β) :
    ∃ f : ℕ → β, StrictMono f := by
  have hf := exists_increasing_or_nonincreasing_subseq (α := β) (· ≤ ·) g

this works, and the error message on failure has the LE instance as a metavariable

[Aaron Liu]

it has to be something involving both, since if you drop the metavariables it works and if you beta-reduce eta-reduce the LE.le it also works

[Jovan Gerbscheid]

The reason is that the discrimination tree cannot eta-reduce fun x1 x2 => @LE.le β (?m.15 x1 x2) x1 x2 (this is eta, not beta). If you get rid of either the eta expanded form, or the metavariable, then this discrimination tree issue doesn't arise.

[Aaron Liu]

oh yeah that's definitely eta