Zulip Chat Archive

Stream: general

Topic: cleaning iff

Patrick Massot (Aug 27 2019 at 09:47):

@Jeremy Avigad in particular: another area (besides calculations) where I'm always angry about automation is many proofs that are only unpackaging and repackaging stuff. The following is an example abstracted from a topological groups and filter context:

example {α : Type*} [has_sub α] (S T : set $ set α) :
 ( {V : set α}, V  S  ( (t : set α) (H : t  T), set.prod t t  (λ (x : α × α), x.2 - x.1) ⁻¹' V)) 
     (U : set α), U  S  ( (M : set α) (H : M  T),  (x y : α), x  M  y  M  y - x  U) := sorry

Patrick Massot (Aug 27 2019 at 09:48):

This has no mathematical content (in the sense that a mathematician wouldn't understand what requires a proof here).

Patrick Massot (Aug 27 2019 at 09:50):

What I would like Lean to do is at least to peel-off layers that are common to both lines.

Patrick Massot (Aug 27 2019 at 09:50):

Note that in this specific example, by simp [subset_def] works.

Patrick Massot (Aug 27 2019 at 09:53):

But it takes time to reach that conclusion. I also experimented writing the following stupid tactic:

open tactic
meta def clean_step : tactic unit :=
do tgt  target,
   match tgt with
   | `(%%a  %%b) := `[intros]
   | `(%%a  %%b) := match a with
                     | `(%%c  %%d) := if c.has_var then `[apply imp_congr] else `[apply forall_congr]
                     | `(Exists %%c) := `[apply exists_congr]
                     | _ := `[exact iff.rfl]
   | _ := fail "Goal is not a forall, implies or iff"

meta def tactic.interactive.clean_iff : tactic unit := do repeat clean_step

doing the peeling-off. In the example above, it reduces the goal to set.prod s s ⊆ (λ (x : α × α), x.snd - x.fst) ⁻¹' a ↔ ∀ (x y : α), x ∈ s → y ∈ s → y - x ∈ a which can be closed by library_search, which is pretty good I think. Should we try to make a smarter version of that tactic?

Johan Commelin (Aug 27 2019 at 10:04):

I've wanted such a "mild" congr tactic as well.

Reid Barton (Aug 27 2019 at 13:04):

This does feel like something within the scope of congr

Jeremy Avigad (Aug 27 2019 at 13:41):

I have had to do similar things, with crazy lambdas and corner brackets. It is funny how much of mathematics is just unpacking and repacking information. This is something that a decent tableau prover should do. (I am disappointed that finish is no help.) It is worth experimenting to see how useful a congr-like tactic is, though eventually it would be nice to see this subsumed by general automation.

Patrick Massot (Aug 27 2019 at 13:42):

I have no opinion about what kind of automation should do it, I only say I don't want to do it.

Patrick Massot (Aug 27 2019 at 13:46):

Here is my short answer to your "automation for the working mathematician" wish-list question:

  • elaboration that works, including coercions, especially to functions, and type class resolution
  • calculations where I only give the intermediate steps I would write on paper, using ring, abel and their non-existent extensions to other algebraic structures, and non-linear linarith
  • packing/unpacking stuff

Jeremy Avigad (Aug 27 2019 at 13:58):

Thanks! I really am taking notes and gathering all the comments I received.

Patrick Massot (Aug 27 2019 at 14:02):

I would have never guessed that when I started Lean and everything was confusing, but today it's clear that elaboration is by far the most important aspect. I spend most of my wasted time fighting the elaborator (and parser maybe).

Johan Commelin (Aug 27 2019 at 14:03):

With good-old-paper-maths you could offload those fights to the reader (-;

Patrick Massot (Aug 27 2019 at 14:03):

This and so many other boring details

Johan Commelin (Aug 27 2019 at 14:03):

The elaborator is the formalisation of "left as an exercise for the reader" :stuck_out_tongue_wink:

Jeremy Avigad (Aug 27 2019 at 14:09):

One important question is what should be done by the elaborator and what should be done by automation at a later stage. The elaborator should be focused on filling in information that is absolutely essential to make sense of an expression. It may be putting too much of a burden on the elaborator to expect it to prove that an operation is commutative or a set is finite. Maybe that is best done by another process later on, that acts when all the implicit data has been inferred.

Patrick Massot (Aug 27 2019 at 14:14):

Let me prove once more that I have no idea how type classes work, and ask: why is it stupid to insert the following two mechanisms into type class search:

  • allow to write instance_for `X my_class := explicit_instance or by apply_instance where, as usual, `X is a name. Then every type Lean wants to infer an instance for my_type X use the database created by that line.
  • If the previous method fails, class search [my_class X Y Z...] by a search by name head_symbol_of_X.class_name

If both fail then use the current algorithm. To me it sounds like this would solve most of the cases where Lean fails or take forever to find an instance. For instance we have files in the perfectoid space where K denotes a field, and it does so for 1000 lines. And each proof involves Lean searching at least twice for comm_ring K. It sounds like looking at a hash table under key K would be much faster.

Patrick Massot (Aug 27 2019 at 14:20):

I don't think I want to put a burden on the elaborator. I only want coercions and type class search to do their jobs. And also, I'd like the elaborator to stop thinking every numeral is in nat

Sebastian Ullrich (Aug 27 2019 at 14:59):

@Patrick Massot Adding a head index (i.e. exactly what simp uses) to the instance search is definitely something we have been thinking about. Though I believe Leo already has new plans for the whole algorithm we haven't talked about yet, so I won't speculate any further for now.

Johan Commelin (Aug 27 2019 at 14:59):

Does that mean it will only become as slow as simp is? (See the other thread...)

Sebastian Ullrich (Aug 27 2019 at 14:59):


Johan Commelin (Aug 27 2019 at 15:00):


Patrick Massot (Aug 27 2019 at 15:00):

I'm pretty sure you have thought about all that. I was honestly asking why things are not that simple.

Sebastian Ullrich (Aug 27 2019 at 15:01):

But generally speaking, it's not immediately clear how exactly the index should work: Does it only index a single parameter of the class? Is it always the first one? Or does this need to be customizable, by an attribute on the class?

Sebastian Ullrich (Aug 27 2019 at 15:02):

I'm sure there are some examples in mathlib where indexing by the first parameter would not be optimal

Patrick Massot (Aug 27 2019 at 15:03):

I guess that using the first parameter would already cover a lot of cases. You don't have to cover all cases since you can always fall back to a more general arguments. It even looks to me like this part of the procedure should be stupid enough to fail very quickly when it fails

Sebastian Ullrich (Aug 27 2019 at 15:07):

Sure, it's a single lookup of the head constant name in a hopefully fast data structure for deciding which algorithm to follow. The big issue in Lean 3 is where to build and store this data structure - this is exactly the issue with simp constantly rebuilding its simpset. This will work completely differently in Lean 4.

Reid Barton (Aug 27 2019 at 15:10):

I know GHC has an index on the head type constructor for ordinary type classes (although it also supports instances that aren't of the Haskell 98 form which specify only the head). I don't remember what it does for multiparameter type classes, I could check at some point.

Patrick Massot (Aug 27 2019 at 15:11):

And what about my even stupider idea of a local indexing by name of variable?

Reid Barton (Aug 27 2019 at 15:11):

My guess is that it's usually best to index the last type argument

Sebastian Ullrich (Aug 27 2019 at 15:11):

It's much easier if you're not an interactive compiler :)

Sebastian Ullrich (Aug 27 2019 at 15:13):

(Also Haskell does not have priorities. Should a head matching always be prioritized over a unification match? Is that intuitive?)

Simon Hudon (Aug 27 2019 at 15:17):

I think I'd be happy if head matching were prioritized. I always feel a bit queasy when I see an instance where the whole type is one variable. It does not use any specific knowledge of the type we're creating an instance for. I think specific insight should be prioritized

Sebastian Ullrich (Aug 27 2019 at 15:18):

And what about my even stupider idea of a local indexing by name of variable?

It would probably help, but I wouldn't hold my breath for such a hack being included in Lean proper. The head index should be strictly better.

Patrick Massot (Aug 27 2019 at 15:21):

They cover different cases (at least the way I dream of it)

Last updated: Aug 03 2023 at 10:10 UTC