max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: fixes #1372

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-26 05:51:02 -07:00
parent 3896244c55
commit 385cfa6001
2 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/Calc.lean
View file

@ -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]

16
tests/lean/run/1372.lean Normal file
View file

@ -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