set α in fintype α

Stream: Is there code for X?

[Joachim Breitner]

I am in a fintype α context, and want to do an inductive proof where set α gets smaller, like this:

instance of_fintype [h : fintype α] : is_atomic α :=
is_atomic.mk begin
  intros b,
  obtain ⟨n, hn⟩ : ∃ n, n = fintype.card { a : α | b < a ∧ a < ⊥ },
  …
end

but it seems that even in fintype α, fintype.card s causes an unsolved typeclass instance for fintype (↑s).
What is the right way to get the cardinality of a set in a fintype?
Or should I use finset? Can I use the nice set syntax with finset?

[Johan Commelin]

I guess you need open_locale classical above your declaration.

[Johan Commelin]

Or maybe call classical at the start of your proof

[Johan Commelin]

It might get nicer with finset, indeed.

[Joachim Breitner]

Is there syntax or should I use finset.univ.filter (λ …)?

[Alex J. Best]

Generally I find that when doing inductive proofs on the size of a set, the smoothest lean translation of that proof is not to talk about the size of the set at all but just to use an induction principle like docs#finset.induction_on

[Alex J. Best]

I think you have to use filter unfortunately

[Joachim Breitner]

I used induction_on elsewhere, but I am not sure if it works well here especially since I need to do strong induction on the size.

[Alex J. Best]

I'd guess its still better to use docs#finset.strong_induction_on if that works in your use case

[Joachim Breitner]

oh, there is a strong variant there too. silly me :-)

[Alex J. Best]

Or maybe docs#finset.strong_downward_induction_on

[Alex J. Best]

Well these variants are in a different file unfortunately, so maybe not the easiest to discover from the docs

[Yaël Dillies]

Wait, I don't think you need induction at all.

[Joachim Breitner]

For the fintype α → is_atomic proof? I wouldn’t be surprised, but I’m curious to hear about it :-)

[Yaël Dillies]

Leave 15min and hopefully I will have cooked up the proof :smile:

[Joachim Breitner]

Sounds good

[Joachim Breitner]

(It’s a lesson I learned in life: A good way to get stuff done by others is to threaten to do it worse…)

[Yaël Dillies]

Absolutely!

[Yaël Dillies]

I have one advantage over you here. It's that I know (actually, authored) docs#locally_finite_order.

[Yaël Dillies]

We need a version of docs#finset.max which works for nonlinear orders.

[Yaël Dillies]

Here's a rough draft. Notice how I push back the need for induction.

import data.finset.locally_finite
import order.atoms
import order.minimal

open finset

variables {α : Type*}

@[simp] lemma mem_minimals_iff (r : α → α → Prop) (s : set α) (a : α) :
  a ∈ minimals r s ↔ a ∈ s ∧ ∀ ⦃b⦄, b ∈ s → r b a → a = b := iff.rfl

lemma set.finite.minimals_nonempty [preorder α] {s : set α} (hs : s.finite) :
  (minimals (≤) s).nonempty ↔ s.nonempty :=
sorry

@[simp] lemma mem_Iic_self [preorder α] [locally_finite_order α] [order_bot α] (a : α) :
  a ∈ Iic a := mem_Iic.2 le_rfl

instance fintype.to_is_atomic [partial_order α] [order_bot α] [fintype α] : is_atomic α :=
⟨λ a, begin
  classical,
  refine or_iff_not_imp_left.2 (λ h, _),
  haveI : locally_finite_order α := fintype.to_locally_finite_order,
  obtain ⟨b, hb⟩ := ((Iic a).erase ⊥).finite_to_set.minimals_nonempty.2
    ⟨a, mem_erase.2 ⟨h, mem_Iic_self _⟩⟩,
  simp_rw [mem_minimals_iff, mem_coe, mem_erase, mem_Iic] at hb,
  refine ⟨b, ⟨hb.1.1, λ c hcb, _⟩, hb.1.2⟩,
  by_contra hc,
  exact hcb.ne' (hb.2 ⟨hc, hcb.le.trans hb.1.2⟩ hcb.le),
end⟩

[Yaël Dillies]

The end manipulation is a bit ugly because is_atomic hasn't been adapted to use docs#is_min yet. I mean to do this refactor and you thinking this is too ugly might be enough to start me.

[Yaël Dillies]

Feel free to PR all that stuff or to tell me to.

[Joachim Breitner]

Thanks! I leave the PRing to you if you don't mind.

[Joachim Breitner]

@Yaël Dillies , this hasn’t made it towards master yet, has it?

[Yaël Dillies]

No, sorry! I'm really running low on time right now. The ITP paper deadline is today.

[Joachim Breitner]

Ok, paper deadline trumps impatient people on zulip. Maybe I can start a draft PR with the above code to take some load off you, but don't worry about it today then :-)

[Joachim Breitner]

Hmm, trying to fill in

lemma set.finite.minimals_nonempty [preorder α] {s : set α} (hs : s.finite) :
  (minimals (≤) s).nonempty ↔ s.nonempty :=

but I wonder if it’s true. If the preorder isn't an order, and you let s be two mutually related but unequal elements, then minimals (≤) s is empty.

But even with a preorder constraint my current attempt at proving this lemma failed; must have taking some wrong corner somewhere. Maybe tomorrow.

[Reid Barton]

I would be inclined to say that the definition of minimals is wrong--both elements should be minimal

[Floris van Doorn]

Yeah, I think the definition should be {a ∈ s | ∀ ⦃b⦄, b ∈ s → r b a → r a b} if you're working with a preorder.

[Yaël Dillies]

Yeah, I did that with docs#is_min and I forgot to copy over the idea to minimals

[Joachim Breitner]

I found this lemma in set which seems to do all the heavy lifting needed here already:

 theorem set.finite.exists_maximal_wrt {α : Type u} {β : Type v} [partial_order β] (f : α → β) (s : set α) (h : s.finite) :
  s.nonempty → (∃ (a : α) (H : a ∈ s), ∀ (a' : α), a' ∈ s → f a ≤ f a' → f a = f a')

and with that I can provide this instance directly, no induction needed:

instance fintype.to_is_atomic [partial_order α] [order_top α] [fintype α] : is_coatomic α :=
begin
  refine is_coatomic.mk (λ b, or_iff_not_imp_left.2 (λ ht, _)),
  obtain ⟨c, hc, hmax⟩ := set.finite.exists_maximal_wrt (λ x, x) { x : α | b ≤ x ∧ x ≠ ⊤ }
    (set.finite.of_fintype _) ⟨b, le_refl _, ht⟩,
  refine ⟨c, ⟨hc.2, λ y hcy, _⟩, hc.1⟩,
  by_contra hyt,
  have : c = y := hmax y ⟨le_trans hc.1 (le_of_lt hcy), hyt⟩ (le_of_lt hcy),
  subst this, convert (lt_self_iff_false _).mp hcy
end

I’ll PR this tomorrow if this is an ok approach

[Yaël Dillies]

Sounds great!

[Yaël Dillies]

le_refl _ = le_rfl

[Damiano Testa]

If this is interactive golf, then also le_of_lt hcy = hcy.le!

[Damiano Testa]

Also le_trans h ... = h.trans ...

[Yaël Dillies]

and (λ x, x) = id