Как доказать что-то, используя определение?

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

Как указал @ user138737, индукция не нужна.Достаточно изучить три случая: x = 0, x = 1 и x = S (S x')).Таким образом, самое короткое доказательство, с которым я могу прийти, состоит в следующем.

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

Answer 3

Вот что я получаю:

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 доказательства, но с предопределенным множеством:

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.