COQ证明“forall n:nat， (n n=0”是错误的

Can someone explain me the following - apparently wrong - COQ derivation?

有人能给我解释一下——显然是错误的——COQ推导吗?

Theorem test: forall n:nat,  ( n <= 0) -> n=0.  
intros n H.  
elim H.  
auto.

COQ answer:

公鸡回答:

1 subgoal  
n : nat  
H : n <= 0 

=================  
forall m : nat, n <= m -> n = m -> n = S m

3 个解决方案

#1

le (<=) has two constructors. In n <= 0 both (somehow) could apply:

le(<=)有两个构造函数。在n <= 0时，两者(以某种方式)都可以适用:

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

auto in your proof solves the first goal / case. The second is unprovable. You should do induction on n to prove the theorem:

汽车在你的证明解决了第一个目标/情况。第二个是无法证实的。你应该用n来证明定理:

Theorem test: forall n, n <= 0 -> n = 0.
intros n H.
induction n.
reflexivity.
inversion H. Qed.

or you could use inversion H tactic (not elim):

或者你也可以使用逆反H策略(不是elim):

Theorem test: forall n, n <= 0 -> n = 0.
intros n H.
inversion H.
auto. Qed.

#2

When using induction on a predicate, you usually need to make sure the arguments to the predicate are variables and not terms. You do so by adding some equations. You also usually need to make sure those variables are distinct and that there aren't any unnecessary hypotheses or quantifiers before the predicate.

当对谓词使用归纳时，通常需要确保谓词的参数是变量而不是术语。你可以通过加入一些方程来实现。您通常还需要确保这些变量是不同的，并且在谓词之前没有任何不必要的假设或量词。

Goal forall n1, n1 <= 0 -> n1 = 0.

assert (H1 : forall n1 n2, n1 <= n2 -> n2 = 0 -> n1 = 0).
induction 1 as [| n2 H1 H2].
intros H1.
eapply H1.
intros H3.
discriminate.

intros n1 H2.
eapply H1.
eapply H2.
eapply eq_refl.
Qed.

#3

It's the other way around: your original goal doesn't imply the unprovable goal; it's the unprovable goal that implies the original.

相反，你最初的目标并不意味着无法证明的目标;这是一个无法证明的目标，它暗示了原始。

The goal

我们的目标

A : B
_____
C

is equivalent to the sequent

等于序列吗

A : B |- C.

When proving something interactively in Coq, you are building a sequent tree from bottom to top. Here's an example.

当在Coq中交互地证明某些东西时，您正在构建一个从下到上的顺序树。这是一个例子。

   -------------------- apply H
   P : Prop, H : P |- P
   -------------------- intro H
    P : Prop |- P -> P
-------------------------- intro P
|- forall P : Prop, P -> P

Of course, when moving backwards to a proof, you can make a wrong move.

当然，当回到证明时，你可能会走错。

            ?
      ------------- ?
      P : Prop |- P
   -------------------- clear H
   P : Prop, H : P |- P
   -------------------- intro H
    P : Prop |- P -> P
-------------------------- intro P
|- forall P : Prop, P -> P

You can learn more about sequent calculus from all over the internet.

你可以在因特网上了解更多关于顺序演算的知识。

#1