tactic for set-theoretic trivialities

Stream: general

[Kevin Buzzard]

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

[Kevin Buzzard]

Is there a tactic which solves them?

[Kevin Buzzard]

[these are sets]

[Kevin Buzzard]

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

[Andrew Ashworth]

by finish?

[Kevin Buzzard]

didn't work for me for this one

[Kevin Buzzard]

cc and simp don't work either

[Kevin Buzzard]

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

[Kenny Lau]

solve_by_elim?

[Kevin Buzzard]

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]

solve_by_elim doesn't work

[Mario Carneiro]

I think finish was intended to work on those goals

[Mario Carneiro]

but you may need to use its options

[Mario Carneiro]

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

[Andrew Ashworth]

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

[Patrick Massot]

by finish[set.subset_def] also works

[Mario Carneiro]

it works on the boolean algebra of propositions...

[Mario Carneiro]

that's why subset_def is needed here

[Kenny Lau]

people just bloody abusing finish

[Kevin Buzzard]

We're too classical for you

[Kevin Buzzard]

Do you think it's true in constructive maths?

[Kevin Buzzard]

I would have no idea :-)

[Kenny Lau]

of course it is

[Kevin Buzzard]

:-)

[Kenny Lau]

they're literally the same set

[Kevin Buzzard]

yeah but you never know with this constructive maths thing

[Patrick Massot]

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]

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

[Kenny Lau]

t r i g g e r e d

[Kevin Buzzard]

Shouldn't you be revising for mechanics?

[Kenny Lau]

I see that you're proving mul_add

[Kenny Lau]

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

[Patrick Massot]

Shouldn't you be marking?

[Kenny Lau]

I think equality is eaiser to prove

[Kenny Lau]

Shouldn't you be marking?

oooooooh

[Kevin Buzzard]

I've just proved something is a ring!

[Kevin Buzzard]

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

[Kevin Buzzard]

[:= v happy]

[Kevin Buzzard]

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

[Kevin Buzzard]

oh wait

[Kevin Buzzard]

I think O_X(U) is a ring!

[Kevin Buzzard]

I still have to prove restriction is a ring homomorphism though

[Kevin Buzzard]

I will save that for after some marking

[Kevin Buzzard]

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]

Why is quot.lift called that?

[Kevin Buzzard]

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

[Kevin Buzzard]

It's a descent

[Patrick Massot]

I remember being puzzled by this terminology while reading TPIL

[Kevin Buzzard]

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

[Kevin Buzzard]

This name was not at all intuitive for me

[Patrick Massot]

Obviously

[Kevin Buzzard]

Is this a CS thing Patrick?

[Patrick Massot]

No idea

[Patrick Massot]

Just crazyness if you ask me

[Kevin Buzzard]

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]

LeanerLea(r)ner