Tactic For Subset/Union/Intersection Problems

Stream: new members

[Henning Dieterichs]

For my program verification proof, I'm currently dealing with many simple tautologies that only involve the equality and subset predicate, unions, intersections, and the empty set (for finset). However, these tautologies turned out to be ugly to prove with lean. After I struggled to library_search my way to close the goals, I figured I could just transform all my subset relations to implications and simplify everything to make it a propositional problem. finish was then able to close the goal. However, finish is quite slow in my case and the *_iff rewrites are also not super beautiful. Are there any recommendations on how to tackle such tautologies? Is there even a specialized tactic?

This is the set-part factored out of my lemma. Do you have ideas to improve this proof? Why is finish so slow here? Thanks ;)

example { α: Type } [decidable_eq α] { l1 l2 l3 l4: finset α }
    (h1: l4 ∩ (l1 ∪ l2) ⊆ l1 ∪ l3)
    (h2: disjoint l1 l2)
    : l4 ∩ l2 ⊆ l3 :=
begin
    rw finset.subset_iff,
    simp,
    assume x h3 h4,

    rw finset.subset_iff at h1,
    specialize @h1 x,

    simp [finset.disjoint_iff_inter_eq_empty, finset.subset.antisymm_iff, finset.subset_iff] at h2,
    specialize @h2 x,

    finish,
end

[Reid Barton]

This isn't really helpful but for set, it's easy to solve these things by hand:

lemma L { α: Type } { l1 l2 l3 l4: set α }
    (h1: l4 ∩ (l1 ∪ l2) ⊆ l1 ∪ l3)
    (h2: disjoint l1 l2)
    : l4 ∩ l2 ⊆ l3 :=
λ x ⟨h₄, h₂⟩, (h1 ⟨h₄, or.inr h₂⟩).resolve_left (λ h₁, h2 ⟨h₁, h₂⟩)

[Henning Dieterichs]

I'm still having a hard time writing term-style proofs. It feels like they require me to know a lot of details by heart.

[Kevin Buzzard]

I think you might be missing some tricks. You just build the proof using _s. [edit: sorry, I hadn't appreciated that it was finsets]

[Reid Barton]

It's true that you need to know a few things, but they are things that appear everywhere anyways

[Kevin Buzzard]

I can quite believe that for finset they're harder though, because fewer "obvious" things are definitional.

[Kevin Buzzard]

import tactic

open finset

example { α: Type } [decidable_eq α] { l1 l2 l3 l4: finset α }
    (h1: l4 ∩ (l1 ∪ l2) ⊆ l1 ∪ l3)
    (h2: disjoint l1 l2)
    : l4 ∩ l2 ⊆ l3 :=
begin
  simp_rw [subset_iff, mem_inter] at h1 ⊢,
  rintros x ⟨h4, h2'⟩,
  specialize h1 ⟨h4, subset_union_right _ _ h2'⟩,
  rw mem_union at h1,
  cases h1,
  { exfalso,
    have h12 : x ∈ l1 ∩ l2 := mem_inter.2 ⟨h1, h2'⟩,
    exact h2 h12 },
  { exact h1 },
end

[Kevin Buzzard]

If you know the names of lemmas then you can just knock off the proof but I totally appreciate that one might hope that automation could do this.

[Henning Dieterichs]

Oh, thanks! You used some tactics I didn't know yet, thanks for demonstrating them here! It is nice that you can prove stuff in lean without knowing much but then can improve your repertoire of techniques progressively. May I ask how long it took you to write that proof? Would you be able to write that proof without lean's info view?

[Kevin Buzzard]

Here is another proof which I wrote "on autopilot", changing the entire question to one in logic and solving it using cc:

import tactic

open finset

example { α: Type } [decidable_eq α] { l1 l2 l3 l4: finset α }
    (h1: l4 ∩ (l1 ∪ l2) ⊆ l1 ∪ l3)
    (h2: disjoint l1 l2)
    : l4 ∩ l2 ⊆ l3 :=
begin
  intro x,
  set p1 := x ∈ l1 with hp1,
  set p2 := x ∈ l2 with hp2,
  set p3 := x ∈ l3 with hp3,
  set p4 := x ∈ l4 with hp4,
  have H1 : p4 ∧ (p1 ∨ p2) → p1 ∨ p3,
    specialize @h1 x,
    simpa [hp1, hp2, hp3, hp4, mem_inter, mem_union] using h1,
  have H2 : p1 ∧ p2 → false,
    specialize @h2 x,
    simpa [hp1, hp2, hp3, hp4, mem_inter, mem_union] using h2,
  simp [← hp1, ← hp2, ← hp3, ← hp4, mem_inter, mem_union],
  cc,
end

[Kevin Buzzard]

I would definitely not be able to do anything without some editor such as emacs or VS Code but I did not use the infoview. The proof took me a couple of minutes to write but I looked at your proof to see the maths argument and then just rewrote it the way I would have written the maths argument.

[Kevin Buzzard]

One could envisage writing a tactic to construct the proof script which I wrote in the second proof.

[Henning Dieterichs]

Kevin Buzzard said:

I would definitely not be able to do anything without some editor such as emacs or VS Code but I did not use the infoview. The proof took me a couple of minutes to write but I looked at your proof to see the maths argument and then just rewrote it the way I would have written the maths argument.

This is really impressive! What do you need of Emacs/VS Code then, if not the info view and the unicode-input?

[Kevin Buzzard]

Oh sorry there's been a misunderstanding! I'm looking at the infoview all the time!

[Kevin Buzzard]

I thought you were asking specifically about the advanced widget functionality of the infoview as opposed to the generic output which one had for many years before the infoview appeared in 2020.

[Kevin Buzzard]

example (p1 p2 p3 p4 : Prop) : (p4 ∧ (p1 ∨ p2) → p1 ∨ p3) →
     (p1 ∧ p2 → false) → p4 ∧ p2 → p3 :=
begin
  cc,
end

The analogous question for propositions can be solved with a tactic.

[Kevin Buzzard]

Emacs doesn't have an infoview, it just has an output displaying the local context. This I certainly need! The infoview has more advanced functionality enabling you to carefully inspect the type or definition of a term by clicking on it. This I didn't use.

[Bryan Gin-ge Chen]

The infoview was called the infoview even before it had widgets.

[Bryan Gin-ge Chen]

(Hopefully this isn't making things more confusing.)

[Kevin Buzzard]

In VS Code the label at the top of the window didn't say Lean Infoview as far as I remember.

[Henning Dieterichs]

Ah, I see. But still impressive to come up with that in a couple of minutes! From my understanding, the "advanced" infoview currently does not offer that much over the classic infoview, or am I missing something? I neither used the advanced type display yet, except when hovering on identifiers in VS Code. But the term selection feature is handy to see the associativity.

[Kevin Buzzard]

I've been calling the Infoview the Infoview for as long as it said "Infoview" at the top which I thought coincided with widgets. Apologies for the confusion!

[Bryan Gin-ge Chen]

I think the label was changed before widgets were added, but it might have only been a few months before. So I suppose I probably only knew the official name from having edited "infoview.ts"...

[Kevin Buzzard]

In May the goal view was titled "Lean Goal" according to this old video I have lying around. I thought that when it changed to Lean Infoview was when widgets were added, and Infoview specifically meant the widgets. We live and learn!

[Kevin Buzzard]

The widget infoview doesn't offer much over the classic infoview in this setting for sure. There are times when it's really helpful though. Sometimes in my work I have to deal with goals where I've lost track of the types of various terms in the goal and then the widgets are a game-changer. Re: a couple of minutes. I didn't have to look up any of the names of the lemmas I used because these are all well-known to me now. I knew how to rewrite under binders; I also knew the maths proof and indeed I was just refactoring your code. I wasn't immediately sure how to deal with disjoint l1 l2 to prove false but the first thing I tried (treating it as [x in things] -> false) worked.

[Bryan Gin-ge Chen]

Kevin Buzzard said:

In May the goal view was titled "Lean Goal" according to this old video I have lying around. I thought that when it changed to Lean Infoview was when widgets were added, and Infoview specifically meant the widgets. We live and learn!

Oh, I checked the history and you're right! Originally, the infoview panel title was always "Lean Messages", and in February I changed it so that it was either "Lean Messages" or "Lean Goal" depending on whether it was displaying all server messages or just the tactic state + messages at the cursor. Then when Ed rewrote the infoview to use widgets in July, the title became "Lean Infoview". I wonder what the Lean 4 extension writers will settle on...

[Kevin Buzzard]

@Henning Dieterichs you have a CS background right? I'm sure a tactic turning questions about finsets into questions about propositions which can be solved with cc would be a tactic which would be welcomed! Of course in the short term learning how to write the tactic would take far longer than solving all your goals manually, but isn't that what CS people do? ;-)

[Henning Dieterichs]

Kevin Buzzard said:

Henning Dieterichs you have a CS background right? I'm sure a tactic turning questions about finsets into questions about propositions which can be solved with cc would be a tactic which would be welcomed! Of course in the short term learning how to write the tactic would take far longer than solving all your goals manually, but isn't that what CS people do? ;-)

Seems like you know CS people pretty well ;) @Peter Nelson has been working on a tactic already (that does not use cc afaik).

I'm concerned about ccs performance though. I pasted your example 50 times into test.lean (and nothing else) and lean test.lean takes a minute on my computer to finish. There are only 4 literals involved, so even a brute force proof with 16 goals should be checkable in way less than a second. 50 instances of your non-cc example only take 7 seconds to be validated...

[Kevin Buzzard]

Oh I think cc might be looking for a constructive proof. You can try finish or tauto! or something.

[Henning Dieterichs]

finish takes about 50 seconds, tauto! about 33. A refactoring that makes a finish explicit would be nice! (it should search for a shortest proof first though)

[Kevin Buzzard]

I could you can just case on whether each prop is true or false, and then use a carefully crafted simp set if you want to get things to go faster.

[Kevin Buzzard]

Hmm, I guess the moment you're casing on 4 T/F statements you have 2^4 theorems to prove. I don't know how any of these tactics work, I'm a mathematician, I just say it's left as an exercise to the reader :-)