feat: improve calc tactic

> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.

Closes #1342

RELEASES.md

@@ -1,6 +1,8 @@
 Unreleased
 ---------
 
+* Improve `calc` term and tactic. See [issue #1342](https://github.com/leanprover/lean4/issues/1342).
+
 * [Relaxed antiquotation parsing](https://github.com/leanprover/lean4/pull/1272) further reduces the need for explicit `$x:p` antiquotation kind annotations.
 
 * Add support for computed fields in inductives. Example:

src/Init/NotationExtra.lean

@@ -88,8 +88,7 @@ macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBi
 syntax calcStep := ppIndent(colGe term " := " withPosition(term))
 syntax (name := calc) "calc" ppLine withPosition(calcStep) ppLine withPosition((calcStep ppLine)*) : term
 
-macro "calc " ppLine step1:withPosition(calcStep) ppLine steps:withPosition((calcStep ppLine)*) : tactic =>
-  `(exact calc $step1 $steps*)
+syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosition((calcStep ppLine)*) : tactic
 
 @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())

src/Lean/Elab/Calc.lean

@@ -12,12 +12,28 @@ open Meta
   Decompose `e` into `(r, a, b)`.
 
   Remark: it assumes the last two arguments are explicit. -/
-private def relation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
+def getCalcRelation? (e : Expr) : MetaM (Option (Expr × Expr × Expr)) :=
   if e.getAppNumArgs < 2 then
     return none
   else
     return some (e.appFn!.appFn!, e.appFn!.appArg!, e.appArg!)
 
+def mkCalcTrans (result resultType step stepType : Expr) : MetaM (Expr × Expr) := do
+  let some (r, a, b) ← getCalcRelation? resultType | unreachable!
+  let some (s, _, c) ← getCalcRelation? (← instantiateMVars stepType) | unreachable!
+  let (α, β, γ)       := (← inferType a, ← inferType b, ← inferType c)
+  let (u_1, u_2, u_3) := (← getLevel α, ← getLevel β, ← getLevel γ)
+  let t ← mkFreshExprMVar (← mkArrow α (← mkArrow γ (mkSort levelZero)))
+  let selfType := mkAppN (Lean.mkConst ``Trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t]
+  match (← trySynthInstance selfType) with
+  | LOption.some self =>
+    let result := mkAppN (Lean.mkConst ``Trans.trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t, self, a, b, c, result, step]
+    let resultType := (← instantiateMVars (← inferType result)).headBeta
+    unless (← getCalcRelation? resultType).isSome do
+      throwError "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
+    return (result, resultType)
+  | _ => throwError "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}"
+
 /--
   Elaborate `calc`-steps
 -/
@@ -26,10 +42,10 @@ def elabCalcSteps (steps : Array Syntax) : TermElabM Expr := do
   let mut types  := #[]
   for step in steps do
     let type  ← elabType step[0]
-    let some (_, lhs, _) ← relation? type |
+    let some (_, lhs, _) ← getCalcRelation? type |
       throwErrorAt step[0] "invalid 'calc' step, relation expected{indentExpr type}"
     if types.size > 0 then
-      let some (_, _, prevRhs) ← relation? types.back | unreachable!
+      let some (_, _, prevRhs) ← getCalcRelation? types.back | unreachable!
       unless (← isDefEqGuarded lhs prevRhs) do
         throwErrorAt step[0] "invalid 'calc' step, left-hand-side is {indentD m!"{lhs} : {← inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← inferType prevRhs}"}"
     types := types.push type
@@ -39,20 +55,7 @@ def elabCalcSteps (steps : Array Syntax) : TermElabM Expr := do
   let mut result := proofs[0]!
   let mut resultType := types[0]!
   for i in [1:proofs.size] do
-    let some (r, a, b) ← relation? resultType | unreachable!
-    let some (s, _, c) ← relation? (← instantiateMVars types[i]!) | unreachable!
-    let (α, β, γ)       := (← inferType a, ← inferType b, ← inferType c)
-    let (u_1, u_2, u_3) := (← getLevel α, ← getLevel β, ← getLevel γ)
-    let t ← mkFreshExprMVar (← mkArrow α (← mkArrow γ (mkSort levelZero)))
-    let selfType := mkAppN (Lean.mkConst ``Trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t]
-    match (← trySynthInstance selfType) with
-    | LOption.some self =>
-      result := mkAppN (Lean.mkConst ``Trans.trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t, self, a, b, c, result, proofs[i]!]
-      resultType := (← instantiateMVars (← inferType result)).headBeta
-      unless (← relation? resultType).isSome do
-        throwErrorAt steps[i]! "invalid 'calc' step, step result is not a relation{indentExpr resultType}"
-    | _ => throwErrorAt steps[i]! "invalid 'calc' step, failed to synthesize `Trans` instance{indentExpr selfType}"
-    pure ()
+    (result, resultType) ← withRef steps[i]! <| mkCalcTrans result resultType proofs[i]! types[i]!
   return result
 
 /-- Step-wise reasoning over transitive relations.

src/Lean/Elab/Tactic.lean

@@ -20,3 +20,4 @@ import Lean.Elab.Tactic.Delta
 import Lean.Elab.Tactic.Meta
 import Lean.Elab.Tactic.Unfold
 import Lean.Elab.Tactic.Cache
+import Lean.Elab.Tactic.Calc

src/Lean/Elab/Tactic/Calc.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Calc
+import Lean.Elab.Tactic.ElabTerm
+
+namespace Lean.Elab.Tactic
+open Meta
+
+def elabCalcSteps (steps : Array Syntax) : TacticM Expr := do
+  /- If error recovery is disabled, we disable `Term.withoutErrToSorry` -/
+  if (← read).recover then
+    go
+  else
+    Term.withoutErrToSorry go
+where
+  go : TermElabM Expr := do
+    let e ← Term.elabCalcSteps steps
+    Term.synthesizeSyntheticMVars
+    instantiateMVars e
+
+@[builtinTactic calcTactic]
+def evalCalc : Tactic := fun stx => do
+  withMainContext do
+    let steps := #[stx[1]] ++ stx[2].getArgs
+    let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
+      let val ← elabCalcSteps steps
+      let valType ← inferType val
+      let target ← getMainTarget
+      if (← isDefEq valType target) then
+        return val
+      else
+        let throwFailed {α} : TacticM α :=
+          throwError "'calc' tactic failed, has type{indentExpr valType}\nbut it is expected to have type{indentExpr target}"
+        let some (_, _, rhs) ← Term.getCalcRelation? valType | throwFailed
+        let some (r, _, rhs') ← Term.getCalcRelation? target | throwFailed
+        let lastStep := mkApp2 r rhs rhs'
+        let lastStepGoal ← mkFreshExprSyntheticOpaqueMVar lastStep (tag := (← getMainTag) ++ `calc.step)
+        let (val, valType) ← Term.mkCalcTrans val valType lastStepGoal lastStep
+        unless (← isDefEq valType target) do throwFailed
+        return val
+    let val ← instantiateMVars val
+    let mvarId ← getMainGoal
+    assignExprMVar mvarId val
+    replaceMainGoal mvarIds

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -64,9 +64,12 @@ def filterOldMVars (mvarIds : Array MVarId) (mvarCounterSaved : Nat) : MetaM (Ar
     return r
   | _ => throwUnsupportedSyntax
 
-def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
+/--
+  Execute `k`, and collect new "holes" in the resulting expression.
+-/
+def withCollectingNewGoalsFrom (k : TacticM Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
   let mvarCounterSaved := (← getMCtx).mvarCounter
-  let val ← elabTermEnsuringType stx expectedType?
+  let val ← k
   let newMVarIds ← getMVarsNoDelayed val
   /- ignore let-rec auxiliary variables, they are synthesized automatically later -/
   let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId)
@@ -79,7 +82,10 @@ def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix :
     logUnassignedAndAbort naturalMVarIds
     pure syntheticMVarIds.toList
   tagUntaggedGoals (← getMainTag) tagSuffix newMVarIds
-  pure (val, newMVarIds)
+  return (val, newMVarIds)
+
+def elabTermWithHoles (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
+  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType?) tagSuffix allowNaturalHoles
 
 /-- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
    Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be

tests/lean/run/1342.lean

@@ -0,0 +1,58 @@
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c :=
+  calc a
+     <= b := h1
+   _ <= c := h2
+   _ <= c := Nat.le_refl _
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c :=
+  calc a
+     <= b := h1
+   _ <= c := h2
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c :=
+  calc a <= b := h1
+  _ <= c := h2
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c :=
+  calc
+  a <= b := h1
+  _ <= c := h2
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c :=
+  calc
+  a <= b := sorry
+  _ <= c := h2
+
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c := by
+  calc a
+     <= b := ?h
+   _ <= c := h2
+  case h => exact h1
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c := by
+  calc  a
+      = a + 0 := rfl
+   _ <= b := ?h
+   _  = b := rfl
+  case h => exact h1
+  exact h2
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c := by
+  calc  _
+     <= b := ?h
+   _  = b := rfl
+  case h => exact h1
+  exact h2
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c := by
+  calc  _
+     <= b := h1
+   _  = b + 0 := rfl
+  exact h2
+
+example (a b c : Nat) (h1 : a <= b) (h2 : b <= c) : a <= c := by
+  calc  a
+     <= b := h1
+   _  = b + 0 := rfl
+  exact h2