microcalc

Stream: lean4

[Daniel Selsam]

Missing features but super cool that you can write this in Lean itself:

open Lean

syntax calcStep  := "..." "=" term:max ":" term
syntax "calc " term:max "=" term ":" term calcStep* : term

partial def expandCalc (rest : Array Syntax) (i : Nat) (stx : Syntax) : MacroM Syntax := do
  if i == rest.size then stx else
    let newStx ← `(Eq.trans $stx ($(rest[i][4]) : _ = $(rest[i][2])))
    expandCalc rest (i+1) newStx

macro_rules
  | `(calc $t1:term = $t2:term : $pf12:term $rest:calcStep*) => do
    expandCalc rest 0 (← `(($pf12 : $t1 = $t2)))

[Daniel Selsam]

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 : pf23
     ... = t4 : pf34

[Scott Morrison]

Now the "relation-polymorphic" version, that allows using other transitive relations besides equality?

[Mario Carneiro]

that seems rather hard, since you would need to add a production for any infix operation. Is it possible to have a programmatic parser at the location of the "=" that does a lookup into the current set of notations to see what infix ops exist?

[Daniel Selsam]

Scott Morrison said:

Now the "relation-polymorphic" version, that allows using other transitive relations besides equality?

I am already exporting Mathlib relation manager attributes, so it wouldn't be hard to replicate the lean3 calc mode. @Mario Carneiro the trick is to elaborate the expression up until the : (which will resolve notation) and then just grab the operator name.

[Mario Carneiro]

That doesn't work for ... <= n though, because that's not a valid expression (nor is <= n)

[Mario Carneiro]

the syntax associated to the infix operator is something like term "<=" term and that doesn't admit either form

[Mario Carneiro]

Perhaps it's possible to fake it by replacing ... in the input with some placeholder that is a term like () and then parse () <= n and postprocess the result

[Daniel Selsam]

I can replace ... with the actual term, i.e. the rhs of the previous line

[Mario Carneiro]

sure, that works too

[Daniel Selsam]

Do people want the exact same calc as before though? I was only implementing microcalc for fun. I am happy to implement a durable calc if people will use it.

[Mario Carneiro]

I'm not sure how you would go about replacing a term in the input stream though

[Mario Carneiro]

I'm sure people will want calc, although it's probably not a high priority ATM

[Kevin Buzzard]

I was using calc with <= and < and = for teaching analysis in lean 3 yesterday, but I don't think I've ever used it in the mathlib code I've written

[Johan Commelin]

I use it regularly in mathlib code

[Sebastien Gouezel]

I use it a lot also. One point that was raised earlier is that it would make sense to have a syntax which resembles more closely other syntax, for instance replacing the weird : with :=.

[Sebastian Ullrich]

Here's one solution for a heterogeneous calc based on a Trans typeclass and ... as a term notation:

class Trans (r : α → β → Prop) (s : β → γ → Prop) (t : outParam (α → γ → Prop)) where
  trans {a b c} : 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'

notation "..." => _
-- enforce indentation of calc steps so we know when to stop parsing them
syntax calcStep := colGe term " := " 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*))

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 := pf23
   ... = t4 := pf34

variable (t5 : Nat)
variable (pf23' : t2 < t3) (pf45' : t4 < t5)

instance [HasLess α] : Trans (α := α) Less Less Less where
  trans := sorry

theorem foo' : t1 < t5 :=
 calc
   t1 = t2 := pf12
   ... < t3 := pf23'
   ... = t4 := pf34
   ... < t5 := pf45'

[Sebastian Ullrich]

In fact ... is now barely carrying its weight and one should probably just use _ directly

[Kevin Buzzard]

I am really not engaged with Lean 4 at all, because as a mathematician with essentially no programming background but ambitions to do serious mathematics in Lean, all I know is that Lean 4 is basically useless to me until I can have mathlib. However I am extremely impressed with the way that people are doing things like this -- "oh by the way there's no calc right now, but of course if you want one then you can just knock one up in a few lines of code". I've never written a line of meta code in my life and I suspect I won't be writing too many macros either, but I can really see that we have something exciting to look forward to.