From ac0e1b2265ac217f836d4ca27c6ddb5a279e6f67 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 23 Jul 2026 11:30:52 +0200 Subject: [PATCH] fix: use pi_congr instead of forall_congr; deprecate the latter (#7577) This PR generalizes the `conv` and `simp` tactics to apply `pi_congr` instead of `forall_congr`. The test case for #7507 has examples that work now, but only worked at universe `v=0` before. Since there are no more remaining uses of `forall_congr`, it is now deprecated. Closes #7507. Co-authored-by: Sebastian Graf --- src/Init/SimpLemmas.lean | 7 ++++--- src/Lean/Elab/Tactic/Conv/Congr.lean | 7 ++++--- src/Lean/Meta/AppBuilder.lean | 4 ++-- src/Lean/Meta/Tactic/Simp/Main.lean | 11 ++++------- src/Lean/Meta/Tactic/Simp/Types.lean | 2 +- tests/elab/1426.lean.out.expected | 4 ++-- tests/elab/7507.lean | 16 ++++++++++++++++ 7 files changed, 33 insertions(+), 18 deletions(-) create mode 100644 tests/elab/7507.lean diff --git a/src/Init/SimpLemmas.lean b/src/Init/SimpLemmas.lean index b604e2a3f096..3819cd0d0ada 100644 --- a/src/Init/SimpLemmas.lean +++ b/src/Init/SimpLemmas.lean @@ -110,6 +110,10 @@ 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 pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a := + (funext h : β = β') ▸ rfl + +@[deprecated pi_congr (since := "2026-07-22")] theorem forall_congr {α : Sort u} {p q : α → Prop} (h : ∀ a, p a = q a) : (∀ a, p a) = (∀ a, q a) := (funext h : p = q) ▸ rfl @@ -123,9 +127,6 @@ theorem forall_prop_congr_dom {p₁ p₂ : Prop} (h : p₁ = p₂) (q : p₁ → (∀ a : p₁, q a) = (∀ a : p₂, q (h.substr a)) := h ▸ rfl -theorem pi_congr {α : Sort u} {β β' : α → Sort v} (h : ∀ a, β a = β' a) : (∀ a, β a) = ∀ a, β' a := - (funext h : β = β') ▸ rfl - theorem let_congr {α : Sort u} {β : Sort v} {a a' : α} {b b' : α → β} (h₁ : a = a') (h₂ : ∀ x, b x = b' x) : (let x := a; b x) = (let x := a'; b' x) := h₁ ▸ (funext h₂ : b = b') ▸ rfl diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index a5fa1888f30f..8e68c50169a7 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -292,14 +292,15 @@ private def extCore (mvarId : MVarId) (userName? : Option Name) : MetaM MVarId : let u ← getLevel d 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 + let (q, h, v, mvarNew) ← withLocalDecl userName bi d fun a => do let pa := b.instantiate1 a let (qa, mvarNew) ← mkConvGoalFor pa + let v ← getLevel pa let q ← mkLambdaFVars #[a] qa let h ← mkLambdaFVars #[a] mvarNew resolveRhs "ext" rhs (← mkForallFVars #[a] qa) - return (q, h, mvarNew) - let proof := mkApp4 (mkConst ``forall_congr [u]) d p q h + return (q, h, v, mvarNew) + let proof := mkApp4 (mkConst ``pi_congr [u, v]) d p q h mvarId.assign proof return mvarNew.mvarId! else if let some mvarId ← extLetBodyCongr? mvarId lhs rhs then diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index c6230e395694..bcfd895cea9a 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -694,8 +694,8 @@ def mkImpCongrCtx (h₁ h₂ : Expr) : MetaM Expr := def mkImpDepCongrCtx (h₁ h₂ : Expr) : MetaM Expr := mkAppM ``implies_dep_congr_ctx #[h₁, h₂] -def mkForallCongr (h : Expr) : MetaM Expr := - mkAppM ``forall_congr #[h] +def mkPiCongr (h : Expr) : MetaM Expr := + mkAppM ``pi_congr #[h] /-- Returns instance for `[Monad m]` if there is one -/ def isMonad? (m : Expr) : MetaM (Option Expr) := diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index b648566cb9eb..1fd36eca8743 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -366,12 +366,11 @@ def simpForall (e : Expr) : SimpM Result := withParent e do trace[Debug.Meta.Tactic.simp] "forall {e}" if e.isArrow then simpArrow e - else if (← isProp e) then - /- The forall is a proposition. -/ + else let domain := e.bindingDomain! - if (← isProp domain) then + if (← isProp e) && (← isProp domain) then /- - The domain of the forall is also a proposition, and we can use `forall_prop_domain_congr` + The domain and codomain of the forall are propositions, and we can use `forall_prop_domain_congr` IF we can simplify the domain. -/ let rd ← simp domain @@ -407,9 +406,7 @@ def simpForall (e : Expr) : SimpM Result := withParent e do let eNew ← mkForallFVars #[x] rb.expr match rb.proof? with | none => return { expr := eNew } - | some h => return { expr := eNew, proof? := (← mkForallCongr (← mkLambdaFVars #[x] h)) } - else - return { expr := (← dsimp e) } + | some h => return { expr := eNew, proof? := (← mkPiCongr (← mkLambdaFVars #[x] h)) } /-- Adapter for `Meta.simpHaveTelescope` -/ def simpHaveTelescope (e : Expr) : SimpM Result := do diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 478b7f82f24f..72e1a9025c6a 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -956,7 +956,7 @@ def Result.addForalls (r : Result) (xs : Array Expr) : MetaM Result := do | none => return { expr := eNew } | some h => let p ← xs.foldrM (init := h) fun x h => do - mkForallCongr (← mkLambdaFVars #[x] h) + mkPiCongr (← mkLambdaFVars #[x] h) return { expr := eNew, proof? := p } diff --git a/tests/elab/1426.lean.out.expected b/tests/elab/1426.lean.out.expected index 1cecf1d7f685..4604511510ff 100644 --- a/tests/elab/1426.lean.out.expected +++ b/tests/elab/1426.lean.out.expected @@ -2,8 +2,8 @@ theorem ex1 : ∀ {a : Nat}, a * 2 = 2 * a := fun {a} => have h := fun a b => Eq.refl (a * b); Eq.mp - (forall_congr fun a => - forall_congr fun b => + (pi_congr fun a => + pi_congr fun b => (fun a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 : Nat), (a = a_3) = (a_2 = a_3)) (fun a_2 => Eq.refl (a = a_2)) e_a) (a * b) (b * a) (Eq.trans (congrArg (fun _a => _a) (Nat.mul_comm a b)) (Eq.refl (b * a))) (a * b)) diff --git a/tests/elab/7507.lean b/tests/elab/7507.lean new file mode 100644 index 000000000000..60b9cacf0ba9 --- /dev/null +++ b/tests/elab/7507.lean @@ -0,0 +1,16 @@ +/-! Tests that conv and simp apply pi_congr rather than the less general forall_congr. + The following examples used to work only at v = 0. +-/ + +axiom f : Sort u → Sort v +axiom g : Sort u → Sort v +axiom fg.eq (α : Sort u) : f α = g α + +example : ((x:Sort u) → f.{u,v} x) = ((x : Sort u) → g.{u,v} x) := + pi_congr fg.eq + +example : ((x:Sort u) → f.{u,v} x) = ((x : Sort u) → g.{u,v} x) := by + conv => lhs; ext; apply fg.eq + +example : ((x:Sort u) → f.{u,v} x) = ((x : Sort u) → g.{u,v} x) := by + simp only [fg.eq]