eliminator for set based on whether it is empty or not

Stream: general

[Bernd Losert]

Say I have a set s. Is there an eliminator on s to deal with what happens when it is empty and when it isn't? Or do I have to useby_cases on is_empty s?

[Eric Wieser]

docs#set.eq_empty_or_nonempty might exist

[Eric Wieser]

Excellent, it does: so

obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Will do all you need in tactic mode

[Bernd Losert]

So that will create two goals? One for the empty case and one for the nonempty case?

[Bernd Losert]

I would prefer an eliminator that I can use outside of tactic mode (if such a thing exists).

[Adam Topaz]

How do you propose to avoid cases?

[Bernd Losert]

I want cases, but in the form of an eliminator, like. set.empty_elim (empty_case_code) (non_empty_case_code).

[Eric Wieser]

In tactic mode you can use s.eq_empty_or_nonempty.elim _ _

[Adam Topaz]

Right, just combine what Eric said with the eliminator for or

[Eric Wieser]

You'll have to rewrite by s = ∅ manually in the first case though

[Eric Wieser]

Or use match s.empty_or_nonempty with | or.inl rfl := _ | or.inr r := _ end, if that works

[Bernd Losert]

So (set.eq_empty_or_nonempty s).elim? Let me try.

[Eric Wieser]

s. should work fine

[Adam Topaz]

You can avoid those parens with the dot notation :) see Mario's comment

[Bernd Losert]

Ah, right.

[Adam Topaz]

Dot notation is really awesome when you get used to it

[Bernd Losert]

OK, it seems to work, but now I'm getting another error. Progress!

[Bernd Losert]

This doesn't work for me:

def f : set nat -> nat := fun (s : set nat),
match s.empty_or_nonempty with
| or.inl rfl := 0
| or.inr _ := 1
end

What am I doing wrong here?

[Bernd Losert]

Could it be that empty_or_nonempty only works in tactic mode?

[Mario Carneiro]

You can't eliminate an or into a non-prop

[Mario Carneiro]

If you change the nat for some proposition then it will work

[Mario Carneiro]

are you trying to construct data, or prove a theorem?

[Mario Carneiro]

for the former I would suggest using if s = ∅ then empty_case_code else non_empty_case_code

[Mario Carneiro]

which also requires open_locale classical at the top of the file or by classical; exact at the start of the function

[Bernd Losert]

Ah, I see. I didn't know about the restriction of or elimination. OK.

[Bernd Losert]

Is there a reason for this restriction?

[Mario Carneiro]

An or does not contain information about which variant is true, there is provably at most one proof of a disjunction. So you can't use a proof of an or to make a case disjunction unless the thing you are trying to prove is already a proposition (in which case it doesn't matter which one is actually true, in the case where both are true)

[Yaël Dillies]

Put simply, you know it's true, but you don't know which

[Yaël Dillies]

So you can't compute

[Bernd Losert]

That makes sense.

[Bernd Losert]

Although it's kind of weird - if you don't know which, how does the pattern matching work?

[Adam Topaz]

It should be mentioned that you can write if _ then _ else _

[Yaël Dillies]

Mario Carneiro said:

for the former I would suggest using if s = ∅ then empty_case_code else non_empty_case_code

It has been :wink:

[Mario Carneiro]

Bernd Losert said:

Although it's kind of weird - if you don't know which, how does the pattern matching work?

The pattern matching only works in the case where it is in a computationally irrelevant position: it is never actually executed

[Bernd Losert]

So it's an illusion.

[Mario Carneiro]

In this case, it is simply nice syntax for the logical theorem or.cases_on

[Bernd Losert]

Thanks for clarifying.

[Mario Carneiro]

It's (ab)using the curry howard isomorphism to allow you to write proofs with some of the same syntax that you use to write programs

[Bernd Losert]

How do I get an element from the set in the nonempty_case_code?

[Bernd Losert]

I mean, when I do this if s = ∅ then empty_case_code else non_empty_case_code.

[Adam Topaz]

We probably have docs#set.nonempty.some or something like that?

[Adam Topaz]

But you would have to show that s \neq \empty implies s.nonempty.

[Adam Topaz]

It might be better to use if s.nonempty then nonempty_case else empty_case. It's very possible that you're trying to do something in a way that's not ideal.

[Adam Topaz]

Can you un- #xy ?

[Bernd Losert]

Well, I'm trying to define has_Inf and I need to deal with the case when the set is empty and do something special in that case.

[Bernd Losert]

So far, Lean is not letting me do what I want. It keeps complaining about:

error: induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop

[Bernd Losert]

When I use if then else, I run into invalid field notation problems.

[Adam Topaz]

What are defining a has_Inf for? A #mwe would be helpful

[Bernd Losert]

import tactic
import order.filter.ultrafilter
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter

variable a : Type*

class convergence_space (a : Type*) :=
(conv : filter a -> a -> Prop)

def indiscrete : convergence_space a := {
  conv := fun l x, l <= pure x,
}

instance : has_Inf (convergence_space a) := {
  Inf := fun ps,
    let ne := ps.nonempty in
    if ne then { conv := @conv a (set.nonempty.some ne) }
    else indiscrete
}

[Adam Topaz]

I don't know if this is the correct definition...

import tactic
import order.filter.ultrafilter
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter

variable (α : Type*)

class convergence_space (α : Type*) :=
(conv : filter α -> α -> Prop)

def indiscrete : convergence_space α := ⟨λ l x, l ≤ pure x⟩

instance {α} : has_Inf (convergence_space α) :=
{ Inf := λ S, ⟨λ F x, ∀ (t : convergence_space α) (ht : t ∈ S),
    by letI : convergence_space α := t; exact convergence_space.conv F x⟩ }

[Adam Topaz]

This is saying that the convergence should hold true for every convergence space structure from the given set.

[Bernd Losert]

That would be has_Sup. I had no problems with that one.

[Mario Carneiro]

If you have a sup, you can just skip the inf

[Bernd Losert]

True, but I wanted to define the instance just to check the theory.

[Mario Carneiro]

in a complete lattice one implies the other, although the expression you get out is ugly and it's good to supply one explicitly if it has a nice expresssion

[Bernd Losert]

In this Inf, it's supposed to be an existensial, but I have to deal with the empty case explicitly.

[Mario Carneiro]

Could you write the expression you want informally?

[Adam Topaz]

Are you looking for something like this?

import tactic
import order.filter.ultrafilter
import order.filter.partial

noncomputable theory
open set filter classical
open_locale classical filter

variable (α : Type*)

class convergence_space (α : Type*) :=
(conv : filter α -> α -> Prop)

def indiscrete : convergence_space α := ⟨λ l x, l ≤ pure x⟩

instance {α} : has_Inf (convergence_space α) :=
{ Inf := λ S, ⟨λ F x, ∃ (t : convergence_space α) (ht : t ∈ S),
    by letI : convergence_space α := t; exact convergence_space.conv F x⟩ }

[Bernd Losert]

Basically, the Inf ps of a set of convergence spaces ps is suppose to defined as so that conv f x in Inf ps means there exists a p in ps such that conv f x in p. In the case the set is empty, use the indiscrete convergence space.

[Mario Carneiro]

btw you can use by exactI instead of that letI

[Bernd Losert]

First time seeing letI and exactI. What do those do?

[Mario Carneiro]

how about F ≤ pure x \/ ∃ (t : convergence_space α) (ht : t ∈ S), by exactI convergence_space.conv F x

[Bernd Losert]

And why does the approach using if then else fail?

[Mario Carneiro]

It can be made to work, but I think it is better to use propositional connectives in this case since you are defining a Prop

[Bernd Losert]

I tried to, but it still complained saying that I wasn't defining a Prop.

[Mario Carneiro]

But the code with { conv := @conv a (set.nonempty.some ne) } is wrong, that is saying that some particular p in the set is converging, not that there exists one that converges

[Bernd Losert]

Ah, you're right. After giving up on the existensial version, I was trying this approach and I didn't realize it was not the same.

[Bernd Losert]

Again, thanks for clarifying. Thank goodness for zulip and the helpful people here. Without them, I would have given up formalizing this stuff.

[Kevin Buzzard]

Without the Zulip most of us would have given up. Without Mario I would never have made it through my first year example sheets, let alone schemes