CODEWITHSUNDEEP
mathcoqproofprop
isPrime
isPrime

Reputation: 141

Coq:prove Prop implies arithmetic relations of natural number

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?

Upvotes: 1

Views: 103

Answers (1)

Anton Trunov
Anton Trunov

Reputation: 15414

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.

Upvotes: 1

Related Questions