sorting `expr`s that "are" `nat`s

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

I am struggling again with meta-programming. My goal is to find the term of maximum degree in a term of a polynomial ring. For simplicity, the code below is adapted to the situation where the input is an expression of the form X ^ a + X ^ b + ... + X ^z.

I can get Lean to extract the list of exponents [a, b,..., z] (see list_exponents below).

My issue is that the extracted list is a list of exprs and I do not know if there is a way to compare them knowing that they really are terms of type nat. I am happy to get trash values for exprs that are not nats or involve variables. I tried to_nat, but it gives none if the expression is 0 + 0, whereas I would like it to be interpreted as some 0 (or some (0 + 0)).

import data.polynomial.degree.lemmas

open tactic interactive expr

namespace tactic.interactive
setup_tactic_parser

meta def get_summands : expr → list expr
| `(%%a + %%b) := get_summands a ++ get_summands b
| a            := [a]

/--  Given an expression `e`, assuming it is a polyomial, `guess_deg e` tries to guess the
`nat_degree` of `e`. -/
meta def guess_deg (e : expr) : tactic expr :=
do
  let n0 := to_expr ``(nat.zero),
  let n1 := to_expr ``(nat.zero.succ),
  pX ← to_expr ``(polynomial.X),
  match e.app_fn with
  | `(coe_fn $ polynomial.C) := n0
  | a := do
          bo ← succeeds $ unify e pX,
          if bo then n1 else
            ( do let margs := e.get_app_args,
              margs.nth 4 >>= return ) <|>
            ( do val ← to_expr ``(polynomial.nat_degree),
              return $ expr.mk_app val [e] )
          end

/--  My work-in-progress `tactic`.  Using `list_exponents` shows the effect of the tactic-so-far. -/
meta def list_exponents : tactic unit :=
do `(polynomial.nat_degree %%tl = %%tr) ← target,
  let summ := (get_summands tl),
  rere ← summ.mmap guess_deg,
  trace "list of exponents",
  trace rere,
  trace "list of to_nats",
  trace $ rere.map expr.to_nat

end tactic.interactive

open polynomial
open_locale polynomial
variables {R : Type*} [semiring R] {f g h : R[X]} {a b c d e : R}

lemma pro {h : C d ≠ 0} (f10 : f.nat_degree ≤ 10) :
  nat_degree (X ^ (0 + 0) + X ^ (1 * 1) + X + X ^ 5 : R[X]) = 10 :=
begin
  list_exponents,
/-
  list of exponents
  [0 + 0, 1 * 1, 1, 5]
  list of to_nats
  [none, none, (some 1), (some 5)]
-/
end

Is there a way to obtain that 5 should be the highest value above?

[Johan Commelin]

I guess you would have to hit the expressions with norm_num first. Or something like that.

[Damiano Testa]

Can i use norm_num on exprs?

[Damiano Testa]

Or did you mean to convert it to "tactic-mode" and do the sorting there?

[Mario Carneiro]

rere.mmap (λ e, do (e', _) ← norm_num.derive e <|> refl_conv e, e'.to_nat)

[Damiano Testa]

Mario, thanks a lot! This is awesome: I had no idea that norm_num could be used in this context!

[Mario Carneiro]

There is another method that works if the expressions actually have type nat and not just some semiring type: rere.mmap (eval_expr ℕ)

[Mario Carneiro]

this is basically just calling #eval on the expression, so it's probably preferable if applicable

[Damiano Testa]

Ok, in my use case, I will have things that are really numbers, but I would also like to support the possibility of variables, as in (n : nat), X ^ n. I may try to sort the two things in separate lists and see if I can get the eval_expr to work.

[Damiano Testa]

Of course, when there are variables, I will have to find a heuristic to decide whether n is bigger or not than 3.

[Damiano Testa]

Anyway, right now I'm still taking apart your initial code to see how it works and how to adapt it.

[Damiano Testa]

Re-reading your comment, it seems that I will have nats the whole time, even if I have variables. The types should always be natural numbers, since otherwise they are not nat_degrees of polynomials!

[Damiano Testa]

So I think that eval_expr ℕ should work. I'll keep on testing.

[Damiano Testa]

I really like that I'm using #eval "inside" a proof!

[Mario Carneiro]

both methods will fail when you have variables, of course. You can wrap the expression in try_core to get a none if it's not a constant

[Damiano Testa]

Ok, thanks! I was running into problems experimenting with these methods.

[Patrick Massot]

Damiano, since you seem interested in learning meta-programming, did you consider learn it in Lean 4 instead? We really really need more people porting tactics to Lean 4 instead of creating more Lean 3 tactics that need to be ported.

[Damiano Testa]

Patrick, I am using this project as an excuse to learn some (meta)programming with a language that is more stable than Lean4. I was planning to switch to Lean4, once I feel that I am able to produce my own code, rather than modifying pre-existing tactics.

Also, I have Lean3 installed, but am a little intimidated by installing Lean4...

[Arthur Paulino]

In my current experience, learning about metaprogramming in Lean 3 helped me to understand what metaprogramming is. But since the API is so drastically different and the overall monadic programming experience is much richer in Lean 4 if compared to Lean 3, it almost feels like I'm starting from scratch

[Arthur Paulino]

Note: I don't mean to demotivate your learning, of course! Metaprogramming in Lean 3 is fun and I enjoy learning more about it to this day. I just wanted to question the idea of knowledge transfer from Lean 3 to Lean 4 regarding metaprogramming, which did not feel smooth for me

[Damiano Testa]

Ok, I'm going to produce quickly a working version of the compute_degree tactic in Lean3, and after that, I will port move_add to Lean4!

[Jannis Limperg]

The core metaprogramming APIs are pretty stable in Lean 4 as well btw. I move a substantial project to the latest nightly every two weeks or so and most of the time this requires no or very few changes.

[Damiano Testa]

Ok, thanks for the information and the encouragement!