failed to unify 0 ≥ 0 with 0 ≥ 0

Stream: new members

[rzeta0]

Developing a proof for an exercise and (end of) my current state is

h1 : 0 ≥ 0
⊢ 0 ≥ 0

When I try to apply h1

apply h1

I get the error

tactic 'apply' failed, failed to unify
0 ≥ 0
with
  0 ≥ 0

This is a puzzle to me as both expressions are the same and should "unify".

Any suggestions?

My previous attempts to apply a hypothesis which matched the current goal using apply worked fine.

[rzeta0]

This works - but I don't see why the above doesn't.

norm_num

Yes, I know I should have simply done this to the current goal, but I'm interested in why h1 couldn't be applied.

[Julian Berman]

It's a lot easier to answer specifically with an #mwe.

[Benjamin Jones]

That's odd. apply works for me in this example, though I would typically use assumption.

example (h : 0 ≥ 0) : 0 ≥ 0 := by
  -- apply h  -- works
  assumption

[Julian Berman]

The answer probably will be "your hypothesis is not actually the same", the zeros are different types.

[rzeta0]

Benjamin - your MWE works for me too.

I will have to come back with an MWE that shows the problem because the exercise I'm doing is not minimal:

example {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b) :
    ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by

[Julian Berman]

If you put your cursor over all of the 0s in your infoview, the tooltip should tell you a bit more about "which" zeros they are, which may help.

[rzeta0]

thanks Julian - I will try that after I get some sleep :)

[Yakov Pechersky]

My guess is that in your actual example, exact_mod_cast h1 would have worked. My hypothesis is that one is over Nat while the other is over Int.

[Edward van de Meent]

Alternatively, it could be the case that you have introduced multiple non-defeq instances.

[Edward van de Meent]

In this case, the conflict is likely two instances of either Zero or Preorder

[Edward van de Meent]

(or something higher in the hierarchy)

[Luigi Massacci]

A standard trick in this case is to use convert

[Luigi Massacci]

This will leave you with goals for those parts it failed to unify

[Luigi Massacci]

So you can see what's going on