feat: upstream congr! from Mathlib

src/Init.lean

@@ -33,3 +33,4 @@ import Init.SizeOfLemmas
 import Init.BinderPredicates
 import Init.Ext
 import Init.Omega
+import Init.Congr!

src/Init/Congr!.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Init.RCases
+
+open Lean
+
+/--
+Equates pieces of the left-hand side of a goal to corresponding pieces of the right-hand side by
+recursively applying congruence lemmas. For example, with `⊢ f as = g bs` we could get
+two goals `⊢ f = g` and `⊢ as = bs`.
+
+Syntax:
+```
+congr!
+congr! n
+congr! with x y z
+congr! n with x y z
+```
+Here, `n` is a natural number and `x`, `y`, `z` are `rintro` patterns (like `h`, `rfl`, `⟨x, y⟩`,
+`_`, `-`, `(h | h)`, etc.).
+
+The `congr!` tactic is similar to `congr` but is more insistent in trying to equate left-hand sides
+to right-hand sides of goals. Here is a list of things it can try:
+
+- If `R` in `⊢ R x y` is a reflexive relation, it will convert the goal to `⊢ x = y` if possible.
+  The list of reflexive relations is maintained using the `@[refl]` attribute.
+  As a special case, `⊢ p ↔ q` is converted to `⊢ p = q` during congruence processing and then
+  returned to `⊢ p ↔ q` form at the end.
+
+- If there is a user congruence lemma associated to the goal (for instance, a `@[congr]`-tagged
+  lemma applying to `⊢ List.map f xs = List.map g ys`), then it will use that.
+
+- It uses a congruence lemma generator at least as capable as the one used by `congr` and `simp`.
+  If there is a subexpression that can be rewritten by `simp`, then `congr!` should be able
+  to generate an equality for it.
+
+- It can do congruences of pi types using lemmas like `implies_congr` and `pi_congr`.
+
+- Before applying congruences, it will run the `intros` tactic automatically.
+  The introduced variables can be given names using a `with` clause.
+  This helps when congruence lemmas provide additional assumptions in hypotheses.
+
+- When there is an equality between functions, so long as at least one is obviously a lambda, we
+  apply `funext` or `hfunext`, which allows for congruence of lambda bodies.
+
+- It can try to close goals using a few strategies, including checking
+  definitional equality, trying to apply `Subsingleton.elim` or `proof_irrel_heq`, and using the
+  `assumption` tactic.
+
+The optional parameter is the depth of the recursive applications.
+This is useful when `congr!` is too aggressive in breaking down the goal.
+For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
+`congr!` produces the goals `⊢ x = y` and `⊢ y = x`,
+while `congr! 2` produces the intended `⊢ x + y = y + x`.
+
+The `congr!` tactic also takes a configuration option, for example
+```lean
+congr! (config := {transparency := .default}) 2
+```
+This overrides the default, which is to apply congruence lemmas at reducible transparency.
+
+The `congr!` tactic is aggressive with equating two sides of everything. There is a predefined
+configuration that uses a different strategy:
+Try
+```lean
+congr! (config := .unfoldSameFun)
+```
+This only allows congruences between functions applications of definitionally equal functions,
+and it applies congruence lemmas at default transparency (rather than just reducible).
+This is somewhat like `congr`.
+
+See `Congr!.Config` for all options.
+-/
+syntax (name := congr!) "congr!" (Parser.Tactic.config)? (ppSpace num)?
+  (" with" (ppSpace colGt rintroPat)*)? : tactic

src/Init/PropLemmas.lean

@@ -26,6 +26,20 @@ set_option linter.missingDocs true -- keep it documented
 theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
   cases propext (iff_of_true hp hq); rfl
 
+theorem proof_irrel_heq {p q : Prop} (hp : p) (hq : q) : HEq hp hq := by
+  cases propext (iff_of_true hp hq); rfl
+
+theorem hfunext {α α' : Sort u} {β : α → Sort v} {β' : α' → Sort v} {f : ∀a, β a} {f' : ∀a, β' a}
+    (hα : α = α') (h : ∀a a', HEq a a' → HEq (f a) (f' a')) : HEq f f' := by
+  subst hα
+  have : ∀a, HEq (f a) (f' a) := λ a => h a a (HEq.refl a)
+  have : β = β' := by funext a
+                      exact type_eq_of_heq (this a)
+  subst this
+  apply heq_of_eq
+  funext a
+  exact eq_of_heq (this a)
+
 /-! ## not -/
 
 theorem not_not_em (a : Prop) : ¬¬(a ∨ ¬a) := fun h => h (.inr (h ∘ .inl))

src/Init/SimpLemmas.lean

@@ -45,7 +45,7 @@ theorem implies_dep_congr_ctx {p₁ p₂ q₁ : Prop} (h₁ : p₁ = p₂) {q₂
 theorem implies_congr_ctx {p₁ p₂ q₁ q₂ : Prop} (h₁ : p₁ = p₂) (h₂ : p₂ → q₁ = q₂) : (p₁ → q₁) = (p₂ → q₂) :=
   implies_dep_congr_ctx h₁ h₂
 
-theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
+theorem forall_congr {α : Sort u} {p q : α → Sort v} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) :=
   (funext h : p = q) ▸ rfl
 
 theorem forall_prop_domain_congr {p₁ p₂ : Prop} {q₁ : p₁ → Prop} {q₂ : p₂ → Prop}

src/Init/Tactics.lean

@@ -958,7 +958,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
 -/
 syntax (name := congr) "congr" (ppSpace num)? : tactic
 
-
 /--
 In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
 ```

src/Lean/Elab/Tactic.lean

@@ -39,3 +39,4 @@ import Lean.Elab.Tactic.SolveByElim
 import Lean.Elab.Tactic.LibrarySearch
 import Lean.Elab.Tactic.ShowTerm
 import Lean.Elab.Tactic.Rfl
+import Lean.Elab.Tactic.Congr!

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

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2023 Kyle Miller. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kyle Miller
+-/
+prelude
+import Init.Congr!
+import Lean.Meta.Tactic.Congr!
+
+/-!
+# The `congr!` tactic
+
+This is a more powerful version of the `congr` tactic that knows about more congruence lemmas and
+can apply to more situations. It is similar to the `congr'` tactic from Mathlib 3.
+
+The `congr!` tactic is used by the `convert` and `convert_to` tactics.
+
+See the syntax docstring for more details.
+-/
+
+open Lean Elab Tactic Meta.Tactic.Congr!
+
+namespace Lean.Elab.Tactic
+
+declare_config_elab elabConfig Config
+
+@[builtin_tactic «congr!»] def evalCongr! : Tactic := fun stx =>
+  match stx with
+  | `(tactic| congr! $[$cfg:config]? $[$n]? $[with $ps?*]?) => do
+    let config ← elabConfig (mkOptionalNode cfg)
+    let patterns := (Lean.Elab.Tactic.RCases.expandRIntroPats (ps?.getD #[])).toList
+    liftMetaTactic fun g ↦
+      let depth := n.map (·.getNat)
+      g.congrN! depth config patterns
+  | _                     => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Congr.lean

@@ -9,7 +9,6 @@ import Lean.Elab.Tactic.Basic
 
 namespace Lean.Elab.Tactic
 
-namespace Lean.Elab.Tactic
 @[builtin_tactic Parser.Tactic.congr] def evalCongr : Tactic := fun stx =>
   match stx with
   | `(tactic| congr $[$n?]?) =>
@@ -19,5 +18,3 @@ namespace Lean.Elab.Tactic
   | _ => throwUnsupportedSyntax
 
 end Lean.Elab.Tactic
-
-

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

@@ -176,6 +176,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
     let lhs := (← instantiateMVars lhs).cleanupAnnotations
     if let .forallE n d b bi := lhs then
       let u ← getLevel d
+      let v ← getLevel b
       let p : Expr := .lam n d b bi
       let userName ← if let some userName := userName? then pure userName else mkFreshBinderNameForTactic n
       let (q, h, mvarNew) ← withLocalDecl userName bi d fun a => do
@@ -187,7 +188,7 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId :
         unless (← isDefEqGuarded rhs rhs') do
           throwError "invalid 'ext' conv tactic, failed to resolve{indentExpr rhs}\n=?={indentExpr rhs'}"
         return (q, h, mvarNew)
-      let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h
+      let proof := mkApp4 (mkConst ``forall_congr [u, v]) d p q h
       mvarId.assign proof
       return mvarNew.mvarId!
     else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then

src/Lean/Elab/Tactic/Rfl.lean

@@ -16,13 +16,6 @@ provided the reflexivity lemma has been marked as `@[refl]`.
 
 namespace Lean.Elab.Tactic.Rfl
 
-/--
-This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
-relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
--/
-elab_rules : tactic
-  | `(tactic| rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)
-
 @[builtin_tactic Lean.Parser.Tactic.applyRfl] def evalApplyRfl : Tactic := fun stx =>
   match stx with
   | `(tactic| apply_rfl) => withMainContext do liftMetaFinishingTactic (·.applyRfl)