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@179: Require Import Arith List Tactics. 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@149: Definition inil : ilist O := tt. adamc@149: Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls). adamc@149: adamc@149: Definition hd n (ls : ilist (S n)) : A := fst ls. adamc@149: Definition tl n (ls : ilist (S n)) : ilist n := snd ls. adamc@149: adamc@149: Implicit Arguments icons [n]. adamc@149: 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@149: adamc@149: Section everywhere. adamc@149: Variable x : A. adamc@149: adamc@149: Fixpoint everywhere (n : nat) : ilist n := adamc@149: match n return ilist n with adamc@149: | O => inil adamc@149: | S n' => icons x (everywhere n') adamc@149: end. adamc@149: End everywhere. adamc@149: adamc@149: Section singleton. adamc@149: Variables x default : A. adamc@149: adamc@149: Fixpoint singleton (n m : nat) {struct n} : ilist n := adamc@149: match n return ilist n with adamc@149: | O => inil adamc@149: | S n' => adamc@149: match m with adamc@149: | O => icons x (everywhere default n') adamc@149: | S m' => icons default (singleton n' m') adamc@149: end adamc@149: end. adamc@149: End singleton. adamc@149: adamc@149: Section map2. adamc@149: Variable f : A -> A -> A. adamc@149: adamc@149: Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n := adamc@149: match n return ilist n -> ilist n -> ilist n with adamc@149: | O => fun _ _ => inil adamc@149: | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2)) adamc@149: end. adamc@149: End map2. adamc@194: adamc@194: Section fold. adamc@194: Variable B : Type. adamc@194: Variable f : A -> B -> B. adamc@194: Variable i : B. adamc@194: adamc@194: Fixpoint foldr (n : nat) : ilist n -> B := adamc@194: match n return ilist n -> B with adamc@194: | O => fun _ => i adamc@194: | S n' => fun ils => f (hd ils) (foldr n' (tl ils)) adamc@194: end. adamc@194: End fold. adamc@114: End ilist. adamc@114: adamc@194: Implicit Arguments inil [A]. adamc@194: Implicit Arguments icons [A n]. adamc@194: adamc@149: Implicit Arguments icons [A n]. adamc@114: Implicit Arguments get [A n]. adamc@149: Implicit Arguments map2 [A n]. adamc@194: Implicit Arguments foldr [A B n]. adamc@114: adamc@196: Section imap. adamc@196: Variables A B : Type. adamc@196: Variable f : A -> B. adamc@196: adamc@196: Fixpoint imap (n : nat) : ilist A n -> ilist B n := adamc@196: match n return ilist A n -> ilist B n with adamc@196: | O => fun _ => inil adamc@196: | S n' => fun ls => icons (f (hd ls)) (imap _ (tl ls)) adamc@196: end. adamc@196: End imap. adamc@196: adamc@196: Implicit Arguments imap [A B n]. adamc@196: 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@194: adamc@194: Variable f : forall x, B x. adamc@194: adamc@194: Fixpoint hmake (ls : list A) : hlist ls := adamc@194: match ls return hlist ls with adamc@194: | nil => hnil adamc@194: | x :: ls' => hcons _ (f x) (hmake ls') adamc@194: end. adamc@196: adamc@196: Implicit Arguments hget [ls]. adamc@196: adamc@196: Theorem hget_hmake : forall ls (m : member ls), adamc@196: hget (hmake ls) m = f elm. adamc@196: induction ls; crush. adamc@196: case a0; reflexivity. adamc@196: Qed. 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@194: Implicit Arguments hmake [A B]. 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). adamc@163: adamc@163: Section hmap. adamc@163: Variable A : Type. adamc@163: Variables B1 B2 : A -> Type. adamc@163: adamc@163: Variable f : forall x, B1 x -> B2 x. adamc@163: adamc@163: Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls := adamc@163: match ls return hlist B1 ls -> hlist B2 ls with adamc@163: | nil => fun _ => hnil adamc@163: | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl) adamc@163: end. adamc@179: adamc@179: Implicit Arguments hmap [ls]. adamc@179: adamc@179: Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1), adamc@179: hmap h1 +++ hmap h2 = hmap (h1 +++ h2). adamc@179: induction ls1; crush. adamc@179: Qed. adamc@197: adamc@197: Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls), adamc@197: hget (hmap hls) m = f (hget hls m). adamc@197: induction ls; crush. adamc@197: case a1; crush. adamc@197: Qed. adamc@163: End hmap. adamc@163: adamc@163: Implicit Arguments hmap [A B1 B2 ls].