两个Coq问题求助：IndProp证明与递归函数定义问题

你的证明思路需要调整，直接destruct自然数m无法利用归纳谓词evenn的结构关联，应该对evenn的假设进行归纳，利用归纳假设建立奇偶加法的递推关系。完整证明如下：

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 n m Hodd Heven.
  (* 对偶数的归纳假设进行归纳 *)
  induction Heven as [ | m' Heven' IH ].
  - (* 基础情况：m=0，n+0=n，直接用原奇数假设 *)
    rewrite plus_n_O. apply Hodd.
  - (* 归纳情况：m = S(S m')，此时n + m = S(S(n + m')) *)
    simpl.
    (* 利用odd2构造子，只需证明n + m'是奇数 *)
    apply odd2.
    (* 调用归纳假设：n是奇数，m'是偶数，则n+m'是奇数 *)
    apply IH. apply Hodd.
Qed.

核心逻辑：通过对evenn的归纳，将“奇数加偶数”拆解为基础情况（加0）和递推情况（加S(S m')），利用归纳假设复用“奇数加更小偶数为奇数”的结论，再通过odd2构造子得到最终结果。

你的count函数结构合法，但缺少isGood的具体实现，报错大概率是isGood未定义导致的连锁问题。以下是完整实现：

(* 定义合格数判断函数：各位数字之和能被5整除 *)
Definition isGood(n:nat) : bool :=
  let digit1 := Nat.modulo n 10 in          (* 个位 *)
  let digit10 := Nat.modulo (Nat.div n 10) 10 in  (* 十位 *)
  let digit100 := Nat.modulo (Nat.div n 100) 10 in (* 百位 *)
  let digit1000 := Nat.modulo (Nat.div n 1000) 10 in (* 千位 *)
  let sum := digit1 + digit10 + digit100 + digit1000 in
  Nat.eqb (Nat.modulo sum 5) 0.

(* 统计≤n的合格数数量，结构递归符合Coq要求 *)
Fixpoint count (n : nat) : nat :=
  match n with
  | 0 => 1  (* 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.

说明： #

1. isGood通过提取四位数的每一位求和，再判断和模5是否为0，符合题目要求。
2. count的递归调用count n'是对S n'的直接子项递归，属于Coq允许的结构递归，不会触发“非递减”报错。

内容的提问来源于stack exchange，提问作者Arnie2C_A