如何在给定规范的情况下证明 Coq 中函数的唯一性？答案

【问题标题】：How to prove uniqueness of a function in Coq given a specification?如何在给定规范的情况下证明 Coq 中函数的唯一性？
【发布时间】：2017-04-01 08:14:27
【问题描述】：

给定一个函数的规范，例如specification_of_sum，我如何在 Coq 中证明只有一个这样的函数存在？

我正在学习数学，我可以亲自证明这一点，但我在 Coq 方面的技能有限（使用 rewrite 和 apply 证明）。

我在下面找到了代码 sn-p，我已经为此苦苦挣扎了一段时间。

我尝试在证明中展开规范，但使用我的老朋友rewrite 似乎并没有让我走得更远。

有人能解释一下如何使用简单的语法来解决这个问题吗？

Definition specification_of_sum (sum : (nat -> nat) -> nat -> nat) :=
  forall f : nat -> nat,
    sum f 0 = f 0
    /\
    forall n' : nat,
      sum f (S n') = sum f n' + f (S n').

(* ********** *)

Theorem there_is_only_one_sum :
  forall sum1 sum2 : (nat -> nat) -> nat -> nat,
    specification_of_sum sum1 ->
    specification_of_sum sum2 ->
    forall (f : nat -> nat)
           (n : nat),
      sum1 f n = sum2 f n.
Proof.  
Abort.

【问题讨论】：

标签： functional-programming coq

【解决方案1】：

下面的开始基本上和ejgallego已经描述的一样。

intros sum1 sum2 H1 H2 f n. (* introduce all the hypotheses *)                                     
unfold specification_of_sum in *. (* unfold definition in all places *)                            
specialize H1 with (f := f). (* narrow statement to be about f *)                                  
specialize H2 with (f := f). (* narrow statement to be about f *)                                  
inversion_clear H1.  (* split up the AND statements *)                                             
inversion_clear H2.                                                                                
(* induction on n, and do rewrites *)

我添加了一些更基本的命令，以使其更慢但更简单。其余的证明只需要rewrite 和reflexivity。

【讨论】：

谢谢，这是启动我的证明所必需的 :-)
是否可以用“更简单”的东西代替 inversion_clear？
确实反转清除不是处理假设的正确方法，您在我的答案中有正确的方法（介绍模式）。

【解决方案2】：

您需要在n 上使用归纳法来证明这一点。想想看，你的规范涵盖了0 和n.+1 的情况，因此使用归纳法是很自然的。

您基本上可以在您选择的 Coq 书籍中阅读有关归纳的内容。

一个关于如何使用你的规范的例子是：

intros sum1 sum2 s1_spec s2_spec f n.
specialize (s1_spec f) as [s1_spec0 s1_specS].
specialize (s2_spec f) as [s2_spec0 s2_specS].

【讨论】：

但是我找不到使用规范的语法。我如何用它重写或应用它？可以给我看看吗？
我建议您使用specialize (spec1 f)，其中spec1 是sum1 的规范。你也可以unfold specification_of_sum in spec1，但这不是必需的，定义通常在 Coq 中自动扩展。