feat: PiFin.mkLiteralQ and Matrix.mkLiteralQ (#24101)

This defines some new functions to match the `Qq.mkSetLiteralQ` from #23025. The commented `pexpr` function is really just the syntax quotation `` `(![$xs,*]) ``, so it is no longer worth keeping around.

This deliberately uses `Fin n → Q($α)` instead of `Vector Q($α) n` as the former saves needing to allocate an auxiliary array, and the latter still can be used by passing in `v.get : Fin n → Q($α)`. 

This also cleans up and adds some related tests.



Co-authored-by: Eric Wieser <efw@google.com>

Author: eric-wieser

Mathlib/Data/Fin/VecNotation.lean

@@ -252,26 +252,25 @@ theorem cons_val_fin_one (x : α) (u : Fin 0 → α) : ∀ (i : Fin 1), vecCons
 theorem cons_fin_one (x : α) (u : Fin 0 → α) : vecCons x u = fun _ => x :=
   funext (cons_val_fin_one x u)
 
+open Lean Qq in
+/-- `mkVecLiteralQ ![x, y, z]` produces the term `q(![$x, $y, $z])`. -/
+def _root_.PiFin.mkLiteralQ {u : Level} {α : Q(Type u)} {n : ℕ} (elems : Fin n → Q($α)) :
+    Q(Fin $n → $α) :=
+  loop 0 (Nat.zero_le _) q(vecEmpty)
+where
+  loop (i : ℕ) (hi : i ≤ n) (rest : Q(Fin $i → $α)) : let i' : Nat := i + 1; Q(Fin $(i') → $α) :=
+    if h : i < n then
+      loop (i + 1) h q(vecCons $(elems (Fin.rev ⟨i, h⟩)) $rest)
+    else
+      rest
+attribute [nolint docBlame] _root_.PiFin.mkLiteralQ.loop
+
 open Lean Qq in
 protected instance _root_.PiFin.toExpr [ToLevel.{u}] [ToExpr α] (n : ℕ) : ToExpr (Fin n → α) :=
   have lu := toLevel.{u}
   have eα : Q(Type $lu) := toTypeExpr α
-  have toTypeExpr := q(Fin $n → $eα)
-  match n with
-  | 0 => { toTypeExpr, toExpr := fun _ => q(@vecEmpty $eα) }
-  | n + 1 =>
-    { toTypeExpr, toExpr := fun v =>
-      have := PiFin.toExpr n
-      have eh : Q($eα) := toExpr (vecHead v)
-      have et : Q(Fin $n → $eα) := toExpr (vecTail v)
-      q(vecCons $eh $et) }
-
--- TODO(eric-wieser): the next decl is commented out.
-
--- /-- Convert a vector of pexprs to the pexpr constructing that vector. -/
--- unsafe def _root_.pi_fin.to_pexpr : ∀ {n}, (Fin n → pexpr) → pexpr
---   | 0, v => ``(![])
---   | n + 1, v => ``(vecCons $(v 0) $(_root_.pi_fin.to_pexpr <| vecTail v))
+  let toTypeExpr := q(Fin $n → $eα)
+  { toTypeExpr, toExpr v := PiFin.mkLiteralQ fun i => show Q($eα) from toExpr (v i) }
 
 /-! ### `bit0` and `bit1` indices
 The following definitions and `simp` lemmas are used to allow

Mathlib/Data/Matrix/Notation.lean

@@ -49,6 +49,13 @@ section toExpr
 
 open Lean Qq
 
+open Qq in
+/-- `Matrix.mkLiteralQ !![a, b; c, d]` produces the term `q(!![$a, $b; $c, $d])`. -/
+def mkLiteralQ {u : Level} {α : Q(Type u)} {m n : Nat} (elems : Matrix (Fin m) (Fin n) Q($α)) :
+    Q(Matrix (Fin $m) (Fin $n) $α) :=
+  let elems := PiFin.mkLiteralQ (α := q(Fin $n → $α)) fun i => PiFin.mkLiteralQ fun j => elems i j
+  q(Matrix.of $elems)
+
 /-- Matrices can be reflected whenever their entries can. We insert a `Matrix.of` to
 prevent immediate decay to a function. -/
 protected instance toExpr [ToLevel.{u}] [ToLevel.{uₘ}] [ToLevel.{uₙ}]

MathlibTest/matrix.lean

@@ -57,12 +57,13 @@ def mkMatrix (rows : Array (Array Term)) : Term := Unhygienic.run `(!![$[$[$rows
 def mkColumnVector (elems : Array Term) : Term := Unhygienic.run `(!![$[$elems];*])
 
 -- Check that the `!![$[$[$rows],*];*]` case can deal with empty arrays even though it uses sepBy1
-run_cmd liftTermElabM do
+run_elab do
   let e ← Term.elabTerm (mkMatrix #[]) q(Matrix (Fin 0) (Fin 0) Nat)
   Term.synthesizeSyntheticMVarsUsingDefault
   let e ← instantiateMVars e
   guard <| e == q(!![] : Matrix (Fin 0) (Fin 0) Nat)
 
+run_elab do
   let e ← Term.elabTerm (mkColumnVector #[]) q(Matrix (Fin 0) (Fin 0) Nat)
   Term.synthesizeSyntheticMVarsUsingDefault
   let e ← instantiateMVars e
@@ -76,6 +77,22 @@ end safety
 #guard !![1,2;3,4;]  = of ![![1,2], ![3,4]]
 #guard !![1,2,;3,4,] = of ![![1,2], ![3,4]]
 
+section to_expr
+
+open Lean Meta
+
+/-- info: !![1 + 1, 1 + 2; 2 + 1, 2 + 2] : Matrix (Fin 2) (Fin 2) ℕ -/
+#guard_msgs in
+#check by_elab return Matrix.mkLiteralQ !![q(1 + 1), q(1 + 2); q(2 + 1), q(2 + 2)]
+
+run_elab do
+  let x := !![1, 2; 3, 4]
+  guard (← withReducible <| isDefEq (toExpr x) q(!![1, 2; 3, 4]))
+
+end to_expr
+
+section delaborators
+
 /-- info: !![0, 1, 2; 3, 4, 5] : Matrix (Fin 2) (Fin 3) ℕ -/
 #guard_msgs in #check (!![0, 1, 2; 3, 4, 5] : Matrix (Fin 2) (Fin 3) ℕ)
 
@@ -91,6 +108,8 @@ end safety
 /-- info: !![] : Matrix (Fin 0) (Fin 0) ℕ -/
 #guard_msgs in #check (!![] : Matrix (Fin 0) (Fin 0) ℕ)
 
+end delaborators
+
 example {a a' b b' c c' d d' : α} :
   !![a, b; c, d] + !![a', b'; c', d'] = !![a + a', b + b'; c + c', d + d'] := by
   simp

MathlibTest/vec_notation.lean

@@ -11,18 +11,22 @@ open Qq
 set_option linter.style.setOption false in
 set_option pp.unicode.fun false
 
+/-- info: ![1, 1 + 1, 1 + 1 + 1] : Fin (Nat.succ 2) → ℤ -/
+#guard_msgs in
+#check by_elab return PiFin.mkLiteralQ ![q(1 : ℤ), q(1 + 1), q(1 + 1 + 1)]
+
 /-! These tests are testing `PiFin.toExpr` and fail with
 `local attribute [-instance] PiFin.toExpr` -/
 
-run_cmd Elab.Command.liftTermElabM do
+run_elab do
   let x : Fin 0 → ℕ := ![]
   guard (← isDefEq (toExpr x) q((![] : Fin 0 → ℕ)))
 
-run_cmd Elab.Command.liftTermElabM do
+run_elab do
   let x := ![1, 2, 3]
   guard (← isDefEq (toExpr x) q(![1, 2, 3]))
 
-run_cmd Elab.Command.liftTermElabM do
+run_elab do
   let x := ![![1, 2], ![3, 4]]
   guard (← isDefEq (toExpr x) q(![![1, 2], ![3, 4]]))