refactor: rewrite: produce simpler proof terms

[nomeata]

Consider

import Std.Tactic.ShowTerm

opaque a : Nat
opaque b : Nat
axiom a_eq_b : a = b
opaque P : Nat → Prop

set_option pp.explicit true

-- Using rw
example (h : P b) : P a := by show_term rw [a_eq_b]; assumption

Before, a typical proof term for rewrite looked like this:

-- Using the proof term that rw produces
example (h : P b) : P a :=
  @Eq.mpr (P a) (P b)
  (@id (@Eq Prop (P a) (P b))
    (@Eq.ndrec Nat a (fun _a => @Eq Prop (P a) (P _a))
      (@Eq.refl Prop (P a)) b a_eq_b))
  h

which is rather round-about, applying ndrec to refl. It would be more direct to write

example (h : P b) : P a :=
  @Eq.mpr (P a) (P b)
  (@id (@Eq Prop (P a) (P b))
    (@congrArg Nat Prop a b (fun _a => (P _a)) a_eq_b))
  h

which this change does.

This makes proof terms smaller, causing mild general speed up throughout the code; if the brenchmarks don’t lie the highlights are

• olean size -2.034 %
• lint wall-clock -3.401 %
• buildtactic execution s -10.462 %

H'T to @digama0 for advice and help.

NB: One might even expect the even simpler

-- Using the proof term that I would have expected
example (h : P b) : P a :=
  @Eq.ndrec Nat b (fun _a => P _a) h a a_eq_b.symm

but that would require non-local changes to the source code, so one step at a time.

[nomeata]

!bench

[leanprover-bot]

Here are the benchmark results for commit 522810c.
There were significant changes against commit 8d04ac1:

  Benchmark   Metric       Change
  =========================================
+ stdlib      task-clock    -1.0% (-36.8 σ)

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2023-12-28 12:15:58) View Log
• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2023-12-28 12:36:23) View Log
• 🟡 Mathlib branch lean-pr-testing-3121 build this PR didn't complete normally. (2023-12-28 14:57:59) View Log
• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2023-12-28 15:17:45) View Log
• 🟡 Mathlib branch lean-pr-testing-3121 build this PR didn't complete normally. (2023-12-28 15:24:13) View Log
• ❌ Mathlib branch lean-pr-testing-3121 built against this PR, but testing failed. (2023-12-28 15:37:45) View Log
• ❌ Mathlib branch lean-pr-testing-3121 built against this PR, but testing failed. (2023-12-28 16:48:57) View Log
• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2023-12-28 19:07:21) View Log
• ❌ Mathlib branch lean-pr-testing-3121 built against this PR, but testing failed. (2023-12-30 12:07:29) View Log
• 🟡 Mathlib branch lean-pr-testing-3121 build against this PR was cancelled. (2024-01-08 11:42:28) View Log
• ✅ Mathlib branch lean-pr-testing-3121 has successfully built against this PR. (2024-01-08 12:53:34) View Log
• 🟡 Mathlib branch lean-pr-testing-3121 build against this PR was cancelled. (2024-01-08 13:41:22) View Log
• ✅ Mathlib branch lean-pr-testing-3121 has successfully built against this PR. (2024-01-08 15:00:02) View Log
• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2024-01-15 14:19:06) View Log
• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2024-01-15 14:36:54) View Log
• 🟡 Mathlib branch lean-pr-testing-3121 build against this PR was cancelled. (2024-01-15 14:55:17) View Log
• ✅ Mathlib branch lean-pr-testing-3121 has successfully built against this PR. (2024-01-15 16:13:41) View Log
• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2024-01-15 16:47:31) View Log
• ✅ Mathlib branch lean-pr-testing-3121 has successfully built against this PR. (2024-01-15 18:47:14) View Log
• ✅ Mathlib branch lean-pr-testing-3121 has successfully built against this PR. (2024-01-15 19:23:06) View Log
• ✅ Mathlib branch lean-pr-testing-3121 has successfully built against this PR. (2024-01-15 21:31:54) View Log
• 💥 Mathlib branch lean-pr-testing-3121 build failed against this PR. (2024-01-20 16:56:26) View Log

[nomeata]

The test suit succeeds but mathlib fails. I hope I can distill a test case from this.

[nomeata]

Hmm, the four breaking cases were easy to fix (leanprover-community/mathlib4@af6cccb925 ):

• Three cases have subgoals in a different order, but it’s not clear to me that the original order was better. Also unclear why this happens. Maybe an instantiateMVars that wasn’t there before?
• In one case there was a porting note

      /- porting note: the following is indented two spaces more than it should be due to
        strange behavior of `erw` -/
      all_goals …
  

  and indeed the fix was to un-indent the all_goals, as one would expect. Did I inadvertently fix a minor bug here? But still a bit mysterious to me why this would happen with this change.

Then mathlib builds, but it’s test suite fails, e.g. at

-- Discharge side conditions from local hypotheses.
/--
info: Try this: rw [h p]
-- "no goals"
-/
#guard_msgs in
example {P : Prop} (p : P) (h : P → 1 = 2) : 2 = 1 := by
  rw?

so there is something fishy going on with side-conditions.

[nomeata]

Note to myself:

Using mkCongrArg reveals that the way I construct the motive here is not always non-dependent:

./././Mathlib/CategoryTheory/Limits/IsLimit.lean:538:20: error: AppBuilder for 'congrArg', non-dependent function expected
  fun _a ↦ { pt := pt✝, π := _a }.π.app j
has type
  (_a : (Functor.cones F).obj (op pt✝)) → ((const J).obj { pt := pt✝, π := _a }.pt).obj j ⟶ F.obj j

(but it is after a bit more evaluation; maybe mkCongrArg is a bit too picky here.)

[kim-em]

Then mathlib builds, but it’s test suite fails, e.g. at

-- Discharge side conditions from local hypotheses.
/--
info: Try this: rw [h p]
-- "no goals"
-/
#guard_msgs in
example {P : Prop} (p : P) (h : P → 1 = 2) : 2 = 1 := by
  rw?

so there is something fishy going on with side-conditions.

@nomeata, the "something fishy" is the rw? tactic inspecting the proof term in order to reconstruct the arguments of the successful rewrite lemma: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Rewrites.lean#L36.

This is obviously evil, but I'm not sure of a better way to do it. In any case it should be easy to update that function to match your new scheme. Let me know if you'd like me to do something in that file.

[nomeata]

Ha, should have thought of that!

I can do it myself when I come back to this (non-pressing) experiment, now that I know where to look.

Should rw? at least warn if it by? doesn’t work (“Could rewrite with lem, but failed to extract arguments, please report a bug”) , or is that an expected error mode?

[nomeata]

Here another benchmark run:
http://speed.lean-fro.org/mathlib4/compare/473da4ea-9efd-484f-a676-b52133e4ad35/to/77c1316a-877a-44d1-abf7-12b72a0e9306

• olean size -2.18 %
• lint wall-clock -1.144 % %
• build tactic execution s -11.514 % %
• build wall-clock -0.745 %
• build instructions -1.714 %

So the gains look relatively stable.