证明涉及在COQ中展开两个递归函数

Question

我开始学习Coq,并试图证明一些看似相当简单的东西:如果列表包含x,那么该列表中x的实例数将> 0.

我已经定义了contains和count函数,如下所示:

Fixpoint contains (n: nat) (l: list nat) : Prop :=
  match l with
  | nil => False
  | h :: t => if beq_nat h n then True else contains n t
  end.

Fixpoint count (n acc: nat) (l: list nat) : nat :=
  match l with
  | nil => acc
  | h :: t => if beq_nat h n then count n (acc + 1) t else count n acc t
  end.

我试图证明:

Lemma contains_count_ge1 : forall (n: nat) (l: list nat), contains n l -> (count n 0 l > 0).

我理解的证据将包括展开数的定义,包含,但后来我想说"列表不能是零,因为包含是真实的,所以必须有一个元素x中l,从而beq_nat h x为真正的",而且我我玩了一下,但无法弄清楚如何使用战术来做到这一点.任何指导将不胜感激.

Answer 1

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不是尾递归.