From 385cfa6001c17137f6ce857b95c01981af002c19 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 Jul 2022 05:51:02 -0700 Subject: [PATCH] fix: fixes #1372 --- src/Lean/Elab/Tactic/Calc.lean | 2 +- tests/lean/run/1372.lean | 16 ++++++++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/1372.lean diff --git a/src/Lean/Elab/Tactic/Calc.lean b/src/Lean/Elab/Tactic/Calc.lean index 65f24ff9c5..4a704209f7 100644 --- a/src/Lean/Elab/Tactic/Calc.lean +++ b/src/Lean/Elab/Tactic/Calc.lean @@ -18,7 +18,7 @@ def elabCalcSteps (steps : Array Syntax) : TacticM Expr := do where go : TermElabM Expr := do let e ← Term.elabCalcSteps steps - Term.synthesizeSyntheticMVars + Term.synthesizeSyntheticMVars (mayPostpone := false) instantiateMVars e @[builtinTactic calcTactic] diff --git a/tests/lean/run/1372.lean b/tests/lean/run/1372.lean new file mode 100644 index 0000000000..634521784a --- /dev/null +++ b/tests/lean/run/1372.lean @@ -0,0 +1,16 @@ +example (x₁ x₂ y₁ y₂ : Nat) : (x₁ + x₂) + (y₁ + y₂) = (x₁ + y₁) + (x₂ + y₂) := by + calc (x₁ + x₂) + (y₁ + y₂) + = x₁ + (x₂ + (y₁ + y₂)) := by rw [Nat.add_assoc] + _ = x₁ + (y₁ + (x₂ + y₂)) := by rw [Nat.add_left_comm x₂ y₁ y₂] + _ = (x₁ + y₁) + (x₂ + y₂) := by rw [Nat.add_assoc] + + +example (n x₁ x₂ y₁ y₂ : Nat) : n = 0 → (x₁ + x₂) + (y₁ + y₂) = (x₁ + y₁) + (x₂ + y₂) := by + intro h + induction n with + | zero => + calc (x₁ + x₂) + (y₁ + y₂) + = x₁ + (x₂ + (y₁ + y₂)) := by rw [Nat.add_assoc] + _ = x₁ + (y₁ + (x₂ + y₂)) := by rw [Nat.add_left_comm x₂ y₁ y₂] + _ = (x₁ + y₁) + (x₂ + y₂) := by rw [Nat.add_assoc] + | succ _ _ => contradiction