Bad error reporting

Stream: general

[Patrick Massot]

Can someone understand why the following code doesn't raise an error on the expected line but rather claims to have solved the goal and puts an error on the example line?

import tactic

namespace tactic
setup_tactic_parser

@[interactive]
meta def bug (pe : parse texpr) (_ : parse $ tk "at") (pe' : parse texpr) :=
do
  tgt ← target,
  e ← to_expr pe,
  e' ← to_expr pe',
  let proof := expr.mk_app e [e'],
  i_to_expr_strict ``(%%proof : %%tgt) >>= tactic.exact

end tactic

example (P Q R : Prop) (hRP : R → P) (hQ : Q) : P :=
begin
  bug hRP at hQ,
end

[Patrick Massot]

@Mario Carneiro?

[Mario Carneiro]

because you built a bad term

[Mario Carneiro]

you basically wrote exact hRP hQ

[Mario Carneiro]

You never typechecked proof, so there is no error

[Patrick Massot]

I know why term I constructed. If I type exact hRP hQ I do get the expected error.

[Patrick Massot]

Did you see how the error is displayed with my code?

[Mario Carneiro]

the expr constructors don't check their arguments (how could they, the function is pure) and antiquoting an expr into a pexpr doesn't typecheck it either for performance reasons, it just uses infer_type on it to figure out how it fits in

[Mario Carneiro]

I think if you use infer_type on hRP hQ you get P so everything looks ok and exact accepts it

[Patrick Massot]

But I run tactic.exact in my code, isn't this type-checking?

[Patrick Massot]

Yes, I noticed that adding an infer_type doesn't fix things.

[Mario Carneiro]

It's doing i_to_expr first, which will give an error at hRP hQ

[Mario Carneiro]

In other words, it is in the conversion from pexpr to expr that local application constraints are checked

[Mario Carneiro]

once you have an expr the assumption is that this term is internally coherent

[Mario Carneiro]

if you use mk_app it will also typecheck the application

[Patrick Massot]

mk_app is not an option, it expects a name

[Patrick Massot]

(that would work in this example but not in my real use case)

[Mario Carneiro]

Here's a low tech solution if you just need a single application:

  expr.pi _ _ a _ ← infer_type e,
  infer_type e' >>= unify a,

[Patrick Massot]

Thanks, but I need to handle several arguments in general.

[Mario Carneiro]

well you can do that multiple times

[Mario Carneiro]

meta def mk_expr_app : expr → list expr → tactic expr
| e [] := pure e
| e (e'::l) := do
  expr.pi _ _ a _ ← infer_type e,
  infer_type e' >>= unify a,
  mk_expr_app (e e') l

[Mario Carneiro]

(this should really be a C++ function though)

[Patrick Massot]

Thanks! I was writing it, but obviously you are much faster.

[Mario Carneiro]

unlike mk_app that won't do anything special with implicit arguments

[Mario Carneiro]

but you can create a metavariable and put it in the list if you want one

[Rob Lewis]

Apparently there's tactic.interactive.mk_mapp' which is misnamed in various ways, undocumented, and in the wrong file, but I think does the same thing!

[Mario Carneiro]

oh yeah that's a bit more robust than the version I just gave

[Patrick Massot]

Thanks Rob!

[Rob Lewis]

(A PR to move, rename, and document this would be fine. I just found it with #find.)

[Mario Carneiro]

wow I didn't know #find was actually good at finding anything

[Rob Lewis]

It's great for things like this. Much better for defs than theorems because you usually know the exact type

[Rob Lewis]

#find expr → list expr → tactic expr

[Kevin Buzzard]

I was talking to Cyril Cohen last week and he said that one reason he liked Coq more than Lean was that Coq's version of #find was so much quicker than Lean's, and I resisted the urge to say "if you're using #find, you're doing it wrong". I too had essentially forgotten that this existed!

[Patrick Massot]

I think that writing a good find would be an excellent exercise for people interested in Lean 4 programming, and a very useful asset.

[Patrick Massot]

Continuing the conversation about docs#tactic.interactive.mk_mapp', I'd be very grateful if a meta-guru could make a version of this tactic that takes a list of pexpr for the function arguments, and elaborate them only when trying to put them inside the function. The current version can lead of bad elaboration.

[Yakov Pechersky]

What type of elaboration do you need? There are several variants of to_expr. This is the most naive conversion:

open tactic tactic.interactive

namespace tactic.interactive

meta def mk_mapp_aux_pexpr' : expr → expr → list pexpr → tactic expr
| fn (expr.pi n bi d b) (a::as) :=
do a ← to_expr a,
   infer_type a >>= unify d,
   fn ← head_beta (fn a),
   t ← whnf (b.instantiate_var a),
   mk_mapp_aux_pexpr' fn t as
| fn _ _ := pure fn

meta def mk_mapp_pexpr' (fn : expr) (args : list pexpr) : tactic expr :=
do t ← infer_type fn >>= whnf,
   mk_mapp_aux_pexpr' fn t args

end tactic.interactive

[Patrick Massot]

Thank you very much Yakov, this seems to help.

[Yakov Pechersky]

I'm interested to know, will the following work in your case?

meta def mk_mapp_pexpr'' (fn : expr) (args : list pexpr) : tactic expr :=
mmap to_expr args >>= mk_mapp' fn

[Yakov Pechersky]

Or does that not work because the elaboration occurs prior to and without the expr.pi resolving?

[Patrick Massot]

Actually I would also need a stupid version that does no elaboration or type checking at all. Isn't it possible to make a function
pexpr -> list pexpr -> pexpr which simply applies the first pexprto all elements of the list?

[Mario Carneiro]

That's just expr.mk_app

[Mario Carneiro]

I'm not sure if it's generic over expr tt and expr ff but if not you can just copy the implementation