(A ∪ B) ⊆ C

Stream: Is there code for X?

[Florent Schaffhauser]

Hi!

I'm looking at the following MWE:

import Mathlib.Tactic

theorem union {X : Type} (A B C : Set X) (hA : A ⊆ C ) (hB : B ⊆ C) : (A ∪ B) ⊆ C := by
  change ∀ x ∈ A ∪ B, x ∈ C
  intro x hx
  sorry

I know the first line is optional but I would like to know if there is a tactic that changes the goal to ∀ x ∈ A ∪ B, x ∈ C without having to enter this expression manually?

If I use simp in the above, the goal gets changed to A ⊆ C ∧ B ⊆ C.

[Sébastien Gouëzel]

You can unfold the definitions, with

    simp only [HasSubset.Subset, LE.le, Set.Subset]

[Sébastien Gouëzel]

Or do

  rw?

see what comes out, and decide that

  rw [Set.subset_def]

is probably a good pick.

[Florent Schaffhauser]

Thanks! rw? suggests many more options that simp? in this case.

[Sébastien Gouëzel]

simp? only uses lemmas that are tagged with simp in the library, while rw? will try to rewrite using all the lemmas in the library. So it will give a lot of noise, but you can be sure that what you want will be in the list.

[Florent Schaffhauser]

I noticed that #Set.Basic contains the following comment just above Set.subset_def.

-- TODO(Jeremy): write a tactic to unfold specific instances of generic notation?
theorem subset_def : (s ⊆ t) = ∀ x, x ∈ s → x ∈ t :=
  rfl
#align set.subset_def Set.subset_def

Is writing such a tactic still a current objective? I think this was written by @Jeremy Avigad, but perhaps a long time ago?

Is there a reason for not tagging this with dsimp or simp?

[Yaël Dillies]

Yes, you don't want every set inclusion to be unfolded. It is pretty rare to need unfolding it, even.

[Florent Schaffhauser]

OK! And how about an explicit tactic to unfold this kind of notation? I mean one that would work without knowing the name of the lemma (such as rw [Set.subset_def]).

[Yaël Dillies]

Do you want it to work without knowing what the result looks like? If not, you can use change ∀ _ ∈ _, _ ∈ _ or similar.

[Florent Schaffhauser]

Yes, indeed, when I use change ∀ x ∈ A ∪ B, x ∈ C, I get exactly what I want.

I just had in mind the case of a user who does not know that (A ∪ B) ⊆ C is definitionally equivalent to ∀ x ∈ A ∪ B, x ∈ C, how can they simplify or rewrite the goal?

Sebastien's suggestion to use rw? is great because it shows a list of things that one can use to rewrite the goal.

Now I am wondering about a tactic that would do that automatically. I think I understand why simp is not the way to go here. But the comment in the docs made me curious about how a tactic to unfold specific instances of generic notation would go. Specifically, its it already exists and, if so, what it is called :sweat_smile:

[Yaël Dillies]

You can always do dsimp [(· ⊆ ·)]and recursively unfold the instances that appear. It's tedious but it works.

[Yaël Dillies]

@Anand Rao Tadipatri has a tactic to unfold notation, although not in mathlib.

[Florent Schaffhauser]

Yaël Dillies said:

You can always do dsimp [(· ⊆ ·)]and recursively unfold the instances that appear. It's tedious but it works.

tactic 'dsimp' failed, nested error:
maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

But I do get something with simp [(· ⊆ ·)], namely (fun x x_1 => x ⊆ x_1) (A ∪ B) C which indeed is not so pleasant to look at.

[Florent Schaffhauser]

Yaël Dillies said:

Anand Rao Tadipatri has a tactic to unfold notation, although not in mathlib.

Sounds interesting! I'll take a look if I can find it.

[Anand Rao Tadipatri]

The unfold tactic that @Jovan Gerbscheid and I wrote is at std4#417. The tactic is meant to unfold one layer of definitions at a time, so it currently takes three invocations to unfold it all the way; but I just tested locally with a recursive version of the same tactic and now unfold' (occs := 1) A ∪ B ⊆ C changes the goal to

∀ ⦃a : X⦄, a ∈ A ∪ B → a ∈ C

in one step.

[Jovan Gerbscheid]

We could add an optional argument for how many times to unfold. Because for general notations like subset notation, the first unfolding turns it into Set.subset, which on its own is not very useful. Or instead we could tag certain lemmata as unfold lemmata, so that this unfolding is in one step.

[Jovan Gerbscheid]

@Anand Rao Tadipatri, what do we still need to do before we can merge this into Std?

[Florent Schaffhauser]

That's great! I look forward to being able to use this tactic :smile:

[Florent Schaffhauser]

Jovan Gerbscheid said:

Or instead we could tag certain lemmata as unfold lemmata, so that this unfolding is in one step.

For the users I have I mind (beginners who are familiar neither with mathlib nor with the mathematical content of the expression A ∪ B ⊆ C), I think that this option would be the best. But I understand that there might be others things to check before such a decision can be made.

[Jovan Gerbscheid]

Another idea would be to tag certain constants as unwanded/implementation detail. So in particular Set.mem, Set.subset, Add.add. Then if one unfolding step gets you to this constant, you unfold again.

[Jovan Gerbscheid]

We also have a library rewrite tactic which is basically a more general version of the unfold' tactic, allowing you to choose which lemma to rewrite with. This would probably give the rewrite into A ⊂ C ∧ B ⊂ C as the first option. The reason to also have a separate unfold tactic is that not all definitions have a corresponding rewrite lemma.

[Florent Schaffhauser]

Jovan Gerbscheid said:

We also have a library rewrite tactic which is basically a more general version of the unfold' tactic, allowing you to choose which lemma to rewrite with. This would probably give the rewrite into A ⊂ C ∧ B ⊂ C as the first option.

Yes, that's also what simp currently does :smile:

[Anand Rao Tadipatri]

Jovan Gerbscheid said:

Anand Rao Tadipatri, what do we still need to do before we can merge this into Std?

I have pushed a few minor formatting fixes, and I think the PR is now ready for review. In the future, I think the tactic could use some (non-essential) improvements to its syntax, as I have mentioned in a new comment on the PR.

[Anand Rao Tadipatri]

Jovan Gerbscheid said:

Another idea would be to tag certain constants as unwanded/implementation detail. So in particular Set.mem, Set.subset, Add.add. Then if one unfolding step gets you to this constant, you unfold again.

That sounds like a good idea. In this case, we want to unfold constants related to notation/typeclass instances.

[Eric Wieser]

I wonder if it makes sense to make the ext tactic work here; right now it only works on equalities, but you could imagine teaching it to do something similar on inequalities too (in practice, for sets / finsets / pi types it would just mean intro x)

[Terence Tao]

In your particular example, intro x; revert x works.

[Florent Schaffhauser]

But then you have to do intro x hx again, am I right?

[Florent Schaffhauser]

Maybe you mean to go back and forth between the two expressions :thinking:

[Terence Tao]

This was to answer your original question of how to perform change ∀ x ∈ A ∪ B, x ∈ C without actually writing out the expression. Obviously it would be redundant if your next step was to introduce variables again. One could imagine a tactic that intros all possible variables and then immediately reverts them in order to change the goal to one in which all quantified variables are made explicit, which could potentially have some pedagogical value perhaps.

[Eric Wieser]

Is there a reason you want to see the ∀ in the goal state? It's not there when you use ext on set equality

[Florent Schaffhauser]

Initially, I tried change ∀ x ∈ A ∪ B, x ∈ C because this is what I wanted in the specific case (A ∪ B) ⊆ C. But maybe there are better options, depending also on the local context.

For (A ∪ B) = C, I would expect (A ∪ B) ⊆ C ∧ C ⊆ (A ∪ B) to come out, which happens if we use rw [Set.Subset.antisymm_iff]. Then we use constructor and we are back to proving (A ∪ B) ⊆ C first.

theorem union {X : Type} (A B C : Set X) (hA : A ⊆ C ) (hB : B ⊆ C) (hC : C ⊆ A ∪ B) : (A ∪ B) = C := by
  rw [Set.Subset.antisymm_iff]  -- A ∪ B ⊆ C ∧ C ⊆ A ∪ B
  constructor
  sorry

Another option is to use rw [Set.ext_iff], which changes the goal (A ∪ B) = C to ∀ (x : X), x ∈ A ∪ B ↔ x ∈ C. So again with the quantifiers.

Both uses of the rw tactic were obtained following Sebastien Gouezel's suggestion rw? and choosing from the list.

Neither change A ∪ B ⊆ C ∧ C ⊆ A ∪ B nor change ∀ (x : X), x ∈ A ∪ B ↔ x ∈ C work in this case (produces a type mismatch).

A slightly modified version of Terence Tao 's suggestion also works here: running ext x; revert x on (A ∪ B) = C changes the goal to ∀ (x : X), x ∈ A ∪ B ↔ x ∈ C . Based on this, we could imagine a set tactic (or something) that runs intro x; revert x on inclusions and ext x; revert x on equalities?

Or the tactic could avoid making the quantifiers explicit, changing (A ∪ B) = C to A ∪ B ⊆ C ∧ C ⊆ A ∪ B first and, after constructor has been applied, changing (A ∪ B) ⊆ C to A ⊆ C ∧ B ⊆ C, which is what rw [Set.union_subset_iff] does.

I wonder what happens if one applies the unfold tactic of @Anand Rao Tadipatri and @Jovan Gerbscheid to the new statement above? The point would be to solve the goal by a succession of unfold, constructor and assumption only.

One final (very minor) question I have is whether it is preferable, in the examples above, to use rw [@Set.ext_iff] as opposed to rw[Set.ext_iff]? Both seem to work in this particular case, but maybe in general the version with @ deals better with implicit variables?

[Ruben Van de Velde]

The version with the @ is an artifact of the rw? tactic; generally I'd remove it

[Ruben Van de Velde]

Also note the difference between ⊂ and ⊆

[Florent Schaffhauser]

Oh, yes, thanks, I'll edit my previous message :+1:

[Florent Schaffhauser]

Still, change A ∪ B ⊆ C ∧ C ⊆ A ∪ B does not rewrite A ∪ B = C, if I'm not mistaken.

[Ruben Van de Velde]

Well, no, you're expecting rather too much from change. change only works with definitional equality; you could try convert_to A ∪ B ⊆ C ∧ C ⊆ A ∪ B and then apply? will likely find the correct lemma

[Jovan Gerbscheid]

Equality is not a constant that can be unfolded definitionally, so unfold' wouldn't be of use there.

[Jovan Gerbscheid]

Although it seems like a good idea to have unfold' try to apply extensionality if other things fail, because people usually think of set extensionality as the "definition" of equality on sets.

[Florent Schaffhauser]

Indeed. But as you say, unfold' should probably try to apply extensionality only if others things fail, not as a first option.

[Florent Schaffhauser]

But based on the discussion we have been having in this thread, I now think that to avoid having ∀ in the goal state might be better.

So I would hope for a tactic that does the following rw automatically (simp takes care of the second one, but not the first one).

theorem union {X : Type} (A B C : Set X) (hA : A ⊆ C ) (hB : B ⊆ C) (hC : C ⊆ A ∪ B) : (A ∪ B) = C := by {
  rw [Set.Subset.antisymm_iff]
  constructor
  rw [Set.union_subset_iff]  -- simp also works
  constructor
  assumption
  assumption
  assumption
}

[Jovan Gerbscheid]

Since the rewrite of set equality that you want is a very natural one, but not the most natural one (which would be extensionality), I would suggest a tactic that gives you multiple options, where the rewrite you want is the first or second option. The targeted library rewrite that @Anand Rao Tadipatri and I have would do this.

[Jovan Gerbscheid]

A separate anti_symm tactic could also solve this, but maybe that would be too specific.

[Florent Schaffhauser]

Indeed, that would probably be too specific. I'll look forward to trying out your library rewrite!

[Jovan Gerbscheid]

I tend to think of extensionality lemmas as Iff statements, but it turns out that unfortunately the extensionality lemmas used by ext are all implications, meaning that I can't use them for rewriting arbitrary sub-expressions, which is what I want with the unfold' tactic.

[Kevin Buzzard]

The iff statements are usually called ext_iff.

[Eric Wieser]

There are a lot of ext lemmas with no corresponding ext_iff lemmas; maybe we should be generating one from the other?

[Eric Wieser]

(usually the reverse direction is a trivial substitution)

[Jovan Gerbscheid]

Kevin Buzzard said:

The iff statements are usually called ext_iff.

I could make the tactic rely on this naming convention: get the name of the type, add ext_iff to the name, and see if this gives a lemma that applies. Would such a hacky approach be accepted?

[Eric Wieser]

I think that probably would not be accepted, it would be better to have the ext attribute include information about where to find the iff lemma

[Eric Wieser]

I think it's ok for an attribute to use heuristics to generate a lookup table, but using heuristics during the lookup seems likely to be fragile

[Eric Wieser]

The former lets you emit an error at the point someone tries to register an ext (iff) lemma if they make a typo, the latter just silently fails

[Dan Velleman]

For How To Prove It with Lean, I wrote a tactic that writes out definitions. Examples of what it does:

• It changes the example that started this discussion, A ∪ B ⊆ C (where A, B, and C have type Set X), into ∀ ⦃a : X⦄, a ∈ A ∪ B → a ∈ C.
• It changes a ∈ A ∪ B into a ∈ A ∨ a ∈ B.
• It changes a ∣ b (where a and b are integers) into ∃ (c : ℤ), b = a * c.

The function that does most of the work of my tactic is similar to whnf. (In fact, I think a tactic that simply called whnf on an expression would do a pretty good job of writing out definitions.) The function repeatedly calls Lean.Meta.whnfCore and Lean.Meta.unfoldDefinition?. At each step, it does some additional checks. Perhaps most significantly, it checks to see if the expression has the form "not (something)". If so, it leaves the "not" there and tries to write out the definition of "something." As a result, not only will it change a ∈ A ∪ B into a ∈ A ∨ a ∈ B, it will also change a ∉ A ∪ B into ¬(a ∈ A ∨ a ∈ B). There are also special checks to prevent certain unfoldings that could be confusing to beginners. For example, "if-then-else" statements unfold to something unreadable, so they don't get unfolded. A statement of the form x ∈ A would unfold to A x, so this unfolding is prevented.

[Jovan Gerbscheid]

This is exactly what the unfold' tactic does as well. I don't understand though how it changes a ∈ A ∪ B into a ∈ A ∨ a ∈ B using just whnf and unfolding definition. Where can i see the code?

[Dan Velleman]

I wrote a version of the tactic that lists all the steps it went through in writing out a definition. Here are the steps in writing out the definition of a ∈ A ∪ B:

dfn_1: a ∈ A ∪ B ↔ Set.instMembershipSet.1 a (A ∪ B)
dfn_2: a ∈ A ∪ B ↔ Set.Mem a (A ∪ B)
dfn_3: a ∈ A ∪ B ↔ (A ∪ B) a
dfn_4: a ∈ A ∪ B ↔ Set.instUnionSet.1 A B a
dfn_5: a ∈ A ∪ B ↔ Set.union A B a
dfn_6: a ∈ A ∪ B ↔ setOf (fun (a : U) => a ∈ A ∨ a ∈ B) a
dfn_7: a ∈ A ∪ B ↔ (fun (a : U) => a ∈ A ∨ a ∈ B) a
dfn_8: a ∈ A ∪ B ↔ a ∈ A ∨ a ∈ B

The code is in the Lean package that accompanies How To Prove It with Lean, which is here:
https://github.com/djvelleman/HTPILeanPackage
The tactic definitions are in the file HTPILib.HTPIDefs, and the main function for the define tactic is called unfoldHeadCore.

[Dan Velleman]

I'm a little embarrassed to have anyone look at the code, because it's so full of kludges.

[Jovan Gerbscheid]

I just realized that whnf does the same simplification of a ∈ A ∪ B. The difference with the unfold' tactic is that this only does one layer of unfolding at a time. It just so happens to be in this case that doing all unfolding gets you to the most natural unfolding.

[Jovan Gerbscheid]

It's a bit awkward that I can't build in special unfold behaviour for set containment since sets are defined in Mathlib, and we're pr-ing this tactic to std.