Coq error: Unable to unify "true" with "is_true (0 < a - b - 3)"

Question

Not sure what I am doing wrong but I thought reflexivity should work on below, but it does not.

a, b : nat
H : (1 <=? a - b - 3) = true
______________________________________(1/7)
is_true (0 < a - b - 3)

I also tried to apply leb_complete in H. which resulted in:

a, b : nat
H : (1 <= a - b - 3)%coq_nat
______________________________________(1/7)
is_true (0 < a - b - 3)

but in both cases, Coq gives me an error saying Unable to unify "true" with "is_true (0 < a - b - 3)"

It shouldn't be that complicated, right? Am I missing something here?

Answer 1

First, “it shouldn’t be complicated” is the wrong question.

reflexivity is a tactic that never uses assumptions, and that tries to prove goals in a very specific way. For “easy” purely numeric goals p, you can use lia.

It can only prove goals convertible to shape R a1 a2 where R is a reflexive relation (like equality) and a1 and a2 are convertible. And two terms are convertible if reducing them to normal form gives “the same” result (modulo some complications for eta-expansion).

For instance, reflexivity can prove that 2 + 2 + 0 = 4, or that 0 + n = n. But it cannot prove that n + 0 = n (which can be proved by lia), because n + 0 is a normal form.