adam@534: (* Copyright (c) 2008-2009, 2015, 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: 
adam@350: (* Dependent list types presented in Chapter 9 *)
adamc@114: 
adam@534: Require Import Arith List Cpdt.CpdtTactics.
adamc@114: 
adamc@114: Set Implicit Arguments.
adam@534: Set Asymmetric Patterns.
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].