avoid `const_name`?

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

to generalize move_add to something that also takes an operation as an input, I would like to match the user supplied operation (e.g. +, *) with the expression that comes from the actual lemma. I found a very convoluted way of doing this, that you can see below.

Can I (in fact, you!) do better? It seems awfully laborious.

Thanks!

import tactic.core
open tactic


meta def list_head_op (op : pexpr) (f : expr) : tactic unit :=
do op ← to_expr op tt ff,
  let name_cond    : bool := f.get_app_fn.const_name = op.get_app_fn.const_name,
  let no_name_cond : bool := f.get_app_fn            = op.get_app_fn,
  trace format!"using name: {name_cond}\nnot using name: {no_name_cond}\n"

example : 0 + 0 = 0 * 0 :=
by do `(%%lhs = %%rhs) ← target,
  list_head_op ``((+)) lhs,
  list_head_op ``((*)) rhs,
  exact_dec_trivial

/-
using name: tt
not using name: ff

using name: tt
not using name: ff

-/

[Damiano Testa]

I realize now that I learned the const_name trick from Mario. This makes me suspicious about the possibility of making this any smoother! :upside_down:

Still, if there is any easy tweak to avoid the pexpr -> expr -> get_app_fn -> const_name sequence, I'd be very happy to hear about it!

[Mario Carneiro]

comparing expr for equality is usually not what you want

[Mario Carneiro]

I don't usually consider laboriousness to be a factor when writing metaprograms. It's always possible to extract things into a function if they come up often enough. The more important question is whether the code actually expresses what you want, and whether there are any weird failure modes that will result in a bug report down the line

[Mario Carneiro]

For example, this code would also consider (a + b) c to have head +

[Mario Carneiro]

is that important? hard to say

[Mario Carneiro]

It's almost certainly unnecessary to elaborate op here only to get the const_name from it. That's a fixed thing you can just inline, probably has_add.add

[Damiano Testa]

Mario Carneiro said:

For example, this code would also consider (a + b) c to have head +

Actually, this is very important for this code: I want to isolate all subexpressions of an expression that contain a sum, but only keeping the very first one in each case. For instance, from e + a / (a + b) + (b / (c + d) + c) I want to extract

e + a / (a + b) + (b / (c + d) + c)   -- and not also, e.g., `b / (c + d) + c`
a + b
c + d

(My code actually seems to do this, based on the tests that I made.)

Mario Carneiro said:

It's almost certainly unnecessary to elaborate op here only to get the const_name from it. That's a fixed thing you can just inline, probably has_add.add

I am probably not understanding this suggestion: I want the user to be able to specify whether they want to collect together sums, or product, or intersections, or whatever. If I inline has_add.add, then this will only extract sums, right?

[Mario Carneiro]

I think you didn't understand my (a + b) c example. That is an application with (a + b) as the function and c as the argument, so the head of that application is + but it's not going to play well with your reasoning about + as a binary operator

[Damiano Testa]

Indeed, I did not understand and I am not yet sure that I understand. Do your a, b have a type different from c? Is that intended to be an application of two additive homomorphisms a, b on a additive monoid containing a term c?

[Mario Carneiro]

kind of; for this to typecheck you would need a and b to be function types and c is the argument type. I think we have an implementation of pointwise addition on function types so it isn't completely crazy to have such a term pop up

[Mario Carneiro]

if it was an "additive homomorphism" as in the type add_monoid_hom then the term would not actually look like that, it would be coe_fn (a + b) c which does not have + at the head

[Damiano Testa]

Ok, something like

example (a b : ℕ → ℕ) (c d : ℕ) : (a + b) c = d :=

Let me switch branch and check it right away! :smile:

[Damiano Testa]

You are right that something is not as I intended it:

example (f g h : ℕ → ℕ) (a b : ℕ) : (f + g * (g + h)) (a + b) = 0 :=
by <my code that is supposed to extract summands>
--  [(f + g * (g + h)) (a + b), g + h]

I am inclined to not worry about this issue: if you want to move around terms in an expression like the one above, you can roll your sleeves up and do it manually, instead of relying on move_add!

I will think about how to make move_add better, but I consider this not a priority, would you agree?

[Damiano Testa]

To be fair, in all the instances that I saw when I was looking for applications of move_add/move_mul not once did this situation arise.

[Damiano Testa]

Anyway, the take-away is that the tactic appears to work, if each subexpression that consists of iterated binary operations is separated by at least one expr-constructor from the next subexpression that has the same head symbol.

[Damiano Testa]

At least in the case mentioned above, move_add/move_mul appear to work as intended after applying simp, which "applies" the functions.

[Damiano Testa]

... almost, the third example violates what I said above.

import tactic.move_add
import algebra.group.pi

example (f g : ℕ → ℕ) (a b : ℕ) : (f * g) (a * b) = 1 :=
begin
  move_mul a,  -- fails doing nothing
end

example (f g : ℕ → ℕ) (a b : ℕ) : (f + g) (a * b) = 1 :=
begin
  move_mul a,  -- ⊢ (f + g) (b * a) = 1, as intended
end

example (f g : ℕ → ℕ) (a b : ℕ) : (f * g) (a + b) = 1 :=
begin
  move_mul f,  -- fails doing nothing, I was hoping for ⊢ (g * f) (a + b) = 1
end

I may add a sentence about this in a doc-string.

[Eric Wieser]

I am inclined to not worry about this issue: if you want to move around terms in an expression like the one above, you can roll your sleeves up and do it manually, instead of relying on move_add!

I would argue that your program should treat (f + g * (g + h)) (a + b) as a single term (making move_add a no-op) rather than incorrectly splitting it into two terms

[Damiano Testa]

Eric, you are probably right, but then I need to think about how to do this. In any case, whether or not the program that gathers operands treats (f + g * (g + h)) (a + b) as a single block or not, the rest of the program does not seem to care much and mostly considers it a single block anyway.

[Eric Wieser]

Does the code I provided in your earlier PR fail on this example?

[Eric Wieser]

That is

open tactic

meta def expr.list_binary_operands_aux (f : expr) : expr → tactic (list expr)
| x@(expr.app (expr.app g a) b) := do
  some _ ← try_core (unify f g) | pure [x],
  as ← a.list_binary_operands_aux,
  bs ← b.list_binary_operands_aux,
  pure (as ++ bs)
| a := pure [a]

/-- Produces a list of all the operands in `x`, ignoring associativity. -/
meta def expr.list_binary_operands (f : pexpr) (x : expr) : tactic (list expr) :=
do
  t ← infer_type x,
  fe ← to_expr ``(%%f : %%t → %%t → %%t ),
  expr.list_binary_operands_aux fe x

[Eric Wieser]

It seems to work fine:

constants f g : ℕ → ℕ
constants a b : ℕ

-- [(f + g) (a * b), 1]
#eval do
  l ← expr.list_binary_operands ``((+)) `((f + g) (a * b) + 1),
  tactic.trace l

[Damiano Testa]

Eric, I think that you are right and that I was confused from the very beginning. I have used your code list_binary_operands, I was simply interpreting the output incorrectly, since I was confusing it with the output of list_head_op as well.

The interpretation that (f + g) (a * b) is a "unit" is clarifying and actually correct for code, as it already is. At least as far as I have tested it.

[Damiano Testa]

If you want to test whether you are confused or not about how move_add and move_mul work, you can scan through the lines of the following code:

import tactic.move_add
import algebra.group.pi

constants f g : ℕ → ℕ
constants a b c : ℕ

example (h : a = c) : 1 + (f * g) (a + b) + a * f (b + a) = c * f (b + a) + 1 + (f * g) (a + b) :=
begin
  move_add a,
  move_add [1, c * _],
  move_mul [a, c],
  move_add (f * _) _,
  simp,
  move_mul f _,
  move_add _ * f _,
  simp [h],
end