feat: calc

src/Init/NotationExtra.lean

@@ -93,6 +93,14 @@ macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``PSi
 macro:35 xs:bracketedExplicitBinders " × " b:term:35  : term => expandBrackedBinders ``Sigma xs b
 macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b
 
+-- enforce indentation of calc steps so we know when to stop parsing them
+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*))
+
 @[appUnexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
   | _       => throw ()

src/Init/Prelude.lean

@@ -380,6 +380,18 @@ class LT (α : Type u) where lt : α → α → Prop
 @[inline] def min [LE α] [DecidableRel (@LE.le α _)] (a b : α) : α :=
   ite (LE.le a b) a b
 
+/-- Transitive chaining of proofs, used e.g. by `calc`. -/
+class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α → γ → Prop)) where
+  trans : r a b → s b c → t a c
+
+export Trans (trans)
+
+instance (r : α → γ → Prop) : Trans Eq r r where
+  trans heq h' := heq ▸ h'
+
+instance (r : α → β → Prop) : Trans r Eq r where
+  trans h' heq := heq ▸ h'
+
 class HAdd (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   hAdd : α → β → γ
 

tests/lean/run/calc.lean

@@ -0,0 +1,23 @@
+variable (t1 t2 t3 t4 : Nat)
+variable (pf12 : t1 = t2) (pf23 : t2 = t3) (pf34 : t3 = t4)
+
+theorem foo : t1 = t4 :=
+  calc
+    t1 = t2 := pf12
+     _ = t3 := id
+     _ = t4 := pf34
+
+variable (t5 : Nat)
+variable (pf23' : t2 < t3) (pf45' : t4 < t5)
+
+instance [LT α] : Trans (α := α) (· < ·) (· < ·) (· < ·) where
+  trans := sorry
+
+theorem foo' : t1 < t5 :=
+  let p := calc
+   t1 = t2 := pf12
+    _ < t3 := pf23'
+    _ = t4 := pf34
+    _ < t5 := pf45'
+  -- dedent terminates the block
+  p