failed to synthesize instance LT α ?

Stream: mathlib4

[Michael]

I'm pretty sure I just don't know the correct way to do this, but I'm trying to do a proof about a LinearOrdered set and something isn't being recognized.

import Mathlib.Data.Set.Lattice

open Set

variable (α : Type)
variable (A : Set α) [LinearOrder A]

example :
    ∀ r ∈ A, ∀ s1 ∈ A, ∀ s2 ∈ A,
      {x ∈ A | r < x ∧ x < s1} = ∅ ∧
      {x ∈ A | r < x ∧ x < s2} = ∅ →
    s1 = s2 := by
  done

This produces errors for all the comparisons (failed to synthesize instance LT α), which I assume means Lean is trying to treat the type α as comparable when that is not guaranteed. As far as I see, all of my variables belong to the set A, and A is comparable, so the comparisons should be fine. I've also tried putting the LinearOrder constraint in the example as example [LinearOrder A] : ..., which doesn't work either.

How am I supposed to do this?

[Eric Wieser]

Are you sure you don't want to work with a linearly ordered type instead?

[Michael]

I am not sure of that, no. I don't really know how the [] annotations work.

[Matt Diamond]

the immediate problem is that you put the order on the set instead of the type, which I think is what Eric is getting at

[Michael]

There doesn't appear to be a syntax error placing it on the set - what does [LinearOrder A] make comparable?

[Matt Diamond]

LinearOrder works with types, so what Lean is doing is coercing the set A to a type, specifically the subtype of elements of A, so elements of that subtype (like x : A) will have the order on them

[Matt Diamond]

so technically if you changed all of the ∈ to :, the error would go away

[Matt Diamond]

Lean also has a concept of subrelation (docs#Subrel) which is when a relation on a type is restricted to members of a set

[Michael]

thanks!

[Michael]

Well, I'm having a problem that I strongly suspect is related to this. I have a theorem about all sets of real numbers. I have another set of type Set ↑(Ico 0 1) - that is, it's a subset of the half-open real interval from 0 to 1. I want to apply my theorem (about all sets of real numbers) to this set that is a subset of [0, 1). Is there a better way to handle this than defining let S' := {Subtype.val x | x ∈ S}?

That works, but I'm not thrilled with the approach:

example (h0 : lubp ℝ) : lubp (Set.Ico 0 1 : Set ℝ) := by
  simp only [lubp] at h0
  simp only [lubp]
  intro S hsne hsba
  simp only [BddAbove, Set.Nonempty] at hsba
  obtain ⟨ub, hub⟩ := hsba
  -- S has a "subset" type; let S' be all the reals in S
  let S' := {Subtype.val x | x ∈ S}
  -- S' = S, and S is nonempty, so S' is also nonempty
  have hs'ne : Set.Nonempty S' := by
    simp only [Set.Nonempty]
    simp only [Set.Nonempty] at hsne
    obtain ⟨s, hs⟩ := hsne
    exists Subtype.val s
    rw [mem_setOf]
    exists s
  -- And since S is bounded above in [0, 1), S' is certainly bounded above in ℝ
  have hs'ba : BddAbove S' := by
    simp only [BddAbove, Set.Nonempty]
    rw [mem_upperBounds] at hub
    exists ub.val
    rw [mem_upperBounds]
    intro x hx
    rw [mem_setOf] at hx
    obtain ⟨r, hr⟩ := hx
    have hr' := hub r hr.left
    rw [← hr.right]
    simp only [← subrel_val]
    exact hr'
  -- [proof continues...]

[Kevin Buzzard]

This is a pain point when working in type theory. Whilst I don't know your actual application, for me the alarm bells would be going off at the coercion from Ico 0 1 to a type. Are you sure you can't make do with a term of type Set \R and a proof that it's a subset of Ico 0 1? This would probably be the idiomatic approach. The moment you make a new type eg coercing a subset to a type, you're asking for trouble (in the form that you're already seeing). Use the default types as much as possible, if you can.

[Matt Diamond]

@Michael could you provide the definition of lubp?

[Michael]

The one applying to a type (as complained about immediately above) was this:

def lubp (α : Type) [LinearOrder α] : Prop :=
  ∀ S : Set α,
  S.Nonempty → S.BddAbove → ∃ x : α, IsLUB S x

(For context, what I'm doing is expressing the assignments of https://ocw.mit.edu/courses/18-901-introduction-to-topology-fall-2004/ in Lean. What's supposed to be expressed is "An ordered set $A$ has the least upper bound property if every nonempty subset $A_0 \subseteq A$ that is bounded above [in $A$] has a least upper bound [in $A$].")

This type-oriented definition works well for the theorem that a set has the least upper bound property only if it has the greatest lower bound property (defined analogously), and benefits from leaning on the stuff like IsLUB that Mathlib already provides.

It causes the problems that I illustrated above for the theorem that, if $\mathbb{R}$ has the lubp, then so does $[0, 1)$. I have managed to finish both proofs using this more set-oriented definition of lubp:

def lubp {α : Type} [LinearOrder α] (A : Set α) : Prop :=
  ∀ S ⊆ A, S.Nonempty → (∃ x ∈ A, x ∈ upperBounds S) →
  ∃ x ∈ A, IsLeast {a ∈ A | a ∈ upperBounds S} x

But there are still some aspects of this that I find less than ideal; it adds a lot of boilerplate to the lubp → glbp theorem, it makes the Mathlib Set.BddAbove predicate unusable (since that gives you a bound of the relevant type, not a bound in a relevant superset), and it leaves weirdnesses in the other proof such as the need to use {y : ℝ | True} for the set of real numbers (since ℝ is a type, not a set). Then, once the proof is finished, I get warnings everywhere I refer to {y : ℝ | True} because the variable y is unused.

[Kevin Buzzard]

This approach is normal in mathlib. For example there are two definitions of compact -- one for subsets of a type and one for types. The main API is developed for subsets of a type and then the theory is developed for types as a corollary of the subset work (applying to Set.univ). This is an unfortunate consequence of using type theory as a foundation; subsets of subsets are not equal to subsets in type theory.

[Kevin Buzzard]

To tidy up your other comments: I would just use Set.univ for the subset representing the entire type rather than rolling your own, and to get rid of an unused variable warning don't name the variable, call it _.