Mercurial > cpdt > repo

annotate src/DepList.v @ 193:8e9499e27b6c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of Generic
author Adam Chlipala <adamc@hcoop.net>
date Fri, 28 Nov 2008 09:55:56 -0500
parents 8f3fc56b90d4
children 063b5741c248
rev   line source
adamc@114 1 (* Copyright (c) 2008, Adam Chlipala
adamc@114 2 *
adamc@114 3 * This work is licensed under a
adamc@114 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@114 5 * Unported License.
adamc@114 6 * The license text is available at:
adamc@114 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@114 8 *)
adamc@114 9
adamc@114 10 (* Dependent list types presented in Chapter 8 *)
adamc@114 11
adamc@179 12 Require Import Arith List Tactics.
adamc@114 13
adamc@114 14 Set Implicit Arguments.
adamc@114 15
adamc@114 16
adamc@114 17 Section ilist.
adamc@123 18 Variable A : Type.
adamc@114 19
adamc@123 20 Fixpoint ilist (n : nat) : Type :=
adamc@114 21 match n with
adamc@114 22 | O => unit
adamc@114 23 | S n' => A * ilist n'
adamc@114 24 end%type.
adamc@114 25
adamc@149 26 Definition inil : ilist O := tt.
adamc@149 27 Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls).
adamc@149 28
adamc@149 29 Definition hd n (ls : ilist (S n)) : A := fst ls.
adamc@149 30 Definition tl n (ls : ilist (S n)) : ilist n := snd ls.
adamc@149 31
adamc@149 32 Implicit Arguments icons [n].
adamc@149 33
adamc@123 34 Fixpoint index (n : nat) : Type :=
adamc@114 35 match n with
adamc@114 36 | O => Empty_set
adamc@114 37 | S n' => option (index n')
adamc@114 38 end.
adamc@114 39
adamc@114 40 Fixpoint get (n : nat) : ilist n -> index n -> A :=
adamc@114 41 match n return ilist n -> index n -> A with
adamc@114 42 | O => fun _ idx => match idx with end
adamc@114 43 | S n' => fun ls idx =>
adamc@114 44 match idx with
adamc@114 45 | None => fst ls
adamc@114 46 | Some idx' => get n' (snd ls) idx'
adamc@114 47 end
adamc@114 48 end.
adamc@149 49
adamc@149 50 Section everywhere.
adamc@149 51 Variable x : A.
adamc@149 52
adamc@149 53 Fixpoint everywhere (n : nat) : ilist n :=
adamc@149 54 match n return ilist n with
adamc@149 55 | O => inil
adamc@149 56 | S n' => icons x (everywhere n')
adamc@149 57 end.
adamc@149 58 End everywhere.
adamc@149 59
adamc@149 60 Section singleton.
adamc@149 61 Variables x default : A.
adamc@149 62
adamc@149 63 Fixpoint singleton (n m : nat) {struct n} : ilist n :=
adamc@149 64 match n return ilist n with
adamc@149 65 | O => inil
adamc@149 66 | S n' =>
adamc@149 67 match m with
adamc@149 68 | O => icons x (everywhere default n')
adamc@149 69 | S m' => icons default (singleton n' m')
adamc@149 70 end
adamc@149 71 end.
adamc@149 72 End singleton.
adamc@149 73
adamc@149 74 Section map2.
adamc@149 75 Variable f : A -> A -> A.
adamc@149 76
adamc@149 77 Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n :=
adamc@149 78 match n return ilist n -> ilist n -> ilist n with
adamc@149 79 | O => fun _ _ => inil
adamc@149 80 | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
adamc@149 81 end.
adamc@149 82 End map2.
adamc@114 83 End ilist.
adamc@114 84
adamc@149 85 Implicit Arguments icons [A n].
adamc@114 86 Implicit Arguments get [A n].
adamc@149 87 Implicit Arguments map2 [A n].
adamc@114 88
adamc@114 89 Section hlist.
adamc@114 90 Variable A : Type.
adamc@114 91 Variable B : A -> Type.
adamc@114 92
adamc@114 93 Fixpoint hlist (ls : list A) : Type :=
adamc@114 94 match ls with
adamc@114 95 | nil => unit
adamc@114 96 | x :: ls' => B x * hlist ls'
adamc@114 97 end%type.
adamc@114 98
adamc@125 99 Definition hnil : hlist nil := tt.
adamc@125 100 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
adamc@125 101 (v, hls).
adamc@125 102
adamc@114 103 Variable elm : A.
adamc@114 104
adamc@114 105 Fixpoint member (ls : list A) : Type :=
adamc@114 106 match ls with
adamc@114 107 | nil => Empty_set
adamc@114 108 | x :: ls' => (x = elm) + member ls'
adamc@114 109 end%type.
adamc@114 110
adamc@126 111 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
adamc@126 112 inl _ pf.
adamc@126 113 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
adamc@126 114 inr _ m.
adamc@126 115
adamc@114 116 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
adamc@114 117 match ls return hlist ls -> member ls -> B elm with
adamc@114 118 | nil => fun _ idx => match idx with end
adamc@114 119 | _ :: ls' => fun mls idx =>
adamc@114 120 match idx with
adamc@114 121 | inl pf => match pf with
adamc@114 122 | refl_equal => fst mls
adamc@114 123 end
adamc@114 124 | inr idx' => hget ls' (snd mls) idx'
adamc@114 125 end
adamc@114 126 end.
adamc@125 127
adamc@125 128 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
adamc@125 129 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
adamc@125 130 | nil => fun _ hls2 => hls2
adamc@125 131 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
adamc@125 132 end.
adamc@114 133 End hlist.
adamc@114 134
adamc@125 135 Implicit Arguments hnil [A B].
adamc@125 136 Implicit Arguments hcons [A B x ls].
adamc@114 137 Implicit Arguments hget [A B elm ls].
adamc@125 138 Implicit Arguments happ [A B ls1 ls2].
adamc@125 139
adamc@126 140 Implicit Arguments hfirst [A elm x ls].
adamc@126 141 Implicit Arguments hnext [A elm x ls].
adamc@126 142
adamc@125 143 Infix ":::" := hcons (right associativity, at level 60).
adamc@125 144 Infix "+++" := happ (right associativity, at level 60).
adamc@163 145
adamc@163 146 Section hmap.
adamc@163 147 Variable A : Type.
adamc@163 148 Variables B1 B2 : A -> Type.
adamc@163 149
adamc@163 150 Variable f : forall x, B1 x -> B2 x.
adamc@163 151
adamc@163 152 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
adamc@163 153 match ls return hlist B1 ls -> hlist B2 ls with
adamc@163 154 | nil => fun _ => hnil
adamc@163 155 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
adamc@163 156 end.
adamc@179 157
adamc@179 158 Implicit Arguments hmap [ls].
adamc@179 159
adamc@179 160 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
adamc@179 161 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
adamc@179 162 induction ls1; crush.
adamc@179 163 Qed.
adamc@163 164 End hmap.
adamc@163 165
adamc@163 166 Implicit Arguments hmap [A B1 B2 ls].