From 52d0f715c30bea99af79d490a3a6bf1fa51d1516 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Fri, 19 Jan 2024 08:20:58 +0100
Subject: [PATCH] refactor: rewrite: produce simpler proof terms (#3121)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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.
---
 src/Lean/Meta/Tactic/Rewrite.lean                | 14 +++++++++-----
 tests/lean/motiveNotTypeCorect.lean              | 11 +++++++++++
 tests/lean/motiveNotTypeCorect.lean.expected.out |  4 ++++
 3 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index 78daecb526..6072f38fa3 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -40,13 +40,17 @@ def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
           -- construct rewrite proof
           let eNew := eAbst.instantiate1 rhs
           let eNew ← instantiateMVars eNew
-          let eEqE ← mkEq e e
-          let eEqEAbst := mkApp eEqE.appFn! eAbst
-          let motive := Lean.mkLambda `_a BinderInfo.default α eEqEAbst
+          let eType ← inferType e
+          let motive := Lean.mkLambda `_a BinderInfo.default α eAbst
           unless (← isTypeCorrect motive) do
             throwTacticEx `rewrite mvarId "motive is not type correct"
-          let eqRefl ← mkEqRefl e
-          let eqPrf ← mkEqNDRec motive eqRefl heq
+          unless (← withLocalDeclD `_a α fun a => do isDefEq (← inferType (eAbst.instantiate1 a)) eType) do
+            -- NB: using motive.arrow? would disallow motives where the dependency
+            -- can be reduced away
+            throwTacticEx `rewrite mvarId "motive is dependent"
+          let u1 ← getLevel α
+          let u2 ← getLevel eType
+          let eqPrf := mkApp6 (.const ``congrArg [u1, u2]) α eType lhs rhs motive heq
           postprocessAppMVars `rewrite mvarId newMVars binderInfos
           let newMVarIds ← newMVars.map Expr.mvarId! |>.filterM fun mvarId => not <$> mvarId.isAssigned
           let otherMVarIds ← getMVarsNoDelayed eqPrf
diff --git a/tests/lean/motiveNotTypeCorect.lean b/tests/lean/motiveNotTypeCorect.lean
index a999327af0..cd9b84fc34 100644
--- a/tests/lean/motiveNotTypeCorect.lean
+++ b/tests/lean/motiveNotTypeCorect.lean
@@ -6,3 +6,14 @@ def mwe (t : Nat) (f : Nat -> Nat) (h : f t = t)
   := by
   rw [h] -- tactic 'rewrite' failed, motive is not type correct
   sorry
+
+def K (x : α) (y : β) : β := y
+example (h : true = false) (A : (b : Bool) → K b Type) (h2 : A false) : A true := by
+  -- the motive is dependent on `true`, but in a non-essential way, so this works fine
+  rw [h]
+  exact h2
+
+example (h : true = false) (A : (b : Bool) → if b then Prop else Nat) : A true :=
+  by
+    rw [h] -- tactic 'rewrite' failed, motive is dependent
+    exact 0
diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorect.lean.expected.out
index cee57716ed..bee1a003f4 100644
--- a/tests/lean/motiveNotTypeCorect.lean.expected.out
+++ b/tests/lean/motiveNotTypeCorect.lean.expected.out
@@ -5,3 +5,7 @@ h : f t = t
 d : D (f t)
 P : (t : Nat) → D t → Prop
 ⊢ P (f t) d
+motiveNotTypeCorect.lean:18:8-18:9: error: tactic 'rewrite' failed, motive is dependent
+h : true = false
+A : (b : Bool) → if b = true then Prop else Nat
+⊢ A true