passing functions

Stream: metaprogramming / tactics

[Damiano Testa]

Dear All,

in the code below, to_oper reads an expression and converts has_mul.mul to has_add.add (the example shows how it works in a simple case).

import algebra.ring.basic

open tactic

/--  Convert the `has_mul.mul` in an expression to `has_add.add`. -/
meta def to_oper : expr → tactic expr
| `(has_mul.mul %%a %%b)     := do oa ← to_oper a, ob ← to_oper b,
                                  mk_app `has_add.add [oa, ob]
| (expr.lam a b c e)         := do oc ← to_oper c, oe ← to_oper e,
                                  return (expr.lam a b oc oe)
| (expr.pi  a b c e)         := do oc ← to_oper c, oe ← to_oper e,
                                  return (expr.pi  a b oc oe)
| (expr.elet a b c e)        := do ob ← to_oper b, oc ← to_oper c, oe ← to_oper e,
                                  return (expr.elet  a ob oc oe)
| (expr.app a b)             := do oa ← to_oper a, ob ← to_oper b,
                                  return (expr.app oa ob)
| (expr.mvar u p e)          := do oe ← to_oper e,
                                  return (expr.mvar u p oe)
| (expr.local_const u p b e) := do oe ← to_oper e,
                                  return (expr.local_const u p b oe)
| (expr.macro md le)         := do ole ← le.mmap to_oper,
                                  return (expr.macro md ole)
| e                          := return e


example {R : Type*} [comm_semiring R] {a b c d : R} : b * (a * (c * d)) = 1 :=
by do
  t ← target,
  trace "before",
  trace t,
  trace "after",
  trace $ to_oper t

/-
before
b * (a * (c * d)) = 1
after
b + (a + (c + d)) = 1
-/

In this case has_mul.mul and has_add.add are hard-coded in to_oper, inside the first match pattern.

Would it be possible to provide instead two "generic" functions? Possibly, functions that do not even exist as declarations, simply making Lean pretend that what we are passing makes sense and checking it at execution time?

Thanks!

[Arthur Paulino]

From what I understand, you need to find a way to receive the function names as terms of name (I believe there's a proper parser for this). Then, instead of mk_app `has_add.add [oa, ob] you'd do mk_app my_fun_name [oa, ob].

But in order to be able to match with `(has_mul.mul %%a %%b) like that, I think you need to pass your function as an expression my_fun2_expr so you'd do `(%%my_fun2_expr %%a %%b).

And you should be able to build my_fun2_expr with let my_fun2_expr := mk_const my_fun2_name. This is all untested, but i'd try this approach

[Damiano Testa]

Ok, thanks! I was trying something like this, but was lacking the name trick. I will try harder!

[Arthur Paulino]

I took the matching idea from the sixth bullet point of Mario's backtick cheat sheet. Maybe @Mario Carneiro himself can validate the idea and shed more light on the matter

[Damiano Testa]

I haven't yet managed to make it work, but I do feel closer, thanks!

[Alex J. Best]

It should be possible to get rid of some of the boilerplate here using docs#expr.replace or docs#expr.mreplace I believe

[Damiano Testa]

Alex, thanks! I'll play with this, although I am a little conscious about the bound on binders: I don't know exactly what the consequences of that are.

E.g. is it 2 in my case, since I have binary operations, or is it unbounded, since I want to recurse into everything? I'll try to sort this out, once I have something that works!

[Damiano Testa]

This is where I got so far:

meta def to_oper : name → name → expr → tactic expr
| f₁ f₂ e := let f₁_expr := mk_const f₁ in
match e with
  | `(has_mul.mul %%a %%b)     := do oa ← to_oper f₁ f₂ a, ob ← to_oper f₁ f₂ b,
                                    mk_app f₂ [oa, ob]
[same as before]
  end

The rhs of the match works as expected!

The lhs is still the hard-coded has_mul.mul, so, right now f₁ just rides along: it gets converted to an expr but not used otherwise.

If I replace

  | `(has_mul.mul %%a %%b)     :=

with

  | `(%%f₁_expr %%a %%b)     :=

Lean complains:

function expected at
  _x_1
term has type
  ?m_1
-- underlines `f₁_expr`

My understanding is that Lean does not trust that I will pass a function of two variables as an f₁_expr, but I do not know how to reassure it that this is ok!

[Arthur Paulino]

Ouch, seems like my idea didn't work. You might still be able to use expr.is_app_of or expr.is_napp_of there

(not exactly there, of course... the code will need some restructuring, but nothing too serious)

[Arthur Paulino]

Something along the lines of

meta def to_oper : name → name → expr → tactic expr
| f₁ f₂ e := do
  if e.is_napp_of f₁ 2 then
    oa ← to_oper f₁ f₂ (e.ith_arg 0),
    ob ← to_oper f₁ f₂ (e.ith_arg 1),
    mk_app f₂ [oa, ob]
  else
    match e with
      [same as before except for the first match]
    end

[untested!]

[Arthur Paulino]

(deleted)

[Mario Carneiro]

instead of using syntax quotations, you can write expr.app (expr.app f₁_expr a) b := ...

[Damiano Testa]

Mario, I tried this, but it matched everything, even the =.

[Damiano Testa]

Anyway, I'm going to be back to my computer in a little bit, and I am going to try exactly what you suggest.

When I had tried passing the converted name and also directly assuming and expr and passing it, it was always extremely eager, ignoring the input that I was giving.

I probably had a mistake somewhere else, though.

[Mario Carneiro]

I've lost track of what you are trying to do. I was responding to this:
Damiano Testa said:

If I replace

  | `(has_mul.mul %%a %%b)     :=

with

  | `(%%f₁_expr %%a %%b)     :=

Lean complains:

If you use expr.app you can use it to write that pattern match

[Damiano Testa]

Ok, once I'm back at my computer I will try this and will report! Thanks!

[Mario Carneiro]

Of course such a match will match all sorts of binary operators, including =. Not sure how you want to search for multiplication-like operators

[Damiano Testa]

I would like to provide the binary operator myself, as a parameter and only match that operator. Would that be possible?

[Mario Carneiro]

you can match expr.app (expr.app f a) b and then say if f = my_op then ... else fallback

[Damiano Testa]

(What you are describing is exactly what had happened then: it matched also the equal sign, even if I had given it has_mul.mul as a name.

[Mario Carneiro]

or perhaps f.get_app_fn.const_name or so

[Damiano Testa]

Ok, you've given me some more ideas: I'll try to make them work! Thanks!

[Damiano Testa]

I understand maybe: even if the typed symbol inside the match coincides with the external name, lean treats is as different, right?

[Mario Carneiro]

since lean doesn't have pattern guards you will want to express this as a cascaded match

[Damiano Testa]

This is the reason for the ite, am I correct?

[Mario Carneiro]

The match will give you any three expressions in the form f a b, lots of subterms have that form

[Damiano Testa]

(this at least is compatible with the fact that I saw it matching everything)

[Mario Carneiro]

you then want to narrow down to the case where f is exactly the op you are looking for

[Damiano Testa]

Yes, the lots of matches is what I observed.

[Mario Carneiro]

you can't put the variable directly in the pattern, you just have to say f = my_op

[Mario Carneiro]

if my_op was a known literal like has_mul.mul then you could put it directly in the match

[Damiano Testa]

Ok, this has clarified quite a bit of syntax for me, thank you so much! I am now much more confident that this will work and moreover I understand what I thought was weird behaviour earlier!

[Damiano Testa]

Yes, inputting directly the has_mul.mul worked, but was a limitation that I did not want.

[Damiano Testa]

Until about 10 days ago, I did not really know what a match was, now, I want to do it everywhere and am surprised when it does not magically work like I want it to!

This has been very helpful: I can't wait to put it in practice! :smile:

[Damiano Testa]

This works:

import data.nat.basic

open tactic

/--  Convert every occurrence of the binary operation with name `f₁` in an expression to
the binary operation with name `f₂`. -/
meta def to_oper (f₁ f₂ : name) : expr → tactic expr
| (expr.app (expr.app op a) b) := do oa ← to_oper a, ob ← to_oper b,
                                    if op.get_app_fn.const_name = f₁ then
                                       (mk_app f₂ [oa, ob]) else (return (op oa ob))
--  The rest of the match is unchanged
| (expr.lam a b c e)         := do oc ← to_oper c, oe ← to_oper e,
                                  return (expr.lam a b oc oe)
| (expr.pi  a b c e)         := do oc ← to_oper c, oe ← to_oper e,
                                  return (expr.pi  a b oc oe)
| (expr.elet a b c e)        := do ob ← to_oper b, oc ← to_oper c, oe ← to_oper e,
                                  return (expr.elet  a ob oc oe)
| (expr.app a b)             := do oa ← to_oper a, ob ← to_oper b,
                                  return (expr.app oa ob)
| (expr.mvar u p e)          := do oe ← to_oper e,
                                  return (expr.mvar u p oe)
| (expr.local_const u p b e) := do oe ← to_oper e,
                                  return (expr.local_const u p b oe)
| (expr.macro md le)         := do ole ← le.mmap (to_oper),
                                  return (expr.macro md ole)
| e                          := return e

example {a b c : ℕ} : b * (a * c) = b + (a + c) :=
by do
  t ← target,
  trace "before",
  trace t,
  trace "after",
  trace $ to_oper `has_add.add `monoid.npow t

/-
before
b * (a * c) = b + (a + c)
after
b * (a * c) = monoid.npow b (monoid.npow a c)
-/

Thank you all for your insights!
:octopus: :tada: