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].