From 5e877b115b617d072ba28a3db57f3fcce777519b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Jul 2022 14:20:55 -0700 Subject: [PATCH] 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 | 2 ++ src/Init/NotationExtra.lean | 3 +- src/Lean/Elab/Calc.lean | 37 ++++++++++--------- src/Lean/Elab/Tactic.lean | 1 + src/Lean/Elab/Tactic/Calc.lean | 47 ++++++++++++++++++++++++ src/Lean/Elab/Tactic/ElabTerm.lean | 12 +++++-- tests/lean/run/1342.lean | 58 ++++++++++++++++++++++++++++++ 7 files changed, 138 insertions(+), 22 deletions(-) create mode 100644 src/Lean/Elab/Tactic/Calc.lean create mode 100644 tests/lean/run/1342.lean diff --git a/RELEASES.md b/RELEASES.md index 1c45fb18be..5c872585b0 100644 --- a/RELEASES.md +++ b/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: diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 97dd75f224..6e4828ef8d 100644 --- a/src/Init/NotationExtra.lean +++ b/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 | `($(_)) => `(()) diff --git a/src/Lean/Elab/Calc.lean b/src/Lean/Elab/Calc.lean index 03c31dbe49..758f614104 100644 --- a/src/Lean/Elab/Calc.lean +++ b/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. diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index 63a49bd0ed..93d03796f7 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/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 diff --git a/src/Lean/Elab/Tactic/Calc.lean b/src/Lean/Elab/Tactic/Calc.lean new file mode 100644 index 0000000000..bfedc8d818 --- /dev/null +++ b/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 diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index a656a2478e..663f45f190 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/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 diff --git a/tests/lean/run/1342.lean b/tests/lean/run/1342.lean new file mode 100644 index 0000000000..b3d98bb8dc --- /dev/null +++ b/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