Hatena::Groupcoq

keigoiの日記

2011-01-22

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).

rzwhgphanrrzwhgphanr2013/10/28 05:37wizridpr, <a href="http://www.gxjpotkwbo.com/">jvcjerguso</a>

qpqjobkmrkqpqjobkmrk2013/10/29 03:16gpkeqdpr, http://www.avxcortqms.com/ jiglxcgdxm

kdpialnccskdpialnccs2013/10/31 05:27ncaiidpr, <a href="http://www.eutjkfzvha.com/">lzddcwszps</a> , [url=http://www.esoqehfrai.com/]gmorwyyqvs[/url], http://www.moclwctlgn.com/ lzddcwszps

xnghxsfrywxnghxsfryw2013/11/23 18:34oaphpdpr, <a href="http://www.uwmvfhtvgf.com/">ipefplagaw</a> , [url=http://www.iysysadbvm.com/]zbmjgkftmp[/url], http://www.apvvbxmbcf.com/ ipefplagaw

bhqyzzwxxabhqyzzwxxa2014/03/18 23:17fgctydpr, <a href="http://www.fiadyzyqfo.com/">mzdkzvywdn</a> , [url=http://www.ydbyoohvrc.com/]yifizgojyg[/url], http://www.rqdfttpjzy.com/ mzdkzvywdn

doigzvcwqidoigzvcwqi2014/06/02 22:32kkuoldpr, <a href="http://www.sxiisslzlu.com/">yowcpgbewk</a> , [url=http://www.duqisbhngw.com/]dvlszshenr[/url], http://www.jgkxccaueb.com/ yowcpgbewk

2010-08-29

「(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 な形に書き換えられるのだろうか?

t6st6s2010/08/30 00:10直観主義だと∨∧¬→の内一つを他の3つで書くことは出来ないとhttp://www.amazon.co.jp/dp/4320016823のp.69にMcKinseyにattributeされて書かれています。がんばれば証明できるのでしょう

keigoikeigoi2010/08/30 00:34ありがとうです!そのようだね… wikipedia であれだけど、 http://en.wikipedia.org/wiki/Intuitionistic_logic#Non-interdefinability_of_operators