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

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

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

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

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

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

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

SailipFoulkSailipFoulk 2017/05/04 02:55 http://undeclaiming.xyz <a href="http://undeclaiming.xyz">norsk kasino</a> http://undeclaiming.xyz - norsk kasino

ゲスト



トラックバック - http://coq.g.hatena.ne.jp/keigoi/20110122