停止性が明らかでない関数を定義するには

池渕未来
公開 2011/9/20

今までは主に Coq での証明の仕方について解説してきましたが、今回は証明についてではなく、Coq で再帰関数を定義することについて順を追って説明します。

3章 では Fixpoint で関数を定義しましたが、Fixpoint だと停止性が明らかな関数しか定義できませんでした。ここでは、Coq にとって停止性が明らかでないけれど確実に停止する関数をいくつか定義してみます。

二重再帰

少し複雑だけれど二つの再帰関数に分けると定義できる関数があります。この節ではその例としてアッカーマン関数とマージ関数を定義してみます。

アッカーマン関数

停止性の問題でよく例に出る、アッカーマン関数を Coq で定義します。

アッカーマン関数は二つの自然数を取って一つの自然数を返す、次のような関数です。

ack 0 n = S n

ack (S m) 0 = ack m 1

ack (S m) (S n) = ack m (ack (S m) n)

この関数は引数にどんな自然数を渡しても停止することが知られています。 これをそのまま Fixpoint で定義して読み込ませようとすると、

Fixpoint ack_bad (n m : nat) : nat :=
  match n with
  | O => S m
  | S n' =>
    match m with
    | O => ack_bad n' 1
    | S m' => ack_bad n' (ack_bad n m')
    end
  end.

Error: Cannot guess decreasing argument of fix.

とエラーが出ます。停止する関数なのに、Coq ではどうしてエラーになってしまうのでしょうか。

逆に、今までどういう関数が Fixpoint で定義されていたかを考えます。

例としてリストの結合 app と、自然数の加算 plus を見てみます。

Fixpoint app (A : Type)(l l' : list A) : list A :=
  match l with
  | nil => l'
  | x :: xs => x :: app A xs l'
  end.

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

どちらの関数も引数の一つをパターンマッチして、"x :: xs" や "S p" のパターンのときに再帰呼び出しをしています。そして、その呼び出しにおける引数には、xs や p など、元の "x :: xs" や "S p" より「小さい」値を渡しています。実はこれが関数が停止する鍵になっていて、呼び出しごとに引数が小さくなるのだから、いつかは nil や O になり、関数が停止するのです。

このように関数のいずれかの引数が再帰呼び出しごとに小さくなっていれば、Coq がその関数は停止すると判断するので Fixpoint コマンドで定義できます。

一方 ack はどうかというと、二回パターンマッチをしていたり再帰呼び出しの ack の引数に ack があったりしていて app や plus のように単純な再帰関数にはなっていなく、引数が小さくなっているかどうかはすぐには分かりません。そのため "Cannot guess decreasing argument of fix" というエラーが出たのです。

ack を定義するには、ack を下のように二つの単純な再帰関数に分けます。

Fixpoint ack' (f : nat -> nat)(m : nat) : nat :=
  match m with
  | O => f 1
  | S m' => f (ack' f m')
  end.

Fixpoint ack (n m : nat) : nat :=
  match n with
  | O => S m
  | S n' => ack' (ack n') m
  end.

先程エラーになった定義

Fixpoint ack_bad (n m : nat) : nat :=
  match n with
  | O => S m
  | S n' =>
    match m with
    | O => ack_bad n' 1
    | S m' => ack_bad n' (ack_bad n m')
    end
  end.

と比べると、"ack' (ack n') m" は ack_bad の二つ目のパターンマッチ部に相当していて、この二つの関数は同じ動作をすることが分かります。

そして ack' や ack は、app や plus のような単純な再帰になっており、さらに呼び出しごとに引数が小さくなっています。よってこのように ack を分けて定義すればエラーにならずに Coq でアッカーマン関数が定義できるようになるのです。

ack' は ack の中でしか使わない補助関数ですから、ack の中で局所的に定義したいと思う方もいるかもしれません。そこで局所的に ack' を定義して ack を書くと以下のようになります。

Fixpoint ack2 (n m : nat) : nat :=
  match n with
  | O => S m
  | S n' =>
    (fix ack2' (p : nat) : nat :=
      match p with
      | O => ack2 n' 1
      | S p' => ack n' (ack2' p')
      end
    ) m
  end.

fix という新しい構文が出てきました。fix は

fix 関数名 (引数1 : 型1)..(引数n : 型n) : 戻り値の型 := 定義

と使って局所的に(関数名)を定義できます。

fix で定義した ack2' は ack' (ack n') に対応していて、これで ack' を局所的に定義することができました。

マージ関数

Fixpoint の中で fix を使うと定義できる関数として、二つのリストをマージする関数があります。マージ関数は二つのリスト l1、l2 を受け取って、それぞれの順序を保ったままそれらを結合します。

マージ関数は以下のように定義できます。

Require Import List.
Require Import Arith.

Fixpoint merge (l1 l2 : list nat) :=
  match l1 with
  | nil => l2
  | x::xs =>
    (fix merge' l' :=
      match l' with
      | nil => l1
      | y::ys => if leb x y then x :: merge xs l' else y :: merge' ys
      end
    ) l2
  end.

if や leb はこれまで出て来なかったので、これから解説します。

上の関数は引数 l1、l2 の場合によって以下のように書けます。

merge nil l2 = l2

merge l1 nil = l1

merge (x::xs) (y::ys) = もし x <= y なら x :: merge xs (y :: ys)、そうでなければ y :: merge (x :: xs) ys

l1 と l2 の二つを場合分けしているところはアッカーマン関数と同じですが、今度は「もし〜ならば」と条件分岐が出てきています。

merge は、具体的に引数を渡すと次のように動作します。

Eval compute in  merge (4 :: 2 :: 6 :: nil) (3 :: 1 :: 5 :: 7 :: nil)

Result for command Eval compute in merge (4 :: 2 :: 6 :: nil) (3 :: 1 :: 5 :: 7 :: nil) . :
     = 3 :: 1 :: 4 :: 2 :: 5 :: 6 :: 7 :: nil
     : list nat

まず二つの引数の先頭、4 と 3 を比べて、3 の方が小さいので 3 を先頭に出します。次は 4 と、二つ目の引数の 1 を比べ、1 の方が小さいので 1 を 3 の後ろに置きます。その次は 4 と 5 を比べ、4 の方が小さいので 4 を 1 の後ろに置き、次は 2 と 5 を比べ……と続いていきます。

merge はこのようにリストの順序を保つので、下のようにもし二つの引数が両方ともソートされていたら、merge が返すリストもソートされています。

Eval compute in  merge (1 :: 4 :: 5 :: nil) (2 :: 3 :: 7 :: nil)

Result for command Eval compute in merge (1 :: 4 :: 5 :: nil) (2 :: 3 :: 7 :: nil) . :
      = 1 :: 2 :: 3 :: 4 :: 5 ::7 :: nil
      : list nat

条件分岐するプログラムを Coq で扱うために、ここで bool 型について説明します。

Coq では今まで命題の型を扱ってきましたが、それと別に bool 型が使えます。bool 型は Inductive コマンドを使って

Inductive bool : Set :=
  | true : bool
  | false : bool.

と定義されています。

bool 型の値を取って bool 型の値を返す基本的な関数は標準ライブラリで以下のように用意されています。

andb (b1 b2 : bool) --- b1 と b2 の論理積
orb (b1 b2 : bool) --- b1 と b2 の論理和
negb (b : bool) --- b の否定
implb (b1 b2 : bool) --- b1 が true なら b2、false なら true を返す
xorb (b1 b2 : bool) --- b1 と b2 の排他的論理和

andb b1 b2 は "b1 && b2"、orb b1 b2 は "b1 || b2" と表記しても使えます。implb の impl は imply の略で、今まで使ってきた -> に対応します。

今までは = や <= などは二つの値を取る型でしたが、Arith モジュールでは自然数に関して bool 型を返す関数として、

beq_nat (n m : nat) n = m なら true、そうでなければ false
leb (n m : nat) n <= m なら true、そうでなければ false

が用意されています。ここで、上のような関数が定義できるのは引数が nat に限っているからだということに注意してください。一般に、ある型に関してのイコールや順序を見て bool 型の値を返す関数が定義されるのは "a = b \/ a <> b" や "a <= b \/ ~ a <= b" が証明できるときのみです。これらは 6章 でも述べたようにすべての命題について成り立つとは限らず、成り立たないときは beq_nat や leb 相当の関数は定義できません。

もし "a = b \/ a <> b" が証明できないとすると、a = b か a <> b かどうか分からないときに true も false も返せなくなってしまいますね。nat に関しては "a = b \/ a <> b" が証明できるので、beq_nat が定義できるのです。

leb を使えば、leb n m が true のときと false のときとでパターンマッチすれば merge が定義できそうです。しかしここでは match を使わず、もっと簡潔に書ける if ... then ... else 表記を紹介します。

if ... then ... else は、

if 項 then 結果1 else 結果2

と書いて使い、項が bool 型なら項が true のとき結果1、false のとき結果2を返します。match で書き直すと

match 項 with
| true => 結果1
| false => 結果2
end.

と等しくなります。

merge の定義をもう一度書いてみます。

Require Import List.
Require Import Arith.

Fixpoint merge (l1 l2 : list nat) :=
  match l1 with
  | nil => l2
  | x::xs =>
    (fix merge' l' :=
      match l' with
      | nil => l1
      | y::ys => if leb x y then x :: merge xs l' else y :: merge' ys
      end
    ) l2
  end.

if ... then ... else で leb x y について場合分けしており、マージ関数になっています。

match で l1 と l2 を同時にパターンマッチしてシンプルに書くこともできます。

Fixpoint merge (l1 l2 : list nat) :=
  (fix merge' l' :=
    match l1, l' with
    | nil, _ => l'
    | _, nil => l1
    | x::xs, y::ys => if leb x y then x :: merge xs l' else y :: merge' ys
    end
  ) l2.

"_" はワイルドカードです。"match l1, l' with" と書くことによって l1 と l' の二つを同時にパターンマッチしています。

Function コマンド

リストや自然数についての関数の多くは Fixpoint コマンドで定義できますが、関数が複雑な動作をするようになるとできなくなる場合が出てきます。 Fixpoint や fix を使っても定義できない場合、別のコマンドを使うと定義できることがあります。この節ではその例としてマージソートを Coq で定義してみます。

マージソートは以下のような方法でリストをソートする関数です。

  1. リストを二分割する
  2. それぞれをソートする(マージソートを再帰的に呼び出す)
  3. ソートされた二つのリストをマージする

これを素直に Coq で実装するには補助関数としてリストを二分割する関数とマージ関数が必要になります。さらに、二分割したリストをペアで扱うために、直積型を使います。

Coq で直積型(型 A と B のペアの型)は "A * B" で表します。値 a と b のペアは (a, b) と書きます。

直積型を扱う主な関数として、(a, b) を受け取ったらそれぞれ a, b を返す関数 fst、snd があります。それぞれの型は fst : forall (A B : Type), A * B -> A と snd : forall (A B : Type), A * B -> B となっています。

マージ関数 merge は前の節で定義しました。それではリストを受け取ってそれを二分割し、リストのペアで返す関数 split を定義してみましょう。split は再帰呼び出しを使って、

Fixpoint split (l : list nat) : list nat * list nat :=
  match l with
  | nil => (nil, nil)
  | x::nil => (x :: nil, nil)
  | x::y::zs => (fun l' => (x :: fst l', y :: snd l')) (split zs)
  end.

と定義できます。今まで定義した関数と違って、split は一つの引数 l に対して三つの場合に分けてパターンマッチをしています。

Command Pane で Eval compute in コマンドを使って具体的な値を渡した結果を見てみましょう。

Eval compute in split (1 :: 2 :: 3 :: 4 :: 5 :: nil) 

Result for command Eval compute in split (1 :: 2 :: 3 :: 4 :: 5 :: nil) . :
     = (1 :: 3 :: 5 :: nil, 2 :: 4 :: nil)
          : list nat * list nat

このように split は リストの奇数番目と偶数番目とに分割します。

merge と split を使うとマージソートは、リストを三つの場合に分けて

msort nil        = nil
msort (x::nil)   = x :: nil
msort (x::y::zs) =
  (fun l' => merge (msort (fst l')) (msort (snd l'))) (split (x :: y :: zs))

と表せます。これは、再帰的に呼び出している msort の引数 l1、l2 がどちらも元の引数 x :: y :: zs より小さくなっているかが自明ではなく、Fixpoint で定義できません。しかし人間の頭で考えると msort に再帰的に渡しているのは元のリスト x :: y :: zs を二分割(split)したリストなので、リストの長さは短くなっていることが分かります。長さが 1 か 0 になれば msort は再帰呼び出しをしないので、Fixpoint で定義できなくても msort は確かに停止します。

Fixpoint で定義できない、停止する関数は Function というコマンドで定義します。Function コマンドを使うには新しく Recdef というモジュールをインポートしなければいけません。

Require Import Recdef.

msort は Function コマンドを使って以下のように定義できます。

Function msort (l : list nat) {measure length l} : list nat :=
  match l with
  | nil => nil
  | x::nil => x::nil
  | x::y::zs => (fun l' => merge (msort (fst l')) (msort (snd l'))) (split l)
  end.

Fixpoint とは違って "{measure length l}" が引数の後に続いています。これは msort の停止性の根拠として「再帰呼び出しごとに引数 l が length(長さ) に関して小さくなる」ことを Coq に教えています。実際にそうなっていることは自分で証明しなければいけません。上の定義CoqIDE に読み込ませると、関数を定義しようとしたのにウィンドウの右上の枠に証明図が現れます。

2 subgoals
______________________________________(1/2)
forall (l : list nat) (x : nat) (l0 : list nat) (y : nat) (zs : list nat),
l0 = y :: zs ->
l = x :: y :: zs ->
length (snd (split (x :: y :: zs))) < length (x :: y :: zs)

______________________________________(2/2)
forall (l : list nat) (x : nat) (l0 : list nat) (y : nat) (zs : list nat),
l0 = y :: zs ->
l = x :: y :: zs ->
length (fst (split (x :: y :: zs))) < length (x :: y :: zs)

二つのサブゴールの最後の項を見てみると、それぞれ

length (snd (split (x :: y :: zs))) < length (x :: y :: zs)

length (fst (split (x :: y :: zs))) < length (x :: y :: zs)

であり、"snd (split (x :: y :: zs))"、"fst (split (x :: y :: zs))" は再帰的に呼び出している msort の引数になっています。これらが「再帰呼び出しごとに引数が長さに関して小さくなる」という命題を表しています。よってこの二つのサブゴールを証明すれば、msort は定義できたことになります。

それではこのサブゴールを証明してみましょう。

まずは intros、simpl、subst で証明図を整理します。

intros.
simpl.
subst.

2 subgoals
x : nat
y : nat
zs : list nat
______________________________________(1/2)
S (length (snd (split zs))) < S (S (length zs))

______________________________________(2/2)
forall (l : list nat) (x : nat) (l0 : list nat) (y : nat) (zs : list nat),
l0 = y :: zs ->
l = x :: y :: zs ->
length (fst (split (x :: y :: zs))) < length (x :: y :: zs)

他に使えそうな仮定もないので induction zs で帰納法をしたいところです。 しかし induction タクティクは nil と x :: xs との場合で帰納法を適用するので、split のように三つの場合でパターンマッチすると induction タクティクとは相性が悪くなってしまいます。

このようなときのために、split の定義に合わせた新しい帰納法を使えるようにする、Functional Scheme コマンドを紹介します。Function コマンドを使う前まで戻って、以下のように書いて読み込ませてください。

Functional Scheme split_ind := Induction for split Sort Prop.

split_ind が新しく作る帰納法の名前で、Induction for に続く split が帰納法を作る元の関数です。こう書くことにより split_ind という名前で split に特化した帰納法による証明ができるようになります。

"Sort Prop" は、生成する帰納法が、Prop を返す関数を取ることを意味します。今回示したい "S (length (snd (split zs))) < S (S (length zs))" の型は Prop なので、Sort Prop と指定しました。示したい命題の型が Type なら、"Sort Prop" を "Sort Type" と置き換えます。

証明に戻り、Functional Scheme コマンドで生成した帰納法で証明を進めてみます。そのためには functional induction タクティクを使います。

functional induction タクティクは、その後に帰納法を適用したい値を書いて、それに適した(Functional Scheme コマンドで生成した)帰納法を与えます。

functional induction (split zs).

4 subgoals
x : nat
y : nat
______________________________________(1/4)
S (length (snd (nil, nil))) < S (S (length nil))


______________________________________(2/4)
S (length (snd (x0 :: nil, nil))) < S (S (length (x0 :: nil)))

______________________________________(3/4)
S (length (snd (x0 :: fst (split zs), y0 :: snd (split zs)))) <
S (S (length (x0 :: y0 :: zs)))

______________________________________(4/4)
forall (l : list nat) (x : nat) (l0 : list nat) (y : nat) (zs : list nat),
l0 = y :: zs ->
l = x :: y :: zs ->
length (fst (split (x :: y :: zs))) < length (x :: y :: zs)

一つ目のサブゴールが三つに分割されました。それぞれのサブゴールはちゃんと split の結果と対応しています。

最初のサブゴールは簡約すると 1 < 2 となるので、< の定義から明らかです。

simpl.

4 subgoals
x : nat
y : nat
______________________________________(1/4)
1 < 2

______________________________________(2/4)
...

constructor.

3 subgoals
x : nat
y : nat
x0 : nat
______________________________________(1/3)
S (length (snd (x0 :: nil, nil))) < S (S (length (x0 :: nil)))

______________________________________(2/3)
S (length (snd (x0 :: fst (split zs), y0 :: snd (split zs)))) <
S (S (length (x0 :: y0 :: zs)))

______________________________________(3/3)
forall (l : list nat) (x : nat) (l0 : list nat) (y : nat) (zs : list nat),
l0 = y :: zs ->
l = x :: y :: zs ->
length (fst (split (x :: y :: zs))) < length (x :: y :: zs)

次のサブゴールも 1 < 3 となって自明ですね。

simpl.
constructor.
constructor.

2 subgoals
x : nat
y : nat
x0 : nat
y0 : nat
zs : list nat
IHp : S (length (snd (split zs))) < S (S (length zs))
______________________________________(1/2)
S (length (snd (x0 :: fst (split zs), y0 :: snd (split zs)))) <
S (S (length (x0 :: y0 :: zs)))

______________________________________(2/2)
forall (l : list nat) (x : nat) (l0 : list nat) (y : nat) (zs : list nat),
l0 = y :: zs ->
l = x :: y :: zs ->
length (fst (split (x :: y :: zs))) < length (x :: y :: zs)

今度は少し複雑になりました。これもまず simpl タクティクで簡約してみます。

simpl.

2 subgoals
x : nat
y : nat
x0 : nat
y0 : nat
zs : list nat
IHp : S (length (snd (split zs))) < S (S (length zs))
______________________________________(1/2)
S (S (length (snd (split zs)))) < S (S (S (S (length zs))))

______________________________________(2/2)
...

length (snd (split zs)) を a、length zs を b、S を (1 +) として書き直してみると IHp は 1 + a < 2 + b、サブゴールは 2 + a < 4 + b となり、不等式の性質から簡単にこのサブゴールは示せそうです。これを示すには Arith モジュールの

lt_S : forall n m, n < m -> n < S m
lt_n_S : forall n m, n < m -> S n < S m

という補題を使います。

apply lt_S.
apply lt_n_S.

2 subgoals
x : nat
y : nat
x0 : nat
y0 : nat
zs : list nat
IHp : S (length (snd (split zs))) < S (S (length zs))
______________________________________(1/2)
S (length (snd (split zs))) < S (S (length zs))

______________________________________(2/2)
...

サブゴールが IHp の型と等しくなりました。

apply IHp.

1 subgoal
______________________________________(1/1)
forall (l : list nat) (x : nat) (l0 : list nat) (y : nat) (zs : list nat),
l0 = y :: zs ->
l = x :: y :: zs ->
length (fst (split (x :: y :: zs))) < length (x :: y :: zs)

初期の状態での二つ目のサブゴールです。これもほとんど同じ手順で示せるので、証明は一度に書きます。

Require Import List.
Require Import Arith.
Require Import Recdef.

Function msort (l : list nat) {measure length l} : list nat :=
  match l with
  | nil => nil
  | x::nil => x::nil
  | x::y::zs => (fun l' => merge (msort (fst l')) (msort (snd l'))) (split l)
  end.
Proof.
 (* length (snd (split (x::y::zs))) < length (x::y::zs) *)
 intros.
 simpl.
 subst.
 functional induction (split zs).
  simpl.
  constructor.
 
  simpl.
  constructor.
  constructor.
 
  simpl.
  apply lt_S.
  apply lt_n_S.
  apply IHp.

 (* length (fst (split (x::y::zs))) < length (x::y::zs) *)
 intros.
 subst.
 functional induction (split zs).
  simpl.
  constructor.

  simpl.
  constructor.

  simpl.
  apply lt_n_S.
  apply lt_S.
  apply IHp.
Defined.
ハート

ここで、証明の最後が Qed ではなく Defined になっていることに注意してください。

これまで定理を証明したときは最後に Qed コマンドを使って証明終了を Coq に伝えていましたが、Function コマンドで始まった、定義する関数の停止性に関する証明に対しては Defined を使います。

Qed で proof-editing mode を抜けると、定義した関数はあくまで証明でしかなく、関数としての振舞いはしません。一方 Defined を使うと、proof-editing mode で定義した関数でも関数として機能するようになるのです。

実際に msort を Eval compute in コマンドで動作を見てみましょう。

Eval compute in msort (2 :: 1 :: 5 :: 3 :: 0 :: 4 :: nil)

result for command Eval compute in msort (2 :: 1 :: 5 :: 3 :: 0 :: 4 :: nil) . :
     = 0 :: 1 :: 2 :: 3 :: 4 :: 5 :: nil
          : list nat

Eval compute in msort (6 :: 2 :: 5 :: 3 :: nil)

Result for command Eval compute in msort (6 :: 2 :: 5 :: 3 :: nil) . :
     = 2 :: 3 :: 5 :: 6 :: nil
          : list nat

ちゃんとソートされたリストが返されていますね。

では最後の Defined を Qed に変えてみます。

Function msort (l : list nat) {measure length l} : list nat :=
  match l with
  | nil => nil
  | x::nil => x::nil
  | x::y::zs => (fun l' => merge (msort (fst l')) (msort (snd l'))) (split l)
  end.
Proof.
 (* length (snd (split (x::y::zs))) < length (x::y::zs) *)
 (* 省略 *)
Qed.

Eval compute in コマンドを使ってみると、

Eval compute in msort (2 :: 1 :: 5 :: 3 :: 0 :: 4 :: nil)

Result for command Eval compute in msort (2 :: 1 :: 5 :: 3 :: 0 :: 4 :: nil) . :
     = let (v, _) := msort_terminate (2 :: 1 :: 5 :: 3 :: 0 :: 4 :: nil) in v
     : list nat

となり、ソートされたリストを返してくれません。

練習問題

問12. nat の二重リストを受け取って、与えられたリストが

(a11 :: a12 :: ... :: a1n :: nil) ::
(a21 :: a22 :: ... :: a2n :: nil) ::
...
(am1 :: am2 :: ... :: amn :: nil) :: nil

のとき

(a11 :: a21 :: ... :: am1 :: nil) ::
(a12 :: a22 :: ... :: am2 :: nil) ::
...
(a1m :: an2 :: ... :: anm :: nil) :: nil

を返す関数 transpose を定義しなさい。ただし引数が nil のときは nil を返し、内側のそれぞれのリストの長さが異なるとき、つまり

(a11 :: a12 :: a13 :: nil) ::
(a21 :: a22 :: a23 :: a24 :: nil) ::
(a31 :: a32 :: nil) :: nil

のようなときは、

(a11 :: a21 :: a31 :: nil) ::
(a12 :: a22 :: a32 :: nil) ::
(a13 :: a24 :: 0   :: nil) :: nil

のように、先頭のリストに長さを合わせて計算するものとします。

ヒント：transpose は、引数が nil、nil :: _、(x::xs) :: nil のときで場合分けすると以下のような等式が成り立ちます。

transpose nil          = nil
transpose nil::_       = nil
transpose (x::xs)::xss = map (hd 0) l :: transpose (map (@tl nat) l)

ここで、(@tl nat) は tl の型変数に nat を明示していることを表します。上の場合は暗黙的に tl の型が推論されないので明示する必要があります。

前回の答え

前回の問題はこうでした。

問10. 以下の命題

forall (n m : nat), n = m \/ n <> m

を証明しなさい。

問11. 任意の P, Q : nat -> Prop に対して、

(1) (forall n, P n -> Q n) -> ((forall n, P n) -> (forall n, Q n))

(2) ((forall n, P n) -> (forall n, Q n)) -> (forall n, P n -> Q n)

はそれぞれ成り立つか。成り立つ場合は証明し、そうでない場合は成り立たなくなるような P、Q を具体的に考えなさい。

問10.

Goal forall (n m : nat), n = m \/ n <> m.
induction n.
 destruct m.
  left.
  reflexivity.
     
  right.
  discriminate.
            
  intro.
  destruct m.
   right.
   discriminate.
                      
   destruct (IHn m).
    left.
    f_equal.
    apply H.
                                     
    right.
    apply not_eq_S.
    apply H.
Qed.

問11.

(1) 成り立つ。

Goal forall (P Q : nat -> Prop), (forall n, P n -> Q n) -> ((forall n, P n) -> (forall n, Q n)).
intros.
apply H.
apply H0.
Qed.

(2) 成り立たない。 P n を「n は偶数」、Q n を「n は奇数」とすると、

((forall n, P n) -> (forall n, Q n))

は

「すべての自然数は偶数」ならば「すべての自然数は奇数」

となり、前提の「すべての自然数は偶数」は偽だから全体も真であるが、

(forall n, P n -> Q n)

は

すべての自然数は、偶数ならば奇数

となり明かに偽。

PAGE TOP