Qq reduceEval: failed to evaluate argument n

Stream: lean4

[Kenny Lau]

import Qq

open Lean Expr Qq

def Nat.mkLiteralQ (n : Nat) : Q(Nat) :=
  have enlit : Q(Nat) := mkRawNatLit n
  q(OfNat.ofNat $enlit)

elab "check_nat%" nStx:num : term =>
  return nStx.getNat.mkLiteralQ
#check 0
#check check_nat% 0
#check 1
#check check_nat% 1
#check 37
#check check_nat% 37

namespace Qq

/-- Given `en : Q(Nat)`, return optionally a natural number `n` and a witness that `en` is defeq
to `OfNat.ofNat (natlit $n)`. -/
def natQ? (en : Q(Nat)) : Option { n : Nat // $en =Q $(n.mkLiteralQ) } :=
  en.nat?.map fun n ↦ ⟨n, ⟨⟩⟩

end Qq
set_option pp.rawOnError true
/-- Interpret a given `e : Expr` as a vector `v : Fin n → Nat`. -/
def test (e : Expr) : MetaM ((n : Nat) × Q(Fin $n → Nat)) := do
  let ⟨1, ~q(Fin $en → Nat), v⟩ ← inferTypeQ e
    | throwError "Invalid input: cannot decompose into Fin n → Nat"
  let .some n := natQ? en
    | throwError "The length of the vector is not determined"
  let ⟨n, _⟩ := n
  let en' : Q(Nat) := n.mkLiteralQ
  have v' : Q(Fin $en' → Nat) := q($v)
  return ⟨n, v'⟩

[Kenny Lau]

I find it slightly difficult to work with Qq, because sometimes the expected type window just stops loading, and I get strange error messages

[Kenny Lau]

e.g. in the code above, on Line 23 the expected type window just fails with error "Error updating: Error fetching goals: Rpc error: InternalError: failed. Try again."

on Line 33 I see the same error, and then Line 34 just stops compiling. What did I do wrong?

[Aaron Liu]

Qq is very picky about what you let and what you have

[Aaron Liu]

Only let something Qq if Qq can recognize the contents

[Kenny Lau]

changing those lets to haves or vice versa doesn't solve anything

[Kenny Lau]

oh btw #check natQ? on L24 is also error

[Kenny Lau]

How should I fix this?

[Aaron Liu]

The problem is the type of natQ?

[Aaron Liu]

Qq can't recognize Nat.mkLiteralQ

[Aaron Liu]

or maybe it can't do the n in the subtype formula, based on the error message

[Aaron Liu]

you will have better luck doing

def natQ? (en : Q(Nat)) :
    Option { n : Nat //
      have k := n.mkLiteralQ
      $en =Q $k } :=

[Kenny Lau]

yeah but then i can't use it afterwards anyway

[Kenny Lau]

like it seems like q($n) is just bad

[Kenny Lau]

import Qq

open Lean Expr Qq

def Nat.mkLiteralQ (n : Nat) : Q(Nat) :=
  have enlit : Q(Nat) := mkRawNatLit n
  q(OfNat.ofNat $enlit)

elab "check_nat%" nStx:num : term =>
  return nStx.getNat.mkLiteralQ
#check 0
#check check_nat% 0
#check 1
#check check_nat% 1
#check 37
#check check_nat% 37

namespace Qq

/-- Given `en : Q(Nat)`, return optionally a natural number `n` and a witness that `en` is defeq
to `OfNat.ofNat (natlit $n)`. -/
def natQ? (en : Q(Nat)) : Option { n : Nat //
    have en' : Q(Nat) := n.mkLiteralQ
    $en =Q $en' } :=
  en.nat?.map fun n ↦ ⟨n, ⟨⟩⟩

end Qq
set_option pp.rawOnError true
/-- Interpret a given `e : Expr` as a vector `v : Fin n → Nat`. -/
def test (e : Expr) : MetaM ((n : Nat) × Q(Fin $n → Nat)) := do
  let ⟨1, ~q(Fin $en → Nat), v⟩ ← inferTypeQ e
    | throwError "Invalid input: cannot decompose into Fin n → Nat"
  let .some ⟨n, _⟩ := natQ? en
    | throwError "The length of the vector is not determined"
  have en' : Q(Nat) := n.mkLiteralQ
  -- have v' : Q(Fin $en' → Nat) := q($v)
  return ⟨n, v'⟩

[Kenny Lau]

This still errors

[Kenny Lau]

is there a better way to use Nat in Qq?

[Aaron Liu]

just do $n maybe

[Aaron Liu]

Don't know if that will work though

[Kenny Lau]

$n also causes errors

[Kenny Lau]

sometimes

[Kenny Lau]

it's very unpredictable (for a noob like me)

[Aaron Liu]

it's unpredictable for me too

[Kenny Lau]

mwe:

import Qq

open Lean Expr Qq

/-- Interpret a given `e : Expr` as a vector `v : Fin n → Nat`. -/
def test (e : Expr) : MetaM ((n : Nat) × Q(Fin $n → Nat)) := do
  let ⟨1, ~q(Fin $en → Nat), v⟩ ← inferTypeQ e
    | throwError "Invalid input: cannot decompose into Fin n → Nat"
  let .some n := en.nat?
    | throwError "The length of the vector is not determined"
  -- have : $en =Q $n := ⟨⟩
  have v' : Q(Fin $n → Nat) := q($v)
  return ⟨n, v'⟩

[Kenny Lau]

Note that the code errors at $v (L12), and if you look at the context you'll see that it's missing the line L11 commented out above, and if you remove the comment then you get another error

[Kenny Lau]

the longer code is when i tried to provide API for nat?

[Wuyang]

working with Qq and Nat literals can be tricky... or avoiding q($n) where possible could help.

Also, you might find related tricks in LeanFinder (www.leanfinder.org).

[Wuyang]

@leanfinder How to correctly quote and unquote Nat values in Lean 4 Qq without type errors when using mkLiteralQ, nat?, and subtype witnesses inside macros or MetaM functions

[leanfinder]

Here’s what I found:

• [definition Mathlib.Meta.NormNum.mkOfNat(α : Q(Type u)) (_sα : Q(AddMonoidWithOne $α)) (lit : Q(ℕ)) :
  MetaM ((a' : Q($α)) × Q($lit = $a')) := do
  if α.isConstOf Nat then let a' : Q(ℕ) := q(OfNat.ofNat $lit : ℕ) pure ⟨a', (q(Eq.refl $a') : Expr)⟩ else if α.isConstOf Int then
  let a' : Q(ℤ) := q(OfNat.ofNat $lit : ℤ)
  pure ⟨a', (q(Eq.refl $a') : Expr)⟩
  else if α.isConstOf `Rat then let a' : Q(ℚ) := q(OfNat.ofNat $lit : ℚ) pure ⟨a', (q(Eq.refl $a') : Expr)⟩ else let some n := lit.rawNatLit? | failure match n with | 0 => pure ⟨q(0 : $α), (q(Nat.cast_zero (R := $α)) : Expr)⟩ | 1 => pure ⟨q(1 : $α), (q(Nat.cast_one (R := $α)) : Expr)⟩ | k+2 => let k : Q(ℕ) := mkRawNatLit k let _x : Q(Nat.AtLeastTwo $lit) := (q(instNatAtLeastTwo (n := $k)) : Expr) let a' : Q($α) := q(OfNat.ofNat $lit) pure ⟨a', (q(Eq.refl $a') : Expr)⟩](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Mathlib.Meta.NormNum.mkOfNat#doc) "Given a type $$\alpha$$ with an AddMonoidWithOne instance and a natural number literal lit, this function constructs an expression a' of type $$\alpha$$ representing the canonical interpretation of lit in $$\alpha$$, along with a proof that lit equals a'. The function handles special cases for $$\alpha$$ being Nat, Int, or Rat directly for efficiency, and falls back to general Nat.cast` for other types." (score: 0.700)

• definition Mathlib.Tactic.AtomM.addAtomQ{u : Level} {α : Q(Type u)} (e : Q($α)) : AtomM (Nat × {e' : Q($α) // $e =Q $e'}) := do let (n, e') ← AtomM.addAtom e return (n, ⟨e', ⟨⟩⟩) "Given an atomic expression e of type α, this function checks if e has been previously encountered (up to definitional equality at the specified transparency level). If it has, it returns the index of the stored version and the stored expression (which is definitionally equal to e). If not, it stores e in the list of atoms and returns its new index along with e itself. The returned expression should be considered the normal form in a normalizing tactic.

This is a strongly-typed version using Qq (quoted expressions) that ensures type safety by maintaining a proof that the returned expression e' is definitionally equal to the input e." (score: 0.695)

• definition Mathlib.Meta.NormNum.mkRawIntLit (n : ℤ) : Q(ℤ) := let lit : Q(ℕ) := mkRawNatLit n.natAbs if 0 ≤ n then q(.ofNat $lit) else q(.negOfNat $lit) "Given an integer $n$, this function constructs a typed expression representing $n$ in Lean's meta-programming environment, using a raw literal representation (.lit (.natVal n)) rather than the standard OfNat.ofNat form. The function handles both non-negative integers (using ofNat) and negative integers (using negOfNat)." (score: 0.686)

• definition Mathlib.Notation3.natLitMatcher (n : Nat) : Matcher := fun s => do guard <| (← getExpr).rawNatLit? == n return s "The function natLitMatcher creates a matcher for raw natural number literals in the notation3 system. Given a natural number n, it checks whether the current expression in the match state is a raw natural number literal equal to n, and if so, returns the unchanged match state." (score: 0.684)

• definition Mathlib.Meta.NormNum.mkRawRatLit (q : ℚ) : Q(ℚ) := let nlit : Q(ℤ) := mkRawIntLit q.num let dlit : Q(ℕ) := mkRawNatLit q.den q(mkRat $nlit $dlit) "Given a rational number \( q \), this function constructs a typed expression representing \( q \) in Lean's meta-programming environment, using raw literal representations for both the numerator (as an integer) and denominator (as a natural number). The construction combines these raw literals via the mkRat function to form the final rational number expression." (score: 0.684)

• definition Mathlib.Tactic.Ring.ExProd.mkNat (n : ℕ) : (e : Q($α)) × ExProd sα e := let lit : Q(ℕ) := mkRawNatLit n ⟨q(($lit).rawCast : $α), .const n none⟩ "Given a natural number n, constructs the expression representing the constant n in the semiring α, along with its representation in the ExProd type (used for normalizing ring expressions). The resulting expression is obtained by casting the natural number literal to the semiring type α." (score: 0.684)

• definition Mathlib.Meta.NormNum.rawIntLitNatAbs (n : Q(ℤ)) : (m : Q(ℕ)) × Q(Int.natAbs $n = $m) := if n.isAppOfArity Int.ofNat 1 then have m : Q(ℕ) := n.appArg! ⟨m, show Q(Int.natAbs (Int.ofNat $m) = $m) from q(Int.natAbs_ofNat $m)⟩ else if n.isAppOfArity Int.negOfNat 1 then have m : Q(ℕ) := n.appArg! ⟨m, show Q(Int.natAbs (Int.negOfNat $m) = $m) from q(Int.natAbs_neg $m)⟩ else panic! "not a raw integer literal" "Given a quoted integer expression n : Q(ℤ), this function returns a pair consisting of:

1. A quoted natural number expression m : Q(ℕ) representing the absolute value of n
2. A proof that the integer absolute value of n equals m (i.e., Q(Int.natAbs $$n = $$m))

The function handles both positive integers (constructed via Int.ofNat) and negative integers (constructed via Int.negOfNat), returning their absolute values with corresponding proofs." (score: 0.677)

• definition Mathlib.Meta.NormNum.Result.ofRawNat {α : Q(Type u)} (e : Q($α)) : Result e := Id.run do let .app (.app _ (sα : Q(AddMonoidWithOne $α))) (lit : Q(ℕ)) := e | panic! "not a raw nat cast" .isNat sα lit (q(IsNat.of_raw $α $lit) : Expr) "Given a typed expression e of type α that is a raw natural number cast (i.e., of the form Nat.cast n), this constructs a Result e containing:

1. The natural number literal lit being cast
2. A proof that e is equal to the coercion of lit into α (i.e., IsNat e lit holds)" (score: 0.676)

• definition Qq.ofNatQ (α : Q(Type $u)) (_ : Q(Semiring $α)) (n : ℕ) : Q($α) := match n with | 0 => q(0 : $α) | 1 => q(1 : $α) | k+2 => have lit : Q(ℕ) := mkRawNatLit n have k : Q(ℕ) := mkRawNatLit k haveI : $lit =Q $k + 2 := ⟨⟩ q(OfNat.ofNat $lit) "The function converts a natural number $n$ into a term of type $\alpha$ (represented as a quoted expression Q($$α)), where $\alpha$ is a type with a semiring structure. For $n = 0$ and $n = 1$, it directly returns the corresponding zero and one elements of $\alpha$. For $n \geq 2$, it constructs the term using the OfNat.ofNat operation with the appropriate numeral." (score: 0.674)

• definition Mathlib.Meta.Nat.unifyZeroOrSucc (n : Q(ℕ)) : MetaM (Nat.UnifyZeroOrSuccResult n) := do match ← isDefEqQ n q(0) with | .defEq pf => return .zero pf | .notDefEq => do let n' : Q(ℕ) ← mkFreshExprMVar q(ℕ) let ⟨(_pf : $n =Q Nat.succ $n')⟩ ← assertDefEqQ n q(Nat.succ $n') let (.some (n'_val : Q(ℕ))) ← getExprMVarAssignment? n'.mvarId! | throwError "could not figure out value of ?n from {n} =?= Nat.succ ?n" pure (.succ n'_val ⟨⟩) "Given a natural number expression n, this function determines whether n is definitionally equal to 0 or can be expressed as Nat.succ k for some natural number k. The function returns a result indicating either that n is zero (with a proof of definitional equality) or that n is a successor (providing the predecessor k)." (score: 0.671)

[Kenny Lau]

I'm not sure if any of these results are relevant

[Kim Morrison]

Yeah, hopefully @Wuyang has learnt that this was really spammy and unhelpful to summon LeanFinder in so many places. :-(