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@114: Variable A : Set. adamc@114: adamc@114: Fixpoint ilist (n : nat) : Set := adamc@114: match n with adamc@114: | O => unit adamc@114: | S n' => A * ilist n' adamc@114: end%type. adamc@114: adamc@114: Fixpoint index (n : nat) : Set := 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@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@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@114: End hlist. adamc@114: adamc@114: Implicit Arguments hget [A B elm ls].