Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: expr structure for coe_fun


view this post on Zulip Yakov Pechersky (Jan 07 2021 at 00:10):

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

view this post on Zulip Simon Hudon (Jan 07 2021 at 00:20):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 00:25):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 00:25):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 00:42):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:05):

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.

view this post on Zulip Simon Hudon (Jan 07 2021 at 01:21):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:22):

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

view this post on Zulip Simon Hudon (Jan 07 2021 at 01:28):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:29):

Which pattern?

view this post on Zulip Simon Hudon (Jan 07 2021 at 01:36):

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

view this post on Zulip Yakov Pechersky (Jan 07 2021 at 01:41):

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)
-/

view this post on Zulip Simon Hudon (Jan 07 2021 at 03:23):

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.

view this post on Zulip Simon Hudon (Jan 07 2021 at 03:33):

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 _

view this post on Zulip Simon Hudon (Jan 08 2021 at 00:31):

Did it work?

view this post on Zulip Yakov Pechersky (Jan 08 2021 at 00:33):

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
  ...

Last updated: May 09 2021 at 22:13 UTC