failed to find pattern

Stream: new members

[Edward van de Meent]

i'm trying to prove that the minimal distance is a strict upper bound to the packing radius, and i'd like to use a proof by contradiction. however, lean doesn't recognise the pattern i'm trying to rewrite...

i'm guessing there is some kind of diamond issue, but i don't quite get exactly what diamond is the issue... can someone help?

import Mathlib.Init.Order.Defs
import Mathlib.Topology.Bornology.Basic

section imports
  section

    @[ext]
    class GDist (α : Type*) (β :Type*) [LinearOrderedAddCommMonoid β] where
      gdist : α → α → β
    open Set
    @[reducible]
    def Bornology.ofGDist {α:Type*} {β :Type*} [LinearOrderedAddCommMonoid β] (gdist : α → α → β) (gdist_comm : ∀ x y, gdist x y = gdist y x)
        (gdist_triangle : ∀ x y z, gdist x z ≤ gdist x y + gdist y z) : Bornology α :=
      Bornology.ofBounded { s : Set α | ∃ C, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → gdist x y ≤ C }
        ⟨0,fun x hx y => hx.elim⟩
        (fun s ⟨c, hc⟩ t h => ⟨c, fun x hx y hy => hc (h hx) (h hy)⟩)
        (fun s hs t ht => by
          rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
          · rwa [empty_union]
          rcases t.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
          · rwa [union_empty]
          rsuffices ⟨C, hC⟩ : ∃ C, ∀ z ∈ s ∪ t, gdist x z ≤ C
          · refine ⟨C + C, fun a ha b hb => (gdist_triangle a x b).trans ?_⟩
            simpa only [gdist_comm] using add_le_add (hC _ ha) (hC _ hb)
          rcases hs with ⟨Cs, hs⟩; rcases ht with ⟨Ct, ht⟩
          refine ⟨max Cs (gdist x y + Ct), fun z hz => hz.elim
            (fun hz => (hs hx hz).trans (le_max_left _ _))
            (fun hz => (gdist_triangle x y z).trans <|
              (add_le_add le_rfl (ht hy hz)).trans (le_max_right _ _))⟩)
        fun z => ⟨gdist z z, forall_eq.2 <| forall_eq.2 le_rfl⟩

    class GPseudoMetricSpace (α : Type u) (β:Type v) [LinearOrderedAddCommMonoid β] extends GDist α β where
      gdist_self : ∀ x : α, gdist x x = 0
      gdist_comm : ∀ x y : α, gdist x y = gdist y x
      gdist_triangle : ∀ x y z : α, gdist x z ≤ gdist x y + gdist y z
      toBornology : Bornology α := Bornology.ofGDist gdist gdist_comm gdist_triangle
      cobounded_sets : (Bornology.cobounded α).sets =
        { s | ∃ C : β, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, gdist x y ≤ C } := by intros; rfl
  end
  section gpseudometricspace
    variable [LinearOrderedAddCommMonoid β] [GPseudoMetricSpace α β]
    variable {x y z : α} {δ ε ε₁ ε₂ : β} {s : Set α}
    def closedBall (x : α) (ε : β) :=
      { y | GDist.gdist y x ≤ ε }
  end gpseudometricspace

  variable {α : Type*} (s:Set α) (β :Type*) [CompleteLattice β] [LinearOrderedAddCommMonoid β] [GPseudoMetricSpace α β]
  def Separates (δ : β): Prop :=
    ∀ x ∈ s, ∀ y ∈ s, x ≠ y → closedBall x δ ∩ closedBall y δ = ∅

  noncomputable def packing_radius : β :=
    ⨆ (x : s) (y:α) (_:Separates s β (GDist.gdist (x:α) y)),GDist.gdist (x:α) y

  noncomputable def minimal_distance : β := ⨅ (x:s) (y:s) (_:x ≠ y), GDist.gdist (x:α) (y:α)
end imports


theorem extracted_1.{u_1, u_2} {α : Type u_1} (s : Set α) (β : Type u_2) [inst : CompleteLattice β]
  [inst_1 : LinearOrderedAddCommMonoid β] [inst_2 : GPseudoMetricSpace α β] :
  (this : ¬minimal_distance s β ≤ packing_radius s β) → packing_radius s β < minimal_distance s β := by
  obtain a := minimal_distance s β
  obtain b := packing_radius s β
  intro h
  rw [← (@not_le β _ a b)]

[Edward van de Meent]

it gives this error at the last line:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  b < a
α : Type u_1
s : Set α
β : Type u_2
inst : CompleteLattice β
inst_1 : LinearOrderedAddCommMonoid β
inst_2 : GPseudoMetricSpace α β
a b : β
h : ¬a ≤ b
⊢ b < a

[Edward van de Meent]

i suppose it doesn't know how to decide between [CompleteLattice] and [LinearOrderedAddCommMonoid]... but how should i go about fixing this?

[Sébastien Gouëzel]

When you use these two instances, you are putting two unrelated orders on your type, so Lean is rightly confused. You should probably just remove the complete lattice one.

[Edward van de Meent]

i need those for the definition of minimal distance and packing radius though...

[Sébastien Gouëzel]

Note that most examples ofLinearOrderedAddCommMonoid are not complete lattices, by the way (for instance the real line is not a complete lattice, neither are the natural numbers).

[Edward van de Meent]

no, but when you include infinity and require non-negative values, they are...

[Sébastien Gouëzel]

Sure. But this becomes quite restrictive.

[Edward van de Meent]

actually, it makes sense when you look at it as a generalised notion of metric space

[Edward van de Meent]

the codomain of a metric is always non-negative, and adding elements to make the codomain of the metric a complete lattice shouldn't pose any restriction on what can and cannot work as codomain

[Sébastien Gouëzel]

In theory, sure. In practice, it makes a big difference having a distance taking values in real numbers or in extended real numbers, as the behavior of operations is much nicer on real numbers.

[Edward van de Meent]

then how do you suggest i fix this? because i don't see a better solution...

[Matt Diamond]

What if you replace the CompleteLattice instance with [SupSet β] [InfSet β]?

(Edit: Yeah this doesn't make sense since it doesn't give you any lemmas about the Sup and Inf... never mind)

[Matt Diamond]

(deleted)

[Matt Diamond]

still, perhaps there's a way to get the assumptions you need in a more piecemeal fashion that avoids combining two different orders

[Matt Diamond]

I'm curious how other types do this... EReal has a CompleteLinearOrder instance and a LinearOrderedAddCommMonoid instance, but somehow that doesn't cause problems

[Matt Diamond]

and if you replace CompleteLattice with CompleteLinearOrder in @Edward van de Meent's code, the problem goes away

[Sébastien Gouëzel]

I would just use the usual ENNReal-valued edist (which is indeed a complete lattice) to define the main objects, and then define real-valued versions by using the junk value 0 when the genuine value is infinite. Just like we do for docs#EMetric.diam and docs#Metric.diam, for instance.