Zulip Chat Archive

Stream: Is there code for X?

Topic: Simple set theory nonsense


view this post on Zulip Adam Topaz (Oct 06 2020 at 15:11):

Is there some tactic that will solve goals of the form

C  (A  B) = A  (B  C)

where A B C : set X ?

view this post on Zulip Simon Hudon (Oct 06 2020 at 15:13):

by ext; tauto!

view this post on Zulip Anne Baanen (Oct 06 2020 at 15:13):

Or by finish

view this post on Zulip Reid Barton (Oct 06 2020 at 15:13):

I think @Chris Hughes also had some incantation that involved finish with some extra arguments

view this post on Zulip Anne Baanen (Oct 06 2020 at 15:15):

This works for me though:

example {α : Type*} {a b c : set α} : c  (a  b) = a  (b  c) := by finish

view this post on Zulip Adam Topaz (Oct 06 2020 at 15:15):

Thanks. finish worked.

view this post on Zulip Adam Topaz (Oct 06 2020 at 15:16):

It had a hard time with this though AA ∩ Q ∩ (AA ∩ Q1) = AA ∩ (Q ∩ Q1).

view this post on Zulip Reid Barton (Oct 06 2020 at 15:18):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/set.20tactic/near/186732870

view this post on Zulip Adam Topaz (Oct 06 2020 at 15:24):

To be fair, I'm using it in a proof that's ~130 lines long, and it fails with a deterministic timeout.

view this post on Zulip Adam Topaz (Oct 06 2020 at 15:26):

But this small example also fails:

example {α : Type*} (a b c : set α) : a  b  (a  c) = a  (b  c) := by finish [set.ext_iff]

view this post on Zulip Adam Topaz (Oct 06 2020 at 15:26):

This fails too :(

example {α : Type*} (a b c : set α) : a  b  (a  c) = a  (b  c) := by ext; tauto!

view this post on Zulip Adam Topaz (Oct 06 2020 at 15:27):

example {α : Type*} (a b c : set α) : a  b  (a  c) = a  (b  c) := by tidy

That works!

view this post on Zulip Reid Barton (Oct 06 2020 at 15:28):

Adam Topaz said:

But this small example also fails:

example {α : Type*} (a b c : set α) : a  b  (a  c) = a  (b  c) := by finish [set.ext_iff]

Interesting, I thought I tried that exact example, but actually what I tried was c ∩ (a ∩ b) = (c ∩ a) ∩ (b ∩ c)


Last updated: May 07 2021 at 22:14 UTC