テンプレート

以下を前提にする

Require Import Arith List Omega ZArith.
From mathcomp Require Import all_ssreflect.
Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Proof handling

証明モード自体への操作

Undo

1手戻す

Restart

最初からやり直す

Show

証明の状態を表示する. コマンドをごちゃごちゃしすぎて今の状態が分からなくなったときに便利.

Abort

証明を諦める. 未証明のままで証明モードから抜ける.

Search

Search

Search

cases

apply - 適用

\(H \colon P \to Q\) が仮定または定理にあり, \(Q\) が goal のとき, apply H は goal を \(P\) にすり替える.

1 subgoal

  P : Type
  Q : Type
  H : P -> Q
  ============================
  Q

pq <   apply H.
1 subgoal
  
  P : Type
  Q : Type
  H : P -> Q
  ============================
  P

apply ... with

適用する仮定（定理）の forall な部分は上手いこと置き換えて適用するよう試みてくれるが, 上手く置き換えを見つけてくれないことがある. その場合には with でヒントを与えることが出来る.

1 subgoal
  
  H : forall (X : Type) (x y z : X), x = y -> y = z -> x = z
  a, b, c, d : nat
  ============================
  [a; b] = [b; c] -> [b; c] = [c; d] -> [a; b] = [c; d]

pq <   apply H with (x := [a;b]) (y := [b;c]).
No more subgoals.

case - 条件分岐

構造に関する条件分岐

変数名を引数に呼ぶと, 構造に関する条件分岐を行う.

例えばそれが nat であれば 0 か n.+1 (ssreflect の場合) かに分岐される.

1 subgoal

  m, n : nat
  H : m + n = 1
  ============================
  m = 0 \/ n = 0

solution <   case m.
2 subgoals

  m, n : nat
  H : m + n = 1
  ============================
  0 = 0 \/ n = 0

subgoal 2 is:
 forall n0 : nat, n0.+1 = 0 \/ n = 0

自由な条件分岐

自由に条件式 (_ == _) を引数に与えると, それが true の場合と false の場合に分岐する.

Definition fizz (n : nat) : bool :=
  if n == 3 then false
  else false.

Example ex : forall n, fizz n = false.
Proof.
  move => n.
  unfold fizz.
  - case (n == 3).
    (* n == 3 が true の場合 *)
    done.
  - (* otherwise *)
    done.

1 subgoal
  
  n : nat_eqType
  ============================
  (if n == 3 then false else false) == false

ex <     case (n == 3).
2 subgoals
  
  n : nat_eqType
  ============================
  false == false

subgoal 2 is:
 false == false

導入した条件式は即座に apply される. 仮定として残しておきたい場合は第2引数に eqn:(name) で名前を与える.

ex <     case (n == 3) eqn:Is3.
2 subgoals
  
  n : nat_eqType
  Is3 : (n == 3) = true
  ============================
  false == false

subgoal 2 is:
 false == false

congruence - 合同

等式 (_ = _) に関するゴールをいい感じに示してくれる証明戦略.

\[ a=b \land b=c \implies a=c \]

1 subgoal

  ============================
  forall (X : Type) (a b c : X), a = b -> b = c -> a = c

three_steps <   intros.
(* congruence がこれもやってくれるので実は不要 *)
1 subgoal

  X : Type
  a, b, c : X
  H : a = b
  H0 : b = c
  ============================
  a = c

three_steps <   congruence.
No more subgoals.

不等号 <> も (_ = _) -> False に過ぎず congruence で対処できることがある.

\[ n+1 \ne m+1 \implies n \ne m \]

1 subgoal
  
  ============================
  forall n m : nat, n.+1 <> m.+1 -> n <> m

ex < Proof.
1 subgoal
  
  ============================
  forall n m : nat, n.+1 <> m.+1 -> n <> m

ex <   congruence.
No more subgoals.

ex < Qed.

discriminate - 構築子の区別

injection は構築子が単射であることを利用して, 同じ構築の仕方を行って得た値は等しいという証明を行った. 同様に構築の仕方が異なるものは等しくないということも明らかなはずである. discriminate はこれを行う.

1 subgoal
  
  ============================
  true <> false

ex <   discriminate.
No more subgoals.

1 subgoal
  
  ============================
  2 <> 5

ex <   discriminate.
No more subgoals.

ちなみに十分明らかなので by done. でも同様に証明できる.

injection - 単射性

全てのコンストラクタ（構築子）は単射である. 例えば nat に対する S や, リスト [] は単射なので, \[ n + 1 = m + 1 \implies n = m, \] \[ [n] = [m] \implies n = m, \] が言える. 実際にこのことを証明で使うのに injection を使う.

1 subgoal

  n, m : nat
  H : n.+1 = m.+1
  ============================
  n = m

ex <   injection H.
1 subgoal

  n, m : nat
  H : n.+1 = m.+1
  ============================
  n = m -> n = m

ex <   done.
No more subgoals.

inversion - 単射の逆

inversion はコンストラクタに関する仮定を逆に戻す.

コンストラクタに関する等式

コンストラクタ S による等式 S x = S y が仮定 H にあったとき, inversion H は新たに x = y を仮定に追加する.

1 subgoal
  
  m, n : nat
  H : m.+1 = n.+1
  ============================
  m = n

ex <   inversion H.
1 subgoal
  
  m, n : nat
  H : m.+1 = n.+1
  H1 : m = n
  ============================
  n = n

命題を返すコンストラクタ

_ -> Prop であるような帰納的コンストラクタがあるとする. 例えば,

Inductive even : nat -> Prop :=
  | even_O : even 0
  | even_SS n (H : even n) : even n.+2.

があると, even m.+2 という仮定を even m に戻すことが出来る.

1 subgoal
  
  n : nat
  H : even n.+4
  ============================
  even n

ex <   inversion H.
1 subgoal
  
  n : nat
  H : even n.+4
  n0 : nat
  H1 : even n.+2
  H0 : n0 = n.+2
  ============================
  even n

このときやはり inversion は仮定を置き換えるのではなく, 新たに追加することしかしない.

simpl - 簡略化

自明な計算で簡略化できる部分をする.

Coq < Theorem test: 1 + 1 = 2.
1 subgoal

  ============================
  1 + 1 = 2

test < simpl.
1 subgoal

  ============================
  2 = 2

cases

仮定と前件の移動

\( \Gamma, P \vdash Q \) という証明と \( \Gamma \vdash P \implies Q \) という証明は等しい. Coq では仮定の中の任意の命題は Goal の一番左に前件として移動できるし, Goal の一番左の前件を仮定に移動することが自由に出来る.

intros

引数なく呼んだ時, 前件を持ってこれるだけ全部仮定に持っていく. このとき仮定の名前は適当に付けられるので注意.

Coq < Example ex : forall P Q R, P -> (P -> Q) -> R.
1 subgoal
  
  ============================
  forall P Q R : Type, P -> (P -> Q) -> R

ex <   intros.
1 subgoal
  
  P : Type
  Q : Type
  R : Type
  X : P
  X0 : P -> Q
  ============================
  R

intros P...

1つ以上の引数を指定した時, その個数だけ順に前件を仮定に移動し, そのとき名前を引数で与える.

1 subgoal
  
  ============================
  forall P Q R : Type, P -> (P -> Q) -> R

ex <   intros P Q.
1 subgoal
  
  P : Type
  Q : Type
  ============================
  forall R : Type, P -> (P -> Q) -> R

intro

ちょうど一つだけを移動する intros. 引数を与えない場合名前は適当に付けられる. ちょうど一つの引数を与える場合はそれが名前に使われる.

move =>

1つ以上の引数を必要とする intros に同じ. ssreflect のコマンド.

revert

仮定を一つ選んで, 前件に追加する.

1 subgoal
  
  P : Type
  Q : Type
  R : Type
  HP : P
  ============================
  (P -> Q) -> R

ex <   revert R.
1 subgoal
  
  P : Type
  Q : Type
  HP : P
  ============================
  forall R : Type, (P -> Q) -> R

move:

revert に同じ. ssreflect のコマンド.

選言の分解

left, right

帰結が \(P \lor Q\) のとき, この一方だけを選んで残す戦略.

これは \(P \lor Q\) を示すには \(P\) だけ（あるいは \(Q\) だけ）が示されれば良いことから.

Coq < Example left_is_true : 0 = 0 \/ 0 = 1.
1 subgoal

  ============================
  0 = 0 \/ 0 = 1

left_is_true < left.
1 subgoal

  ============================
  0 = 0

left_is_true < auto.
No more subgoals.

同値 iff の分解

split

Goal の帰結 \(P \iff Q\) を \(P \implies Q\) と \(Q \implies P\) とに分解する.

1 subgoal
  
  P, Q : Prop
  ============================
  P <-> Q

ex <   split.
2 subgoals
  
  P, Q : Prop
  ============================
  P -> Q

subgoal 2 is:
 Q -> P

注意としてこれは帰結にのみ適用され, 前件は勝手に全て仮定に動かされる.

intros

intros で紹介してない機能があり, 上述の split をしながら仮定に持っていくという機能がある.

Goal が \( ( P \iff Q ) \implies \dots \) のときに, intros [PQ QP] とすると, 前件 \( P \iff Q \) を split してからそれぞれを PQ QP という名前で仮定に移動する.

1 subgoal
  
  P, Q : Prop
  ============================
  P <-> Q -> Q <-> P

ex <   intros PQ.
(* ただの intros だと <-> のまま持ってくだけ *)
1 subgoal
  
  P, Q : Prop
  PQ : P <-> Q
  ============================
  Q <-> P

ex < Undo.
1 subgoal
  
  P, Q : Prop
  ============================
  P <-> Q -> Q <-> P

ex <   intros [PQ QP].
(* 同時に split もされる!! *)
1 subgoal
  
  P, Q : Prop
  PQ : P -> Q
  QP : Q -> P
  ============================
  Q <-> P

補題の導入

証明中に一時的に補題を導入することで証明自体が構造的になって楽になる.

assert

名前を付けて補題を主張する.

assert (LemmaName : LemmaProp).

新しい Goal としてこれを追加し, 今までの証明には LemmaName の名前で仮定として追加される.

1 subgoal
  
  n, m : nat
  ============================
  n = m

ex <   assert (Base : 0 = 0).
(* 補題の主張, その証明が goal に追加される *)
2 subgoals
  
  n, m : nat
  ============================
  0 = 0

subgoal 2 is:
 n = m

ex <   by done.
(* 証明完了. 仮定に追加された *)
1 subgoal
  
  n, m : nat
  Base : 0 = 0
  ============================
  n = m

have

assert と同様に,

have: LemmaProp.

の形式で補題を主張する. 新たに Goal としてこれが追加され, 他の証明には前件として追加される.

1 subgoal

  ============================
  1 = 1

ex < have: 0 = 0.
2 subgoals

  ============================
  0 = 0

subgoal 2 is:
 0 = 0 -> 1 = 1

= と == の言い換え

eqP
     : reflect (?x = ?y) (?x == ?y)

を move/ して使う.

1 subgoal
  
  n, m : nat
  ============================
  n = m -> n == m

ex <   move/eqP.
1 subgoal
  
  n, m : nat
  ============================
  n == m -> n == m

1 subgoal
  
  n, m : nat
  ============================
  n == m -> n = m

ex <   move/eqP.
1 subgoal
  
  n, m : nat
  ============================
  n = m -> n = m

存在量化子

仮定の存在量化子を消去する

仮定 H が \( \exists x, P(x) \) であるときに, destruct H をすると, H の代わりに新しく \( x \) という仮定と, \( P(x) \) という仮定が追加される.

1 subgoal
  
  n : nat
  H : exists m : nat, n = m
  ============================
  ...

ex <   destruct H.
1 subgoal
  
  n, x : nat
  H : n = x
  ============================
  ...

仮定に x と新しい H が追加された.

Goal の存在量化子を消去する

Goal が \( \exists x, P(x) \) という形をしている場合, そして具体的に \(P(x)\) を満たす \(x\) の値が分かっている場合は, exists コマンドでその値を代入することが出来る.

1 subgoal
  
  n : nat
  ============================
  exists m : nat, m - 1 = n

ex <   exists (n + 1).
1 subgoal
  
  n : nat
  ============================
  n + 1 - 1 = n

m に (n+1) が代入された. 証明はこの代入された後の式について続いて行われるので注意.