I'm trying to prove the following Lemma in coq --
Lemma less_than_two_equivalent: forall x, less_than_two x = true -> x < 2.
based on the definition below.
Fixpoint less_than (a b:nat): bool:=
match a, b with
|0, 0 => false
|0, _ => true
|S a', 0 => false
|S a', S b' => less_than a' b'
end.
Fixpoint less_than_two (x:nat) : bool := if less_than x 2 then true else false.
Mathematically, there are only 2 cases, 0 or 1. And destructionshould be the hammer, but there won't be enough information about the S x for further reasoning.
Should I modify the less_than into inductive datatypes? If not, how to resolve it?
Let me begin by redefining less_than_two. First, it's not recursive, so there is no point in defining it as a Fixpoint. Next, if less_than x 2 then true else false is essentially the same thing as less_than x 2. And at this point I wouldn't bother with introducing a new definition, so your lemma becomes
Lemma less_than_two_equivalent x: less_than x 2 = true -> x < 2.
Proof.
do 2 (destruct x; auto); simpl.
destruct x; discriminate.
Qed.
I don't know what went wrong with your proof exactly, but you might have forgotten to destruct x one more time. When you see less_than x 0 = true -> S (S x) < 2 you can't still use discriminate to finish your goal, because evaluation is blocked on the variable -- less_than first pattern-matches on the a parameter and only then checks b. Destruction of x unblocks computation and lets Coq see that you have false = true as your premise, hence the goal becomes provable.
Note that this depends on the particular implementation of the comparison function. Had you chose this one
(* (!) the [struct] annotation is important here, as well as as
the order of the parameters [b, a] in the match expression *)
Fixpoint less_than' (a b : nat) {struct b} : bool :=
match b, a with
| 0, _ => false
| _, 0 => true
| S b', S a' => less_than' a' b'
end.
you would have a bit simpler proof (one less destruct):
Lemma less_than_two_equivalent x: less_than' x 2 = true -> x < 2.
Proof.
do 2 (destruct x; auto).
discriminate.
Qed.