Coq leb <=? does not give me an hypothesis after case or induction

Question

I have simplified my situation to the following piece of code, hopefully this makes it easier to understand.

I would like to prove the following Lemma:

Require Import Arith.
Lemma example: forall a b, 
  if a<=?b then a<=b else a > b.

Doing the following step in the proof

Proof.
intros.

Gives me the result

1 subgoal
a, b : nat
______________________________________(1/1)
if a <=? b then a <= b else a > b

It seems trivial that either a is smaller than or equal to b, in which case I could prove a<=b. In the other case that b is larger than a I could prove that a>b.

I've tried to prove this with induction(a<=?b) or case (a<=?b) but both give me the following result.

2 subgoals
a, b : nat
______________________________________(1/2)
a <= b
______________________________________(2/2)
a > b

Now I have no way to prove these goals. I expected to gain an hypothesis such as H: a <= b and H: a > b in the second case. This way, I would be able to prove my goals.

Could anybody tell me how I could this issue of the non-appearing hypothesis?

Edit: The whole lemma can be proven as follows:

Require Import Arith.
Lemma example: forall a b, 
  if a<=?b then a<=b else a > b.
Proof.
intros.
Check Nat.leb_spec.
case (Nat.leb_spec a b);intuition.

Answer 1

What's happening is that <=? is function returning a boolean, either true or false. When you ask Coq to do an induction or a case analysis on the expression a <=? b, it does exactly that and reduces the proof to two cases: one where a <=? b is substituted by true and another where it is substituted by false. If you want to keep track of the destructed value, you should ask explicitly for it using destruct (a <=? b) eqn:H. (see the documentation).

Answer 2

To do the case distinction that you are looking for you can use

Nat.leb_spec : forall x y : nat, BoolSpec (x <= y) (y < x) (x <=? y)

The type BoolSpec embodies exactly what you are trying to do: if (x <=? y) is the boolean true, then the proposition x <= y is true, and if (x <=? y is false then y < x is true. Thus, Nat.leb_spec embodies the specification of the function x <=? y, as its name suggests.

Now using case (Nat.leb_spec a b) does exactly what you were trying to do with case (a <=? b): it gives you two subgoals, one where x <=? y is replaced by true and you have x <= y as an extra hypothesis, and the other where x <=? y is replaced by false and you have y < x as an hypothesis instead. The fact that you case distinction was on a term of type BoolSpec rather than simply bool did the trick.