分からない理由4 すぐ実装してみることが出来ない

Coqのような定理証明系の言語を覚えれば、理論や証明をコンピュータ上で実装してみることが出来ます。
覚えるのには時間がかかります。地道に勉強しましょう。

昨日は、Coqチュートリアルをやってみました。

以下のようなファイルを用意して、CoqIDEで上行ったり、下行ったりして眺めています。

(* 1.1.1 Declarations 宣言 *)
Module Playground1.

Check O.
Check nat.

Section Declaration.
  Variable n : nat.

  (* 仮定 Hypothesis *)
  Hypothesis Pos_n : ( gt n 0).

  Check gt.
  Check (nat -> Prop).
  Check gt n O.

(* 1.1.2 Definitions 定義 *)

  Definition one := (S O).
  Definition two : nat := S one.
  Definition three : nat := S two.
  Definition double (m:nat) := plus m m.
  Check (forall m:nat, gt m 0).

(* Reset Declaration. *)
End Declaration.

End Playground1.


Module Playground2.

(* 1.2 Introduction to the proof engine: Minimal Logic (3) Minimal Logic *)

Section Minimal_Logic.

  Variables A B C : Prop.
  Check (A -> B).

  Goal (A -> B -> C) -> (A -> B) -> A -> C.
    intro H.
    intros H' HA.
    apply H.
    exact HA.
    apply H'.
    assumption.
  Save trivial_lemma.

  Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
    intros.
    apply H; [ assumption | apply H0; assumption ].
  Save.

  Lemma distr_imp : (A -> B -> C) -> (A -> B) -> A -> C.
    auto.
  Abort.

  Inspect 3.


(* 1.3 Propositional Calculus *)
(* 1.3.1 Conjunction *)

  Lemma and_commutative : A /\ B -> B /\ A.
    intro.
    elim H.
    split.
    Restart.
    intro H; elim H; auto.
  Qed.

  Check conj.

(* 1.3.2 Disjunction *)

  Lemma or_commutative : A \/ B -> B \/ A.
    intro H; elim H.
    intro HA.
    clear H.
    right.
    trivial.
    auto.

(* 1.3.3 Tauto *)
    Restart.
    tauto.
  Qed.

  Print or_commutative.

  Lemma distr_and : A -> B /\ C -> (A -> B) /\ (A -> C).
    tauto.
  Qed.

(* 1.3.4 Classical reasoning *)

  Lemma Peirce : ((A -> B) -> A) -> A.
    try tauto.
  Abort.

  Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A).
    tauto.
  Qed.

  Require Import Classical.
  Check NNPP.

  Lemma Peirce : ((A -> B) -> A) -> A.
    apply NNPP; tauto.
  Qed.
End Minimal_Logic.
End Playground2.

Module Club.
Section club.

  Variables Scottish RedSocks WearKilt Married GoOutSunday : Prop.

  Hypothesis rule1 : ~ Scottish -> RedSocks.
  Hypothesis rule2 : WearKilt \/ ~ RedSocks.
  Hypothesis rule3 : Married -> ~ GoOutSunday.
  Hypothesis rule4 : GoOutSunday <-> Scottish.
  Hypothesis rule5 : WearKilt -> Scottish /\ Married.
  Hypothesis rule6 : Scottish -> WearKilt.

  Lemma NoMember : False.
    tauto.
  Qed.

End club.

Check NoMember.
End Club.



(* Reset Initial. *)
(* 1.4 Predicate Calculus page 18. *)
(* 1.4.1 Sections and signatures *)

Module Playground3.

Section Predicate_calculus.
  Variable D : Set.
  Variable R : D -> D -> Prop.

  Section R_sym_trans.
    Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
    Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.

(* 1.4.2 Existential quantification *)

    Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
      intros.
      Check ex.
      Restart.
      intros x x_Rlinked.
      (* intro y.*)
      Restart.
      intros x x_Rlinked.
      elim x_Rlinked.
      intros y Rxy.
      apply R_transitive with y.
      assumption.
      apply R_symmetric; assumption.
    Qed.
  End R_sym_trans.

(* 1.4.3 Paradoxes of classical predicate calculus *)

  Variable P : D -> Prop.
  Variable d : D.

  Lemma weird : (forall x:D, P x) -> exists a, P a.
    intro UnivP.
    exists d; trivial.
  Qed.

  Hypothesis EM : forall A:Prop, A \/ ~ A.

  Lemma drinker : exists x:D, P x -> forall x:D, P x.
    elim (EM (exists x, ~ P x)).
    intro Non_drinker; elim Non_drinker; intros Tom Tom_does_not_drink.
    exists Tom; intro Tom_drinks.
    absurd (P Tom); trivial.
    intro No_nondrinker; exists d; intro d_drinks.
    intro Dick; elim (EM (P Dick)); trivial.
    intro Dick_does_not_drink; absurd (exists x, ~ P x); trivial.
    exists Dick; trivial.
  Qed.
End Predicate_calculus.
Check refl_if.
Check weird.
Check drinker.

(* 1.4.4 Flexible use of local assumptions *)
Section Predicate_Calculus.
  Variables P Q : nat -> Prop.
  Variable R : nat -> nat -> Prop.
  
  Lemma PQR :
    forall x y:nat, (R x x -> P x -> Q x) -> P x -> R x y -> Q x.
    intros.
    generalize H0.
    cut (R x x); trivial.
  Abort.

(* 1.4.5 Equality *)

  Variable f : nat -> nat.
  Hypothesis foo : f 0 = 0.

  Lemma L1 : forall k:nat, k = 0 -> f k = k.
    intros k E.
    rewrite E.
    apply foo.
  Qed.

  Hypothesis f10 : f 1 = f 0.
  Lemma L2 : f (f 1) = 0.
    replace (f 1) with 0.
    apply foo.
    transitivity (f 0); symmetry; trivial.
    Restart.
    replace (f 0) with 0.
    rewrite f10; rewrite foo; trivial.
  Qed.

(* 1.5 Using definitions *)
(* 1.5.1 Unfolding definitions *)

  Variable U : Type.
  Definition set := U -> Prop.
  Definition element (x:U) (S:set) := S x.
  Definition subset (A B:set) := forall x:U, element x A -> element x B.
  Definition transitive (T:Type) (R:T -> T -> Prop) :=
  forall x y z:T, R x y -> R y z -> R x z.
  Lemma subset_transitive : transitive set subset.
    unfold transitive.
    unfold subset.
    auto.
    Undo 2.
    unfold subset at 2.
    intros.
    unfold subset in H.
    red.
    auto.
  Qed.
End Predicate_Calculus.

End Playground3.

(* 1.5.2 Principle of proof irrelevance *)

(* Chapter 2 *)
(* Induction *)
(* 2.1 Data Types as Inductively Defined Mathematical Collections *)
(* 2.1.1 Booleans *)
Module Playground4.

  Inductive bool : Set := true | false.
  Check bool_ind.
  Check bool_rec.
  Check bool_rect.

  Lemma duality : forall b:bool, b = true \/ b = false.
    intro b.
    elim b.
    left; trivial.
    right; trivial.
    Restart.
    simple induction b; auto.
  Qed.

(* 2.1.2 Natural numbers *)

  Inductive nat : Set :=
    | O : nat
    | S : nat -> nat.

  Check nat_ind.
  Check nat_rec.
  Definition prim_rec := nat_rec (fun i:nat => nat).
  Check prim_rec.
  Eval cbv beta in
    ((fun _:nat => nat) O ->
      (forall y:nat, (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
       forall n:nat, (fun _:nat => nat) n).

  Definition addition (n m:nat) := prim_rec m (fun p rec:nat => S rec) n.

  Eval compute in (addition (S (S O)) (S (S (S O)))).

  Fixpoint plus (n m:nat) {struct n} : nat :=
    match n with
    | O => m
    | S p => S (plus p m)
  end.

(*  Reset bool. *)
End Playground4.

(* 2.1.3 Simple proofs by induction *)

  Lemma plus_n_O : forall n:nat, n = n + 0.
    intro n; elim n.
    simpl.
    auto.
    simpl; auto.
  Qed.

  Check eq_S.
  Hint Resolve plus_n_O .

  Lemma plus_n_S : forall n m:nat, S (n + m) = n + S m.
    simple induction n; simpl; auto.
  Qed.

  Hint Resolve plus_n_S .

  Lemma plus_com : forall n m:nat, n + m = m + n.
    simple induction m; simpl; auto.
    intros m' E; rewrite <- E; auto.
  Qed.

(* 2.1.4 Discriminate *)

  Definition Is_S (n:nat) := match n with
  | O => False
  | S p => True
  end.

  Lemma S_Is_S : forall n:nat, Is_S (S n).
    simpl; trivial.
  Qed.

  Lemma no_confusion : forall n:nat, 0 <> S n.
    red; intros n H.
    change (Is_S 0).
    rewrite H; trivial.
    simpl; trivial.
    Restart.
    intro n; discriminate.
  Qed.

(* 2.2 Logic Programming *)

Inductive le (n:nat) : nat -> Prop :=
| le_n : le n n
| le_S : forall m:nat, le n m -> le n (S m).
Check le.
Check le_ind.
Lemma le_n_S : forall n m:nat, le n m -> le (S n) (S m).
intros n m n_le_m.
elim n_le_m.
apply le_n; trivial.
intros; apply le_S; trivial.
Restart.
Hint Resolve le_n le_S .
simple induction 1; auto.
Qed.
Lemma tricky : forall n:nat, le n 0 -> n = 0.
intros n H; inversion_clear H.
trivial.
Qed.

(* Chapter 3 *)
(* Modules *)
(* 3.1 Opening library modules *)

Require Import Arith.
Require Import Coq.Arith.Arith.

(* 3.2 Creating your own modules *)

(* 3.3 Managing the context *)

SearchAbout le.
Search le.
SearchPattern (_ + _ = _).


(* 3.4 Now you are on your own *)