Qq list

Stream: Is there code for X?

[Adam Topaz]

Do we have something which can accomplish something similar to the following?

partial def Qq.list {u : Level} {S : Q(Type u)} (L : Q(List $S)) : MetaM (List Q($S)) := do
  let L : Q(List $S) ← whnf L
  match L with
    | ~q([]) => return []
    | ~q($x :: $xs) => return x :: (← Qq.list xs)
    | _ => throwError "Failed"

[Eric Wieser]

I doubt it; though we might have the reverse direction

[Adam Topaz]

Sure, the reverse direction is more "obvious" i guess.

[Eric Wieser]

In general I guess you could generate something like this for any parameterized inductive type?

[Adam Topaz]

What are parameterized inductive types?

[Adam Topaz]

Oh you mean just an inductive type with parameters.

[Adam Topaz]

yes

[Adam Topaz]

But such a function would be more complicated, as one would have to obtain the constructors of that type inside of MetaM, etc.

[Kyle Miller]

Reflection like this wouldn't work for all inductive types, but it seems like it should for a large class of them (For example, what if your inductive type T has a constructor with a Nat -> T argument?)

By the way, Qq pattern matching does defeq tests, so if you care about efficiency you probably would want to match on constructors directly.

Here's just some messing around, adding a couple more of these functions to be able to evaluate Finsets too.

import Lean
import Qq
import Mathlib.Data.Multiset.Basic
import Mathlib.Data.Fintype.Basic

open Lean Meta Qq

/-- Reduce the spine of a List expression to yield a List of expressions. -/
partial def Qq.list {u : Level} {S : Q(Type u)} (L : Q(List $S)) : MetaM (List Q($S)) := do
  match ← whnf L with
    | .app (.const ``List.nil _) _ => return []
    | .app (.app (.app (.const ``List.cons _) _) (x : Q($S))) (xs : Q(List $S)) =>
      return x :: (← Qq.list xs)
    | L' => throwError "Failed to reduce List expression. Got{indentD L'}"

/-- Reduce a Multiset expression to give its underlying List of expressions. -/
partial def Qq.multiset {u : Level} {S : Q(Type u)} (m : Q(Multiset $S)) : MetaM (List Q($S)) := do
  match ← whnfD m with
  | .app (.app (.app (.const ``Quot.mk _) _) _) (L : Q(List $S)) => Qq.list L
  | m' => throwError "Failed to reduce Multiset to a `Quot.mk` application. Got{indentD m'}"

/-- Reduce a Multiset expression to give its underlying List of expressions. -/
partial def Qq.finset {u : Level} {S : Q(Type u)} (s : Q(Finset $S)) : MetaM (List Q($S)) := do
  match ← whnf s with
  | .app (.app (.app (.const ``Finset.mk _) _) (m : Q(Multiset $S))) _ => Qq.multiset m
  | s' => throwError "Failed to reduce Finset to a constructor application. Got{indentD s'}"

#eval show MetaM Unit from do
  let e : Q(Finset Bool) := q(Finset.univ : Finset Bool)
  let l ← Qq.finset e
  dbg_trace "Elements: {l}"
  -- Elements: [Bool.true, Bool.false]

#eval show MetaM Unit from do
  let e : Q(Finset Nat) := q(Finset.range 10 : Finset Nat)
  let l ← Qq.finset e
  dbg_trace "Elements: {l}"
  -- Elements: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

[Kyle Miller]

It would be kind of neat to use a simp-like procedure to do whnf, so that way you can do bigger steps in reduction if you happen to know special properties of a function (or even to be able to reduce things that the kernel can't reduce), while also generating a proof that the result actually represents the original list.

[Thomas Murrills]

Btw, I did something like this (the non-Qq List version) way back when for tfae; I’m on mobile but I believe it’s called something like getExplicitList! (It might be missing a whnf though…) If you’re PRing something feel free to factor it out, rename it, and/or improve it. :)

[Anne Baanen]

We have the non-recursive matching step as docs#Mathlib.Meta.List.proveNilOrCons. I used a definition like you proposed in the Lean 3 norm_num big operators plugin. I found out that it was nicer to only do the case distinction and handle recursion in the tactic itself.