Zulip Chat Archive

Stream: new members

Topic: finset members


view this post on Zulip Damiano Testa (Sep 22 2020 at 09:29):

Dear All,

I am trying to prove either one of the two lemmas below, but Lean is not allowing me to. I would like to convert set.mem_union_right ↑s, but I am not able to proceed from there. As usual, I imagine that Lean is obtaining different sources for something and cannot reconcile them, but I am not able to figure out what.

Thank you!

import tactic

lemma mem_in_union {α : Type*} [decidable_eq α] [has_union (finset α)] {s t : finset α} (x : α) : x  t  x  (s  t) :=
begin
  sorry,
end

lemma mem_in_union_singleton {α : Type*} [decidable_eq α] [has_union (finset α)] {s : finset α} (x : α) : x  (s  {x}) :=
begin
  sorry,
end

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:30):

You shouldn't need has_union... Lean should figure it out by itself.

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:30):

That indeed adds a second (unrelated, out-of-the-blue) notion of union for finset \a

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:32):

lemma mem_in_union {α : Type*} [decidable_eq α] {s t : finset α} (x : α) : x  t  x  (s  t) :=
begin
  library_search
end

view this post on Zulip Damiano Testa (Sep 22 2020 at 09:32):

I added has_union since Lean wanted it, but I will try to remove it again!

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:32):

The decidable_eq enables the union instance. Without it, lean can't find it. (But then, if you open_locale classical everything works again)

view this post on Zulip Damiano Testa (Sep 22 2020 at 09:33):

ah, I think that I added first has_union, prompted by Lean, and then added decidable_eq (again prompted by Lean)

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:33):

@Damiano Testa this is the "eternal(?)" conflict between proving and computing...

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:34):

I think, if you do maths, you should forget about the decidable_eq stuff, and just use open_locale classical at the top of your files.

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:34):

But sometimes decidable_* is really powerful.

view this post on Zulip Damiano Testa (Sep 22 2020 at 09:34):

ok, I will do that!

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:35):

E.g., if you want to know that squares mod 8 are equal to 0, 1, or 4, then dec_trivial will prove it for you.

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:35):

And that 1 line proof is of course a lot more convenient than whatever crazy case-split you would have to do otherwise.

view this post on Zulip Damiano Testa (Sep 22 2020 at 09:36):

ok, indeed, with open_locale classical i do not need to add decidable_eq!! Thank you very much!

view this post on Zulip Johan Commelin (Sep 22 2020 at 09:56):

@Damiano Testa What open_locale classical does, is that it makes every proposition decidable, using LEM. Of course it is "cheating" and using an axiom, and Lean knows this. So you can't use it to decide the truth of you favourite conjecture afterwards. But at the same time, Lean also won't get hung up on the fact that it doesn't know how to decide whether x \in s is true or not.

view this post on Zulip Patrick Massot (Sep 22 2020 at 10:42):

I don't understand why you write "cheating". This has nothing to do with cheating.

view this post on Zulip Johan Commelin (Sep 22 2020 at 10:42):

It is "cheating" in the sense that "decidable" no longer means what it usually means.

view this post on Zulip Patrick Massot (Sep 22 2020 at 10:43):

This command simply gives up hope to get Lean to compute a number of things. That's all. You can still do reasoning, without cheating, but you cannot compute.

view this post on Zulip Patrick Massot (Sep 22 2020 at 10:43):

The command says "don't try to use decidability".

view this post on Zulip Johan Commelin (Sep 22 2020 at 10:45):

If someone tells you that the Riemann Hypothesis is decidable, usually that would mean that you can run an algorithm and it will spit out true or false in the end. But if you have open_locale classical, then everything is decidable, and no such algorithms need to exist.

view this post on Zulip Damiano Testa (Sep 22 2020 at 12:00):

Well, there is an algorithm that spits out true if the Riemann hypothesis is true and false otherwise. Just no one seems to know which one it is, at the moment!

view this post on Zulip Damiano Testa (Sep 22 2020 at 12:00):

Anyway, I think that I am getting an idea of what is going on here: thank you!


Last updated: May 17 2021 at 22:15 UTC