Coqの初歩メモ

13447 ワード

Coq Coq テキストリンク

命題論理に興味があったし，Coqにも興味があった．適切な題材を探していたところよさそうなものを見つけた．これを理解する際のメモ．

命題論理がよくわからない
自然演繹，シーケント計算など，理解できていない．自分の理解を形式的に検証するためにCoqを使う
命題論理を勉強しようと思っても本によって用語等がちょっとずつ違う
このメモにおいて一貫した用語を使う．
本の用語との対応を明確にする
Coqがよくわからない
命題論理を題材にして，Coqの機能を覚えたい

暗黙引数とモジュールを使わずに考える

Coqに不慣れなため，考え方に慣れるために，省略，モジュール，Notationは使わないでしばらくやってみる．ただし，Initは読み込む．

listについて

list

listはCoq.Init.Datatypesで定義される．

Inductive list (A : Type) : Type :=
    nil : list A | cons : A -> list A -> list A

or

Coq.Init.Logicで定義される．

Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B

orのnotationも設定されている

eq

Coq.Init.Logicで定義される．

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

eqのnotationも設定されている

In

Coq.Lists.Listで定義される．

Fixpoint In A (a:A) (l:list A) : Prop :=
  match l with
    | nil => False
    | cons b m => b = a \/ In A a m
  end.

False

Coq.Init.Logicで定義される．

Inductive False : Prop :=

propとSC_proves

簡易版

まずは実際のpropではなく，最初のcaseだけで定義してみる．

Inductive prop1 atom : Type  : Type :=
  | atom_prop1 : atom -> prop1 atom.

Inductive SC_proves1 atom : list (prop1 atom) -> prop1 atom -> Prop :=
  | SC_init1  Γ P : In (prop1 atom) P Γ -> SC_proves1 atom Γ P.

簡易版はできたようだ．

prop

論理式を定義する．

Inductive prop atom : Type :=
| atom_prop : atom -> prop atom
| bot_prop : prop atom
| top_prop : prop atom
| and_prop : prop atom -> prop atom -> prop atom
| or_prop : prop atom -> prop atom -> prop atom
| impl_prop : prop atom -> prop atom -> prop atom.

すなわち論理式は次のいずれかである．

原子論理式
⊥
⊤
かつ
または
ならば

not_prop

否定を定義する．

Definition not_prop atom (P : prop atom) :=
  impl_prop atom P (bot_prop atom).

これは，Pの否定は「P⊃⊥」ということで定義している．

SC_proves

シーケント計算の推論規則を定める．

Inductive SC_proves atom : list (prop atom) -> prop atom -> Prop :=
| SC_init P Γ : In (prop atom) P Γ -> SC_proves atom Γ P
| SC_bot_elim P Γ : In (prop atom) (bot_prop atom) Γ -> SC_proves atom Γ P
| SC_top_intro Γ : SC_proves atom Γ (top_prop atom)
| SC_and_intro Γ P Q : SC_proves atom Γ P -> SC_proves atom Γ Q -> SC_proves atom Γ (and_prop atom P Q)
| SC_and_elim Γ P Q R : In (prop atom) (and_prop atom P Q) Γ -> 
        SC_proves atom (cons P (cons Q Γ)) R -> SC_proves atom Γ R
| SC_or_introl Γ P Q : SC_proves atom Γ P -> SC_proves atom Γ (or_prop atom P Q)
| SC_or_intror Γ P Q : SC_proves atom Γ Q -> SC_proves atom Γ (or_prop atom P Q)
| SC_or_elim Γ P Q R : In (prop atom) (or_prop atom P Q) Γ -> SC_proves atom (cons P Γ)  R ->
        SC_proves atom (cons Q Γ) R -> SC_proves atom Γ R
| SC_impl_intro Γ P Q : SC_proves atom (cons P Γ) Q -> SC_proves atom Γ (impl_prop atom P Q)
| SC_impl_elim Γ P Q R : In (prop atom) (impl_prop atom P Q) Γ -> SC_proves atom Γ P ->
        SC_proves atom (cons Q Γ) R -> SC_proves atom Γ R.

これは，シーケント計算の推論規則が以下の10個であるということ．

PがΓにあるならΓ⇒P
⊥がΓにあるなら任意のPについてΓ⇒P
任意のΓについてΓ⇒⊤
Γ⇒PかつΓ⇒QならΓ⇒P∧Q
P∧QがΓにあり，P,Q,Γ⇒RならΓ⇒R
Γ⇒PならばΓ⇒P∨Q
Γ⇒QならばΓ⇒P∨Q
P∨QがΓにあり，P,Γ⇒RかつQ,Γ⇒RならΓ⇒R
P,Γ⇒QならΓ⇒P⊃Q
P⊃QがΓにあり，Γ⇒PかつQ,Γ⇒RならΓ⇒R

例題

いくつか例題をやってみたい

P⊃P

Theorem PP : forall atom P, SC_proves atom nil (impl_prop atom P P).
Proof.
intros.
apply SC_impl_intro.
apply SC_init.
simpl. apply or_introl. reflexivity. Qed.

P∧Q⊃Q∧P

Theorem and_comm : forall atom P Q, SC_proves atom nil 
    (impl_prop atom (and_prop atom P Q) (and_prop atom Q P)).
Proof.
 intros.
 apply SC_impl_intro.
 apply SC_and_intro.
 + apply (SC_and_elim atom _ P Q _).
    - simpl. apply or_introl. reflexivity.
    - apply SC_init. simpl. apply or_intror. apply or_introl. reflexivity.
 + apply (SC_and_elim atom _ P Q _).
    - simpl. apply or_introl. reflexivity.
    - apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

P∨Q⊃Q∨P

Theorem or_comm : forall atom P Q, SC_proves atom nil
    (impl_prop atom (or_prop atom P Q) (or_prop atom Q P)).
Proof.
  intros.
  apply SC_impl_intro.
  apply (SC_or_elim _ (cons (or_prop atom P Q) nil) P Q (or_prop atom Q P)).
  + simpl. apply or_introl. reflexivity.
  + apply SC_or_intror. apply SC_init. simpl. apply or_introl. reflexivity.
  + apply SC_or_introl. apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

P⊃(Q⊃P)

Theorem PQP : forall atom P Q, SC_proves atom nil 
    (impl_prop atom P (impl_prop atom Q P)).
Proof.
  intros.
  apply SC_impl_intro.
  apply SC_impl_intro.
  apply SC_init.
  simpl. apply or_intror. apply or_introl. reflexivity.
Qed.

P⊃Q,Q⊃R⇒P⊃R

Theorem syllogism : forall atom P Q R, SC_proves atom
    (cons (impl_prop atom P Q) (cons (impl_prop atom Q R) nil)) (impl_prop atom P R).
Proof.
  intros.
  apply SC_impl_intro.
  apply (SC_impl_elim _ _ P Q R).
  +  simpl. apply or_intror. apply or_introl. reflexivity.
  +  apply SC_init. simpl. apply or_introl. reflexivity.
  +  apply (SC_impl_elim _ _ Q R R).
      -  simpl. apply or_intror. apply or_intror. apply or_intror. apply or_introl. reflexivity.
      -  apply SC_init. simpl. apply or_introl. reflexivity.
      -  apply SC_init. simpl. apply or_introl. reflexivity.
Qed.

⊥⊃P

Theorem exp : forall atom P, SC_proves atom nil 
      (impl_prop atom (bot_prop atom) P).
Proof.
  intros.
  apply SC_impl_intro.
  apply SC_bot_elim.
  simpl. apply or_introl. reflexivity.
Qed.

この辺でやっと気づいた．今までやってたのは直観主義論理でした．

ここまでのソースコードはここにあります．

Coqの便利化をやってみる

今まででわかったことは，「Coqを使って命題論理のいろいろなことできそう」ということです．一方で「本質的でないキーワードをたくさん入力する必要がある」ということもわかりました．ここでは，implicit argument，Context，Notationを使ってCoqを使いやすくしてみましょう．

implicit arguments

implicit argumentsを使うとInの定義は次のようになります．

Fixpoint In {A} (a:A) (l:list A) : Prop :=
  match l with
    | nil => False
    | cons b m => b = a \/ In a m
  end.

propの定義も簡単になります．

Inductive prop {atom} : Type :=
| atom_prop : atom -> prop
| bot_prop : prop
| top_prop : prop
| and_prop : prop -> prop  -> prop
| or_prop : prop  -> prop  -> prop
| impl_prop : prop  -> prop  -> prop.

シーケント計算の推論規則も次のようになります．

Inductive SC_proves {atom} : list (@prop atom) -> @prop atom -> Prop :=
| SC_init P Γ : In P Γ -> SC_proves Γ P
| SC_bot_elim P Γ : In bot_prop Γ -> SC_proves Γ P
| SC_top_intro Γ : SC_proves Γ top_prop
| SC_and_intro Γ P Q : SC_proves Γ P -> SC_proves Γ Q -> SC_proves Γ (and_prop P Q)
| SC_and_elim Γ P Q R : In (and_prop P Q) Γ -> 
        SC_proves (cons P (cons Q Γ)) R -> SC_proves Γ R
| SC_or_introl Γ P Q : SC_proves Γ P -> SC_proves Γ (or_prop P Q)
| SC_or_intror Γ P Q : SC_proves Γ Q -> SC_proves Γ (or_prop P Q)
| SC_or_elim Γ P Q R : In (or_prop P Q) Γ -> SC_proves (cons P Γ)  R ->
        SC_proves (cons Q Γ) R -> SC_proves Γ R
| SC_impl_intro Γ P Q : SC_proves (cons P Γ) Q -> SC_proves Γ (impl_prop P Q)
| SC_impl_elim Γ P Q R : In (impl_prop P Q) Γ -> SC_proves Γ P ->
        SC_proves (cons Q Γ) R -> SC_proves Γ R.

ここまでのソースコードはここにあります．

Context

次にContextを使ってatomをパラメータにしてみましょう．

次の行を先頭の方に追加します．

Context {atom : Type}.

propの定義は次のように書けるようになります．

Inductive prop : Type :=
| atom_prop : atom -> prop
| bot_prop : prop
| top_prop : prop
| and_prop : prop -> prop  -> prop
| or_prop : prop  -> prop  -> prop
| impl_prop : prop  -> prop  -> prop.

ここまでのソースコードはここにあります．

Notation

最後にNotationを設定してみましょう．

次のような行を追加して設定します．

Notation "⊥" := bot_prop.
Notation "⊤" := top_prop.
Infix "∧" := and_prop (left associativity, at level 52).
Infix "∨" := or_prop (left associativity, at level 53).
Infix "⊃" := impl_prop (right associativity, at level 54).

Notation "¬ P" := (not_prop P) (at level 51).

Infix "∈" := In (right associativity, at level 55).
Notation "x → y" := (x -> y) (at level 99, y at level 200, right associativity).

Open Scope list_scope.

Reserved Notation "Γ ⇒ P" (no associativity, at level 61).

Notation "⇒ P" := (nil ⇒ P) (no associativity, at level 61).

推論規則は次のように書けます．

Inductive SC_proves : list prop -> prop -> Prop :=
| SC_init P Γ : P ∈ Γ → Γ  ⇒ P
| SC_bot_elim P Γ : ⊥ ∈ Γ → Γ ⇒ P
| SC_top_intro Γ : Γ ⇒ ⊤
| SC_and_intro Γ P Q : Γ ⇒ P → Γ ⇒ Q → Γ ⇒ P ∧ Q
| SC_and_elim Γ P Q R : P ∧ Q ∈ Γ → P :: Q :: Γ ⇒ R → Γ ⇒ R
| SC_or_introl Γ P Q :  Γ ⇒ P → Γ ⇒ P ∨ Q
| SC_or_intror Γ P Q : Γ ⇒ Q → Γ ⇒ P ∨ Q
| SC_or_elim Γ P Q R : P ∨ Q ∈ Γ → P :: Γ ⇒ R → Q :: Γ ⇒ R → Γ ⇒ R
| SC_impl_intro Γ P Q : P :: Γ ⇒ Q → Γ ⇒ P ⊃ Q
| SC_impl_elim Γ P Q R : P ⊃ Q ∈ Γ → Γ ⇒ P → Q :: Γ ⇒ R → Γ ⇒ R
  where "Γ ⇒ P" := (SC_proves Γ P).

例題の主張は次のようになります．

Theorem PP : forall P, ⇒ P⊃P.
Theorem and_comm : forall P Q, ⇒ P∧Q ⊃ Q∧P.
Theorem or_comm : forall P Q, ⇒ P∨Q ⊃ Q∨P.
Theorem PQP : forall P Q, ⇒ P ⊃ Q⊃P.
Theorem syllogism : forall P Q R, P⊃Q :: Q⊃R :: nil ⇒ P⊃R.
Theorem exp : forall P, ⇒ ⊥⊃P.

ここまでのソースコードはここにあります．

ショートカットキーを使って記号を入力する方法についてはこちらの記事もご覧ください．

Author And Source

この問題について(Coqの初歩メモ), 我々は、より多くの情報をここで見つけました https://qiita.com/lion/items/b773d76538f57ead9599

著者帰属：元の著者の情報は、元のURLに含まれています。著作権は原作者に属する。

Content is automatically searched and collected through network algorithms . If there is a violation . Please contact us . We will adjust (correct author information ,or delete content ) as soon as possible .