Errors with order hierarchy

Stream: maths

[Heather Macbeth]

I contributed some theorems for conditionally complete linear orders (#3843), now I want to use them for real analysis. How can I get the conditionally complete linear order property for an interval? I want:

variables [conditionally_complete_linear_order α] {a b : α}

instance subtype.conditionally_complete_linear_order :
  conditionally_complete_linear_order (Ioo a b) :=
sorry

Since mathlib already has docs#subtype.linear_order, I had thought it might be enough to show the 4 new properties for docs#conditionally_complete_linear_order, doing something like

instance subtype.conditionally_complete_linear_order :
  conditionally_complete_linear_order (Ioo a b) :=
{ le_cSup := _,
  cSup_le := _,
  cInf_le := _,
  le_cInf := _,
  ..subtype.linear_order (Ioo a b) }

But this gives me no end of errors -- things like, "invalid structure value { ... }, field 'sup' was not provided".

[Heather Macbeth]

With some trial and error, I got this working as

noncomputable instance subtype.conditionally_complete_lattice [inhabited (Ioo a b)] :
  conditionally_complete_lattice (Ioo a b) :=
{ Sup := _,
  le_cSup := _,
  cSup_le := _,
  Inf := _,
  cInf_le := _,
  le_cInf := _,
  ..distrib_lattice.to_lattice (Ioo a b) }

for suitable _.

[Mario Carneiro]

You know, I think this is true for any open subset of R

[Heather Macbeth]

You mean, without the inhabited? Yes, I am playing with that at the moment.

[Heather Macbeth]

I use the inhabited in order to define

Sup := λ t, if ht : Sup (coe '' t : set α) ∈ (Ioo a b) then ⟨Sup (coe '' t : set α), ht⟩ else default (Ioo a b),

Hard to avoid this, but I could do a case analysis with a separate case for non-inhabited α. Is there a typeclass for empty α or similar? I haven't had to reason about them before.

[Heather Macbeth]

Oh -- maybe you mean any open subset, not just an interval. That may well be true, but I think it fits less well in the library. The statement about open intervals can live in order.conditionally_complete_lattice. The statement about open sets would have to be deferred to topology.algebra.ordered.

[Mario Carneiro]

I don't mean the instance should be registered, just that it is a mathematically more general theorem

[Heather Macbeth]

While I have your attention ( :smiley:), how do I do this?

Heather Macbeth said:

I could do a case analysis with a separate case for non-inhabited α. Is there a typeclass for empty α or similar? I haven't had to reason about them before.

[Mario Carneiro]

Do by_cases h : nonempty A

[Heather Macbeth]

Thanks!!

[Mario Carneiro]

under the assumption that it is false, you can prove that A is empty

[Mario Carneiro]

we don't have any particular typeclass for this but generally whatever you are proving will become trivial under this assumption

[Heather Macbeth]

Do I need to enter tactic mode in my definition, then? Is there a more idiomatic way?

noncomputable instance subtype.conditionally_complete_linear_order :
  conditionally_complete_linear_order (Ioo a b) :=
begin
  by_cases h : nonempty (Ioo a b),
  { sorry },
  { sorry }
end

[Heather Macbeth]

Never mind -- the inhabited hypothesis is necessary. docs#has_Sup_to_nonempty

[Sebastien Gouezel]

It is not true for arbitrary nonempty open subsets of $\mathbb{R}$. Consider for instance the union A of the open intervals centered at 1/n of small enough radius r_n to make sure that these intervals are disjoint, and of (-1, 0). Then the intersection of A with the positive half-line has no Inf in A, even though it is bounded below.

[Sebastien Gouezel]

Better example: $(-1, 0) \cup (0,1)$.

[Heather Macbeth]

Ah, nice!

[Heather Macbeth]

#3991