分からない理由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 *)