Доказательство, включающее развертывание двух рекурсивных функций в COQ

Ну, вы задаете много вопросов о базовом Coq, помимо того, что ИМО может здесь решить. Для этой конкретной проблемы я бы поступил так (на самом деле я бы использовал уже предоставленные леммы в MathComp):

From Coq Require Import PeanoNat Bool List.

Fixpoint contains (n: nat) (l: list nat) : bool :=
  match l with
  | nil    => false
  | h :: t => if Nat.eqb h n then true else contains n t
  end.

Fixpoint count (n : nat) (l: list nat) : nat :=
  match l with
  | nil => 0
  | h :: t => if Nat.eqb h n then S (count n t) else count n t
  end.

Lemma contains_count_ge1 n l : contains n l = true -> count n l > 0.
Proof.
induction l as [|x l IHl]; simpl; [now congruence|].
now destruct (Nat.eqb_spec x n); auto with arith.
Qed.

Мое "стандартное" решение:

Lemma test n (l : list nat) : n \in l -> 0 < count_mem n l.
Proof. by rewrite lt0n => /count_memPn/eqP. Qed.

и различные определения count и contains, которые могут оказаться полезными:

Fixpoint contains (n: nat) (l: list nat) : bool :=
  match l with
  | nil    => false
  | h :: t => Nat.eqb h n || contains n t
  end.

Fixpoint count (n : nat) (l: list nat) : nat :=
  match l with
  | nil    => 0
  | h :: t => Nat.b2n (Nat.eqb h n) + (count n t)
  end.

ejgallego уже дал отличное решение вашей проблемы в своем ответе. Я хотел бы еще выделить важный момент, который он упустил: в Coq всегда нужно рассуждать из первых принципов, и быть очень педантичным и точным в своих доказательствах.

Вы утверждали, что доказательство должно проходить следующим образом:

Список не может быть nil, так как contains истинно, поэтому должен быть элемент x в l, такой что beq_nat h x равен true.

Несмотря на то, что это имеет интуитивно понятный смысл для людей, Coq не может его понять. Проблема, как показывает ответ ejgallego, заключается в том, что ваши неформальные рассуждения скрывают использование индукции. В самом деле, полезно попытаться развернуть свою аргументацию более подробно еще до того, как превратить ее в тактику. Мы могли бы действовать, например, так:

Докажем, что для любых n : nat и ns : list nat из contains n ns следует count n 0 ns > 0. Проведем индукцию по списку ns. Если ns = nil, определение contains подразумевает, что выполняется False; противоречие. Таким образом, мы остаемся со случаем ns = n' :: ns', где мы можем использовать следующую гипотезу индукции: contains n ns' -> count n 0 ns' > 0. Необходимо рассмотреть два подслучая: является ли beq_nat n n' true или нет.

• Если beq_nat n n' равно true, по определению count мы видим, что нам просто нужно показать это count n (0 + 1) ns' > 0. Обратите внимание, что здесь нет прямого способа продолжить. Это потому, что вы написали count хвостовой рекурсии, используя аккумулятор. Хотя это вполне разумно в функциональном программировании, это может затруднить доказательство свойств около count. В этом случае нам понадобилась бы следующая вспомогательная лемма, доказываемая также по индукции: forall n acc ns, count n acc ns = acc + count n 0 ns. Я дам вам понять, как это доказать. Но если предположить, что мы уже установили его, цель сводится к тому, чтобы показать, что 1 + count n 0 ns' > 0. Это верно с точки зрения простой арифметики. (Есть еще более простой способ, не требующий вспомогательной леммы, но требующий небольшого обобщения доказываемого вами утверждения.)

• Если beq_nat n n' равно false, по определениям contains и count нам нужно будет показать, что contains n ns' подразумевает count n 0 ns' > 0. Это именно то, что дает нам гипотеза индукции, и мы закончили.

Здесь нужно усвоить два урока. Во-первых, выполнение формальных доказательств часто требует перевода вашей интуиции в формальные термины, понятные системе. Мы интуитивно знаем, что значит наличие некоторого элемента внутри списка. Но если бы мы объяснили, что это значит более формально, мы бы прибегли к некоему рекурсивному обходу списка, который, вероятно, оказался бы тем самым определением count, которое вы написали в Coq. А чтобы рассуждать о рекурсии, нам нужна индукция. Второй урок заключается в том, что то, как вы определяете вещи в Coq, имеет важные последствия для написанных вами доказательств. Решение ejgallego не требовало каких-либо вспомогательных лемм, помимо лемм из стандартной библиотеки, именно потому, что его определение count не было хвостовой рекурсией.