feat: add congr conv tactic

src/Lean/Elab/Tactic/Conv.lean

@@ -4,3 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Tactic.Conv.Basic
+import Lean.Elab.Tactic.Conv.Congr

src/Lean/Elab/Tactic/Conv/Basic.lean

@@ -11,11 +11,15 @@ import Lean.Elab.Tactic.BuiltinTactic
 namespace Lean.Elab.Tactic.Conv
 open Meta
 
-def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
+def mkConvGoalFor (lhs : Expr) : TacticM (Expr × Expr) := do
   let lhsType ← inferType lhs
   let rhs ← mkFreshExprMVar lhsType
   let targetNew ← mkEq lhs rhs
   let newGoal ← mkFreshExprSyntheticOpaqueMVar targetNew
+  return (rhs, newGoal)
+
+def convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × Expr) := do
+  let (rhs, newGoal) ← mkConvGoalFor lhs
   let savedGoals ← getGoals
   try
     setGoals [newGoal.mvarId!]

src/Lean/Elab/Tactic/Conv/Congr.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.Main
+import Lean.Elab.Tactic.Conv.Basic
+
+namespace Lean.Elab.Tactic.Conv
+open Meta
+
+@[builtinTactic Lean.Parser.Tactic.Conv.congr] def evalCongr : Tactic := fun stx => do
+   withMainContext do
+     let (lhs, rhs) ← getLhsRhs
+     unless lhs.isApp do
+       throwError "invalid 'congr' conv tactic, application expected{indentD lhs}"
+     lhs.withApp fun f args => do
+      let infos := (← getFunInfoNArgs f args.size).paramInfo
+      let mut r := { expr := f : Simp.Result }
+      let mut newGoals := #[]
+      let mut i := 0
+      for arg in args do
+        trace[Debug.Meta.Tactic.simp] "app [{i}] {infos.size} {arg} hasFwdDeps: {infos[i].hasFwdDeps}"
+        let addGoal ←
+          if i < infos.size && !infos[i].hasFwdDeps then
+            pure true
+          else
+            pure (← whnfD (← inferType r.expr)).isArrow
+        if addGoal then
+          let (rhs, newGoal) ← mkConvGoalFor arg
+          newGoals := newGoals.push newGoal.mvarId!
+          r ← Simp.mkCongr r { expr := rhs, proof? := newGoal }
+        else
+          r ← Simp.mkCongrFun r arg
+        i := i + 1
+      let proof ← r.getProof
+      assignExprMVar rhs.mvarId! r.expr
+      assignExprMVar (← getMainGoal) proof
+      replaceMainGoal newGoals.toList
+
+end Lean.Elab.Tactic.Conv

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -31,12 +31,12 @@ private def mkEqTrans (r₁ r₂ : Result) : MetaM Result := do
     | none    => return { r₂ with proof? := r₁.proof? }
     | some p₂ => return { r₂ with proof? := (← Meta.mkEqTrans p₁ p₂) }
 
-private def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
+def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
   match r.proof? with
   | none   => return { expr := mkApp r.expr a, proof? := none }
   | some h => return { expr := mkApp r.expr a, proof? := (← Meta.mkCongrFun h a) }
 
-private def mkCongr (r₁ r₂ : Result) : MetaM Result :=
+def mkCongr (r₁ r₂ : Result) : MetaM Result :=
   let e := mkApp r₁.expr r₂.expr
   match r₁.proof?, r₂.proof? with
   | none,     none   => return { expr := e, proof? := none }

tests/lean/run/conv1.lean

@@ -5,6 +5,10 @@ def p (x y : Nat) := x = y
 example (x y : Nat) : p (x + y) (y + x + 0) := by
   conv =>
     whnf
+    congr
     skip
-  simp
+    whnf
+    skip
+  traceState
   rw [Nat.add_comm]
+  rfl