keigoiの日記

CPDT Reflexive Inductive Types

17:49

(* CPDT Chap.3 exercise 4. *)
Inductive btree (A : Set) : Set := 
| Leaf : A -> btree A
| Node : btree A -> btree A -> btree A
.
Inductive trexp : Set :=
| Base : nat -> trexp
| Tree : btree trexp -> trexp
.

(* total1 の引数が減ってないといわれてNG *)
Fixpoint total (t : trexp) {struct t} : nat :=
match t with
| Base n => n
| Tree ts => total1 ts
end
with total1 (b : btree trexp) {struct b} : nat :=
match b with
| Leaf a => total a
| Node l r => total1 l + total1 r
end.

(* 再帰のネストでうまくいった *)
Fixpoint total (t : trexp) : nat :=
match t with
| Base n => n
| Tree ts => 
    (fix total1 (b : btree trexp) : nat :=
     match b with
     | Leaf a => total a
     | Node l r => total1 l + total1 r
     end) ts
end.

CPDT Coinductive

15:10

Exercises of http://adam.chlipala.net/cpdt/html/Coinductive.html

(* Define a co-inductive type of infinite trees carrying data of a fixed parameter type. Each node should contain a data value and two child trees. *)
Section Inf_tree.
  Variable A : Set.
  CoInductive my_inf_tree : Set := 
  | Node : A -> my_inf_tree -> my_inf_tree -> my_inf_tree.
End Inf_tree.

(* Define a function everywhere for building a tree with the same data value at every node. *)
CoFixpoint everywhere (A:Set) (x:A) : my_inf_tree A :=
Node A x (everywhere A x) (everywhere A x).

「(AならばB) ⇔ (~A または B)」と直観主義論理

23:46

今日はCoq庵でした。演習の時間にやった証明でふと思い立ったので帰宅後にもCoqを触っています。

初等コンピュータサイエンスでは、論理結合子の「ならば」について、ざっくりと「A ならば B」は 「(not A) または B」 と同じだよーという感じの説明をすると思います(論理回路、離散数学、数理論理学etcetc)。で、真理値表を見て、ああそういう風に決まってるのね、とひとまず納得するんですが。

Coqでも確かめてみたいなと思い、次の2つの定理を書いてみた。

Theorem or_imply : forall P Q : Prop, ~P \/ Q -> P -> Q.
Theorem imply_or : forall P Q : Prop, (P -> Q) -> ~P \/ Q.

前者はごく平易に証明できた。

Coq < Theorem or_imply : forall P Q : Prop, ~P \/ Q -> P -> Q.
Proof.
intros.
case H.
 intro.
 contradiction .
 
 trivial.
Qed.

ところが後者((P -> Q) -> ~P \/ Q)はCoqの直観主義論理の世界では成立しないそうだ。 実際、証明のλ項を書き下そうとしてもP -> Q を関数と見立てた場合にPがないのでQが得られない。かといって~Pも証明できない。手詰まり。

(forall P Q, (P -> Q) -> ~P \/ Q) は古典論理でしか成立せず、排中律(forall P, ~P \/ P)と同値だそうです。なるほどそれはすごい。じゃそれを証明しよう。

Theorem exm_imply_or : (forall P : Prop, ~P \/ P) -> (forall P Q : Prop, (P -> Q) -> ~P \/ Q).
Theorem imply_or_exm : (forall P Q : Prop, (P -> Q) -> ~P \/ Q) -> (forall P : Prop, ~P \/ P).

前者は、古典論理の世界での forall P Q : Prop, (P -> Q) -> ~P \/ Q と同義です。後者はその逆。

Theorem exm_imply_or : (forall P : Prop, ~P \/ P) -> (forall P Q : Prop, (P -> Q) -> ~P \/ Q).
Proof.
intros.
case (H P).
 intro.
 left.
 apply H1.
 
 intro.
 right.
 apply (H0 H1).
Qed.

簡単です。

Theorem imply_or_exm : (forall P Q : Prop, (P -> Q) -> ~P \/ Q) -> (forall P : Prop, ~P \/ P).
Proof.
intros.
apply (H P P (fun x => x)).
Qed.

じゃ、直観主義論理における 「A ならば B」は 古典論理における 「~A または B」 のように ならば-free な形に書き換えられるのだろうか？