Trying to complete a Coq proof but I ended up getting stuck on the last goal. I transformed the goal to S n' <= m and have a hypothesis (S n' <=? m) = true, but am unable to unify these.
I tried to define an extra lemma leb_true to fix this but failed to do so. Is there something simple I'm missing?
<=? and <= are two different things, but the Coq programmers who included these two things in the library know that they are related. This knowledge is stored in the libraries about arithmetic.
So you should perform the following operation:
Require Import Arith.
Search (_ <=? _) (_ <= _).
This gives you a collection of theorems that you can use in proofs.
Nat.leb_spec0: forall x y : nat, Bool.reflect (x <= y) (x <=? y)
Nat.leb_spec: forall x y : nat, BoolSpec (x <= y) (y < x) (x <=? y)
leb_complete: forall m n : nat, (m <=? n) = true -> m <= n
leb_correct: forall m n : nat, m <= n -> (m <=? n) = true
Nat.leb_le: forall n m : nat, (n <=? m) = true <-> n <= m
Nat.leb_nle: forall x y : nat, (x <=? y) = false <-> ~ x <= y
Now, you can use any of these 6 theorems to prove what you need. For instance, if your goal's conclusion has the shape formula1 <= formula2 and you have an hypothesis that says (formula1 <=? formula2) = true it is useful to use the equivalence in Nat.leb_le, through a rewrite statement:
rewrite <- Nat.leb_le.
The new produced goal will contain (formula1 <=? formula2) = true and you will be able to conclude.