rm ind/OldMaterial.v

ind/OldMaterial.v

-
-
-(** 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 : forall (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 : forall (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 : forall (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' : forall (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 := forall (x x' : my_nat), f x = f x' -> x = x'.
-
-  Definition sur (f : my_nat -> nat) : Prop := forall (y : nat), exists (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 : forall (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 : forall (n : my_nat), mulN n zero = zero.
-  Proof.
-  Admitted.
-
-  Lemma mulN_n_succ_m : forall (n m' : my_nat), mulN n (succ m') = addN (mulN n m') n.
-  Proof.
-  Admitted.
-
-  Theorem mulN_comm : forall (n m : my_nat), mulN n m = mulN m n.
-  Proof.
-  Admitted.
-
-  Theorem addN_mulN_distr_1 : forall x y z, mulN x (addN y z) = addN (mulN x y) (mulN x z).
-  Proof.
-  Admitted.
-
-  Theorem addN_mulN_distr_2 : forall x y z, mulN (addN x y) z = addN (mulN x z) (mulN y z).
-  Proof.
-  Admitted.
-
-  Theorem mulN_assoc : forall (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 : forall (n : my_nat), mulN (succ (succ zero)) (addRow n) = mulN n (succ n).
-  Proof.
-  Admitted.
-  
-End nat_exercises.