如何通过定义来证明某事？

Question

如果我像这样定义乘法（drugi_c），我该如何证明，例如X*0=0？ （如何根据定义证明某事？）

Fixpoint drugi_c(x y: nat): nat:=

 match x, y with
  | _, O => O
  | O, _ => O
  | S O, _ => y
  | _,S O => x
  | S x', S y' => plus y (drugi_c x' y)
end.

Notation "x * y" := (drugi_c x y) (at level 40, left associativity).

每当我使用“简单”时。在证明而不是0 = 0，我得到结果的定义。

Lemma neka2 x:
   x * 0 =  0.
Proof.
   induction x.
  -simpl. reflexivity.
  -simpl. (*right here*)
Abort.

最后一次简化后的结果。

1 subgoal
x : nat
IHx : x * 0 = 0
______________________________________(1/1)
match x with
| 0 | _ => 0
end = 0

在最后一次simpl.完成证明之后要写什么？

Answer 1

你的目标在x上有一个模式匹配，但无论x是什么值它将返回0.为了简化这一点，你可以destruct x。

请注意，你从不在这里使用归纳假设，所以你可以在开头做destruct x而不是induction x。

Answer 2

这是我最终得到的：

Lemma neka2 x:
   x * 0 =  0.
Proof.
 destruct x.
  -simpl. reflexivity.
  -simpl. (**) 
Abort.

结果：

1 subgoal
x : nat
______________________________________(1/1)
x * 0 = 0

我想你必须用感应来证明它，因为当我试图用预定义的多路径破坏x时也会发生同样的事情。

这是x * 0 = 0证明但具有预定义的mult：

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  intros n.
  induction n as [|n'].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Answer 3

正如@ user138737指出的那样，你不需要归纳法。探讨三种情况就足够了：x = 0，x = 1和x = S (S x'))。因此，我可以提供的最短证据如下。

destruct x as [| [|] ]; reflexivity.