expr structure for coe_fun

Stream: metaprogramming / tactics

[Yakov Pechersky]

What's the correct way to destruct something like ⇑(swap 2 4) 5 as an expr?

[Simon Hudon]

Can you elaborate on what you’re trying to do?

[Yakov Pechersky]

I'm trying to write the norm_num extension a la norm_digits following Mario's comments in https://github.com/leanprover-community/mathlib/pull/5637

[Yakov Pechersky]

I have

@[norm_num] meta def eval : expr → tactic expr
| `(swap %%ea %%eb %%ec) := do
  a ← expr.to_nat ea,
  b ← expr.to_nat eb,
  c ← expr.to_nat ec,
  if c = a then return eb
  else if c = b then return ea
  else return ec
| _ := failed

but that doesn't work, I need a coe_fn somewhere in there

[Yakov Pechersky]

I see I misunderstood what the norm_num extension should be. I'll try to fix it.

[Yakov Pechersky]

I think it has to be something like

@[norm_num] meta def eval : expr → tactic (expr × expr)
| (app (app coe_fn (app (app `(equiv.swap) ea) eb)) ec) := do
  a ← expr.to_nat ea,
  b ← expr.to_nat eb,
  c ← expr.to_nat ec,
  t ← infer_type ea,
  u ← mk_meta_univ,
  infer_type t >>= unify (expr.sort (level.succ u)),
  u ← get_univ_assignment u,
  ic ← mk_instance_cache t,
  (ic, d) ← ic.get ``decidable_eq,
  trace a,
  trace b,
  trace c,
  if ha : c = a
    then
    return (eb, `(@swap_apply_left %%t %%d %%ea %%eb))
  else if hb : c = b
    then
    return (ea, `(@swap_apply_right %%t %%d %%ea %%eb))
  else return (ec, `(@swap_apply_of_ne_of_ne %%t %%d _ _))
| _ := failed

but I'm not sure how to properly pass the universe metavariable, nor generate the inequality proofs for the final case.

[Simon Hudon]

Ok coe_fn takes two parameters in your case: swap a b and c

[Yakov Pechersky]

Getting closer:

@[norm_num] meta def eval : expr → tactic (expr × expr)
| (app (app coe_fn (app (app `(equiv.swap) ea) eb)) ec) := do
  a ← expr.to_nat ea,
  b ← expr.to_nat eb,
  c ← expr.to_nat ec,
  t ← infer_type ea,
  u ← mk_meta_univ,
  infer_type t >>= unify (expr.sort (level.succ u)),
  u ← get_univ_assignment u,
  ic ← mk_instance_cache t,
  (ic, d) ← ic.get ``decidable_eq,
  trace a,
  trace b,
  trace c,
  trace u,
  trace t,
  trace d,
  if ha : c = a
    then do
      unify ec ea,
      trace a,
      trace b,
      trace c,
      (ic, p) ← ic.mk_app ``swap_apply_left [ea, eb],
      return (eb, p)
  else if hb : c = b
    then do
      unify ec eb,
      trace a,
      trace b,
      trace c,
      (ic, p) ← ic.mk_app ``swap_apply_right [ea, eb],
      return (eb, p)
  else return (ec, `(@swap_apply_of_ne_of_ne %%t %%d _ _))
| _ := failed

[Simon Hudon]

Try writing the pattern in a `( ) quotation. It will let you omit implicit parameters

[Yakov Pechersky]

Which pattern?

[Simon Hudon]

`(coe_fn (swap %%a %%b) %%c)

[Yakov Pechersky]

Doesn't work:

@[norm_num] meta def eval : expr → tactic (expr × expr)
| `(coe_fn (swap %%ea %%eb) %%ec) := do
/-
function expected at
  ⇑(swap _x_1 _x_2)
term has type
  has_coe_to_fun.F (swap _x_1 _x_2)
-/

[Simon Hudon]

I didn't see that coming. The issue is that coe_fn (swap _ _) only has a function type if we find the right has_coe_to_fun instance. Give me a moment, I'll see how to synthesize it first.

[Simon Hudon]

Ok, try this:

meta def eval (e : expr) : tactic (expr x expr) :=
do if e.is_app_of ``coe_fn then do
      [_α, _inst,`(equiv.swap %%ea %%eb), ec] ← pure e.get_app_args,
      _
   else _

[Simon Hudon]

Did it work?

[Yakov Pechersky]

Yes, I generalized it so:

/-
If `e : expr` is of the form `const name _`, `app name _`,
or `app (app name _) _`, or so on, get back the `name`.
-/
meta def expr.name_of_const_or_app : expr → tactic name
| (const n _) := pure n
| (app f r) := expr.name_of_const_or_app f
| _ := fail "not const or app"

/-
If `e : expr` is of the form `app (⇑f) x`, get back the `expr`s for
type of `f`, the `has_coe_to_fun` instance, `f` itself, and `x`.
-/
meta def expr.get_of_coe_fn (e : expr) (f : name) : tactic (expr × expr × expr × expr) :=
do
  if e.is_app_of ``coe_fn
  then do
    [α, inst, fexpr, x] ← pure e.get_app_args,
    fname ← expr.name_of_const_or_app fexpr,
    decorate_error ("retrieved function name " ++ fname.to_string ++ " is not the expected " ++ f.to_string)
      $ guard (fname = f),
    pure (α, inst, fexpr, x)
  else fail "not of coe_fn form with a single argument"

@[norm_num] meta def eval : expr → tactic (expr × expr) := λ e, do
  (swapt, coe_fn_inst, f, c) ← expr.get_of_coe_fn e ``equiv.swap,
  [α, deceq_inst, a, b] ← pure f.get_app_args, -- the swap should have exactly two arguments applied
  ...