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