Zulip Chat Archive

Stream: general

Topic: tactic for set-theoretic trivialities


view this post on Zulip Kevin Buzzard (May 21 2018 at 10:24):

I am beginning to tire of goals of the form Ua ∩ Ub ∩ Uc ⊆ Ua ∩ Ub ∩ (Ua ∩ Uc)

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:24):

Is there a tactic which solves them?

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:24):

[these are sets]

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:25):

[let me stress that I can solve them, it's just the novelty is wearing off]

view this post on Zulip Andrew Ashworth (May 21 2018 at 10:25):

by finish?

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:25):

didn't work for me for this one

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:27):

cc and simp don't work either

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:27):

[Prediction : in about 8 hours Scott wakes up and remarks that one of his secret tactics does the job immediately]

view this post on Zulip Kenny Lau (May 21 2018 at 10:30):

solve_by_elim?

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:32):

Note that any such tactic will have to deal with the fact that exact ⟨Ha,Hb,⟨Ha,Hc⟩⟩ is not a proof of y ∈ Ua ∩ Ub ∩ (Ua ∩ Uc) because of stupid left associativity of \cap

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:33):

solve_by_elim doesn't work

view this post on Zulip Mario Carneiro (May 21 2018 at 10:33):

I think finish was intended to work on those goals

view this post on Zulip Mario Carneiro (May 21 2018 at 10:34):

but you may need to use its options

view this post on Zulip Mario Carneiro (May 21 2018 at 10:36):

example {α} (Ua Ub Uc : set α) : Ua ∩ Ub ∩ Uc ⊆ Ua ∩ Ub ∩ (Ua ∩ Uc) :=
by simp [set.subset_def] {contextual := tt}

view this post on Zulip Andrew Ashworth (May 21 2018 at 10:38):

it reminds me I don't know what finish solves. Does it work on any boolean algebra?

view this post on Zulip Patrick Massot (May 21 2018 at 10:38):

by finish[set.subset_def] also works

view this post on Zulip Mario Carneiro (May 21 2018 at 10:39):

it works on the boolean algebra of propositions...

view this post on Zulip Mario Carneiro (May 21 2018 at 10:39):

that's why subset_def is needed here

view this post on Zulip Kenny Lau (May 21 2018 at 10:46):

people just bloody abusing finish

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:46):

We're too classical for you

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:47):

Do you think it's true in constructive maths?

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:47):

I would have no idea :-)

view this post on Zulip Kenny Lau (May 21 2018 at 10:47):

of course it is

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:47):

:-)

view this post on Zulip Kenny Lau (May 21 2018 at 10:47):

they're literally the same set

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:47):

yeah but you never know with this constructive maths thing

view this post on Zulip Patrick Massot (May 21 2018 at 10:47):

Using finish does not only finishes the goal. It also conveys the meaning that the goal is now something we don't want to discuss at all

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:47):

I mean not not P is literally the same as P, right?

view this post on Zulip Kenny Lau (May 21 2018 at 10:48):

t r i g g e r e d

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:48):

Shouldn't you be revising for mechanics?

view this post on Zulip Kenny Lau (May 21 2018 at 10:48):

I see that you're proving mul_add

view this post on Zulip Kenny Lau (May 21 2018 at 10:48):

can't you prove that the two sets are equal instead?

view this post on Zulip Patrick Massot (May 21 2018 at 10:48):

Shouldn't you be marking?

view this post on Zulip Kenny Lau (May 21 2018 at 10:48):

I think equality is eaiser to prove

view this post on Zulip Kenny Lau (May 21 2018 at 10:48):

Shouldn't you be marking?

oooooooh

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:48):

I've just proved something is a ring!

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:49):

I'm sitting on the tube platform at South Ken, completely elated

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:49):

[:= v happy]

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:49):

Now if only someone had proved that a product of rings was a ring

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:50):

oh wait

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:50):

I think O_X(U) is a ring!

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:50):

I still have to prove restriction is a ring homomorphism though

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:50):

I will save that for after some marking

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:51):

What I am actually pleased about is that I seriously engaged with quotient types for the first time in my life, and I have come out alive

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:52):

Why is quot.lift called that?

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:52):

It's the opposite of a lift, the way things are set up in my brain

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:52):

It's a descent

view this post on Zulip Patrick Massot (May 21 2018 at 10:52):

I remember being puzzled by this terminology while reading TPIL

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:52):

I think that this observation was genuinely something which added to my confusion when looking at quotient type stuff

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:52):

This name was not at all intuitive for me

view this post on Zulip Patrick Massot (May 21 2018 at 10:52):

Obviously

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:53):

Is this a CS thing Patrick?

view this post on Zulip Patrick Massot (May 21 2018 at 10:53):

No idea

view this post on Zulip Patrick Massot (May 21 2018 at 10:53):

Just crazyness if you ask me

view this post on Zulip Kevin Buzzard (May 21 2018 at 10:54):

Anyway, we live and learn, and I've certainly learnt something over the last couple of days. Thanks to everyone that helped. I genuinely feel like a better Leaner.

view this post on Zulip Sean Leather (May 21 2018 at 11:02):

LeanerLea(r)ner


Last updated: May 09 2021 at 19:11 UTC