Mercurial > cpdt > repo

comparison src/DepList.v @ 149:e70fbfc56c46

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Reflection exercise
author Adam Chlipala <adamc@hcoop.net>
date Wed, 29 Oct 2008 14:39:00 -0400
parents d7aec67f808b
children ba306bf9ec80
comparison
equal deleted inserted replaced
148:0952c4ba209b 149:e70fbfc56c46
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* Dependent list types presented in Chapter 8 *) 10 (* Dependent list types presented in Chapter 8 *)
11 11
12 Require Import List. 12 Require Import Arith List.
13 13
14 Set Implicit Arguments. 14 Set Implicit Arguments.
15 15
16 16
17 Section ilist. 17 Section ilist.
20 Fixpoint ilist (n : nat) : Type := 20 Fixpoint ilist (n : nat) : Type :=
21 match n with 21 match n with
22 | O => unit 22 | O => unit
23 | S n' => A * ilist n' 23 | S n' => A * ilist n'
24 end%type. 24 end%type.
25
26 Definition inil : ilist O := tt.
27 Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls).
28
29 Definition hd n (ls : ilist (S n)) : A := fst ls.
30 Definition tl n (ls : ilist (S n)) : ilist n := snd ls.
31
32 Implicit Arguments icons [n].
25 33
26 Fixpoint index (n : nat) : Type := 34 Fixpoint index (n : nat) : Type :=
27 match n with 35 match n with
28 | O => Empty_set 36 | O => Empty_set
29 | S n' => option (index n') 37 | S n' => option (index n')
36 match idx with 44 match idx with
37 | None => fst ls 45 | None => fst ls
38 | Some idx' => get n' (snd ls) idx' 46 | Some idx' => get n' (snd ls) idx'
39 end 47 end
40 end. 48 end.
49
50 Section everywhere.
51 Variable x : A.
52
53 Fixpoint everywhere (n : nat) : ilist n :=
54 match n return ilist n with
55 | O => inil
56 | S n' => icons x (everywhere n')
57 end.
58 End everywhere.
59
60 Section singleton.
61 Variables x default : A.
62
63 Fixpoint singleton (n m : nat) {struct n} : ilist n :=
64 match n return ilist n with
65 | O => inil
66 | S n' =>
67 match m with
68 | O => icons x (everywhere default n')
69 | S m' => icons default (singleton n' m')
70 end
71 end.
72 End singleton.
73
74 Section map2.
75 Variable f : A -> A -> A.
76
77 Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n :=
78 match n return ilist n -> ilist n -> ilist n with
79 | O => fun _ _ => inil
80 | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
81 end.
82 End map2.
41 End ilist. 83 End ilist.
42 84
85 Implicit Arguments icons [A n].
43 Implicit Arguments get [A n]. 86 Implicit Arguments get [A n].
87 Implicit Arguments map2 [A n].
44 88
45 Section hlist. 89 Section hlist.
46 Variable A : Type. 90 Variable A : Type.
47 Variable B : A -> Type. 91 Variable B : A -> Type.
48 92