CODEWITHSUNDEEP
coq
domino
domino

Reputation: 99

How to prove a odd number is the successor of double of nat in coq?

I have the odd number definition as below:

Definition Odd n := exists k, n = 2*k+1.

And I have an oddb define that whether a number is odd or not.

Fixpoint oddb (n : nat) { struct n } : bool :=

match n with
  | 0 => false
  | 1 => true
  | S (S n) => oddb n
  end.

I am trying to prove if a number is the successor of a double of nat; then it is a odd number.

Theorem question_1c:
  forall n, Odd n -> (oddb n = true).
Proof.
  unfold Odd. intros. inversion H. 
  rewrite H0. simpl. induction x. 
  - simpl. reflexivity.
  - Admitted.

I stuck on the second goal.. it showed that I need to prove Sx.. and the hypothesis I have from now seems like not helpful...

1 subgoal
n : nat
H : exists k : nat, n = 2 * k + 1
x : nat
H0 : n = 2 * S x + 1
IHx : n = 2 * x + 1 -> oddb (x + (x + 0) + 1) = true
______________________________________(1/1)
oddb (S x + (S x + 0) + 1) = true

Can anyone help me?? tHnak you

Upvotes: 0

Views: 249

Answers (1)

Lolo
Lolo

Reputation: 649

Standard induction let you jump from n to n+1. Here with your odd function you need to jump from n to n+2. So what is needed is a stronger induction. One way to do this is to prove:

Theorem question_1c:
  forall n m, m <= n -> Odd m -> (oddb m = true).

by standard induction on n (but for all m smaller)

Upvotes: 2

Related Questions