在 Coq 中证明定理，列表中的出现次数为 <= 此列表的长度

Question

Fixpoint num_occ (x : nat)(xs : list nat) : nat :=
match xs with
| [] => 0
| (y :: ys) => if eq_dec x y
then 1 + num_occ x ys
else num_occ x ys
end.


Theorem exercise2
: forall x xs, num_occ x xs <= length xs.
Proof.

我试过了，但我不知道我该如何证明，我正在用这种语言。。。。

我试过这个：

内含子xxs。归纳xs。simpl。反射性。案例1。simpl。析构函数x。simpl。

并显示：

2个目标x、 n:nat______________________________________(1/2(0=n______________________________________(2/2(num_occ x(n0:：l(=n

Answer 1

我认为情况1没有必要。试试这个：

Theorem exercise2
: forall x xs, num_occ x xs <= length xs.
Proof.
intros x xs. induction xs; simpl.
- reflexivity.
- destruct (eq_dec x a).
+ apply le_n_S. assumption.
+ apply le_le_succ_r. assumption.
Qed.