adamc@216: (* Copyright (c) 2008-2009, 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: adam@314: Require Import Arith List CpdtTactics. adamc@114: adamc@114: Set Implicit Arguments. adamc@114: adamc@114: adamc@114: Section ilist. adamc@123: Variable A : Type. adamc@114: adamc@216: Inductive ilist : nat -> Type := adamc@216: | INil : ilist O adamc@216: | ICons : forall n, A -> ilist n -> ilist (S n). adamc@114: adamc@216: Definition hd n (ls : ilist (S n)) := adamc@216: match ls in ilist n' return match n' with adamc@216: | O => unit adamc@216: | S _ => A adamc@216: end with adamc@216: | INil => tt adamc@216: | ICons _ x _ => x adamc@216: end. adamc@216: Definition tl n (ls : ilist (S n)) := adamc@216: match ls in ilist n' return match n' with adamc@216: | O => unit adamc@216: | S n => ilist n adamc@216: end with adamc@216: | INil => tt adamc@216: | ICons _ _ ls' => ls' adamc@114: end. adamc@114: adamc@216: Inductive fin : nat -> Set := adamc@216: | First : forall n, fin (S n) adamc@216: | Next : forall n, fin n -> fin (S n). adamc@216: adamc@216: Fixpoint get n (ls : ilist n) : fin n -> A := adamc@216: match ls with adamc@216: | INil => fun idx => adamc@216: match idx in fin n' return (match n' with adamc@216: | O => A adamc@216: | S _ => unit adamc@216: end) with adamc@216: | First _ => tt adamc@216: | Next _ _ => tt adamc@114: end adamc@216: | ICons _ x ls' => fun idx => adamc@216: match idx in fin n' return (fin (pred n') -> A) -> A with adamc@216: | First _ => fun _ => x adamc@216: | Next _ idx' => fun get_ls' => get_ls' idx' adamc@216: end (get ls') 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@216: match n with adamc@216: | O => INil adamc@216: | 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@216: Fixpoint singleton (n m : nat) : ilist n := adamc@216: match n with adamc@216: | O => INil adamc@149: | S n' => adamc@149: match m with adamc@216: | O => ICons x (everywhere default n') adamc@216: | 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@216: Fixpoint map2 n (il1 : ilist n) : ilist n -> ilist n := adamc@216: match il1 in ilist n return ilist n -> ilist n with adamc@216: | INil => fun _ => INil adamc@216: | ICons _ x il1' => fun il2 => ICons (f x (hd il2)) (map2 il1' (tl il2)) 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@216: Fixpoint foldr n (il : ilist n) : B := adamc@216: match il with adamc@216: | INil => i adamc@216: | ICons _ x il' => f x (foldr il') adamc@194: end. adamc@194: End fold. adamc@114: End ilist. adamc@114: adamc@216: Implicit Arguments INil [A]. adamc@216: Implicit Arguments First [n]. adamc@114: adamc@196: Section imap. adamc@196: Variables A B : Type. adamc@196: Variable f : A -> B. adamc@196: adamc@216: Fixpoint imap n (il : ilist A n) : ilist B n := adamc@216: match il with adamc@216: | INil => INil adamc@216: | ICons _ x il' => ICons (f x) (imap il') adamc@196: end. adamc@196: End imap. adamc@196: adamc@114: Section hlist. adamc@114: Variable A : Type. adamc@114: Variable B : A -> Type. adamc@114: adamc@216: Inductive hlist : list A -> Type := adamc@216: | HNil : hlist nil adamc@216: | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls). adamc@114: adamc@216: Definition hhd ls (hl : hlist ls) := adamc@216: match hl in hlist ls return match ls with adamc@216: | nil => unit adamc@216: | x :: _ => B x adamc@216: end with adamc@216: | HNil => tt adamc@216: | HCons _ _ v _ => v adamc@216: end. adamc@216: adamc@216: Definition htl ls (hl : hlist ls) := adamc@216: match hl in hlist ls return match ls with adamc@216: | nil => unit adamc@216: | _ :: ls' => hlist ls' adamc@216: end with adamc@216: | HNil => tt adamc@216: | HCons _ _ _ hl' => hl' adamc@216: end. adamc@125: adamc@114: Variable elm : A. adamc@114: adamc@216: Inductive member : list A -> Type := adamc@216: | HFirst : forall ls, member (elm :: ls) adamc@216: | HNext : forall x ls, member ls -> member (x :: ls). adamc@114: adamc@216: Fixpoint hget ls (mls : hlist ls) : member ls -> B elm := adamc@216: match mls with adamc@216: | HNil => fun mem => adamc@216: match mem in member ls' return (match ls' with adamc@216: | nil => B elm adamc@216: | _ :: _ => unit adamc@216: end) with adamc@216: | HFirst _ => tt adamc@216: | HNext _ _ _ => tt adamc@114: end adamc@216: | HCons _ _ x mls' => fun mem => adamc@216: match mem in member ls' return (match ls' with adamc@216: | nil => Empty_set adamc@216: | x' :: ls'' => adamc@216: B x' -> (member ls'' -> B elm) -> B elm adamc@216: end) with adamc@216: | HFirst _ => fun x _ => x adamc@216: | HNext _ _ mem' => fun _ get_mls' => get_mls' mem' adamc@216: end x (hget mls') adamc@114: end. adamc@125: adamc@216: Fixpoint happ (ls1 : list A) (hl1 : hlist ls1) : forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) := adamc@216: match hl1 in hlist ls1 return forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) with adamc@216: | HNil => fun _ hl2 => hl2 adamc@216: | HCons _ _ x hl1' => fun _ hl2 => HCons x (happ hl1' hl2) 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@216: match ls with adamc@216: | nil => HNil adamc@216: | x :: ls' => HCons (f x) (hmake ls') adamc@194: end. adamc@196: adamc@196: Theorem hget_hmake : forall ls (m : member ls), adamc@196: hget (hmake ls) m = f elm. adamc@216: induction ls; crush; adamc@216: match goal with adamc@216: | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E adamc@216: end; crush. adamc@196: Qed. adamc@114: End hlist. adamc@114: adamc@216: Implicit Arguments HNil [A B]. adamc@216: Implicit Arguments HCons [A B x ls]. adamc@194: Implicit Arguments hmake [A B]. adamc@125: adamc@216: Implicit Arguments HFirst [A elm ls]. adamc@216: Implicit Arguments HNext [A elm x ls]. adamc@126: adamc@216: 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@216: Fixpoint hmap (ls : list A) (hl : hlist B1 ls) : hlist B2 ls := adamc@216: match hl with adamc@216: | HNil => HNil adamc@216: | HCons _ _ x hl' => f x ::: hmap hl' adamc@163: end. 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@216: induction h1; 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@216: induction hls; crush; adamc@216: match goal with adamc@216: | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E adamc@216: end; crush. adamc@197: Qed. adamc@163: End hmap. adamc@163: adamc@163: Implicit Arguments hmap [A B1 B2 ls].