From bc233831945b168861e5720b37d5938ea21bb7f5 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 2 May 2024 09:02:40 +0200 Subject: [PATCH] =?UTF-8?q?feat:=20subst=20notation=20(heq=20=E2=96=B8=20h?= =?UTF-8?q?)=20tries=20both=20orientation=20(#4046)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit even when rewriting the type of `h` becuase there is no expected type. (When there is an expected type, it already tried both orientations.) Also feeble attempt to include this information in the docstring without writing half a manual chapter. --- src/Lean/Elab/BuiltinNotation.lean | 10 +++++++--- src/Lean/Parser/Term.lean | 4 ++++ tests/lean/substFails.lean | 4 +++- tests/lean/substFails.lean.expected.out | 24 ++++++++++-------------- 4 files changed, 24 insertions(+), 18 deletions(-) diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 3bde3e64da..56cdc5e0df 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -388,7 +388,7 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex return (← mkEqRec motive h (← mkEqSymm heq), none) let motive ← mkMotive lhs expectedAbst if badMotive?.isSome || !(← isTypeCorrect motive) then - -- Before failing try tos use `subst` + -- Before failing try to use `subst` if ← (isSubstCandidate lhs rhs <||> isSubstCandidate rhs lhs) then withLocalIdentFor heqStx heq fun heqStx => do let h ← instantiateMVars h @@ -408,9 +408,13 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex | none => let h ← elabTerm hStx none let hType ← inferType h - let hTypeAbst ← kabstract hType lhs + let mut 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}" + hTypeAbst ← kabstract hType rhs + unless hTypeAbst.hasLooseBVars do + throwError "invalid `▸` notation, the equality{indentExpr heq}\nhas type {indentExpr heqType}\nbut neither side of the equality is mentioned in the type{indentExpr hType}" + heq ← mkEqSymm heq + (lhs, rhs) := (rhs, lhs) let motive ← mkMotive lhs hTypeAbst unless (← isTypeCorrect motive) do throwError "invalid `▸` notation, failed to compute motive for the substitution" diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index e71e7788bb..49d610a5b0 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -807,6 +807,10 @@ It is especially useful for avoiding parentheses with repeated applications. Given `h : a = b` and `e : p a`, the term `h ▸ e` has type `p b`. You can also view `h ▸ e` as a "type casting" operation where you change the type of `e` by using `h`. + +The macro tries both orientations of `h`. If the context provides an +expected type, it rewrites the expeced type, else it rewrites the type of e`. + See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lean" for additional information. -/ diff --git a/tests/lean/substFails.lean b/tests/lean/substFails.lean index 612cd7acd5..6b3999e14f 100644 --- a/tests/lean/substFails.lean +++ b/tests/lean/substFails.lean @@ -2,13 +2,15 @@ def foo := 3 def bar := 4 def ex1 (heq : foo = bar) (P : Nat → Prop) (h : P foo) := heq ▸ h +#check ex1 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 ex7 (heq : bar = foo) (P : Nat → Prop) (h : P foo) := heq ▸ h +#check ex7 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 diff --git a/tests/lean/substFails.lean.expected.out b/tests/lean/substFails.lean.expected.out index f046afa8c9..84d2fde039 100644 --- a/tests/lean/substFails.lean.expected.out +++ b/tests/lean/substFails.lean.expected.out @@ -1,43 +1,39 @@ -substFails.lean:5:67-5:74: error: invalid `▸` notation, expected result type of cast is +ex1 (heq : foo = bar) (P : Nat → Prop) (h : P foo) : P bar +substFails.lean:6:67-6: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 +substFails.lean:8:67-8:74: error: invalid `▸` notation, the equality heq has type foo = bar -but its left hand side is not mentioned in the type +but neither side of the equality is mentioned in the type P 3 -substFails.lean:8:67-8:74: error: invalid `▸` notation, expected result type of cast is +substFails.lean:9:67-9: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 +ex7 (heq : bar = foo) (P : Nat → Prop) (h : P foo) : P bar +substFails.lean:14:67-14: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 +substFails.lean:16:67-16:74: error: invalid `▸` notation, the equality heq has type bar = foo -but its left hand side is not mentioned in the type +but neither side of the equality is mentioned in the type P 3 -substFails.lean:15:67-15:74: error: invalid `▸` notation, expected result type of cast is +substFails.lean:17:67-17:74: error: invalid `▸` notation, expected result type of cast is P 4 however, the equality heq