From 34d8ecc0665136a370dea796bf36f5ebab983d21 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Aug 2021 11:33:50 -0700
Subject: [PATCH] fix: use `show .. from ..` to implement `calc`

Recall that `show .. from ..` ensures that proof has exactly the type
provided by the user.
In the new test, `rw [ih]` without this change because the goal would
be
```
... |- 0 + succ n = succ n
```
---
 src/Init/NotationExtra.lean |  4 ++--
 tests/lean/run/calcBug.lean | 15 +++++++++++++++
 2 files changed, 17 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/calcBug.lean

diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index 2a3c1758c0..a62107e949 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -98,8 +98,8 @@ syntax calcStep := colGe term " := " withPosition(term)
 syntax "calc " withPosition(calcStep+) : term
 
 macro_rules
-  | `(calc $p:term := $h:term) => `(($h : $p))
-  | `(calc $p:term := $h:term $rest:calcStep*) => ``(trans ($h : $p) (calc $rest:calcStep*))
+  | `(calc $p:term := $h:term) => `(show $p from $h)
+  | `(calc $p:term := $h:term $rest:calcStep*) => ``(trans (show $p from $h) (calc $rest:calcStep*))
 
 @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
diff --git a/tests/lean/run/calcBug.lean b/tests/lean/run/calcBug.lean
new file mode 100644
index 0000000000..f04caf586b
--- /dev/null
+++ b/tests/lean/run/calcBug.lean
@@ -0,0 +1,15 @@
+namespace Hidden
+
+open Nat
+
+theorem zero_add (n : Nat) : 0 + n = n :=
+  Nat.recOn (motive := fun x => 0 + x = x)
+   n
+   (show 0 + 0 = 0 from rfl)
+   (fun (n : Nat) (ih : 0 + n = n) =>
+    show 0 + succ n = succ n from
+    calc
+       0 + succ n = succ (0 + n) := rfl
+                _ = succ n       := by rw [ih])
+
+end Hidden