Coq を使った証明 : まとめ 稲葉.

Presentation on theme: "Coq を使った証明 : まとめ 稲葉."— Presentation transcript:

1 Coq を使った証明 : まとめ 稲葉

2 今日の内容 型システム 対話的証明環境 Minimal Logic での証明 自動証明探索 Inductive な定義と証明 論理演算子
「＝」とreduction CoInductive な定義と証明

3 型システム （階層構造） Set Type Prop P→Q odd 3 nat → nat fun n => n+1 など
list nat [1, 2, 3] など Type P→Q P→Q の証明 Prop odd 3 odd 3 の証明

4 型システム（２つのプリミティブ） Product ( → ) Dependent Product ( ∀ )
(P->Q) -> (Q->R) -> (P->R) nat -> nat Dependent Product ( ∀ ) forall x:nat, odd x -> even (S x) forall A:Set, list A -> list A forall x:nat, int_type_with_bits x forall x:nat, 0<x -> nat 全称量化命題 Set以外に依存した型 多相型 部分関数

5 型システム(ユーザー定義の型) Inductive 後述 CoInductive

6 対話的証明環境 (1) Theorem 名前 : 命題. Lemma 名前 : 命題. Remark 名前 : 命題.
Fact 名前 : 命題. …などで証明開始 Qed. Defined. …などで証明おわり。

7 対話的証明環境 (2) Restart. Undo. Abort. Suspend. と Resume. …で証明を振り出しに戻す
…で１ステップ戻る Abort. …でその定理の証明を破棄 Suspend. と Resume. …で、証明を一時中断してTopLevelに帰る

8 対話型証明環境 (3) 命題Pを型とするtermは、「命題Pの証明」であった。 したがって、「命題Pを証明すること」
「仮定(型環境) ├ t : ゴール」 を満たすterm t を対話的に構築する

9 Minimal Logic での証明 (1) Product と Dependent Product のみの場合
使う tactic は、基本的には２つだけ intro x H├ A→B を H,x:A ├ B に apply f H,f:A→B├B’ を H,f:A→B├A’ に

10 Minimal Logic での証明 (2) intro 変数名 intros 変数名… apply 変数名
ゴールが (Dependent) Product の時、ゴールの前件を仮定にもってくる apply 変数名 apply 変数名 with (名:= term)… (Dependent) Product 型を持つ変数を指定すると、その後件とゴールをunifyしてゴールを前件に書き換える

11 Minimal Logic での証明 (3) 便利機能 exact H. assumption. eapply H.
apply H と同じ。Hの型がゴールと完全一致するとき使う assumption. 仮定の中のどれかが exact. eapply H. unify の結果、束縛が完全に決まらず変数が残ってしまう場合、エラーとせずに、変数を残してゴールを変形する。Prolog っぽい動作になる。

12 Minimal Logic での証明 (4) 便利機能 H├ B を H├A と H├A→B に
cut A H├ B を H├A と H├A→B に generalize x intro しすぎたときに「戻す」 H,x:A├ B を H,x:A ├ A→B に xがBでFreeならDependent, そうでなければ普通のProduct generalize (Bのsubterm) という使い方もできる

13 Minimal Logic での証明 (5) 便利機能 SearchPattern Set Implicit Arguments.
指定したパターンにapply可能な定義のリストを表示 Set Implicit Arguments. Dependent Product の引数を省略しても推論してくれるようになるオプション。

14 自動証明探索 (1) auto eauto trivial 「intro」と、「仮定のapply」を使ってひたすら探索
autoでのapplyの代わりにeapplyを使う trivial auto 1. と同じ 各tacticには「コスト」が設定されている。introは0, 仮定のapplyは1, …。

15 自動証明探索 (2) auto with ヒントデータベース Hint Resolve 定理名達 : データベース名
仮定だけでなく、ヒントデータベースにある定理のapplyも試みるauto Hint Resolve 定理名達 : データベース名 データベースの作成 Hint ～ ～ ～ ～ で、apply以外のtacticも探索させられるらしい…

16 Inductive な定義と証明 (1) Inductive な型定義 Inductive nat : Set := | O : nat
こんな感じ Inductive nat : Set := | O : nat | S : nat -> nat. Inductive list (A:Set) : Set := | nil : list A | cons : A -> list A -> list A.

17 Inductiveな定義と証明 (2) 同時に、帰納法の公理が定義される Inductive nat : Set := | O : nat
| S : nat -> nat. nat_ind : forall P: nat -> Prop, P 0 -> forall n:nat, (P n -> P (S n)) -> forall n:nat, P n

18 Inductive な定義と証明 (3) Inductive な命題の定義 (同様) ev0 は even 0 の証明
ev2 4 (ev2 2 ev0) は even 4 の証明 Inductive even : nat->Prop := | ev0 : even 0 | ev2 : forall n:nat, even n -> even (S(S n)).

19 Inductive な定義と証明 (4) 同時に、帰納法の公理 even_ind : forall P: nat -> Prop,
forall n:nat, (even n -> P n -> P SSn) -> forall n:nat, even n -> P n

20 Inductive な定義と証明 (5) 基本的に使うtacticは、intro, apply ともう２つ elim H. case H.
H の型が Inductive T のとき、かなり賢く 「apply T_ind. 」してくれるtactic pattern ; apply T_ind with …; try exact H. case H. T_ind を使わず、単純にInductive定義のコンストラクタごとに場合わけ。「帰納法の仮定」なし

21 Inductive な定義と証明 (6) 便利機能 induction H. intros [H1 H2 H3 …]
「intro ; intro ; … ; elim H」 と同じ intros [H1 H2 H3 …] 「intro X; case X; intros H1 H2 H3 …」 と同じ intros [H1 | H2 | H3 | …] 「intro X; case X; (intros H1 | intro H2 | …)」 と同じ

22 Inductive な定義と証明 (7) 便利機能 constructor N. split left right exists t
「apply N番目のコンストラクタ」 と同じ split 「constructor 1」 と同じ （コンストラクタ１個のとき専用） left 「constructor 1」 と同じ （コンストラクタ２個のとき専用） right 「constructor 2」 と同じ　（コンストラクタ２個のとき専用） exists t 「constructor 1 with t」 と同じ (１個専用)

23 Inductive な定義と証明 (8) 便利機能 discriminate H. discriminate. injection H.
仮定 H: A = B があって A と B が違うコンストラクタ discriminate. ゴールが ~(A=B). で A と B が違うコンストラクタ injection H. H:c x=c y├G を H:c x=c y├x=y→G に inversion H. H:P x のとき。P xの全ての可能なコンストラクタの前件を仮定にもってくる。１個もなければ証明終了。

24 Inductive な定義と証明 (9) inversion なしで discriminate なしで ~(even 1) の証明
forall n:nat, even n -> n<>1 なら even_ind で証明できる discriminate なしで H:0=S 0 ├ False の証明 (fun n:nat => match n with 0->True | S _-> False) (S 0) = False は証明できる。rewrite。

25 論理演算子 (1) Inductive True : Prop := Inductive False : Prop := .
I : True. Inductive False : Prop := . Inductive and (A B: Prop) : Prop := conj : A -> B -> and A B Inductive or (A B: Prop) : Prop := or_introl : A -> or A B or_intror : B -> or A B. Inductive ex (A:Type)(P:A->Prop) : Prop := ex_intro : forall x:A, P x -> ex A P. Inductive eq (A:Type)(x:A) : A->Prop := refl_equal : eq A x x.

26 論理演算子 (2) not に関する証明に便利な tactic.
Definition not (P:Prop) := P->False. not に関する証明に便利な tactic. apply False_ind. ゴールをFalseに変える absurd P. ゴールがFalseのとき、それをPと~Pの２つに変える contradiction 現在の仮定の中から型がFalseのものを探す

27 「＝」とreduction (1) 「H : A = B」 のとき… rewrite H. rewrite <- H.
ゴール内の B を A に置き換える 実は elim H rewrite H in H2. 仮定H2内の A を B に置き換える

28 「＝」とreduction (2) unfold t. unfold t in H. red.
ゴールの subterm t の定義を展開 unfold t in H. 仮定の subterm を unfold. red. ゴールが _→…→_→(c t … t) なら unfold c. simpl. cbv… lazy… compute…. がんばってδβιζ変換 pattern t at 場所. ゴールの t をラムダ抽象。tが複数あるときは指定できる

29 CoInductive な定義と証明 (1) Inductiveな定義と文法はほぼ同じ ただし帰納法のための公理は定義されない
Base Case がなくてもよい CoInductive Llist (A:Set) : Set := | Lnil : Llist A | Lcons : A -> Llist A -> Llist A.

30 CoInductive な定義と証明 (2) 基本的に使うtacticは、intro, apply と
elim, induction は使えない case, discriminate, injection, inversion は使える cofix 現在の(CoFixpointな述語による)ゴールを、そのまま仮定部にコピーする。ただし、その仮定は「apply コンストラクタ」の直下でしか使えない