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: May 09 2021 at 19:11 UTC