是否有可能证明'forall n:nat，le n 0->n =0.在Coq中不使用反演吗? [英] Is it possible to prove `forall n: nat, le n 0 -> n = 0.` in Coq without using inversion?

问题描述

在官方coq教程中，他们定义了以下小于或等于的归纳定义.等于:

In the official coq tutorial they define the following inductive definition of less than or equal to:

Inductive le (n : nat) : nat -> Prop :=
          | le_n : le n n
          | le_S : forall m : nat, le n m -> le n (S m).

我对此的理解是，它正在定义两个类型构造函数:

My understanding of this is that it is defining two type constructors:

1. le_n ，它可以采用任何自然数并构造 le n n 的证明.
2. le_S 取任何自然数 m ，证明为 le nm ，并构造证明为 le n(S m)

1. le_n which takes any natural number and constructs a proof of le n n.
2. le_S which takes any natural number m, a proof of le n m and constructs a proof of le n (S m)

到目前为止，一切都很好.但是，他们随后着手介绍以下引理和证明

So far so good. However, they then proceed to introduce the following lemma and proof

Lemma tricky : forall n:nat, le n 0 -> n = 0.
Proof.
  intros n0 H.
  inversion H.
  trivial.
Qed.

倒置"步骤让我感到困惑.我知道除非n等于0，否则无法构造le n 0，因为0没有后继，但是我不确定反转策略如何解决这个问题.

The 'inversion' step is where I am getting confused. I understand that there is no way to construct le n 0 unless n is equal to 0, since 0 has no successor, but I am not sure at how the inversion tactic figures this out.

为了尝试了解它的更好之处，我尝试不使用反转策略来证明该引理.但是，到目前为止，我的所有尝试(即对n0和H使用elim，试图利用 forall n:nat，0<> S n.等事实)失败.

To try and understand what it was doing better, I attempted to prove this lemma without using the inversion tactic. However, all of my attempts so far (i.e. using elim on n0, and on H, trying to use the fact that forall n : nat, 0 <> S n., etc.) have failed.

尽管我的计算机科学"大脑在这种推理上是完全可以的，但是我的数学家大脑"在接受这一点时遇到了一些麻烦，因为没有任何假设认为这是唯一"的方式构造 le 的居民.这使我认为也许使用反转策略是实现此目的的唯一方法.

Although my 'Computer science' brain is completely fine with this reasoning, my 'mathematician brain' is having a little bit of trouble accepting this, since there is no hypothesis that this is the only way to construct an inhabitant of le. This made me think that perhaps using the inversion tactic was the only way to do this.

如果没有反演策略，是否有可能证明这一引理?如果是这样，怎么办?

Is it possible to prove this lemma without the inversion tactic? If so, how can it be done?

推荐答案

可以不倒置地证明这一引理:重要的一点是对适当的目标进行归纳(消除).

It is possible to prove this lemma without inversion: the important point is to do induction (elimination) on the appropriate goal.

首先请注意，当您对类型为 le n 0 的假设应用 elim 时，底层情况是Coq将应用与 le相关的消除原理.在这里，这种消除原理称为 le_ind ，您可以查询其类型:

First note that when you apply elim on a hypothesis of type le n 0, what's happening underneath is that Coq will apply the elimination principle associated with le. Here that elimination principle is called le_ind and you can query its type:

forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0

这可能有点令人生畏，但重要的是，为了从假设 n< = n0 中证明目标 P n0 两种情况，一种是 le 的每个构造函数.

This might be a bit intimidating but the important point is that in order to prove a goal P n0 out of an hypothesis n <= n0 you need to consider two cases, one for each constructor of le.

那么这对您的问题有什么帮助?在假设 n< = 0 的情况下，这意味着您的目标的形状应为 P(n0)和 n0:= 0 .现在考虑要证明 n = 0 ， P 的形状应该是什么?您可以尝试采用最简单的解决方案 P(n0):= n = 0 (如果您直接在代码中调用 elim H ，这实际上就是Coq所做的事情)，但是然后，您将无法证明您的两种情况中的任何一种.问题在于，选择 P(n0):= n = 0 时，您会忘记 n0 的值，因此您不能使用它等于> 0 .该问题的解决方案是完全记住 n0 为 0 ，即设置 P(n0):= n0 = 0->n = 0 .

So how does that help with your issue ? With an hypothesis n <= 0, this means that your goal should be of the shape P(n0) with n0 := 0. Now considering that you want to prove n = 0, what should be the shape of P ? You could try to take the simplest solution P(n0) := n = 0 (and that's actually what Coq is doing if you call directly elim H in your code) but you are then unable to prove any of your two cases. The problem is that with this choice of P(n0) := n = 0 you are forgetting about the value of n0 so you cannot use that it is equal to 0. The solution to that problem is exactly to remember that n0 is 0, that is to set P(n0) := n0 = 0 -> n = 0.

我们如何在实践中做到这一点?这是一种解决方案:

How do we do that in practice ? Here is one solution:

Goal forall n, le n 0 -> n = 0.
Proof.
  intros n H.
  remember 0 as q eqn: Hq. (* change all the 0s to a new variable q and add the equation Hq : q = 0 *)
  revert Hq. (* now the goal is of the shape q = 0 -> n = 0 and H : le n q *)
  elim H.
  - intros; reflexivity. (* proves n = n *)
  - intros; discriminate. (* discriminates S m = 0 *)
Qed.

归纳所有 0 的所有工作实际上是 inversion 试图为您完成的工作.

All this work of generalizing 0 is actually what inversion is trying to do for you.

请注意，我提出的谓词 P 不是唯一可能的解决方案.另一个有趣的解决方案是基于 match (关键字是小规模倒置)，其中 P(n0):=将n0与0 =>n = 0 |S _ =>真实结束.而且，策略总是总是在最后产生空洞的术语，因此您总是可以(至少在理论上)写出可以证明与任何策略相同的术语.这是一个使用Coq功能强大但冗长的模式匹配的示例:

Note that the predicate P that I propose is not the only possible solution. Another interesting solution is based on match (the keyword is small-scale inversions) with P(n0) := match n0 with 0 => n = 0 | S _ => True end. Also, tactics are always producing bare gallina terms in the end, so you can always (at least theoretically) write a term that proves the same thing as any tactic. Here's an example using Coq's powerful albeit verbose pattern-matching:

Definition pf : forall n, le n 0 -> n = 0 :=
  fun n H =>
    match H
          in le _ q
          return match q return Prop with
                 | 0 => n = q
                 | S _ => True
                 end
    with
    | le_n _ => match n with 0 => eq_refl | S _ => I end
    | le_S _ _ _ => I
    end.

使用 remember 战术简化战术脚本.最初的主张是手动重新实现 remember :

Simplifying the tactic script using the remember tactic. The original proposition was reimplementing remember by hand:

set (q := 0). (* change all the 0s in the goal into q and add it as hypothesis *)
  intro H.
  generalize (eq_refl : q = 0). (* introduce q = 0 *)
  revert H.
  generalize q ; clear q.  (* generalizes q *)
  (* Now the goal is of the shape
     forall q : nat, n <= q -> q = 0 -> n = q
     and we can apply elim *)
  intros q H ; elim H.

这篇关于是否有可能证明'forall n:nat，le n 0->n =0.在Coq中不使用反演吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！