How to use the simplifier?

Stream: general

[Kevin Buzzard]

I never use simp really, because I don't understand how it works. Here is a simple example from this thread where I write a simple 7 line tactic mode proof of something which any mathematician would be able to work out in their head.

import tactic

universes u v

open set

-- Say X and Y are types, U=univ is a subset of X
-- and V is a subset of Y. If C is a subset of X × Y
-- such that U × V is in the complement of C, then
-- V is in the complement of the projection of C down to Y.
-- Maths proof : "if you can't solve this, you shouldn't be taking my class"
-- Alternate maths proof: "draw a rectangle".

example (X : Type u) (Y : Type v) (U : set X) (hXU : univ ⊆ U)
  (V : set Y) (C : set (X × Y)) (hUV : set.prod U V ⊆ -C) :
  V ⊆ -(prod.snd '' C) :=
-- my Lean proof:
begin
  -- Suppose for a contradiction that the intersection is non-empty.
  -- Then we must have an element of C whose second component is in V
  rintros v hvV ⟨uv, huv, rfl⟩,
  -- To get the contradiction it suffices to prove that this element is in U × V
  revert huv,
  apply hUV,
  -- so we need to check its first component is in U and its second is in V
  rw set.mem_prod,
  split,
    -- but U is all of X so the first component must be in U
    apply hXU, apply set.mem_univ,
  -- and by assumption the second component is in V
  exact hvV,
  -- so done
end

I am in the middle of a big tactic mode proof so I can't really massage the hypotheses and there's no advantage slipping into term mode.

I observe that (a) this proof is pretty simple; (b) both of the theorems I use from data.set.basic (mem_prod and mem_univ) are tagged @[simp] (and one proof is iff.rfl and the other is trivial); (c) simp * at * doesn't work.

Now what I don't really understand is whether I should even be expecting the simplifier to solve this little logic puzzle, even though the proof looks very much "follow your nose". I don't even know if simp [hXU, hUV] is meaningful -- it compiles, it doesn't solve the goal. Is this clearly too much for the simplifier? Does the simplifier only prove goals of the form X = Y and only in the situation where subterms of X can be rewritten using simp lemmas until X becomes Y? How should I be solving this goal in fewer than 7 lines? What would a mathlib proof of this look like? This is a big hole in my understanding of how to write mathlib-ready Lean code and it's things like this which are a major contributor to the fact that I've not written more mathlib code.

[Kevin Buzzard]

Hmm:

begin
  rintros v hvV ⟨uv, huv, rfl⟩,
  exact hUV ⟨hXU (set.mem_univ _), hvV⟩ huv,
end

Maybe I'm barking up the wrong tree and I should just concentrate on building terms as compactly as possible.

[Mario Carneiro]

Perhaps this helps.

example (X : Type u) (Y : Type v) (U : set X) (hXU : univ ⊆ U)
  (V : set Y) (C : set (X × Y)) (hUV : set.prod U V ⊆ -C) :
  V ⊆ -(prod.snd '' C) :=
begin
  simp [subset_def] at *,
  exact λ v hvV u, hUV _ _ (hXU _) hvV,
end

[Mario Carneiro]

Note the goal after the first line

[Mario Carneiro]

Basically, simp has a whole bunch of basic unfolding type rules in its database, and we just apply everything until it stops changing. Now subset is not usually a thing you want to unfold eagerly, however once you have membership there are a whole bunch of simp lemmas that can trigger, to unfold what it means for something to be an element of a complicated set. So here it cleans up all the unions and images and complements, but it hasn't really done anything with the "logic" part - you still have to plumb hXU and hvV together, but it is much more obvious what to do this time

[Mario Carneiro]

Because these are almost all definitional simplifications, the direct term proof is not much longer in this case. The only real change is you don't have to do that rcases with <a, rfl> dance

[Mario Carneiro]

Your second proof is almost exactly what I would have used for the mathlib proof of this. (I would have used by and squeezed it on one line because it's basically a short term proof.) I wouldn't use the simp proof because that is slower and the savings in proof size are minimal here