set tactic

Stream: metaprogramming / tactics

[Edward Lee]

@Peter Nelson , @Mathieu Guay-Paquet and I have been working off-and-on on a tactic for automatically discharging goals involving set equalities and inequalities. Sets come up often in matroid theory and in combinatorics, and we've gotten tired of manually solving these goals as they come up all the time and devolve into long rewrite chains using the set lemmas.

Ideally, we'd like to get some sort of set automation into mathlib eventually; we've (minimally) tried it out in our own work, but our tactic is nowhere near production ready. If anyone's interested, especially if you use sets on a regular basis, we would really appreciate it if you could give our tactic a spin and leave feedback: https://github.com/apnelson1/lean-set-tactic -- thanks!

[Mario Carneiro]

Once upon a time the finish tactic was intended for this

[Mario Carneiro]

is there more to it than ext; tauto?

[Mario Carneiro]

ideally the tauto tactic itself would be adapted to work on arbitrary boolean algebras

[Edward Lee]

We've found finish to be too slow and tauto doesn't fill in/automatically specialize forall hypotheses. It currently is a wrapper around tauto that repeatedly does ext, intro in some order and automatically fills in hypotheses.

[Mario Carneiro]

what kind of lemmas require you to fill foralls?

[Edward Lee]

we rewrite set constraints using set extensionality so that finish/tauto can work -- https://github.com/apnelson1/lean-set-tactic/blob/main/src/extensionality.lean -- which puts foralls everywhere.

[Mario Carneiro]

I see, so only the trivial kind, you aren't trying to actually solve arbitrary FOL problems

[Edward Lee]

our tactic started life as a thin wrapper around finish, and at least in an earlier commit we've found something like this broke tauto.

example (α : Type) [boolean_algebra α]  (A B C D E F G : α) :
  A ≤ B →
  B ≤ C →
  C ≤ D ⊓ E →
  D ≤ Fᶜ →
  (A ⊓ F = ⊥) :=
begin
  tactic.timetac "fast" $ `[(do
    types <- gather_types,
    types.mmap rewrite_for_type,
    tactic.skip),
  intros H1 H2 H3 H4,
  -- tauto!, -- here fails
  split; intros e;
  specialize (H1 e);
  specialize (H2 e);
  specialize (H3 e);
  specialize (H4 e); tauto!],
end

[Mario Carneiro]

If you have indexed unions or something then I can imagine real FOL stuff arising

[Mario Carneiro]

are you using an unusual has_mem instance to make that proof strategy work on arbitrary boolean algebras?

[Edward Lee]

no, we don't have that, though those do come up -- we're just trying to solve all the trivial set goals that come up all the time.

[Edward Lee]

and yeah, @Mathieu Guay-Paquet defined a has_mem for boolean algebras -- it's at priority 90 so it doesn't conflict with anything else.

[Mario Carneiro]

you can also make it a local instance if it's only needed for the tactic

[Edward Lee]

does local work across lean files in the same subfolder?

[Mario Carneiro]

no but you can use local attribute [instance] my_instance in all relevant files

[Mario Carneiro]

Also, you might not need the has_mem instance at all, if you just use le instead

[Mario Carneiro]

that is, you keep the boolalg_ext_lemmas but write the lemmas with universally quantified le

[Mario Carneiro]

and then it doesn't need to be a class, it can just be regular lemmas on boolean_algebra

[Mario Carneiro]

oh, you are using ultrafilters as members. Well the principle still applies

[Edward Lee]

yeah, I see, but IIRC we really wanted elements as we're mostly dealing with sets / finsets. @Mathieu Guay-Paquet wrote some technical lemmas using ultrafilters to get a notion of elements for boolean algebras which is why we've got has_mem.

[Edward Lee]

the various boolalg_ext_lemmas typeclasses is us using typeclass inference to automatically select the right set of lemmas to rewrite by.

[Mario Carneiro]

sure, but this is a tactic internal thing. I think the external view should just be, you need a boolean_algebra instance and that's it

[Edward Lee]

oh yeah for sure. The only thing this is meant to be external is the solver itself.

[Edward Lee]

We were going to hide all the special typeclasses somehow but we haven't gotten around to doing that yet.

[Edward Lee]

speaking of, is there a way to mark all definitions as local to a subfolder and its subdirectories or do we just have to use local attribute everywhere?

[Mario Carneiro]

so when you instantiate it on sets you will end up with some weird statements about ultrafilters of sets, but it doesn't matter as long as you have reduced everything to logic

[Mario Carneiro]

but again, it would be a lot more straightforward to just have tauto do what it does but with boolean algebra lemmas instead of prop calc

[Mario Carneiro]

You can put the local attributes in a locale and use open_locale to abbreviate a whole group of local instances and things

[Edward Lee]

Cool. Yeah, we talked to Rob earlier this year about tauto and his suggestion then was to wrap around tauto instead of modifying it as tauto looks complicated...

[Edward Lee]

We do try to avoid the ultrafilters on sets with instances of boolalg_ext_lemmas for set T and finset T so that the tactic does work as expected when the goal and hypothesis do have concrete sets and elements of those sets.

[Mario Carneiro]

I'm actually thinking of extending itauto for this instead of tauto, which is more of a heuristic procedure

[Mario Carneiro]

itauto is currently for intuitionistic logic only but you can easily make it complete for classical logic by starting with by_contradiction and then running itauto on the result

[Mario Carneiro]

in particular, itauto does all its work on a shadow syntax, and replays the proof over Prop. So it would not be hard to replay the proof over some other boolean algebra instead

[Mario Carneiro]

and hey, you get a heyting algebra prover for free

[Mario Carneiro]

(do we even have heyting algebras?)

[Bryan Gin-ge Chen]

There was a PR on them but it seems to be abandoned.

[Bryan Gin-ge Chen]

#5527

[Edward Lee]

Yeah, when we looked at tauto we thought maybe it would be easy to extend it but at the time it looked like it was really tied into Prop. The proofs for boolean algebras really ought to be the same as those for Prop so itauto ought to work well here.

[Edward Lee]

I guess all you'd really need to do is to select the boolean algebra/set/finset proof terms instead of the prop proof terms and you're all good.

[Edward Lee]

Cool, that's great to hear! Yeah, we really just wrap tauto, so a more principled way of dealing with boolean algebras is nice to have, and itauto already has the reflection infrastructure all set up.

[Bryan Gin-ge Chen]

BTW, Boolean algebras in mathlib were recently refactored so that they extend docs#generalized_boolean_algebra, which are basically Boolean algebras without a top. I don't know if that's relevant for your tactic though.

[Edward Lee]

I don't think it affects us too much but we could probably split how we deal with boolean algebras into those with top and those without (we have to do so anyways as finsets might not have top)

[Mario Carneiro]

also itauto is pretty good about only using the rules it actually needs to use to destruct the goal, so I think if the input doesn't reference top then it won't use any top rules

[Edward Lee]

@Mario Carneiro So on that note on itauto, now that I have a chance at looking at things again, what would be required to get it to work for boolean algebras/sets in detail? I figure I need new versions of reify and apply_proof specialized to the right terms, but I imagine there's some setup work in itauto itself that needs to change?

[Edward Lee]

Specifically, what do you think needs to change in here:https://github.com/leanprover-community/mathlib/blob/2b9aca75e6c1a1dc6b5b1b80734b05b3e07d193f/src/tactic/itauto.lean#L592-L643

[Mario Carneiro]

Since we last talked, itauto has grown the ability to prove classical theorems by using decidable instances and/or introducing its own

[Mario Carneiro]

Most of that code is constructing the initial context from the hypotheses, but it's not clear to me that this is still applicable in a different heyting algebra

[Mario Carneiro]

How would you do ND proofs in the target algebra? How is the context of assumptions encoded?

[Edward Lee]

I see...for us, our context would be the set of Props in the hypothesis tactic state that deal exclusively with sets and set membership. I imagine most of the ND rules for Prop would also hold over set (membership), after observing that P \subset Q <--> forall x, x \in P \implies x \in Q, with some fussing around necessary.

[Edward Lee]

Essentially I'm trying to figure out if we should keep our existing tactic and merge it in to mathlib or work something out a little cleaner using the infrastructure in itauto

[Mario Carneiro]

For set membership problems specifically, does it help to do simp [set.ext_iff, set.subset_def]; intro; itauto?

[Edward Lee]

Not really. I don't have a set membership example off hand, but this simplifies after simp [set.ext_iff, set.subset_def]; repeat {intro} to a set membership question:

example (α : Type*) [decidable_eq α] (A B C D E F G : set α) :
  A ⊆ B →
  B ⊆ C →
  C ⊆ D ∩ E →
  D ⊆ Fᶜ →
  (A ∩ F = (∅ : set α)) :=
begin
  /- tactic.timetac "slow" $ set_solver, -/
   simp [set.ext_iff, set.subset_def]; repeat {intro}, itauto,
end

[Edward Lee]

itauto fails in this state:

α: Type ?
_inst_1: decidable_eq α
ABCDEFG: set α
ᾰ: ∀ (x : α), x ∈ A → x ∈ B
ᾰ_1: ∀ (x : α), x ∈ B → x ∈ C
ᾰ_2: ∀ (x : α), x ∈ C → x ∈ D ∧ x ∈ E
ᾰ_3: ∀ (x : α), x ∈ D → x ∉ F
x: α
ᾰ_4: x ∈ A
ᾰ_5: x ∈ F
⊢ false

[Edward Lee]

Something like finish works here, probably I assume from instantiating the foralls in the hypothesis and deriving a contradiction.