Induction.Multiplication

(*
    CoMoEx - Example of inductive proofs: Natural multiplication
    Copyright (C) 2024  Max Ole Elliger

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <https://www.gnu.org/licenses/>.
*)

From Induction Require Export Intro.

Wir wollen nun eine Multiplikation auf NAT definieren und anschließend zeigen, dass sich unsere Multiplikation kommutativ und assoziativ verhält.

Definition

Fixpoint mul (n1 n2 : NAT) : NAT :=
  match n1 with
  | zero => zero
  | succ (n1') => add (mul n1' n2) n2
  end.

Beispiele

Example mul_test_0_1 : mul zero (succ (zero)) = zero.
Proof.
  reflexivity.
Qed.

Example mul_test_1_0 : mul (succ (zero)) zero = zero.
Proof.
  reflexivity.
Qed.

Example mul_test_2_2 :
  mul (succ (succ (zero))) (succ (succ (zero))) = succ (succ (succ (succ (zero)))).
Proof.
  reflexivity.
Qed.

Beweise

Hilfslemmatas

Lemma mul_zero_r :
  forall n,
    mul n zero = zero.
Proof.
Admitted.

Lemma mul_succ_r :
  forall n1 n2,
    mul n1 (succ n2) = add n1 (mul n1 n2).
Proof.

Im sogenannten Induktionsschritt ist es hilfreich, bereits bewiesene Tatsachen über add zu verwenden, z.B. add_succ_r.

Admitted.

Kommutativität

Theorem mul_comm :
forall (n1 n2 : NAT),
mul n1 n2 = mul n2 n1.
Proof.
Admitted.

Distributivität

Theorem add_mul_distr_1 :
  forall n1 n2 n3,
    mul n1 (add n2 n3) = add (mul n1 n2) (mul n1 n3).
Proof.
  induction n1 as [|n1' IH].
  -
    admit.
  -
    intros n2 n3.
    simpl.
    rewrite IH.

Dieser Teilbeweis erfordert einen erhöhten Einsatz von rewrite. Wir müssen einige Male unser Lemma add_assoc sowie add_comm verwenden. Wir formen zunächst die linke Seite um.

    rewrite <- add_assoc with
      (n1 := mul n1' n2)
      (n2 := mul n1' n3)
      (n3 := add n2 n3).
    rewrite add_assoc with
      (n1 := (mul n1' n3))
      (n2 := n2)
      (n3 := n3).
    rewrite add_comm with
      (n1 := mul n1' n3)
      (n2 := n2).

Nun zur rechten Seite:

    rewrite <- add_assoc with
      (n1 := mul n1' n2)
      (n2 := n2)
      (n3 := add (mul n1' n3) n3).
    rewrite add_assoc with
      (n1 := n2)
      (n2 := mul n1' n3)
      (n3 := n3).
    reflexivity.
Admitted.

Theorem add_mul_distr_2 :
  forall n1 n2 n3,
    mul (add n1 n2) n3 = add (mul n1 n3) (mul n2 n3).
Proof.

Hier kann man ähnlich vorgehen wie in add_mul_distr_1. Es gibt aber auch einen leichteren Weg:

  intros n1 n2 n3.
  rewrite mul_comm with
    (n1 := add n1 n2)
    (n2 := n3).
  rewrite add_mul_distr_1 with
    (n1 := n3)
    (n2 := n1)
    (n3 := n2).
  rewrite mul_comm with
    (n1 := n3)
    (n2 := n1).
  rewrite mul_comm with
    (n1 := n3)
    (n2 := n2).
  reflexivity.

Probier den Beweis aber ruhig nochmal mit Induktion!

Restart.

Admitted.

Assoziativität

Theorem mul_assoc :
forall (n1 n2 n3 : NAT),
mul n1 (mul n2 n3) = mul (mul n1 n2) n3.
Proof.
Admitted.