我该如何重写"+1"? (加一)改为"S" (succ)在Coq? [英] How can I rewrite "+ 1" (plus one) to "S" (succ) in Coq?

问题描述

我的以下引理不完整:

Lemma (s_is_plus_one : forall n:nat, S n = n + 1).
Proof.
  intros.
  reflexivity.
Qed.

此证明失败

Unable to unify "n + 1" with "S n".

似乎可以用eq_S来证明这一点，但是我不能应用它(它不能将n + 1识别为S n:Error: Unable to find an instance for the variable y.).我也尝试过ring，但是找不到关系.当我使用rewrite时，它只是减少到相同的最终目标.

It seems like eq_S would be the way to prove this, but I can't apply it (it doesn't recognize n + 1 as S n: Error: Unable to find an instance for the variable y.). I've also tried ring, but it can't find a relation. When I use rewrite, it just reduces to the same final goal.

我如何完成此证明?

推荐答案

这与(+)的定义方式有关.通过关闭符号(在View > Display notations中的CoqIDE中)，可以看到(+)的基础定义，请注意符号(+)对应于功能Nat.add，然后调用Print Nat.add，这将为您提供:

This is related to the way (+) is defined. You can access (+)'s underlying definition by turning notations off (in CoqIDE that's in View > Display notations), seeing that the notation (+) corresponds to the function Nat.add and then calling Print Nat.add which gives you:

Nat.add = 
fix add (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (add p m)
  end

您可以看到(+)是通过匹配其第一个参数(在n + 1中为变量n)定义的.因为n都不以O或S开头(不是以构造函数为首")，所以match不能减少.这意味着您将无法仅仅通过说两件事以相同的标准形式(这就是reflexivity要求的形式)来证明相等性.

You can see that (+) is defined by matching on its first argument which in n + 1 is the variable n. Because n does not start with either O or S (it's not "constructor-headed"), the match cannot reduce. Which means you won't be able to prove the equality just by saying that the two things compute to the same normal form (which is what reflexivity claims).

相反，您需要解释一下为什么对于任何n均等将成立.对于递归函数(例如Nat.add)，经典的做法是进行induction的证明.它确实在这里完成了工作:

Instead you need to explain to coq why it is the case that for any n the equality will hold true. A classic move in the case of a recursive function like Nat.add is to proceed with a proof by induction. And it does indeed do the job here:

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros. induction n.
 - reflexivity.
 - simpl. rewrite <- IHn. reflexivity.
Qed.

您可以做的另一件事是，注意1另一方面是构造函数为首，这意味着只有您拥有1 + n而不是n + 1时，匹配才会触发.好吧，我们很幸运，因为在标准库中已经有人证明Nat.add是可交换的，因此我们可以使用它:

Another thing you can do is notice that 1 on the other hand is constructor-headed which means that the match would fire if only you had 1 + n rather than n + 1. Well, we're in luck because in the standard library someone already has proven that Nat.add is commutative so we can just use that:

Lemma s_is_plus_one : forall n:nat, S n = n + 1.
Proof.
intros.
rewrite (Nat.add_comm n 1).
reflexivity.
Qed.

最后一个选择:使用SearchAbout (?n + 1)，我们可以找到所有关于某些变量?n的模式?n + 1的定理(这里的问号很重要).第一个结果是真正相关的引理:

A last alternative: using SearchAbout (?n + 1), we can find all the theorems talking about the pattern ?n + 1 for some variable ?n (the question mark is important here). The first result is the really relevant lemma:

Nat.add_1_r: forall n : nat, n + 1 = S n

这篇关于我该如何重写"+1"? (加一)改为"S" (succ)在Coq?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！