Zulip Chat Archive

Stream: general

Topic: why is this happening


view this post on Zulip Koundinya Vajjha (Jan 16 2019 at 21:53):

open tactic expr

meta def wat : tactic unit :=
do ctx  local_context,
  let a := app ctx.head (list.reverse ctx).head,
  type  infer_type a,
  trace type,
  skip

lemma begins  (f :   ) (a : bool) : Prop :=
begin
wat,  -- returns ℕ
end

But

variables (a : bool) (g :     )
#check g a

returns a type mismatch error?

view this post on Zulip Kenny Lau (Jan 16 2019 at 21:56):

namespace tactic.interactive
open tactic lean.parser interactive expr
meta def wat : tactic unit :=
do ctx  local_context,
  let a := app ctx.head (list.reverse ctx).head,
  type  infer_type a,
  trace type,
  skip
end tactic.interactive

lemma begins  (f :   ) (a : bool) : Prop :=
begin
wat,  -- returns ℕ
end

view this post on Zulip Kenny Lau (Jan 16 2019 at 21:59):

more info:

namespace tactic.interactive
open tactic lean.parser interactive expr
meta def wat : tactic unit :=
do ctx  local_context,
  let a := app ctx.head (list.reverse ctx).head,
  type  infer_type a,
  tactic.interactive.let none none ``(%%a),
  skip
end tactic.interactive

lemma begins  (f :   ) (a : bool) : Prop :=
begin
wat,
sorry
end

tactic state after wat:

f : ℕ → ℕ,
a : bool,
this : ℕ := f a
⊢ Prop

and error message of lemma after I put sorry:

type mismatch at application
  f a
term
  a
has type
  bool
but is expected to have type
  ℕ

view this post on Zulip Reid Barton (Jan 16 2019 at 22:01):

You manually built an expr= supposedly fully elaborated expression, but the expr you constructed is not actually valid. I guess that infer_type assumes the expression is valid and then according to the typing rules its type must be the return type of f. You didn't get an error because you didn't do anything with the expr.

view this post on Zulip Rob Lewis (Jan 16 2019 at 22:04):

Yeah, infer_type doesn't completely type check the expression, otherwise it would be very expensive. There's another tactic called type_check that should fail if you call it on a.

view this post on Zulip Reid Barton (Jan 16 2019 at 22:04):

If you used tactic.exact a (supposing you change the goal to nat) then I imagine the tactic would succeed but then you would get a type error at a later stage.

view this post on Zulip Koundinya Vajjha (Jan 16 2019 at 22:05):

@Reid Barton yeah seems like that's what is happening.

view this post on Zulip Kenny Lau (Jan 16 2019 at 22:06):

well it's meta so it can be unsound anyway

view this post on Zulip Koundinya Vajjha (Jan 16 2019 at 22:06):

type_check is exactly what I needed.

view this post on Zulip Kenny Lau (Jan 16 2019 at 22:06):

you aren't actually changing the partially generated proof by trace

view this post on Zulip Rob Lewis (Jan 16 2019 at 22:08):

In general, making applications manually can be difficult. Do it if you're confident in what you're doing, since it will be more efficient. Otherwise mk_app and mk_mapp are your friends. In particular the error messages will be more helpful.

view this post on Zulip Koundinya Vajjha (Jan 16 2019 at 22:16):

I'm having trouble figuring out how to use mk_app. I have f : ℕ → ℝ and b : ℕ. How do I use this to make the application f b?

view this post on Zulip Kenny Lau (Jan 16 2019 at 22:19):

namespace tactic.interactive
open tactic lean.parser interactive expr
meta def wat : tactic unit :=
do ctx  local_context,
  let a := expr.mk_app ctx.head [ctx.reverse.head],
  tactic.type_check a,
  type  infer_type a,
  trace type,
  tactic.interactive.let none none ``(%%a),
  skip
end tactic.interactive

lemma begins  (f :   ) (a : ) :  :=
begin
wat,  -- returns ℕ
end

view this post on Zulip Koundinya Vajjha (Jan 16 2019 at 22:21):

Okay that was silly. Thanks @Kenny Lau


Last updated: May 17 2021 at 23:14 UTC