Mercurial > cpdt > repo

annotate src/DepList.v @ 136:d6b1e9de7fc1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Free variables in unification variables issue
author Adam Chlipala <adamc@hcoop.net>
date Sun, 26 Oct 2008 14:39:21 -0400
parents d7aec67f808b
children e70fbfc56c46
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@114 12 Require Import List.
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@123 26 Fixpoint index (n : nat) : Type :=
adamc@114 27 match n with
adamc@114 28 | O => Empty_set
adamc@114 29 | S n' => option (index n')
adamc@114 30 end.
adamc@114 31
adamc@114 32 Fixpoint get (n : nat) : ilist n -> index n -> A :=
adamc@114 33 match n return ilist n -> index n -> A with
adamc@114 34 | O => fun _ idx => match idx with end
adamc@114 35 | S n' => fun ls idx =>
adamc@114 36 match idx with
adamc@114 37 | None => fst ls
adamc@114 38 | Some idx' => get n' (snd ls) idx'
adamc@114 39 end
adamc@114 40 end.
adamc@114 41 End ilist.
adamc@114 42
adamc@114 43 Implicit Arguments get [A n].
adamc@114 44
adamc@114 45 Section hlist.
adamc@114 46 Variable A : Type.
adamc@114 47 Variable B : A -> Type.
adamc@114 48
adamc@114 49 Fixpoint hlist (ls : list A) : Type :=
adamc@114 50 match ls with
adamc@114 51 | nil => unit
adamc@114 52 | x :: ls' => B x * hlist ls'
adamc@114 53 end%type.
adamc@114 54
adamc@125 55 Definition hnil : hlist nil := tt.
adamc@125 56 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
adamc@125 57 (v, hls).
adamc@125 58
adamc@114 59 Variable elm : A.
adamc@114 60
adamc@114 61 Fixpoint member (ls : list A) : Type :=
adamc@114 62 match ls with
adamc@114 63 | nil => Empty_set
adamc@114 64 | x :: ls' => (x = elm) + member ls'
adamc@114 65 end%type.
adamc@114 66
adamc@126 67 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
adamc@126 68 inl _ pf.
adamc@126 69 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
adamc@126 70 inr _ m.
adamc@126 71
adamc@114 72 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
adamc@114 73 match ls return hlist ls -> member ls -> B elm with
adamc@114 74 | nil => fun _ idx => match idx with end
adamc@114 75 | _ :: ls' => fun mls idx =>
adamc@114 76 match idx with
adamc@114 77 | inl pf => match pf with
adamc@114 78 | refl_equal => fst mls
adamc@114 79 end
adamc@114 80 | inr idx' => hget ls' (snd mls) idx'
adamc@114 81 end
adamc@114 82 end.
adamc@125 83
adamc@125 84 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
adamc@125 85 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
adamc@125 86 | nil => fun _ hls2 => hls2
adamc@125 87 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
adamc@125 88 end.
adamc@114 89 End hlist.
adamc@114 90
adamc@125 91 Implicit Arguments hnil [A B].
adamc@125 92 Implicit Arguments hcons [A B x ls].
adamc@114 93 Implicit Arguments hget [A B elm ls].
adamc@125 94 Implicit Arguments happ [A B ls1 ls2].
adamc@125 95
adamc@126 96 Implicit Arguments hfirst [A elm x ls].
adamc@126 97 Implicit Arguments hnext [A elm x ls].
adamc@126 98
adamc@125 99 Infix ":::" := hcons (right associativity, at level 60).
adamc@125 100 Infix "+++" := happ (right associativity, at level 60).