cleaning iff

Stream: general

[Patrick Massot]

@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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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]
                     end
   | _ := fail "Goal is not a forall, implies or iff"
   end

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]

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

[Reid Barton]

This does feel like something within the scope of congr

[Jeremy Avigad]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

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]

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

[Patrick Massot]

This and so many other boring details

[Johan Commelin]

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

[Jeremy Avigad]

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]

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]

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]

@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]

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

[Sebastian Ullrich]

no

[Johan Commelin]

Great!

[Patrick Massot]

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

[Sebastian Ullrich]

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]

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

[Patrick Massot]

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]

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]

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]

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

[Reid Barton]

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

[Sebastian Ullrich]

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

[Sebastian Ullrich]

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

[Simon Hudon]

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]

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]

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