## Stream: lean4

### Topic: microcalc

#### Daniel Selsam (Feb 05 2021 at 01:45):

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 (Feb 05 2021 at 01:45):

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 (Feb 05 2021 at 01:49):

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

#### Mario Carneiro (Feb 05 2021 at 01:51):

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 (Feb 05 2021 at 02:45):

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 (Feb 05 2021 at 02:46):

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

#### Mario Carneiro (Feb 05 2021 at 02:46):

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

#### Mario Carneiro (Feb 05 2021 at 02:48):

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 (Feb 05 2021 at 02:54):

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

#### Mario Carneiro (Feb 05 2021 at 02:54):

sure, that works too

#### Daniel Selsam (Feb 05 2021 at 02:55):

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 (Feb 05 2021 at 02:55):

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

#### Mario Carneiro (Feb 05 2021 at 02:55):

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

#### Kevin Buzzard (Feb 05 2021 at 06:07):

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 (Feb 05 2021 at 06:09):

I use it regularly in mathlib code

#### Sebastien Gouezel (Feb 05 2021 at 07:53):

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 (Feb 05 2021 at 10:47):

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 (Feb 05 2021 at 10:50):

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

#### Kevin Buzzard (Feb 05 2021 at 10:53):

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.

Last updated: May 07 2021 at 13:21 UTC