## Stream: metaprogramming / tactics

### Topic: expr structure for coe_fun

#### Yakov Pechersky (Jan 07 2021 at 00:10):

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

#### Simon Hudon (Jan 07 2021 at 00:20):

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

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

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

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

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

#### Simon Hudon (Jan 07 2021 at 01:21):

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

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


#### Simon Hudon (Jan 07 2021 at 01:28):

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

Which pattern?

#### Simon Hudon (Jan 07 2021 at 01:36):

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

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


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

#### 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 _


Did it work?

#### 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 exprs 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