CoMoEx Induction.Induction


In diesem File möchte ich ein paar Worte zum Beweisprinzip Induktion verlieren. Ich beabsichtige hier nicht, eine komplette Einführung in Coq zu geben; vielmehr möchte ich ein paar (hoffentlich selbsterklärende) Beispiele geben, die jeweils die Struktur des Induktionsbeweises aufzeigen sollen.

Module nat_playground.
Der typische Fall struktureller Induktion ist die vollständige Induktion. Diese baut auf den natürlichen Zahlen auf. Diese können wir mittels folgender Grammatik angeben:
n ::= O | S n
Solche Strukturen kann man auch in Coq formalisieren:

  Inductive my_nat :=
    | zero : my_nat
    | succ (n : my_nat) : my_nat
        .

  Check my_nat.
  Print my_nat.

So eine Definition gibt es natürlich schon standardmäßig in Coq:

  Check nat.
  Print nat.

Man kann auf den natürlichen Zahlen rekursive Funktionen definieren, sogenannte Fixpunkte.

  Fixpoint addN (n m : my_nat) : my_nat :=
    match n with
    | zero ⇒ m
    | succ n' ⇒ succ (addN n' m)
Ich rechne also wie folgt: (n+1) + m = 1 + (n + m)
    end
  .

Die folgenden 3 Beweise sind mathematisch gesehen sehr elementar. Mir geht es hier primär darum, einen Blick auf das Beweisprinzip der (hier) vollständigen Induktion zu lenken; ein genaues Nachvollziehen der einen Unterbeweise ist nicht mein Ziel. Trotzdem hoffe ich, halbwegs lesbare Beweise geschrieben zu haben trotz wahrscheinlich noch unbekannter Taktiken.

  Lemma addN_zero_r : ∀ (n : my_nat), addN n zero = n.
  Proof.
    intro n.
    induction n as [ | n' IV].
Wir machen also nun Induktion über n: Im Induktionsanfang nehmen wir n = 0 an, im Induktionsschritt n = n' + 1, wobei wir die Aussage als schon gezeigt für n' annehmen. Das kann man übrigens auch sichtbar machen mit der folgenden alternativen Zeile. Einfach mal statt dieser Zeile ausführen. induction n as | n' IV eqn:eq.
    -
IA: "P(0)" bzw. "P(zero)"
      simpl.
      reflexivity.
    -
IS: "P(n) ~> P(n+1)" bzw. "P(n) ~> P(succ n)"
      simpl.
      f_equal.
      exact IV.
  Qed.

  Lemma addN_n_succ_m : ∀ (n m : my_nat), addN n (succ m) = succ (addN n m).
  Proof.
    intro n.
    induction n as [ | n' IV].
    -
IA: "P(0)" bzw. "P(zero)"

      intro m.
      simpl.
      reflexivity.
    -
IS: "P(n) ~> P(n+1)" bzw. "P(n) ~> P(succ n)"

      intro m.
      simpl.
      f_equal.
      apply IV.
  Qed.

  Theorem addN_comm : ∀ (n m : my_nat), addN n m = addN m n.
  Proof.
    intros n .
    induction n as [| n' IV].
    -
IA: "P(0)" bzw. "P(zero)"

      intro m.
      simpl.
      symmetry.
      apply addN_zero_r.
    -
IS: "P(n) ~> P(n+1)" bzw. "P(n) ~> P(succ n)"

      intro m.
      simpl.
      rewrite IV.
      rewrite addN_n_succ_m.
      reflexivity.
  Qed.

Man kann das Induktionsprinzip auch explizit anschauen und anwenden statt der `induction`-Taktik:

  Check my_nat_ind.
  Check nat_ind.
  • >
    nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

  Theorem addN_comm' : ∀ (m n : my_nat), addN n m = addN m n.
  Proof.
    intro m.
    apply my_nat_ind.
    -
      simpl.
      symmetry.
      apply addN_zero_r.
    -
      intro n.
      intro IV.
      simpl.
      rewrite IV.
      rewrite addN_n_succ_m.
      reflexivity.
  Qed.

End nat_playground.

Module logic_vol1.

Nun ein komplexeres Beispiel:
x,y ::= bot | A | neg x | conj x y | disj x y | impl x y | iff x y

  Definition atoms : Type := nat.

  Inductive form :=
    | bot : form
bottom, Falsum
    | top : form
top, Verum
    | atom (A : atoms) : form
Konstruktor für ein Atom, z.B. entspricht die logische Aussage "A" einfach "atom A" hier.
    | neg (x : form) : form
Negation
    | conj (x y : form) : form
Konjunktion
    | disj (x y : form) : form
Disjunktion
    | impl (x y : form) : form
Implikation
    | iff (x y : form) : form
Biimplikation
        .

  Print form.

  Fixpoint evaluate (f : form) (k : atoms → Prop) : Prop :=
    match f with
    | bot ⇒ False
    | top ⇒ True
    | atom A ⇒ k A
    | neg x ⇒ ¬ evaluate x k
    | conj x y ⇒ evaluate x k ∧ evaluate y k
    | disj x y ⇒ evaluate x k ∨ evaluate y k
    | impl x y ⇒ evaluate x k → evaluate y k
    | iff x y ⇒ evaluate x k ↔ evaluate y k
    end.

  Fixpoint contains (f : form) (A : atoms) : Prop :=
    match f with
    | bot ⇒ False
    | top ⇒ False
    | atom X ⇒ A = X
    | neg x ⇒ contains x A
    | conj x y ⇒ contains x A ∨ contains y A
    | disj x y ⇒ contains x A ∨ contains y A
    | impl x y ⇒ contains x A ∨ contains y A
    | iff x y ⇒ contains x A ∨ contains y A
    end.

  Fixpoint only_bot_atom_disj (f : form) : Prop :=
    match f with
    | bot ⇒ True
    | top ⇒ False
    | atom A ⇒ True
    | neg x ⇒ False
    | conj x y ⇒ False
    | disj x y ⇒ only_bot_atom_disj x ∧ only_bot_atom_disj y
    | impl x y ⇒ False
    | iff x y ⇒ False
    end.

  Section mini_ex.

    Variable f : form.
    Variable A : atoms.
    Variable k : atoms → Prop.

    Hypothesis H1 : k A.
    Hypothesis H2 : contains f A.
    Hypothesis H3 : only_bot_atom_disj f.

    Theorem disjunctive_correctness : evaluate f k.
    Proof.
      induction f as [| |B|x IVx|x IVx y IVy|x IVx y IVy|x IVx y IVy|x IVx y IVy].
Hier ist vielleicht schon aufgefallen, dass ich pro Operation jeweils einzeln die Induktionsvoraussetzungen aufschreiben muss. Bei einem Pen-And-Paper-Induktionsbeweis würde man vermutlich im Normalfall IV's für alle Induktionsschritte gemeinsam verwenden, um sich Schreibarbeit zu sparen. Technisch gesehen hat man aber offenbar pro Operation eigene IV's.
      -
"P(bot)"
        simpl in H2.
        contradiction.
Widerspruch: f enthält nicht das Atom A.
      -
"P(top)"
        simpl in H3.
        contradiction.
Widerspruch: Formel besteht nicht nur aus bot, atom und disj.
      -
"P(A)"
        simpl.
        simpl in H2, H3.
        subst.
Damit das ein nicht-trivialer Fall wird, muss A=B gelten. Kann man also vereinfachen.
        exact H1.
      -
"P(x) ~> P(neg x)"
        simpl in H3.
        contradiction.
Widerspruch: Formel besteht nicht nur aus bot, atom und disj.
      -
"P(x),P(y) -> P(conj x y)"
        simpl in H3.
        contradiction.
siehe neg
      -
"P(x),P(y) ~> P(disj x y)"
        simpl.
        simpl in H2, H3.
        destruct H3 as [H4 H5].
        destruct H2 as [H6|H6].
        +
          left.
          apply IVx.
          exact H6.
          exact H4.
        +
          right.
          apply IVy.
          exact H6.
          exact H5.
      -
"P(x),P(y) ~> P(impl x y)"
        simpl in H3.
        contradiction.
siehe neg
      -
"P(x),P(y) ~> P(iff x y)"
        simpl in H3.
        contradiction.
siehe neg
    Qed.

  End mini_ex.

End logic_vol1.

Module nat_exercises.

Hier nun noch ein paar Theoreme zum selbst ausprobieren.
  Import nat_playground.

Wir haben vorhin die natürlichen Zahlen neu definiert mittels my_nat:

  Print my_nat.

Ich möchte nun zeigen, dass die beiden Mengen nat und my_nat isomorph, also gleichmächtig sind. Dazu brauche ich eine Bijektion my_nat_to_nat:

  Fixpoint my_nat_to_nat (x : my_nat) : nat :=
    match x with
    | zero ⇒ O
    | succ x' ⇒ S (my_nat_to_nat x')
    end.

Was heißt es für eine Funktion, bijektiv zu sein? Sie muss injektiv und surjektiv sein.

  Definition inj (f : my_nat → nat) : Prop := ∀ (x x' : my_nat), f x = f x' → x = x'.

  Definition sur (f : my_nat → nat) : Prop := ∀ (y : nat), ∃ (x : my_nat), f x = y.

  Definition bij (f : my_nat → nat) : Prop := inj f ∧ sur f.

  Theorem my_nat_iso_to_nat : bij my_nat_to_nat.
  Proof.
An den folgenden 3 Zeilen sieht man auch nochmal schön, dass es eine gute Beweisstrategie ist, erstmal Definitionen "auszupacken":
    unfold bij.
    unfold inj.
    unfold sur.
    split.
    -
inj
      intro x.
      admit.
    -
sur
      intro y.
      admit.
  Admitted.

Widmen wir uns wieder den praktischen Sachen: Assoziativität.

  Theorem addN_assoc : ∀ (x y z : my_nat), addN x (addN y z) = addN (addN x y) z.
  Proof.
  Admitted.

Nun wollen wir noch die Multiplikation rekursiv definieren:

  Fixpoint mulN (n m : my_nat) : my_nat :=
    match n with
    | zero ⇒ zero
    | succ n' ⇒ addN m (mulN n' m)
    end.

  Lemma mulN_zero_r : ∀ (n : my_nat), mulN n zero = zero.
  Proof.
  Admitted.

  Lemma mulN_n_succ_m : ∀ (n m' : my_nat), mulN n (succ m') = addN (mulN n m') n.
  Proof.
  Admitted.

  Theorem mulN_comm : ∀ (n m : my_nat), mulN n m = mulN m n.
  Proof.
  Admitted.

  Theorem addN_mulN_distr_1 : ∀ x y z, mulN x (addN y z) = addN (mulN x y) (mulN x z).
  Proof.
  Admitted.

  Theorem addN_mulN_distr_2 : ∀ x y z, mulN (addN x y) z = addN (mulN x z) (mulN y z).
  Proof.
  Admitted.

  Theorem mulN_assoc : ∀ (x y z : my_nat), mulN x (mulN y z) = mulN (mulN x y) z.
  Proof.
  Admitted.

  Fixpoint addRow (n : my_nat) : my_nat :=
    match n with
    | zero ⇒ zero
    | succ n' ⇒ addN n (addRow n')
    end.

  Theorem know_this_one : ∀ (n : my_nat), mulN (succ (succ zero)) (addRow n) = mulN n (succ n).
  Proof.
  Admitted.

End nat_exercises.