Possible improvements to Lean/Mathlib

Stream: mathlib4

[Jovan Gerbscheid]

I kept a list of things I noticed I think could be improved in Lean/Mathlib. Some easier and some harder to fix. I'm not sure of the most efficient way to deal with these, so I'll just post this list, and I'm wondering which of these points people agree with.

Mathlib

(1) norm_cast doesn't use Fin.cast_val_eq_self, i.e. doesn't simplify Nat.cast (Fin.val n) to n.
(2) cases (r:ℚ) should replace r with _ / _ instead of an application of Rat.mk'.
(3) push_neg should be aware of Infinite, Finite, Set.Infinite and Set.Finite.
This should be easy to implement since push_neg isn't imported where these are defined.
(4) add_self should be the lemma two_mul in the opposite rewrite direction,
as this is the more simplifying direction of the rewrite. (similarly mul_self)
(5) a ring_nf option to normalize a ring equality a = b to a - b = 0.
This helps when terms are on different sides of = in different places.
(6) I want to be able to add something to both sides of an equation.
It is possible to add the same thing on both sides with add_left_inj _.
But I also want to be able to add h : a = b (i.e. add a to one side and b to the other)
linear_combination does this, but for some reason it is a terminal tactic.
Not all such goals are terminated by linear_combination.

Lean

(7) Not.imp should be an alias of mt, instead of having its arguments swapped,
to match lemmas like And.imp and Exists.imp.
(8) suffices should work with incremental elaboration,
when working inside the suffices block, just like with have.
(9) in conv mode, simp, unfold, etc should throw errors when doing nothing (like they usually do)
(10) simp should keep variable names:

Import Mathlib
example : 1 = Finset.sum Finset.univ (fun y : (Fin 20) ↦ (y.val + 1 - 1 : Nat)) := by
  simp -- `y` turns into `x`

(11) The apply tactic should deal with autoparams, instead of creating a goal of type autoParam _ _.

example (n : Nat) : ({a | a = 0} ∩ {a | a = n}).ncard ≤ 1 := by
  trans; apply Set.ncard_inter_le_ncard_right
  -- case ht
  -- n : ℕ
  -- ⊢ autoParam {a | a = n}.Finite _auto✝

  -- n : ℕ
  -- ⊢ {a | a = n}.ncard ≤ 1

(12) higher order unification that can solve unifications of the form ?P n.val =?= ... where ... contains n.val.
This should be an opt-in configuration in simp, rw etc. This is also useful for rewriting with something like ← Classical.skolem
(13) An improved version of kabstract/generalize that avoids "motive not type correct" by
only abstracting the abstractable terms.
For example, if the goal is something like
f : ℕ → ℕ h : ∀ (n : ℕ), f n = f (n + 1) ⊢ (5 : Fin 10) = 5 ∧ f 0 = f 10
Then I want induction 10 (or rw) to realize which 10 can be inducted on,
and that the 10 in Fin 10 cannot be abstracted.
This can be done in a way that doesn't inhibit performance,
by only doing this after encountering the motive type error.
The way to implement this, is to create a metavariable hole for each occurrence of 10,
and then run check on this expression. This will instantiate some of these metavariables to
10 if that is needed for typechecking. Then the remaining metaviarbles can be abstracted.

[Kim Morrison]

1-6 sound good to me, but need separate threads if you're hoping to persuade others to implement them. :-) PRs welcome for all those.

[Kim Morrison]

9, definitely, PR welcome

[Kim Morrison]

@Joachim Breitner is working on 10

[Kim Morrison]

11, PR welcome, I think

[Eric Wieser]

8 sounds non-controversial, but perhaps Sebastian is best placed to implement it?

[Kim Morrison]

8 is probably a task for Sebastian U, or at least to wait for him to write an account of how to enable incremental elaboration for more tactics.

[Kim Morrison]

No opinion on 7

[Kim Morrison]

12 will have to wait, we don't have bandwidth for that

[Kim Morrison]

13 seems like a good experiment, and without promising merging, I'd be very interested to see a performant implementation

[Rob Lewis]

linear_combination does this, but for some reason it is a terminal tactic.

This was the behavior of linear_combination at one point. IIRC it was changed for technical reasons that I can't remember (@Heather Macbeth ?)

[Jireh Loreaux]

(6) Can be done with congr()

[Joachim Breitner]

Kim Morrison said:

Joachim Breitner is working on 10

To be precise: I have added the binderNameHint in https://github.com/leanprover/lean4/pull/6947 which allows you to annotate rewrite rules such that binder names are preserved. This leaves the task of actually using it all the rewrite rules that have binders on the right hand side.

In the example given, it seems the x comes from not from a rewrite rule, but from a congruence rule (docs#Finset.sum_congr), so unfortunately, binderNameHint isn't quite applicable there yet.

I reproduced the issue on nightly (using List.map to avoid mathlib), and this needs more work before it works for congruence rules:

section no_congr
/--
error: tactic 'fail' failed
xs : List Nat
⊢ xs = List.map (fun y => 1 + y) xs
-/
#guard_msgs in
example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
  simp
  fail

end no_congr

section with_congr

/--
info: List.map_congr_left.{u_1, u_2} {α✝ : Type u_1} {l : List α✝} {α✝¹ : Type u_2} {f g : α✝ → α✝¹}
  (h : ∀ (a : α✝), a ∈ l → f a = g a) : List.map f l = List.map g l
-/
#guard_msgs in
#check List.map_congr_left

attribute [local congr] List.map_congr_left

/--
error: tactic 'fail' failed
xs : List Nat
⊢ xs = List.map (fun a => 1 + a) xs
-/
#guard_msgs in
example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
  simp -- NB: Changes variable name!
  fail

end with_congr

section with_congr_hint

-- Trying to use the binderNameHint on a congruence rule


--  this loops:
theorem List.map_congr_left' {f g : α → β}  (h : ∀ (a : α), a ∈ l → (f a = g a)) : List.map f l = List.map (fun x => binderNameHint x f (g x)) l  :=
  List.map_congr_left h

-- this is not effective
theorem List.map_congr_left'' {f g : α → β}  (h : ∀ (a : α), a ∈ l → (binderNameHint a f (f a) = g a)) : List.map f l = List.map g l  := List.map_congr_left h

attribute [congr] List.map_congr_left''

/--
error: tactic 'fail' failed
xs : List Nat
⊢ xs = List.map (fun a => 1 + a) xs
-/
#guard_msgs in
example : xs = List.map (fun y => 1 + (y + 1 - 1)) xs := by
  simp -- the binderNameHint is not effective on congruence rules yet :-()
  fail

end with_congr_hint

Noted at issue https://github.com/leanprover/lean4/issues/7052

[Joachim Breitner]

Possible fix for binderNameHint in congruence rules in lean4#7053.

[Jovan Gerbscheid]

I've created PRs for the first 4 points now:
(1) #21775
(2) #21767 in addition to a cases eliminator for Rat, I've also added Int.induction_on as the default induction eliminator for Int.
(3) #21769 Unfortunately the extra import of Mathlib.Data.Finite.Defsis quite large. The question is whether this is OK, or if push_neg needs to be reimplemented to be extensible.
(4) #21761

[Eric Wieser]

For 3, I think extensibility of push_neg is the right thing to do

[Jovan Gerbscheid]

Do you think is should use the discrimination tree infrastructure of simp for applying lemmas? Currently it is implemented with a simple match on the name of the head constant after the not.

[Jovan Gerbscheid]

I guess we could also use the simpler docs#Lean.HeadIndex

[Patrick Massot]

Extensibility looks a lot more future-proof.

[Damiano Testa]

For the sake of the bots, I'll repost the PRs, one per message.

[Damiano Testa]

(1) #21775

[Damiano Testa]

(2) #21767 in addition to a cases eliminator for Rat, I've also added Int.induction_on as the default induction eliminator for Int.

[Damiano Testa]

(3) #21769 Unfortunately the extra import of Mathlib.Data.Finite.Defsis quite large. The question is whether this is OK, or if push_neg needs to be reimplemented to be extensible.

[Damiano Testa]

(4) #21761

[Yaël Dillies]

I really want push_neg to become extensible so that it can use docs#Finset.nonempty_iff_ne_empty

[Jovan Gerbscheid]

I think it already does that?

[Yaël Dillies]

Nope, it does that for Set, not for Finset (which makes it even more irritating)

[Eric Wieser]

Would extensionality here just amount to a simp set?

[Eric Wieser]

(in fact, is the whole tactic anything other than a simp set?)

[Jovan Gerbscheid]

It differs from just a simp set because it doesn't traverse the whole expression, only pushing the head negation. Yes, a simp set should do the job for extensibility.

[Bolton Bailey]

@Jovan Gerbscheid Thanks for posting these, do you mind if I add some of them to a tactic improvements tracking issue I maintain (#10361)?

[Jovan Gerbscheid]

I was looking at push_cast as inspiration for how to implement push_neg, but then I noticed that they both don't throw errors when doing nothing. So let's make that item (14) on the list: push_cast and norm_cast should throw an error when doing nothing.

[Damiano Testa]

"Doing nothing" should be caught by the unusedTactic linter, right?

[Jovan Gerbscheid]

Yes, but not when you are in the middle of writing a proof, only when the proof is complete. I want the tactic to tell me "hey, I shouldn't exeist" as soon as I write it.

[Damiano Testa]

That might be achievable: the linter explicitly shuts up if there are errors, but it need not do it.

[Damiano Testa]

When there are errors, it may be less clear that the tactic is really not doing anything, but if there is enough information available to read the state before and after the tactic, it may be reliable.

[Damiano Testa]

I just never tried it on syntax that was not fully formed.

[Patrick Massot]

I didn’t pay attention to the Lean 4 port of push_neg but I can tell you why the Lean 3 version was not a simp set. The main point was to keep variable names.

[Patrick Massot]

I mean bound variables of course.

[Jovan Gerbscheid]

Yes, and the rewrite rule of ¬ a = b → a ≠ b cannot be expressed using simp, because this lemma is applicable to its own result.

[Jovan Gerbscheid]

But, what we can do is to keep the implementation for pushing negation through forall and exists, and the ¬ a = b → a ≠ b rule, and let all the other rewrites be handled by a simp set.

[Jovan Gerbscheid]

On #10361, I saw that people would like to generalize the push_neg tactic for other constants. I think that this can be done nicely using a single simp set for all push lemmas. Then the user could specify e.g. push not, which then would mean that it would only try to rewrite with these push lemmas on subexpressions that have head constant not.

[Jovan Gerbscheid]

Another reason for not using a simp lemma is to implement the option push_neg.use_distrib, which determines how to simplify ¬ (p ∧ q)

[Jovan Gerbscheid]

@Joachim Breitner, in the following example, simp still changes the bound variable name on the current nightly, which is because exists_prop_congr doesn't use the binderNameHint:

example (a : α) (o : Option α) : ∃ x, o.get x ≠ a := by
  simp -- `x` turns into `h`
  sorry

[Joachim Breitner]

Oh, yes, I just added the binderNameHint mechanism. When, whether and how to annotate all simp lemmas in the standard library and mathlib is completely open yet :-)

(And maybe binderNameHint isn’t the final word here, and there could be more automatic cleverness in simp)

[Jovan Gerbscheid]

(Note that this one is a congr lemma, not a simp lemma)

[Joachim Breitner]

Right; I should have said “lemma used by simp”