タクティクリファレンス: 帰納法と場合分け

`fix` タクティク

fix タクティクは低レベルの帰納法を行うタクティクである。一般的には、後述の induction や elim タクティクを用いて帰納法を実行する方が分かりやすいが、これらのタクティクでは扱えない複雑な命題を証明する際には fix タクティクが役に立つかもしれない。

fix ident num

現在のゴールにおける num 番目の仮定に対して帰納法を行う。帰納法の仮定が ident という名前で追加される。fix タクティクを使った後は必ず num で指定した仮定を intro しなければならない。

Coq < Goal forall n : nat, 0 <= n.
1 subgoal

  ============================
   forall n : nat, 0 <= n

Unnamed_thm < fix IH 1; intro n.
1 subgoal

  IH : forall n : nat, 0 <= n
  n : nat
  ============================
   0 <= n

Unnamed_thm < destruct n as [ | n' ].
2 subgoals

  IH : forall n : nat, 0 <= n
  ============================
   0 <= 0

subgoal 2 is:
 0 <= S n'

Unnamed_thm < apply le_n.
1 subgoal

  IH : forall n : nat, 0 <= n
  n' : nat
  ============================
   0 <= S n'

Unnamed_thm < apply le_S, IH.
Proof completed.

上の例では、fix IH 1; intro n は実質的に refine (fix IH (n : nat) {struct n} := _) に等しい。

帰納法の仮定は無条件に使えるわけではなく、構文的により小さな値に対してしか使えない。上の例では、自然数 n に対して帰納法を用いているので、n に対する場合分けで得られた n' に対して帰納法の仮定を使うことができる。もし n そのものに対して帰納法の仮定を使うと、証明を検証する際にエラーとなる。

Unnamed_thm < fix IH 1; intro n.
1 subgoal

  IH : forall n : nat, 0 <= n
  n : nat
  ============================
   0 <= n

Unnamed_thm < apply (IH n).
Proof completed.

Unnamed_thm < Qed.
fix IH 1; intro n.
apply (IH n).

Error:
Recursive definition of IH is ill-formed.
In environment
IH : forall n : nat, 0 <= n
n : nat
Recursive call to IH has principal argument equal to
"n"
instead of a subterm of n.

このエラーは証明の最後に Qed (または Defined などの) コマンドによって証明を検証するときに初めて検査されるので、これに気付かずに複雑で時間のかかる証明を進めてしまうと悲惨である。Guarded コマンドを使って、帰納法の仮定の使い方があっているかどうかを証明の途中で適宜確かめるとよい。

Unnamed_thm < fix IH 1; intro n.
1 subgoal

  IH : forall n : nat, 0 <= n
  n : nat
  ============================
   0 <= n

Unnamed_thm < apply IH.
Proof completed.

Unnamed_thm < Guarded.
Error:
Recursive definition of IH is ill-formed.
In environment
IH : forall n : nat, 0 <= n
n : nat
Recursive call to IH has principal argument equal to
"n"
instead of a subterm of n.

fix num

fix ident num に同じだが、帰納法の仮定の名前 ident を処理系が自動的に選ぶ。選ばれる名前は常に同じとは限らないので、名前に依存した証明を書く場合には使わないこと。

fix ident₁ num₁ with (ident₂ params₂ {struct param₂} : type₂) … (ident_n params_n {struct param_n} : type_n)

相互再帰的な帰納法による証明を行う。

`cofix` タクティク

cofix タクティクは fix タクティクに似ているが、帰納法ではなく余帰納法による証明を行う。

cofix ident
cofix ident with (ident₂ params₂ : type₂) … (ident_n params_n : type_n): 余帰納法の仮定として ident を導入する。余帰納法の仮定は無条件に使えるのではなく、余帰納的に定義されたデータ型のコンストラクタの引数としてしか使えない。fix タクティクを使う場合と同様に、Guarded コマンドで余帰納法の仮定の使い方があっているかどうかを証明の途中で確かめるとよい。
cofix: cofix ident に同じだが、余帰納法の仮定の名前 ident を処理系が自動的に選ぶ。選ばれる名前は常に同じとは限らないので、名前に依存した証明を書く場合には使わないこと。

`elim` タクティク

elim は帰納法による証明を行うための基本的なタクティクである。ただし、帰納法の対象となる型が再帰的に定義されたものではない場合、elim は case と実質的に等しくなる。

elim term

帰納的に定義された型を持つ項 term に対応する、帰納法を行うための関数を適用する。

Coq < Goal forall n : nat, 0 <= n.
1 subgoal

  ============================
   forall n : nat, 0 <= n

Unnamed_thm < intro n; elim n.
2 subgoals

  n : nat
  ============================
   0 <= 0

subgoal 2 is:
 forall n0 : nat, 0 <= n0 -> 0 <= S n0

Unnamed_thm < apply le_n.
1 subgoal

  n : nat
  ============================
   forall n0 : nat, 0 <= n0 -> 0 <= S n0

Unnamed_thm < apply le_S.
Proof completed.

この例で elim n がやっていることは、refine (nat_ind (fun n => 0 <= n) _ _ n) に等しい。すなわち、項 n の型 nat に対応する帰納法の関数 nat_ind を、現在のゴールと項 n に適用しているのである。これにより、「n が 0 の場合にゴールが成り立つこと」と「n が n0 の場合にゴールが成り立つならば n が S n0 の場合にも成り立つこと」の二つがサブゴールとして残る。

elim に与える項は前提を表す識別子に限られず、対応する帰納法の関数を持つ任意の項を与えることができる。

Coq < Goal forall n : nat, 0 <= S n.
1 subgoal

  ============================
   forall n : nat, 0 <= S n

Unnamed_thm < intro n; elim (S n).
2 subgoals

  n : nat
  ============================
   0 <= 0

subgoal 2 is:
 forall n0 : nat, 0 <= n0 -> 0 <= S n0

この例で生成されているサブゴールは、「S n が 0 の場合にゴールが成り立つこと」と「S n が n0 の場合にゴールが成り立つならば S n が S n0 の場合にも成り立つこと」である。

elim はゴールに現れる term を置換するが、前提に現れる term は置換しない。よって、elim の前に intros しすぎる (あるいはし足りない) とうまくいかないことがある。

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

  ============================
   forall m n p : nat, p + m <= n -> m <= n

Unnamed_thm < intros m n p H; elim p.
2 subgoals

  m : nat
  n : nat
  p : nat
  H : p + m <= n
  ============================
   m <= n

subgoal 2 is:
 nat -> m <= n -> m <= n

Unnamed_thm < Restart.
1 subgoal

  ============================
   forall m n p : nat, p + m <= n -> m <= n

Unnamed_thm < intros m n p; elim p.
2 subgoals

  m : nat
  n : nat
  p : nat
  ============================
   0 + m <= n -> m <= n

subgoal 2 is:
 forall n0 : nat, (n0 + m <= n -> m <= n) -> S n0 + m <= n -> m <= n

Unnamed_thm < simpl plus; trivial.
1 subgoal

  m : nat
  n : nat
  p : nat
  ============================
   forall n0 : nat, (n0 + m <= n -> m <= n) -> S n0 + m <= n -> m <= n

elim term with …

term が関数であって、帰納法を適用可能なデータ型を得るために引数が必要な場合に、その引数を指定する。apply … with … の例を参照。

elim term using term₂

デフォルトの帰納法の関数の代わりに term₂ を適用する。

elim term using term₂ with …

term₂ を適用するにあたって推論できない引数があるとき、それを with で明示的に与える。apply … with … の例を参照。

elim … with … using … with …

elim タクティクの最も一般的な形。

elim … as … (Coq 8.3 以降)

elim … in … (Coq 8.3 以降)

elim … as … in … (Coq 8.3 以降)

elim … with … as … using … in … (Coq 8.3 以降)

induction … with … as … using … in … に同じ。

`induction` タクティク

induction タクティクは帰納法による証明を行うタクティクである。ただし、帰納法の対象となる型が再帰的に定義されたものではない場合、induction は destruct と実質的に等しくなる。

induction term

帰納的に定義された型を持つ項 term に対応する、帰納法を行うための関数を適用する。elim term との違いは、

ゴールだけでなく前提の中に現れる term もデフォルトで置換する。
帰納法を適用する前に必要ならば自動的に intros する。
帰納法の仮定は自動的に intros される。
term が前提名ならば自動的に clear される。

as によって前提名を指定しないで induction を使うと、処理系によって自動的に前提名が生成される。生成される前提名は常に同じとは限らないので、前提名に依存した証明を書く場合は以下の as を用いる構文を使うこと。

induction term as intropattern

自動的に intros される前提名を指定して induction する。前提名の指定の仕方は intros に準ずる。

Coq < Goal forall n : nat, 0 <= n.
1 subgoal

  ============================
   forall n : nat, 0 <= n

Unnamed_thm < induction n as [ | n' IH ].
2 subgoals

  ============================
   0 <= 0

subgoal 2 is:
 0 <= S n'

Unnamed_thm < apply le_n.
1 subgoal

  n' : nat
  IH : 0 <= n'
  ============================
   0 <= S n'

Unnamed_thm < apply le_S, IH.
Proof completed.

induction term with …

term が関数であって、帰納法を適用可能なデータ型を得るために引数が必要な場合に、その引数を指定する。apply … with … の例を参照。

induction term using term₂

デフォルトの帰納法の関数の代わりに term₂ を適用する。

induction term using term₂ with …

term₂ を適用するにあたって推論できない引数があるとき、それを with で明示的に与える。apply … with … の例を参照。

induction term in occurence

前提やゴールに含まれる term の内どれを置換するかを occurence で指定する。occurence の指定の仕方は pattern タクティクを参照。

induction … with … as … using … with … in …

induction タクティクの最も一般的な形。

simple induction ident

intros until ident; elim ident に同じ。

`case` タクティク

case は代数的データ型に対して場合分けを行うための基本的なタクティクである。

case term

代数的データ型を持つ項 term に対する場合分けを行う。動作は elim term に似ているが、帰納法の仮定は生成されず、term の型のコンストラクタの引数だけが生成される。

Coq < Goal forall b : bool, b = true \/ b = false.
1 subgoal

  ============================
   forall b : bool, b = true \/ b = false

Unnamed_thm < intro b; case b.
2 subgoals

  b : bool
  ============================
   true = true \/ true = false

subgoal 2 is:
 false = true \/ false = false

Unnamed_thm < left; reflexivity.
1 subgoal

  b : bool
  ============================
   false = true \/ false = false

Unnamed_thm < right; reflexivity.
Proof completed.

上の例では、case b は実質的に refine (match b with true => _ | false => _ end) に等しい。

Coq < Goal forall P Q : Prop, P /\ Q -> P.
1 subgoal

  ============================
   forall P Q : Prop, P /\ Q -> P

Unnamed_thm < intros P Q H; case H.
1 subgoal

  P : Prop
  Q : Prop
  H : P /\ Q
  ============================
   P -> Q -> P

Unnamed_thm < intros H' H''; apply H'.
Proof completed.

この例では、case H は実質的に refine (match H with conj A B => _ A B end) に等しい。

case term with …

term が関数であって、代数的データ型を得るために引数が必要な場合に、その引数を指定する。apply … with … の例を参照。

case … as … (Coq 8.3 以降)

case … in … (Coq 8.3 以降)

case … as … in … (Coq 8.3 以降)

case … with … as … in … (Coq 8.3 以降)

destruct … with … as … in … に同じ。

`case_eq` タクティク

Coq 8.1β 以降で使える。

case_eq term

case term に似ているが、場合分けする値に関する等式を仮定に追加する。これにより、ゴールの中で置き換えられる term の値を場合分けの後まで覚えておくことができる。

以下の例では定理 xorb_move_l_r_1 をその仮定に適用している。

Coq < Require Import Coq.Bool.Bool.

Coq < Check xorb_move_l_r_1.
xorb_move_l_r_1
     : forall b b' b'' : bool, xorb b b' = b'' -> b' = xorb b b''

Coq < Goal forall a b : bool,
Coq <  if (xorb a b) then (b = xorb a (xorb a b)) else (b = xorb a (xorb a b)).
1 subgoal

  ============================
   forall a b : bool,
   if xorb a b then b = xorb a (xorb a b) else b = xorb a (xorb a b)

Unnamed_thm < intros a b.
1 subgoal

  a : bool
  b : bool
  ============================
   if xorb a b then b = xorb a (xorb a b) else b = xorb a (xorb a b)

Unnamed_thm < case (xorb a b).
2 subgoals

  a : bool
  b : bool
  ============================
   b = xorb a true

subgoal 2 is:
 b = xorb a false

Unnamed_thm < Undo.  (* case ではうまくいかない! *)
1 subgoal

  a : bool
  b : bool
  ============================
   if xorb a b then b = xorb a (xorb a b) else b = xorb a (xorb a b)

Unnamed_thm < case_eq (xorb a b).
2 subgoals

  a : bool
  b : bool
  ============================
   xorb a b = true -> b = xorb a true

subgoal 2 is:
 xorb a b = false -> b = xorb a false

Unnamed_thm < apply xorb_move_l_r_1.
1 subgoal

  a : bool
  b : bool
  ============================
   xorb a b = false -> b = xorb a false

Unnamed_thm < apply xorb_move_l_r_1.
Proof completed.

この例で case_eq (xorb a b) がしていることは、generalize (refl_equal (xorb a b)); pattern (xorb a b) at - 1; case (xorb a b) に等しい。

`destruct` タクティク

destruct タクティクは場合分けを行うタクティクである。

destruct term

代数的データ型を持つ項 term に対する場合分けを行う。動作は induction term に似ているが、帰納法の仮定は生成されず、term の型のコンストラクタの引数だけが前提に加えられる。case term との違いは、

ゴールだけでなく前提の中に現れる term もデフォルトで置換する。
場合分けをする前に必要ならば自動的に intros する。
場合分けで得られるコンストラクタの引数は自動的に intros される。
term が前提名ならば自動的に clear される。

Coq < Goal forall b : bool, b = true \/ b = false.
1 subgoal

  ============================
   forall b : bool, b = true \/ b = false

Unnamed_thm < destruct b.
2 subgoals

  ============================
   true = true \/ true = false

subgoal 2 is:
 false = true \/ false = false

Unnamed_thm < left; reflexivity.
1 subgoal

  ============================
   false = true \/ false = false

Unnamed_thm < right; reflexivity.
Proof completed.

as によって前提名を指定しないで destruct を使うと、処理系によって自動的に前提名が生成される。生成される前提名は常に同じとは限らないので、前提名に依存した証明を書く場合は以下の as を用いる構文を使うこと。

destruct term as intropattern

自動的に intros される前提名を指定して destruct する。前提名の指定の仕方は intros に準ずる。

Coq < Goal forall P Q : Prop, P \/ Q -> Q \/ P.
1 subgoal

  ============================
   forall P Q : Prop, P \/ Q -> Q \/ P

Unnamed_thm < destruct 1 as [ H | H ].
2 subgoals

  P : Prop
  Q : Prop
  H : P
  ============================
   Q \/ P

subgoal 2 is:
 Q \/ P

Unnamed_thm < right; apply H.
1 subgoal

  P : Prop
  Q : Prop
  H : Q
  ============================
   Q \/ P

Unnamed_thm < left; apply H.
Proof completed.

上の例では、destruct 1 as [ H | H ] は実質的に intros P Q X; case X; clear X; [ intro H | intro H ] に等しい。なお、ここでの 1 は、関数型のゴールにおける一つ目の非依存的引数すなわち P \/ Q を指している (詳しくは intros until … を参照)。

destruct term as intropattern _eqn

destruct term as intropattern _eqn:ident

case_eq と同様に、場合分けする値に関する等式を前提に追加する。ident でその名前を指定する。

Coq < Require Import Coq.Bool.Bool.

Coq < Check xorb_move_l_r_1.
xorb_move_l_r_1
     : forall b b' b'' : bool, xorb b b' = b'' -> b' = xorb b b''

Coq < Goal forall a b : bool,
Coq <  if (xorb a b) then (b = xorb a (xorb a b)) else (b = xorb a (xorb a b)).
1 subgoal

  ============================
   forall a b : bool,
   if xorb a b then b = xorb a (xorb a b) else b = xorb a (xorb a b)

Unnamed_thm < intros a b; destruct (xorb a b) as [] _eqn: Heq.
2 subgoals

  a : bool
  b : bool
  Heq : xorb a b = true
  ============================
   b = xorb a true

subgoal 2 is:
 b = xorb a false

Unnamed_thm < apply xorb_move_l_r_1; apply Heq.
1 subgoal

  a : bool
  b : bool
  Heq : xorb a b = false
  ============================
   b = xorb a false

Unnamed_thm < apply xorb_move_l_r_1; apply Heq.
Proof completed.

destruct term with … (Coq 8.2 以降)

term が関数であって、帰納法を適用可能なデータ型を得るために引数が必要な場合に、その引数を指定する。apply … with … の例を参照。

destruct term using …

destruct term using … with … (Coq 8.2 以降)

induction term using … (with …) に同じ。すなわち、この場合 destruct は帰納法を実行することができる。

destruct term in occurence (Coq 8.2 以降)

前提やゴールに含まれる term の内どれを置換するかを occurence で指定する。occurence の指定の仕方は pattern タクティクを参照。

destruct … with … as … _eqn: … using … with … in …

destruct タクティクの各キーワードを使う最も一般的な形。

destruct …, …, … (Coq 8.3 以降)

カンマで区切った複数の destruct を順に行う。

simple destruct ident

intros until ident; case ident に同じ。

`intros` タクティク

intros タクティクは、依存積の型 (forall …, … または A -> B の形) を持つゴールに対して、引数部を前提に移動する。また、let 束縛の形 (let … := … in …) のゴールに対して、束縛を前提に移動する。

intros

repeat intros ? に同じ。追加される前提の名前は処理系によって自動的に選ばれることに注意。

intros ident

ゴールが依存積の型を持つ場合、その最初の引数の部分を ident という名前で前提に移動する。

Coq < Goal forall m n : nat, m <= m + n.
1 subgoal
  
  ============================
   forall m n : nat, m <= m + n

Unnamed_thm < intros k.
1 subgoal
  
  k : nat
  ============================
   forall n : nat, k <= k + n

ゴールが let 束縛の形の場合、束縛を定義とともに前提に移動する。

Coq < Goal let a := 1 + 2 in a = 3.
1 subgoal
  
  ============================
   let a := 1 + 2 in a = 3

Unnamed_thm < intros n.
1 subgoal
  
  n := 1 + 2 : nat
  ============================
   n = 3

intros ?ident (Coq 8.2 以降)

intros ? (Coq 8.1β 以降)

intros ident に同じ。ただし、名前が重複する場合は処理系が別な近い名前を自動的に選ぶ。ident を省略した場合も処理系が名前を選ぶ。処理系が選ぶ名前は常に同じとは限らないので、名前に依存した証明を書く場合には使わないこと。

intros _

ゴールの仮定を前提に追加する代わりに、消去する。

形式的には let H := fresh in intros H; clear H に等しい。

intros -> (Coq 8.1β 以降)

intros <- (Coq 8.1β 以降)

ゴールの仮定を前提として追加する代わりに、等式による書き換えを行う。仮定が等式の場合のみ使える。矢印は書き換えを行う方向を表す。

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

Unnamed_thm < intros m; intros n.
1 subgoal
  
  m : nat
  n : nat
  ============================
   m = n -> n = m

Unnamed_thm < intros ->.
1 subgoal
  
  n : nat
  ============================
   n = n

Unnamed_thm < reflexivity.
Proof completed.

この形の intros は、上記のより単純な形の intros や rewrite、clear との組み合わせにより実現される。上の例では、intros -> は実質的に intro H; rewrite -> H in * |- *; clear H m に等しい。

intros [ … | … | … ]

ゴールの仮定を前提に移動する代わりに場合分けを行い、その結果得られる新たな仮定に対して intros を適用する。仮定が代数的データ型の場合 (または代数的データ型を返す関数の型の場合) のみ使える。場合分けの数に応じて [ ] 内を | で区切り、それぞれに新たな仮定に対して行う intros の引数を指定する。

形式的には intros [ p₁₁ p₁₂… | p₂₁ p₂₂… | … ] は let H := fresh in intros H; case H; clear H; [ intros p₁₁ p₁₂… | intros p₂₁ p₂₂… | … ] に等しい。

Coq < Goal forall P Q : Prop, P \/ Q -> Q \/ P.
1 subgoal
  
  ============================
   forall P Q : Prop, P \/ Q -> Q \/ P

Unnamed_thm < intros P; intros Q.
1 subgoal
  
  P : Prop
  Q : Prop
  ============================
   P \/ Q -> Q \/ P

Unnamed_thm < intros [ H | H ].
2 subgoals
  
  P : Prop
  Q : Prop
  H : P
  ============================
   Q \/ P

subgoal 2 is:
 Q \/ P

Unnamed_thm < right; exact H.
1 subgoal
  
  P : Prop
  Q : Prop
  H : Q
  ============================
   Q \/ P

Unnamed_thm < left; exact H.
Proof completed.

場合分けの対象が代数的データ型を返す関数の場合は、関数の引数がサブゴールに追加される。

Coq < Goal forall P Q1 Q2 R : Prop,
Coq <      P -> (Q1 -> R) -> (Q2 -> R) -> (P -> Q1 \/ Q2) -> R.
1 subgoal
  
  ============================
   forall P Q1 Q2 R : Prop,
   P -> (Q1 -> R) -> (Q2 -> R) -> (P -> Q1 \/ Q2) -> R

Unnamed_thm < intros P Q1 Q2 R H1 H2 H3.
1 subgoal
  
  P : Prop
  Q1 : Prop
  Q2 : Prop
  R : Prop
  H1 : P
  H2 : Q1 -> R
  H3 : Q2 -> R
  ============================
   (P -> Q1 \/ Q2) -> R

Unnamed_thm < intros [ H4 | H4 ].
3 subgoals
  
  P : Prop
  Q1 : Prop
  Q2 : Prop
  R : Prop
  H1 : P
  H2 : Q1 -> R
  H3 : Q2 -> R
  ============================
   P

subgoal 2 is:
 R
subgoal 3 is:
 R

Unnamed_thm < exact H1.
2 subgoals
  
  P : Prop
  Q1 : Prop
  Q2 : Prop
  R : Prop
  H1 : P
  H2 : Q1 -> R
  H3 : Q2 -> R
  H4 : Q1
  ============================
   R

subgoal 2 is:
 R

Unnamed_thm < exact (H2 H4).
1 subgoal
  
  P : Prop
  Q1 : Prop
  Q2 : Prop
  R : Prop
  H1 : P
  H2 : Q1 -> R
  H3 : Q2 -> R
  H4 : Q2
  ============================
   R

Unnamed_thm < exact (H3 H4).
Proof completed.

intros (p₁, p₂, …)

intros [p₁ p₂ …] に同じ。

intros (p₁ & p₂ & …) (Coq 8.2 以降)

intros (p₁, (p₂, (…))) に同じ。

Coq < Goal forall P Q R : Prop, P /\ Q /\ R -> R /\ Q /\ P.
1 subgoal
  
  ============================
   forall P Q R : Prop, P /\ Q /\ R -> R /\ Q /\ P

Unnamed_thm < intros P; intros Q; intros R.
1 subgoal
  
  P : Prop
  Q : Prop
  R : Prop
  ============================
   P /\ Q /\ R -> R /\ Q /\ P

Unnamed_thm < intros (H1 & H2 & H3).
1 subgoal
  
  P : Prop
  Q : Prop
  R : Prop
  H1 : P
  H2 : Q
  H3 : R
  ============================
   R /\ Q /\ P

Unnamed_thm < repeat split; assumption.
Proof completed.

intros p₁ p₂…

複数の intros を一度に行う。おおよそ intros p₁; intros p₂; … に等しいが、複数の場合分けを一度に行った場合などの動作が異なる。

intros until ident

intros until num

名前 ident を持つゴールの仮定または num 番目の名前の無いゴールの仮定まで intros する。追加される前提名は処理系が自動的に選ぶので、前提名に依存した証明を書く際には使わないこと。

Coq < Goal forall P Q R : Prop, P /\ Q /\ R -> R /\ Q /\ P.
1 subgoal
  
  ============================
   forall P Q R : Prop, P /\ Q /\ R -> R /\ Q /\ P

Unnamed_thm < intros until R.
1 subgoal
  
  P : Prop
  Q : Prop
  R : Prop
  ============================
   P /\ Q /\ R -> R /\ Q /\ P

Coq < Goal forall P Q R : Prop, P /\ Q /\ R -> R /\ Q /\ P.
1 subgoal
  
  ============================
   forall P Q R : Prop, P /\ Q /\ R -> R /\ Q /\ P

Unnamed_thm < intros until 1.
1 subgoal
  
  P : Prop
  Q : Prop
  R : Prop
  H : P /\ Q /\ R
  ============================
   R /\ Q /\ P

`decompose` タクティク

decompose タクティクは代数的データ型を持つ項を分解して、結果を前提に追加する。前提名は処理系が自動的に選ぶので、前提名に依存した証明を書く場合は使わないこと。

decompose [ident₁ ident₂ …] term

項 term を分解して、前提に追加する。分解は型 ident₁, ident₂, … に対して行われる。

Coq < Goal forall m : nat, (exists n : nat, m <= n) -> exists n : nat, S m <= n.
1 subgoal
  
  ============================
   forall m : nat, (exists n : nat, m <= n) -> exists n : nat, S m <= n

Unnamed_thm < intros m H.
1 subgoal
  
  m : nat
  H : exists n : nat, m <= n
  ============================
   exists n : nat, S m <= n

Unnamed_thm < decompose [ex] H.
1 subgoal
  
  m : nat
  H : exists n : nat, m <= n
  x : nat
  H0 : m <= x
  ============================
   exists n : nat, S m <= n

Coq < Goal forall P Q R : Prop, P /\ Q \/ Q /\ R -> Q.
1 subgoal
  
  ============================
   forall P Q R : Prop, P /\ Q \/ Q /\ R -> Q

Unnamed_thm < intros P Q R H.
1 subgoal
  
  P : Prop
  Q : Prop
  R : Prop
  H : P /\ Q \/ Q /\ R
  ============================
   Q

Unnamed_thm < decompose [and or] H; assumption.
Proof completed.

decompose sum term

項 term を和型 (or など) について分解して、前提に追加する。

decompose record term

項 term をレコード型 (and や exists など、コンストラクタが一つしかない型) について分解して、前提に追加する。

`inversion` タクティク

inversion タクティクは、case タクティクや destruct タクティクのように代数的データ型に対する場合分けを行うが、コンストラクタの引数に関する条件を保存する。

特定の値に関する条件を表す述語が代数的データ型として定義してあり、そのような述語が実際に前提として得られている場合に、その述語から具体的な値に関する条件を取り出すのに使う。

Coq < Print le.
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

Coq < Goal forall n : nat, n <= 0 -> n = 0.
1 subgoal
  
  ============================
   forall n : nat, n <= 0 -> n = 0

Unnamed_thm < intros n H.
1 subgoal
  
  n : nat
  H : n <= 0
  ============================
   n = 0

Unnamed_thm < inversion H as [ H' | ].
1 subgoal
  
  n : nat
  H : n <= 0
  H' : n = 0
  ============================
   0 = 0

Unnamed_thm < reflexivity.
Proof completed.

上の例では、前提 H : n <= 0 から条件 n = 0 を取り出すために inversion を用いている。述語 le には二つのコンストラクタがあるが、le_S から作ることのできる条件の型 n <= S m は前提 H の型 n <= 0 に適合しないため、この場合は自動的に除外される。le_n の型 n <= n と H の型 n <= 0 とを照らし合わせた結果として条件 n = 0 が前提に追加され、この等式を利用して自動的にゴールの n が 0 に書き換えられる。

inversion ident

前提 ident に対して inversion を適用し、得られる条件を前提に追加する。指定した前提が存在しない場合は、先に intros until ident を試みる。

as によって前提名を指定しないで inversion を使うと、処理系によって自動的に前提名が生成される。生成される前提名は常に同じとは限らないので、前提名に依存した証明を書く場合は以下の as を用いる構文を使うこと。

inversion num

intros until num を行い、最後に追加された前提に対して inversion を適用する。

inversion … as intropattern

追加される前提の名前を指定して inversion する。名前の指定のしかたは destruct … as … と似ているが、inversion が取り出した条件 (等式) の名前も追加で指定する必要がある。条件の名前の指定は injection … as … に準ずる。名前が足りない場合は処理系が自動的に名前を選ぶので注意。

Coq < Require Import Coq.Lists.List.

Coq < Inductive list_in {A : Type} : A -> list A -> Prop :=
Coq < | in_hd : forall a l, list_in a (a :: l)
Coq < | in_tl : forall a b l, list_in a l -> list_in a (b :: l).
list_in is defined
list_in_ind is defined

Coq < Goal forall l, list_in 0 (1 :: l) -> list_in 0 l.
1 subgoal
  
  ============================
   forall l : list nat, list_in 0 (1 :: l) -> list_in 0 l

Unnamed_thm < inversion 1 as [ | a b l' H' H1 [H2 H3] ].
1 subgoal
  
  l : list nat
  H : list_in 0 (1 :: l)
  a : nat
  b : nat
  l' : list nat
  H' : list_in 0 l
  H1 : a = 0
  H2 : b = 1
  H3 : l' = l
  ============================
   list_in 0 l

Unnamed_thm < exact H'.
Proof completed.

上の例では、述語 list_in の二つのコンストラクタのうち in_hd の場合については条件が合わずに自動的に除外されるので名前を指定していない。in_tl の場合の名前の指定は、まず a, b, l', H' の四つがそれぞれ in_tl の四つの引数に対応しており (ここまでは destruct と同じ)、その後の H1 と [H2 H3] はそれぞれ list_in の二つの引数 (A 型と list A 型) に対応して得られる二つの条件 a = 0 と b :: l' = 1 :: l に対応している。後者は自動的に適用される injection により b = 1 と l' = l とに分解されるため、それに合わせて H2 と H3 の二つの名前を指定している。

inversion … in ident₁ … ident_n

ゴールだけでなく前提 ident₁ … ident_n においても、得られた条件に基づいた書き換えを行う。

inversion … as … in …

inversion タクティクの最も一般的な形。

inversion_clear ident

inversion_clear ident as …

inversion_clear ident in …

inversion_clear ident as … in …

inversion した後に、ident および不要な条件等を自動的に前提から消去する。

inversion ident₁ using ident₂

inversion ident₁ using ident₂ in …

Derive Inversion コマンドで作成した補題 ident₂ を使用して inversion ident₁ を行う。

Coq < Derive Inversion le_0_inv with (forall n, n <= 0) Sort Prop.

Coq < Check le_0_inv.
le_0_inv
     : forall (n : nat) (P : nat -> Prop),
       (n <= 0 -> n = 0 -> P 0) -> n <= 0 -> P n

Coq < Goal forall n, n <= 0 -> n = 0.
1 subgoal
  
  ============================
   forall n : nat, n <= 0 -> n = 0

Unnamed_thm < intros n H.
1 subgoal
  
  n : nat
  H : n <= 0
  ============================
   n = 0

Unnamed_thm < inversion H using le_0_inv.
1 subgoal
  
  n : nat
  H : n <= 0
  ============================
   n <= 0 -> n = 0 -> 0 = 0

Unnamed_thm < reflexivity.
Proof completed.

この例で inversion H using le_0_inv がしていることは、pattern n; apply le_0_inv, H に等しい。

Derive Inversion コマンドの亜種として、Derive Inversion_clear, Derive Dependent Inversion, Derive Dependent Inversion_clear コマンドがある。

dependent inversion ident

dependent inversion ident as …

dependent inversion ident with …

dependent inversion ident as … with …

dependent inversion_clear ident

dependent inversion_clear ident as …

dependent inversion_clear ident with …

dependent inversion_clear ident as … with …

ident 自体がゴールの型に含まれる場合に使う。通常の inversion/inversion_clear の処理をする他に、ゴールの型に含まれる ident を実際に場合分けされた値に置換する。

simple inversion ident

simple inversion num

より単純な inversion を行う。すなわち、場合分けの際に条件が噛み合わない場合を除外したり、得られた条件を元にゴールを書き換えたりしない。追加される前提名は処理系が自動的に選ぶので、前提名に依存した証明を書く際には使わないこと。

タクティクリファレンス: 帰納法と場合分け

fix タクティク

cofix タクティク

elim タクティク

induction タクティク

case タクティク

case_eq タクティク

destruct タクティク

intros タクティク

decompose タクティク

inversion タクティク

`fix` タクティク

`cofix` タクティク

`elim` タクティク

`induction` タクティク

`case` タクティク

`case_eq` タクティク

`destruct` タクティク

`intros` タクティク

`decompose` タクティク

`inversion` タクティク