Zulip Chat Archive

Stream: lean4

Topic: microcalc


view this post on Zulip 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)))

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 05 2021 at 01:49):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Daniel Selsam (Feb 05 2021 at 02:54):

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

view this post on Zulip Mario Carneiro (Feb 05 2021 at 02:54):

sure, that works too

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 05 2021 at 02:55):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 05 2021 at 06:09):

I use it regularly in mathlib code

view this post on Zulip 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 :=.

view this post on Zulip 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'

view this post on Zulip Sebastian Ullrich (Feb 05 2021 at 10:50):

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

view this post on Zulip 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