apply failed to unify

Stream: general

[David Richey]

Hello, it is not clear to me why this would be the case:

invalid apply tactic, failed to unify
  bool_big_step_to s (leq (const 1) (const 2)) (to_bool (1 ≤ 2))
with
  bool_big_step_to ?m_1 (leq ?m_2 ?m_3) (to_bool (?m_4 ≤ ?m_5))

does anyone have any suggestions for figuring out why?

[Trebor Huang]

Is bool_big_step_to a function? If that's the case, then Lean correctly gives up, since it might not be injective, so s has no reason to be equal to ?m_1.

[David Richey]

sorry, I should have posted that as well. It is an inductive:

inductive bool_big_step_to (s : string →. int) : ibool -> bool -> Prop
| bbs_true : bool_big_step_to itrue tt
| bbs_false : bool_big_step_to ifalse ff
| bbs_leq {a1 n1 a2 n2} : arith_big_step_to s a1 n1 -> arith_big_step_to s a2 n2
                          -> bool_big_step_to (leq a1 a2) (n1 <= n2)

(where ibool is also an inductive defined in the obvious way)

[David Richey]

does that change things?

[Kevin Buzzard]

Can you make a #mwe rather than just posting code fragments? That way we can all see the tactic failing on our own computers.

[David Richey]

yes, sorry about that. I was originally really just looking for debugging suggestions so that I can learn how to debug such issues on my own in the future. But maybe it is a more complicated issue than I thought. Here's a whole example:

inductive myarith
| const : int -> myarith

inductive mybool
| leq : myarith -> myarith -> mybool

inductive myarith_evals_to : myarith -> int -> Prop
| arith_eval_const {n} : myarith_evals_to (myarith.const n) n

inductive mybool_evals_to : mybool -> bool -> Prop
| bool_eval_leq {a1 n1 a2 n2} : myarith_evals_to a1 n1 -> myarith_evals_to a2 n2
                                -> mybool_evals_to (mybool.leq a1 a2) (n1 <= n2)

theorem foo : mybool_evals_to (mybool.leq (myarith.const 1) (myarith.const 2)) (1 <= 2) :=
begin
  apply mybool_evals_to.bool_eval_leq,
end

[David Richey]

(in case anyone has already copied it, I had a typo which I have fixed now ^)

[Kevin Buzzard]

theorem foo : mybool_evals_to (mybool.leq (myarith.const 1) (myarith.const 2)) ((1 : ℤ) <= 2) :=
begin
  apply mybool_evals_to.bool_eval_leq, -- works
end

By default Lean's numerals default to naturals; you have to explicitly tell Lean that these are integers.

[Kevin Buzzard]

(note also that your original question was impossible to answer because the problem was in a part of the code which we couldn't see; mwe's are always the way to go around here)

[David Richey]

ah, got it. That's quite interesting that it can't infer they must be ints. Thank you very much I will keep that in mind!

[Kevin Buzzard]

1 <= 2 is in fact a Prop in Lean, you're coercing it to a boolean, and the coercion doesn't start thinking about types of things, it just notices you want a bool, you gave it a Prop involving two terms of a type, and who knows what type you meant, so let's go with nat.