From bb1a3734202257e5b3432bb7bcd418d3fa833cf1 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Sun, 28 Apr 2024 22:29:04 +0200 Subject: [PATCH] =?UTF-8?q?fix:=20subst=20notation=20(heq=20=E2=96=B8=20h)?= =?UTF-8?q?=20should=20fail=20if=20it=20does't=20subst=20(#3994)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The subst notation substitues in the expected type, if present, or in the type of the argument, if no expected type is known. If there is an expected type it already fails if it cannot find the equations' left hand side or right hand side. But if the expected type is not known and the equation's lhs is not present in the second argument's type, it will happily do a no-op-substitution. This is inconsistent and unlikely what the user intended to do, so we now print an error message now. This still only looks for the lhs; search for the rhs as well seems prudent, but I’ll leave that for a separate PR, to better diagnose the impact on mathlib. This triggers a small number of pointless uses of subst in mathlib, see https://github.com/leanprover-community/mathlib4/pull/12451 --- src/Lean/Elab/BuiltinNotation.lean | 2 ++ tests/lean/substFails.lean | 16 +++++++++ tests/lean/substFails.lean.expected.out | 46 +++++++++++++++++++++++++ 3 files changed, 64 insertions(+) create mode 100644 tests/lean/substFails.lean create mode 100644 tests/lean/substFails.lean.expected.out diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 6edf9ad042..3bde3e64da 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -409,6 +409,8 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex let h ← elabTerm hStx none let hType ← inferType h let hTypeAbst ← kabstract hType lhs + unless hTypeAbst.hasLooseBVars do + throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut its left hand side is not mentioned in the type{indentExpr hType}" let motive ← mkMotive lhs hTypeAbst unless (← isTypeCorrect motive) do throwError "invalid `▸` notation, failed to compute motive for the substitution" diff --git a/tests/lean/substFails.lean b/tests/lean/substFails.lean new file mode 100644 index 0000000000..612cd7acd5 --- /dev/null +++ b/tests/lean/substFails.lean @@ -0,0 +1,16 @@ +def foo := 3 +def bar := 4 + +def ex1 (heq : foo = bar) (P : Nat → Prop) (h : P foo) := heq ▸ h +def ex2 (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P 4 := heq ▸ h -- error +def ex3 (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h +def ex4 (heq : foo = bar) (P : Nat → Prop) (h : P 3) := heq ▸ h -- error +def ex5 (heq : foo = bar) (P : Nat → Prop) (h : P 3) : P 4 := heq ▸ h -- error +def ex6 (heq : foo = bar) (P : Nat → Prop) (h : P 3) : P bar := heq ▸ h + +def ex7 (heq : bar = foo) (P : Nat → Prop) (h : P foo) := heq ▸ h -- error +def ex8 (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P 4 := heq ▸ h -- error +def ex9 (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar := heq ▸ h +def ex10 (heq : bar = foo) (P : Nat → Prop) (h : P 3) := heq ▸ h -- error +def ex11 (heq : bar = foo) (P : Nat → Prop) (h : P 3) : P 4 := heq ▸ h -- error +def ex12 (heq : bar = foo) (P : Nat → Prop) (h : P 3) : P bar := heq ▸ h diff --git a/tests/lean/substFails.lean.expected.out b/tests/lean/substFails.lean.expected.out new file mode 100644 index 0000000000..f046afa8c9 --- /dev/null +++ b/tests/lean/substFails.lean.expected.out @@ -0,0 +1,46 @@ +substFails.lean:5:67-5:74: error: invalid `▸` notation, expected result type of cast is + P 4 +however, the equality + heq +of type + foo = bar +does not contain the expected result type on either the left or the right hand side +substFails.lean:7:67-7:74: error: invalid `▸` notation, the equality + heq +has type + foo = bar +but its left hand side is not mentioned in the type + P 3 +substFails.lean:8:67-8:74: error: invalid `▸` notation, expected result type of cast is + P 4 +however, the equality + heq +of type + foo = bar +does not contain the expected result type on either the left or the right hand side +substFails.lean:11:67-11:74: error: invalid `▸` notation, the equality + heq +has type + bar = foo +but its left hand side is not mentioned in the type + P foo +substFails.lean:12:67-12:74: error: invalid `▸` notation, expected result type of cast is + P 4 +however, the equality + heq +of type + bar = foo +does not contain the expected result type on either the left or the right hand side +substFails.lean:14:67-14:74: error: invalid `▸` notation, the equality + heq +has type + bar = foo +but its left hand side is not mentioned in the type + P 3 +substFails.lean:15:67-15:74: error: invalid `▸` notation, expected result type of cast is + P 4 +however, the equality + heq +of type + bar = foo +does not contain the expected result type on either the left or the right hand side