証明事例集: 自前で inversion を行う

ここでは、組み込みの inversion タクティクを使わずに自前で inversion 相当の手続きを行うやり方を、いくつかの例を通じて紹介する。

単純な例: even

自然数が偶数であることを表す述語 even を以下のように定義する。

Inductive even : nat -> Prop :=
  | even_O : even O
  | even_SS : forall n, even n -> even (S (S n))

この述語を使って 1 が偶数でないことを表し、inversion を使ってそれを証明してみよう。

まず、組み込みの inversion タクティクを使って証明する例を挙げる。

Coq < Goal ~ even 1.
1 subgoal
  
  ============================
   ~ even 1

Unnamed_thm < intro H.
1 subgoal
  
  H : even 1
  ============================
   False

Unnamed_thm < inversion H.
Proof completed.

even 1 には even_O と even_SS のどちらも当てはまらないため、inversion を使うと直ちに証明が完了する。

では、組み込みの inversion タクティクを使わない場合はどうするか。以下のように単純に case H をしただけでは、even の引数が 1 であることが場合分けの後に忘れられてしまうので、False を導くための条件が揃わない。実際、case H した後の一つ目のサブゴールは case H をする前と全く変わっていない。

Coq < Goal ~ even 1.
1 subgoal
  
  ============================
   ~ even 1

Unnamed_thm < intro H.
1 subgoal
  
  H : even 1
  ============================
   False

Unnamed_thm < case H.
2 subgoals
  
  H : even 1
  ============================
   False

subgoal 2 is:
 forall n : nat, even n -> False

even の引数が 1 であることを場合分けの後まで覚えておきたいので、ゴールに等式を追加し、等式の片方の辺だけを場合分けで書き換えるようにする。すると場合分けの後に矛盾を導くことのできる条件 (等式) が残る。

Coq < Goal ~ even 1.
1 subgoal
  
  ============================
   ~ even 1

Unnamed_thm < intro H.
1 subgoal
  
  H : even 1
  ============================
   False

Unnamed_thm < generalize (refl_equal 1).
1 subgoal
  
  H : even 1
  ============================
   1 = 1 -> False

Unnamed_thm < pattern 1 at 2.
1 subgoal
  
  H : even 1
  ============================
   (fun n : nat => 1 = n -> False) 1

Unnamed_thm < case H.
2 subgoals
  
  H : even 1
  ============================
   1 = 0 -> False

subgoal 2 is:
 forall n : nat, even n -> 1 = S (S n) -> False

Unnamed_thm < intros; discriminate.
1 subgoal
  
  H : even 1
  ============================
   forall n : nat, even n -> 1 = S (S n) -> False

Unnamed_thm < intros; discriminate.
Proof completed.

pattern によって等式の片方の辺だけを取り出しておくことで、case H に等式の片方の辺だけを書き換えさせることができる。なお、上の例の pattern 1 at 2; case H は以下の refine タクティクにほぼ等しい。

refine (match H in (even n) return (1 = n -> False) with
        | even_O => _
        | even_SS n' H' => _
        end)

今度は、S (S n) が偶数ならば n も偶数であることを示そう。自前 inversion のやり方は上の例と同じ。

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

Unnamed_thm < intros n H.
1 subgoal
  
  n : nat
  H : even (S (S n))
  ============================
   even n

Unnamed_thm < generalize (refl_equal (S (S n))).
1 subgoal
  
  n : nat
  H : even (S (S n))
  ============================
   S (S n) = S (S n) -> even n

Unnamed_thm < pattern (S (S n)) at 2.
1 subgoal
  
  n : nat
  H : even (S (S n))
  ============================
   (fun n0 : nat => S (S n) = n0 -> even n) (S (S n))

Unnamed_thm < case H.
2 subgoals
  
  n : nat
  H : even (S (S n))
  ============================
   S (S n) = 0 -> even n

subgoal 2 is:
 forall n0 : nat, even n0 -> S (S n) = S (S n0) -> even n

Unnamed_thm < intros; discriminate.
1 subgoal
  
  n : nat
  H : even (S (S n))
  ============================
   forall n0 : nat, even n0 -> S (S n) = S (S n0) -> even n

Unnamed_thm < intros n' H' Heq.
1 subgoal
  
  n : nat
  H : even (S (S n))
  n' : nat
  H' : even n'
  Heq : S (S n) = S (S n')
  ============================
   even n

Unnamed_thm < injection Heq as Heq'.
1 subgoal
  
  n : nat
  H : even (S (S n))
  n' : nat
  H' : even n'
  Heq : S (S n) = S (S n')
  Heq' : n = n'
  ============================
   even n

Unnamed_thm < rewrite Heq'; exact H'.
Proof completed.

複数の引数を取る述語: succ

場合分けをする述語が複数の引数を取る場合は、それに合わせて複数の等式をゴールに追加する必要がある。ここでは、二つの自然数の後者関係を表す述語 succ を定義し、任意の自然数は自分自身の後者ではないことを示そう。

Inductive succ : nat -> nat -> Prop :=
  succ_intro : forall n, succ n (S n)

succ は二つの引数を取るので、それらに対応する二つの等式をゴールに追加してから case する。

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

Unnamed_thm < intros n H.
1 subgoal
  
  n : nat
  H : succ n n
  ============================
   False

Unnamed_thm < generalize (refl_equal n) (refl_equal n).
1 subgoal
  
  n : nat
  H : succ n n
  ============================
   n = n -> n = n -> False

Unnamed_thm < pattern n at 2, n at 4.
1 subgoal
  
  n : nat
  H : succ n n
  ============================
   (fun n0 n1 : nat => n = n0 -> n = n1 -> False) n n

Unnamed_thm < case H.
1 subgoal
  
  n : nat
  H : succ n n
  ============================
   forall n0 : nat, n = n0 -> n = S n0 -> False

Unnamed_thm < intros _ <- H'.
1 subgoal
  
  n : nat
  H : succ n n
  H' : n = S n
  ============================
   False

Unnamed_thm < exact (n_Sn n H').
Proof completed.

固定パラメータのある述語: le

ここでは自然数の大小関係を表す組み込みの述語 le に関する inversion を自前でやってみよう。le の定義は以下のようになっている。

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

le は二つの引数を受け取るように見えるが、実際には最初の引数は固定されたパラメータである。すなわち正確には、任意の自然数 n に対して le n が一つの引数を受け取ると考える必要がある。そのため、inversion では最初の引数 n に関する条件は得られず、最後の引数に関する条件だけが得られる。最後の引数に関する条件を場合分けの後まで覚えておくために、最後の引数に関する等式をゴールに追加してから場合分けを行う。

なぜ最初の引数に関する等式を追加してはいけないのかというと、もしそうすると pattern 後の case で正しく値が置き換えられないからである。

以下の例は、n <= 0 から n = 0 を導く証明である。

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 < generalize (refl_equal 0); pattern 0 at 2.
1 subgoal
  
  n : nat
  H : n <= 0
  ============================
   (fun n0 : nat => 0 = n0 -> n = 0) 0

Unnamed_thm < case H.
2 subgoals
  
  n : nat
  H : n <= 0
  ============================
   0 = n -> n = 0

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

Unnamed_thm < congruence.
1 subgoal
  
  n : nat
  H : n <= 0
  ============================
   forall m : nat, n <= m -> 0 = S m -> n = 0

Unnamed_thm < intros; discriminate.
Proof completed.

Dependent inversion: vector その 1

vector は Coq.Bool.Bvector モジュールで定義されているリストデータ構造であり、以下のように定義されている。vector A n は、要素の型が A で要素数が n の単方向連結リストを表す型である。

Inductive vector (A : Type) : nat -> Type :=
  | Vnil : vector A 0
  | Vcons : A -> forall n : nat, vector A n -> vector A (S n)

これに対し、ある値があるリストに含まれているということを表す述語 vector_in を以下のように定義する。vector_in A a n v は型 A の値 a が要素数 n のリスト v に含まれていることを表す。

Inductive vector_in A : A -> forall n, vector A n -> Prop :=
  | vin_head :
      forall a n tl, vector_in A a (S n) (Vcons A a n tl)
  | vin_tail :
      forall a b n tl, vector_in A a n tl ->
      vector_in A a (S n) (Vcons A b n tl)

空でないリストを与えるとその最初の要素を取り出し、その要素が確かにそのリストに含まれているという証明とともに返す関数 first を定義しよう。

場合分けの対象となるリスト v の型に含まれている S n は、これまでの他の例と同様にゴールに等式を追加して場合分けの後まで値を覚えておく。さらにこの例の場合は、場合分けの対象 v そのものもゴールの型の中に含まれており、それを場合分けの結果で置換する必要がある (この様な操作は dependent inversion タクティクの動作に相当する)。generalize でゴールに等式を追加するところまではこれまでと同様だが、case タクティクでは S n と v をうまく同時に置換できないので、refine タクティクに match 式を指定して手動で型を指定する必要がある。

Coq < Definition first :
Coq <   forall A n (v : vector A (S n)), {a : A | vector_in A a (S n) v}.
1 subgoal
  
  ============================
   forall (A : Type) (n : nat) (v : vector A (S n)),
   {a : A | vector_in A a (S n) v}

first < intros A n v.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  ============================
   {a : A | vector_in A a (S n) v}

first < generalize (refl_equal (S n)).
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  ============================
   S n = S n -> {a : A | vector_in A a (S n) v}

first < refine (match v as vv in (vector _ nn)
first <         return (S n = nn -> {a : A | vector_in A a nn vv})
first <         with
first <         | Vnil => _
first <         | Vcons a' n' v' => _
first <         end).
2 subgoals
  
  A : Type
  n : nat
  v : vector A (S n)
  ============================
   S n = 0 -> {a : A | vector_in A a 0 (Vnil A)}

subgoal 2 is:
 S n = S n' -> {a : A | vector_in A a (S n') (Vcons A a' n' v')}

first < intros; discriminate.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  a' : A
  n' : nat
  v' : vector A n'
  ============================
   S n = S n' -> {a : A | vector_in A a (S n') (Vcons A a' n' v')}

first < intros H; injection H as H'; rewrite H' in v; clear H H'.
1 subgoal
  
  A : Type
  n : nat
  n' : nat
  v : vector A (S n')
  a' : A
  v' : vector A n'
  ============================
   {a : A | vector_in A a (S n') (Vcons A a' n' v')}

first < exists a.
1 subgoal
  
  A : Type
  n : nat
  n' : nat
  v : vector A (S n')
  a' : A
  v' : vector A n'
  ============================
   vector_in A a' (S n') (Vcons A a' n' v')

first < apply vin_head.
Proof completed.

refine (match … end) が何をしているか詳しく見てみよう。

refine (match v as vv in (vector _ nn)
        return (S n = nn -> {a : A | vector_in A a nn vv})
        with
        | Vnil => _
        | Vcons a' n' v' => _
        end)

この match 式では、v に対する場合分けを行っている。as vv により変数 vv が v の値に束縛される。また式 v の型は vector A (S n) なので、in (vector _ nn) により S n に対応する変数 nn が束縛される (A は固定されたパラメータなので in で束縛することはできない)。as と in で束縛された vv と nn は、直後の return 式内で使用することができる。return 式に示した型 (S n = nn -> {a : A | vector_in A a nn vv}) は、この match 式全体の型すなわち場合分けの後にそれぞれ導きたい値の型を表している。この型は元のゴールの型 (S n = S n -> {a : A | vector_in A a (S n) v}) と等しくなければならない。しかしこの例で行おうとしている場合分けでは、ゴールの型に含まれている S n と v を置き換えたい。それらに対応する変数として nn と vv を束縛したので、置き換えたい部分をこれらの変数に置き換えて return 式に指定している。

Dependent destruction: vector その 2

前の例では dependent inversion を自前で行った。ここでは空でないリストに対するより一般的な inversion を行おう。すなわち、空でないリストを与えると、それを先頭の要素と残りのリストに分解し、分解前のリストとの関係を示す等式の証明とともに返す関数 Vcons_inv を定義する。

今回の場合は、dependent inversion を使おうとすると以下のようにエラーとなる。

Coq < Definition Vcons_inv : forall A n (v : vector A (S n)),
Coq <   {a : A & {v' : vector A n | v = Vcons A a n v'}}.
1 subgoal
  
  ============================
   forall (A : Type) (n : nat) (v : vector A (S n)),
   {a : A &  {v' : vector A n | v = Vcons A a n v'}}

Vcons_inv < dependent inversion v.
Toplevel input, characters 0-21:
> dependent inversion v.
> ^^^^^^^^^^^^^^^^^^^^^
Error: Abstracting over the terms "S n" and "v" leads to a term
"fun (n0 : nat) (v : vector A n0) =>
 {a : A &  {v' : vector A n | v = Vcons A a n v'}}" which is ill-typed.

dependent inversion タクティクはゴールの型に含まれる n と v を書き換えようとするが、書き換え後に v = Vcons A a n v' の左辺が持つ型が vector A n0 であるのに対し右辺の型は vector A (S n) であるので、等式の型付けができなくなるのである。

dependent destruction タクティクは、両辺で型が異なる値の等式を表す述語 Coq.Logic.JMeq.JMeq を用いて式を書き換えることにより、このような型エラーを回避する。これを自前でやるとどのようになるか見てみよう。ポイントは、通常の等式 eq ではなく JMeq を generalize で導入する点である。場合分けの後二つ目のサブゴールでは、得られた等式 n = n' を利用して式を書き換えようとしているが、普通に rewrite タクティクを使おうとしてもうまくいかないので、いったん v' を前提からゴールに戻してから case タクティクで等式を分解する。JMeq を普通の等式に変換する際には公理 JMeq_eq が必要となる。

Coq < Definition Vcons_inv : forall A n (v : vector A (S n)),
Coq <   {a : A & {v' : vector A n | v = Vcons A a n v'}}.
1 subgoal
  
  ============================
   forall (A : Type) (n : nat) (v : vector A (S n)),
   {a : A &  {v' : vector A n | v = Vcons A a n v'}}

Vcons_inv < intros A n v.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  ============================
   {a : A &  {v' : vector A n | v = Vcons A a n v'}}

Vcons_inv < generalize (refl_equal (S n)) (JMeq_refl v).
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  ============================
   S n = S n -> JMeq v v -> {a : A &  {v' : vector A n | v = Vcons A a n v'}}

Vcons_inv < refine (match v as vv in (vector _ n')
Vcons_inv <         return (S n = n' -> JMeq v vv ->
Vcons_inv <           {a : A & {v' : vector A n | v = Vcons A a n v'}})
Vcons_inv <         with
Vcons_inv <         | Vnil => _
Vcons_inv <         | Vcons a' n' v' => _
Vcons_inv <         end).
2 subgoals
  
  A : Type
  n : nat
  v : vector A (S n)
  ============================
   S n = 0 ->
   JMeq v (Vnil A) -> {a : A &  {v' : vector A n | v = Vcons A a n v'}}

subgoal 2 is:
 S n = S n' ->
 JMeq v (Vcons A a' n' v') ->
 {a : A &  {v'0 : vector A n | v = Vcons A a n v'0}}

Vcons_inv < intros; discriminate.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  a' : A
  n' : nat
  v' : vector A n'
  ============================
   S n = S n' ->
   JMeq v (Vcons A a' n' v') ->
   {a : A &  {v'0 : vector A n | v = Vcons A a n v'0}}

Vcons_inv < intro Heq; injection Heq as Heq'; clear Heq.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  a' : A
  n' : nat
  v' : vector A n'
  Heq' : n = n'
  ============================
   JMeq v (Vcons A a' n' v') ->
   {a : A &  {v'0 : vector A n | v = Vcons A a n v'0}}

Vcons_inv < revert v'.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  a' : A
  n' : nat
  Heq' : n = n'
  ============================
   forall v' : vector A n',
   JMeq v (Vcons A a' n' v') ->
   {a : A &  {v'0 : vector A n | v = Vcons A a n v'0}}

Vcons_inv < case Heq'.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  a' : A
  n' : nat
  Heq' : n = n'
  ============================
   forall v' : vector A n,
   JMeq v (Vcons A a' n v') ->
   {a : A &  {v'0 : vector A n | v = Vcons A a n v'0}}

Vcons_inv < clear Heq'; intros v' Heq.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  a' : A
  n' : nat
  v' : vector A n
  Heq : JMeq v (Vcons A a' n v')
  ============================
   {a : A &  {v'0 : vector A n | v = Vcons A a n v'0}}

Vcons_inv < apply JMeq_eq in Heq.
1 subgoal
  
  A : Type
  n : nat
  v : vector A (S n)
  a' : A
  n' : nat
  v' : vector A n
  Heq : v = Vcons A a' n v'
  ============================
   {a : A &  {v'0 : vector A n | v = Vcons A a n v'0}}

Vcons_inv < exists a'; exists v'; exact Heq.
Proof completed.