0

如果我定义这样的乘法 ( drugi_c)，我如何证明 eg 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.来完成证明？

4

3 回答 3

2

您的目标在 上有一个模式匹配x，但无论是什么值x，它都会返回 0。为了强制简化，您可以destruct x.

请注意，您在这里从不使用归纳假设，因此您可以destruct x在开始时使用而不是induction x.

于 2019-03-23T20:15:10.407 回答
0

正如@user138737 指出的那样，您不需要归纳。探索三种情况就足够了x = 0：x = 1和x = S (S x'))。因此，我能得出的最短证明如下。

destruct x as [| [|] ]; reflexivity.
于 2019-04-04T10:20:07.183 回答
0

这是我最终得到的：

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

结果：

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

我想你必须用归纳法来证明它，因为当我尝试用预定义的 mult 破坏 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.
于 2019-03-23T23:14:36.803 回答