(* 4. Let oddn and evenn be the predicates that test whether a given number
is odd or even. Show that the sum of an odd number with an even number is odd. *)
Inductive oddn : nat -> Prop :=
 | odd1 : oddn 1
 | odd2 : forall n, oddn n -> oddn (S (S n)).

Inductive evenn : nat -> Prop :=
 | even1 : evenn 0
 | even2 : forall n, evenn n -> evenn (S (S n)).

Theorem odd_add : forall n m, oddn n -> evenn m -> oddn (n   m).
Proof. intros. destruct m.
  Search add. rewrite <- plus_n_O. apply H.
  destruct H. 
     simpl. apply odd2. 

I don't know how can I prove this theorem, since I can not link oddn with evenn.

(* 6. We call a natural number good if the sum of all 
   its digits is divisible by 5. For example 122 is good 
   but 93 is not. Define a function count such that 
   (count n) returns the number of good numbers smaller than 
   or equal to n. Here we assume that 0 <= n < 10000. 
   Hint: You may find the "let ... in" struct useful. You may 
   directly use the div and modulo functions defined in the 
   standard library of Coq. *)



Definition isGood(n:nat) : bool := 


Fixpoint count (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' => if isGood n then 1   count n'
            else count n'
end.

Compute count 15.

Example count_test1 : count 15 = 3.
Proof. reflexivity. Qed.

Example count_test2 : count 2005 = 401.
Proof. reflexivity. Qed.

For the second problem, I got stuck because the recursion I defined won't be accepted by Coq(non-decreasing?).

I just got stuck with these two problems, can anyone work them out?

CodePudding user response：

If you want to define independently oddnand even, you may prove a lemma which relates these two predicates, like:

Remark R : forall n, (evenn n <-> oddn (S n)) /\
                     (oddn n <-> evenn (S n)).
(* proof by induction on n *)

Then, it's easy to apply this remark for solving your first exercise.

Please note that you may define even and odd in several other ways:

• as mutually inductive predicates
• with existential quantifiers
• define even, then oddin function of even
• ...

I don't understand the problem with the second exercise.

A few days ago, we discussed about a function sum_digits you can use (with modulo) to define isGood.

Your function count looks OK, but quite inefficient (with Peano natural numbers).