adamc@114: (* Copyright (c) 2008, Adam Chlipala adamc@114: * adamc@114: * This work is licensed under a adamc@114: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 adamc@114: * Unported License. adamc@114: * The license text is available at: adamc@114: * http://creativecommons.org/licenses/by-nc-nd/3.0/ adamc@114: *) adamc@114: adamc@114: (* Dependent list types presented in Chapter 8 *) adamc@114: adamc@114: Require Import List. adamc@114: adamc@114: Set Implicit Arguments. adamc@114: adamc@114: adamc@114: Section ilist. adamc@123: Variable A : Type. adamc@114: adamc@123: Fixpoint ilist (n : nat) : Type := adamc@114: match n with adamc@114: | O => unit adamc@114: | S n' => A * ilist n' adamc@114: end%type. adamc@114: adamc@123: Fixpoint index (n : nat) : Type := adamc@114: match n with adamc@114: | O => Empty_set adamc@114: | S n' => option (index n') adamc@114: end. adamc@114: adamc@114: Fixpoint get (n : nat) : ilist n -> index n -> A := adamc@114: match n return ilist n -> index n -> A with adamc@114: | O => fun _ idx => match idx with end adamc@114: | S n' => fun ls idx => adamc@114: match idx with adamc@114: | None => fst ls adamc@114: | Some idx' => get n' (snd ls) idx' adamc@114: end adamc@114: end. adamc@114: End ilist. adamc@114: adamc@114: Implicit Arguments get [A n]. adamc@114: adamc@114: Section hlist. adamc@114: Variable A : Type. adamc@114: Variable B : A -> Type. adamc@114: adamc@114: Fixpoint hlist (ls : list A) : Type := adamc@114: match ls with adamc@114: | nil => unit adamc@114: | x :: ls' => B x * hlist ls' adamc@114: end%type. adamc@114: adamc@125: Definition hnil : hlist nil := tt. adamc@125: Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) := adamc@125: (v, hls). adamc@125: adamc@114: Variable elm : A. adamc@114: adamc@114: Fixpoint member (ls : list A) : Type := adamc@114: match ls with adamc@114: | nil => Empty_set adamc@114: | x :: ls' => (x = elm) + member ls' adamc@114: end%type. adamc@114: adamc@126: Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) := adamc@126: inl _ pf. adamc@126: Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) := adamc@126: inr _ m. adamc@126: adamc@114: Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm := adamc@114: match ls return hlist ls -> member ls -> B elm with adamc@114: | nil => fun _ idx => match idx with end adamc@114: | _ :: ls' => fun mls idx => adamc@114: match idx with adamc@114: | inl pf => match pf with adamc@114: | refl_equal => fst mls adamc@114: end adamc@114: | inr idx' => hget ls' (snd mls) idx' adamc@114: end adamc@114: end. adamc@125: adamc@125: Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) := adamc@125: match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with adamc@125: | nil => fun _ hls2 => hls2 adamc@125: | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2) adamc@125: end. adamc@114: End hlist. adamc@114: adamc@125: Implicit Arguments hnil [A B]. adamc@125: Implicit Arguments hcons [A B x ls]. adamc@114: Implicit Arguments hget [A B elm ls]. adamc@125: Implicit Arguments happ [A B ls1 ls2]. adamc@125: adamc@126: Implicit Arguments hfirst [A elm x ls]. adamc@126: Implicit Arguments hnext [A elm x ls]. adamc@126: adamc@125: Infix ":::" := hcons (right associativity, at level 60). adamc@125: Infix "+++" := happ (right associativity, at level 60).