finset members

Stream: new members

[Damiano Testa]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

But sometimes decidable_* is really powerful.

[Damiano Testa]

ok, I will do that!

[Johan Commelin]

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.

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

@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.

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Johan Commelin]

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.

[Damiano Testa]

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!

[Damiano Testa]

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