!4#3215 and data.matrix.notation

Stream: mathlib4

[Jireh Loreaux]

It seems that !4#3215 (meta code) is holding up data.matrix.notation, which is now at the top of the port dashboard (with 614 dependents). From my, admittedly unexperienced, eyes, this seems like it's ready. Is there any reason we're not merging it?

[Eric Wieser]

!4#3215

[Eric Wieser]

In principle we could port data.matrix.notation without the actual notation, and comment out all the lemmas that use the notation (there aren't all that many)

[Jireh Loreaux]

But isn't 3215 ready? Is it controversial or unfinished for some reason I'm missing?

[Eric Wieser]

It might well be, there just aren't many people qualified to review (and I don't really consider myself one of them)

[Jireh Loreaux]

Indeed, I'm just looking to get some experienced eyes on it since data.matrix.notation is at the top of the #port-dashboard. @Mario Carneiro or @Scott Morrison, if you have the time to look it would be great. If not, I understand.

[Scott Morrison]

Sorry about the long delay on this one. I've merged.

[Eric Wieser]

I'll make a start on data.matrix.notation

[Eric Wieser]

It looks like there's a bug in start_port.sh that makes it think entries in #port-comments are porting PRs...

[Eric Wieser]

@Mario Carneiro, how much work is it to teach mathport about !![] syntax? (And ask it to leave it alone)

[Mario Carneiro]

If it was defined with notation then it should just work. What is it doing currently?

[Eric Wieser]

It's @[user_notation] (docs#matrix.notation)

[Eric Wieser]

I don't expect to get valid lean4 code to parse the syntax

[Eric Wieser]

But right now every lemma with !![a, b; c, d] in it gets replaced with «expr!![ » and the a, b; c, d are dropped completely

[Mario Carneiro]

Oh, I didn't know mathlib had any user notations, somehow this fell through the cracks during the original census

[Mario Carneiro]

!4#3429 has to be merged before mathport can be updated

[Eric Wieser]

Is there a reason that doesn't know about ", "?

[Eric Wieser]

The full breadth of syntax is outlined here: https://github.com/leanprover-community/mathlib/blob/master/test/matrix.lean#L27-L35

[Mario Carneiro]

It does both ; and ,, although I don't know what's up with those empty cells in your quote

[Mario Carneiro]

i.e. !![1, 2; 3, 4; 5, 6] was tested and works

[Mario Carneiro]

but not !![;;]

[Mario Carneiro]

what does that even mean?

[Mario Carneiro]

if you want to write the syntax I'll use it

[Mario Carneiro]

mathport#235

[Eric Wieser]

!![;;] is a 0x2 matrix

[Eric Wieser]

But I guess we can always improve the handling of those corner cases laterr

[Mario Carneiro]

How about this:

syntax (name := matrixNotation) "!![" sepBy1(term,+, "; ") "]" : term
syntax (name := matrixNotationCx0) "!![" ";"* "]" : term
syntax (name := matrixNotation0xR) "!![" ","+ "]" : term

[Eric Wieser]

I'm afraid I haven't learnt how to read Lean4 syntax yet

[Eric Wieser]

But that looks plausible

[Eric Wieser]

Trailing commas and ; are legal (no-ops) in matrixNotation too

[Mario Carneiro]

you can test it out by writing #check !![1, 2] immediately afterward

[Eric Wieser]

I think adding allowTrailingSep will do the job

[Mario Carneiro]

syntax (name := matrixNotation) "!![" sepBy1(term,+,?, ";", "; ", allowTrailingSep) "]" : term
syntax (name := matrixNotationCx0) "!![" ";"* "]" : term
syntax (name := matrixNotation0xR) "!![" ","+ "]" : term

#check !![1,;2,3,;]

[Mario Carneiro]

it's a thing of beauty

[Eric Wieser]

That passes all my tests:

#check !![]
#check !![;]
#check !![;;]
#check !![,]
#check !![,,]
#check !![1]
#check !![1,]
#check !![1;]
#check !![1,2;3,4]

#check !![1;2]
#check !![1,3]
#check !![1,2;3,4]
#check !![1,2;3,4;]
#check !![1,2,;3,4,]

[Eric Wieser]

Though the names are maybe backwards, matrixNotationCx0 is the column matrix with C rows and 0 columns; so maybe Rx0 is better

[Reid Barton]

Wow I never knew about @[user_notation]!

[Eric Wieser]

Unfortunately all the time I spent trying to work out what it did in lean 3 is now useless in lean 4!

[Eric Wieser]

Here's some more prework for data.matrix.notation: !4#3430. For reasons I haven't attempted to understand, adding this ToExpr instance (or the imports needed to add it) has made a very-downstream rw more powerful

[Eric Rodriguez]

!4#3430

[Eric Wieser]

I'd appreciate some lean4 metaprogramming help in the tests in !4#3427; the Lean 3 code was

meta def get_dims (e : pexpr) : tactic (expr × expr) :=
do
  elem_t ← tactic.mk_meta_var (expr.sort level.zero.succ),
  e ← tactic.to_expr ``(%%e : matrix _ _ %%elem_t) tt ff,
  t ← tactic.infer_type e,
  `(matrix.{0 0 0} (fin %%m) (fin %%n) %%elem_t) ← tactic.infer_type e,
  return (m, n)

which essentially just elaborates e with type matrix _ _ X for some unspecified X, and then verifies that the result matches matrix (fin m) (fin n) _. I've made an uneducated guess at what the translation might be, but it doesn't actually compile and it would probably be easier for someone already familiar with Lean4 meta code to finish it up

[Eric Wieser]

My lean 4 attempt is

def getDims (e : Lean.TSyntax `term) : Lean.MetaM (Q(Nat) × Q(Nat)) :=
do
  let elem_t ← mkFreshExprMVarQ q(Type)
  let e ← Lean.Elab.Term.elabTerm e (some q(Matrix _ _ $elem_t)) true false
  let t ← Lean.Meta.inferType e
  let ~q(Matrix (Fin $m) (Fin $n) $elem_t) ← t | failure
  return (m, n)

[Kyle Miller]

@Eric Wieser I wasn't sure how to use qq here, but I think I got getDims working. I also added support for trailing separators, given that some of the tests had them.

[Eric Wieser]

Thanks! It looks like my confusion was caused by not knowing what the lean 4 version of pexpr is; I guess it's docs4#Lean.Term not Syntax?

[Kyle Miller]

I think pexpr sort of corresponds to Term (which is TSyntax `term, which is a thin wrapper around Syntax just to keep track of what the syntax is for -- Syntax is sort of like a raw s-expression with source position information). Lean 4 is more careful about distinguishing Syntax vs Expr, rather than trying to do everything with unelaborated exprs vs elaborated exprs.

[Thomas Murrills]

Just exploring a bit here—thought I'd share a variation of Kyle's solution that uses Qq (and shortens the overall test syntax). Oddly the have el : Q(Type v) is necessary for q(Matrix ...) to work, even though el : Q(Type v) already appears in the context. I wonder if this is a Qq bug (something to do with ldecls, maybe?).

syntax "#guard_dims " term ":" term : command

open Lean Meta Elab Term Command in
elab_rules : command
| `(command|#guard_dims $e : $dims) => liftTermElabM <| do
  let dims ← instantiateMVars <|← elabTerm dims (some q(Nat × Nat))
  let m ← mkFreshExprMVarQ q(Nat)
  let n ← mkFreshExprMVarQ q(Nat)
  let v ← mkFreshLevelMVar
  let el ← mkFreshExprMVarQ q(Type v); have el : Q(Type v) := el
  let _ ← elabTerm e (some q(Matrix (Fin $m) (Fin $n) $el))
  Elab.Term.synthesizeSyntheticMVarsUsingDefault
  let dims' ← instantiateMVars q(($m,$n))
  unless dims' == dims do
    throwError "inferred dimensions {dims'} are not exactly equal to {dims}"

#guard_dims !![] : (0, 0)
#guard_dims !![;] : (1, 0)
#guard_dims !![;] : (Nat.succ 0, 0) -- inferred dimensions (1, 0) are not exactly equal to (Nat.succ 0, 0)

[Kyle Miller]

@Thomas Murrills Nice idea to use a command. I'm still seeming to have troubles with using qq so I didn't use your code directly, but I've used your idea to make a #guard command and a dims% elaborator, so you can write

#guard dims% !![1,2;3,4] is (2, 2)

There's a #guard x is y command and a #guard x command, where the first checks that they elaborate to the same thing and the second checks that x is a Bool that evaluates to true (allowing you to do #guard x = y when you have decidable equality for value-based equality). (commit)

(edit: in a more recent commit it now looks like #guard_expr dims% !![1,2;3,4] =ₛ (2, 2) to match the guard_expr tactic)

[Jeremy Tan]

By the way, mathport seems to be handling matrix notation fairly well now: https://github.com/leanprover-community/mathlib3port/commit/ce473067ae4fc0609b3199853f1de1c5ede921cf#diff-1a50515965a8e7d8b2cb284a9c8f815b7aabef01bda2b89d74f950e28a82c9c1

[Jeremy Tan]

There's just the constant /- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/, but the non-commented output looks fine

[Eric Wieser]

Oh, I thought we'd have to wait overnight for that to have an effect

[Eric Wieser]

It's unfortunate that it loses our nice formatting, translating

def E₆ : matrix (fin 6) (fin 6) ℤ := !![ 2,  0, -1,  0,  0,  0;
                                         0,  2,  0, -1,  0,  0;
                                        -1,  0,  2, -1,  0,  0;
                                         0, -1, -1,  2, -1,  0;
                                         0,  0,  0, -1,  2, -1;
                                         0,  0,  0,  0, -1,  2]

to

def e₆ : Matrix (Fin 6) (Fin 6) ℤ :=
  !![2, 0, -1, 0, 0, 0; 0, 2, 0, -1, 0, 0; -1, 0, 2, -1, 0, 0; 0, -1, -1, 2, -1, 0; 0, 0, 0, -1, 2,
    -1; 0, 0, 0, 0, -1, 2]

[Eric Wieser]

Does Syntax have a way of specifying preferred positions for line-breaks like Std.Format does?

[Eric Wieser]

If not, can we teach mathport to output -- porting todo: please re-wrap or something?

[Jeremy Tan]

It's only the fetching of data from mathlib3 that runs every day. The script that parses the mathlib3 notation and pushes the results to mathlib3port runs every 2 hours

[Eric Wieser]

Right; I wasn't sure where the line between "fetching mathlib3 data" and "parsing mathlib3 notation" fell

[Eric Wieser]

Fixed with help from Gabriel Ebner; it's now

def e₆ : Matrix (Fin 6) (Fin 6) ℤ :=
  !![2, 0, -1, 0, 0, 0;
    0, 2, 0, -1, 0, 0;
    -1, 0, 2, -1, 0, 0;
    0, -1, -1, 2, -1, 0;
    0, 0, 0, -1, 2, -1;
    0, 0, 0, 0, -1, 2]

which I think is probably ok enough not to worry about.

[Eric Wieser]

Jeremy Tan said:

There's just the constant /- ./././Mathport/Syntax/Translate/Tactic/Basic.lean:31:4: unsupported: too many args: matrix.notation ... #[[]] -/, but the non-commented output looks fine

@Mario Carneiro, is removing these comments an easy fix?

[Mario Carneiro]

if it's producing those comments then it's broken

[Eric Wieser]

Is this something to do with docs#matrix.notation taking two arguments, a dummy token and then the actual parser?

[Mario Carneiro]

oh, I think it is not that but rather the matrix.notation is itself a value of type parser expr, i.e. it can do more parsing in the body. I think it doesn't, from what I can tell, but it still makes a nullary call to the parser (equivalent to an extra argument parse (pure ())) which should be accounted for

[Mario Carneiro]

it would have made more sense to just put the val part inside the body, that's what other user notations do

[Eric Wieser]

I don't think I had many examples to go by when I wrote it

[Eric Wieser]

Are you proposing changing mathlib3, or just adding a hack in mathport? The latter has the advantage of being 24 hours faster

[Eric Wieser]

(I guess cleaning up all the comments during porting is also an option, but not a great one)

[Mario Carneiro]

it's a one line change in mathport, so I'll just do that

[Mario Carneiro]

(which takes an hour to test)

[Jeremy Tan]

Mario Carneiro said:

(which takes an hour to test)

It passed: https://github.com/leanprover-community/mathlib3port/commit/7809aa1d4c28275702b162020c7a69e28593397e#diff-6d63022fcbe48e608f5e19d1e048ee1f19b2ec0f33bdc1db4293f74dc3314712

[Jeremy Tan]

How close is !4#3215 to being merged?

[Arthur Paulino]

!4#3225

[Arthur Paulino]

It's missing the awaiting-review label

[Jeremy Tan]

Yes, now what?

[Arthur Paulino]

Now it's awaiting review

[Jeremy Tan]

wait… I meant !4#3427

[Eric Wieser]

The remaining work is the PR the guard_expr stuff separately

[Eric Wieser]

cc @Kyle Miller

[Eric Wieser]

I don't know if we would prefer to put it straight in std, or just dump it in the test directory and move it later

[Scott Morrison]

I merged. Let's still clean up #guard_expr, however! I've been wanting this elsewhen.