## Stream: general

### Topic: tactic for set-theoretic trivialities

#### 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)

#### Kevin Buzzard (May 21 2018 at 10:24):

Is there a tactic which solves them?

[these are sets]

#### Kevin Buzzard (May 21 2018 at 10:25):

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

#### Andrew Ashworth (May 21 2018 at 10:25):

by finish?

#### Kevin Buzzard (May 21 2018 at 10:25):

didn't work for me for this one

#### Kevin Buzzard (May 21 2018 at 10:27):

cc and simp don't work either

#### 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]

#### Kenny Lau (May 21 2018 at 10:30):

solve_by_elim?

#### 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

#### Kevin Buzzard (May 21 2018 at 10:33):

solve_by_elim doesn't work

#### Mario Carneiro (May 21 2018 at 10:33):

I think finish was intended to work on those goals

#### Mario Carneiro (May 21 2018 at 10:34):

but you may need to use its options

#### 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}


#### 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?

#### Patrick Massot (May 21 2018 at 10:38):

by finish[set.subset_def] also works

#### Mario Carneiro (May 21 2018 at 10:39):

it works on the boolean algebra of propositions...

#### Mario Carneiro (May 21 2018 at 10:39):

that's why subset_def is needed here

#### Kenny Lau (May 21 2018 at 10:46):

people just bloody abusing finish

#### Kevin Buzzard (May 21 2018 at 10:46):

We're too classical for you

#### Kevin Buzzard (May 21 2018 at 10:47):

Do you think it's true in constructive maths?

#### Kevin Buzzard (May 21 2018 at 10:47):

I would have no idea :-)

of course it is

:-)

#### Kenny Lau (May 21 2018 at 10:47):

they're literally the same set

#### Kevin Buzzard (May 21 2018 at 10:47):

yeah but you never know with this constructive maths thing

#### 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

#### Kevin Buzzard (May 21 2018 at 10:47):

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

#### Kenny Lau (May 21 2018 at 10:48):

t r i g g e r e d

#### Kevin Buzzard (May 21 2018 at 10:48):

Shouldn't you be revising for mechanics?

#### Kenny Lau (May 21 2018 at 10:48):

I see that you're proving mul_add

#### Kenny Lau (May 21 2018 at 10:48):

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

#### Patrick Massot (May 21 2018 at 10:48):

Shouldn't you be marking?

#### Kenny Lau (May 21 2018 at 10:48):

I think equality is eaiser to prove

#### Kenny Lau (May 21 2018 at 10:48):

Shouldn't you be marking?

oooooooh

#### Kevin Buzzard (May 21 2018 at 10:48):

I've just proved something is a ring!

#### Kevin Buzzard (May 21 2018 at 10:49):

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

[:= v happy]

#### Kevin Buzzard (May 21 2018 at 10:49):

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

oh wait

#### Kevin Buzzard (May 21 2018 at 10:50):

I think O_X(U) is a ring!

#### Kevin Buzzard (May 21 2018 at 10:50):

I still have to prove restriction is a ring homomorphism though

#### Kevin Buzzard (May 21 2018 at 10:50):

I will save that for after some marking

#### 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

#### Kevin Buzzard (May 21 2018 at 10:52):

Why is quot.lift called that?

#### Kevin Buzzard (May 21 2018 at 10:52):

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

It's a descent

#### Patrick Massot (May 21 2018 at 10:52):

I remember being puzzled by this terminology while reading TPIL

#### 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

#### Kevin Buzzard (May 21 2018 at 10:52):

This name was not at all intuitive for me

Obviously

#### Kevin Buzzard (May 21 2018 at 10:53):

Is this a CS thing Patrick?

No idea

#### Patrick Massot (May 21 2018 at 10:53):

Just crazyness if you ask me

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

#### Sean Leather (May 21 2018 at 11:02):

LeanerLea(r)ner

Last updated: Dec 20 2023 at 11:08 UTC