DepList.v 4.16 KB
Newer Older
Adam Chlipala's avatar
Adam Chlipala committed
1 2 3 4 5 6 7 8 9 10 11
(* Copyright (c) 2008, Adam Chlipala
 * 
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)

(* Dependent list types presented in Chapter 8 *)

Adam Chlipala's avatar
Adam Chlipala committed
12
Require Import Arith List.
Adam Chlipala's avatar
Adam Chlipala committed
13 14 15 16 17

Set Implicit Arguments.


Section ilist.
Adam Chlipala's avatar
Adam Chlipala committed
18
  Variable A : Type.
Adam Chlipala's avatar
Adam Chlipala committed
19

Adam Chlipala's avatar
Adam Chlipala committed
20
  Fixpoint ilist (n : nat) : Type :=
Adam Chlipala's avatar
Adam Chlipala committed
21 22 23 24 25
    match n with
      | O => unit
      | S n' => A * ilist n'
    end%type.

Adam Chlipala's avatar
Adam Chlipala committed
26 27 28 29 30 31 32 33
  Definition inil : ilist O := tt.
  Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls).

  Definition hd n (ls : ilist (S n)) : A := fst ls.
  Definition tl n (ls : ilist (S n)) : ilist n := snd ls.

  Implicit Arguments icons [n].

Adam Chlipala's avatar
Adam Chlipala committed
34
  Fixpoint index (n : nat) : Type :=
Adam Chlipala's avatar
Adam Chlipala committed
35 36 37 38 39 40 41 42 43 44 45 46 47 48
    match n with
      | O => Empty_set
      | S n' => option (index n')
    end.

  Fixpoint get (n : nat) : ilist n -> index n -> A :=
    match n return ilist n -> index n -> A with
      | O => fun _ idx => match idx with end
      | S n' => fun ls idx =>
        match idx with
          | None => fst ls
          | Some idx' => get n' (snd ls) idx'
        end
    end.
Adam Chlipala's avatar
Adam Chlipala committed
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82

  Section everywhere.
    Variable x : A.

    Fixpoint everywhere (n : nat) : ilist n :=
      match n return ilist n with
        | O => inil
        | S n' => icons x (everywhere n')
      end.
  End everywhere.

  Section singleton.
    Variables x default : A.

    Fixpoint singleton (n m : nat) {struct n} : ilist n :=
      match n return ilist n with
        | O => inil
        | S n' =>
          match m with
            | O => icons x (everywhere default n')
            | S m' => icons default (singleton n' m')
          end
      end.
  End singleton.

  Section map2.
    Variable f : A -> A -> A.

    Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n :=
      match n return ilist n -> ilist n -> ilist n with
        | O => fun _ _ => inil
        | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
      end.
  End map2.
Adam Chlipala's avatar
Adam Chlipala committed
83 84
End ilist.

Adam Chlipala's avatar
Adam Chlipala committed
85
Implicit Arguments icons [A n].
Adam Chlipala's avatar
Adam Chlipala committed
86
Implicit Arguments get [A n].
Adam Chlipala's avatar
Adam Chlipala committed
87
Implicit Arguments map2 [A n].
Adam Chlipala's avatar
Adam Chlipala committed
88 89 90 91 92 93 94 95 96 97 98

Section hlist.
  Variable A : Type.
  Variable B : A -> Type.

  Fixpoint hlist (ls : list A) : Type :=
    match ls with
      | nil => unit
      | x :: ls' => B x * hlist ls'
    end%type.

99 100 101 102
  Definition hnil : hlist nil := tt.
  Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
    (v, hls).

Adam Chlipala's avatar
Adam Chlipala committed
103 104 105 106 107 108 109 110
  Variable elm : A.

  Fixpoint member (ls : list A) : Type :=
    match ls with
      | nil => Empty_set
      | x :: ls' => (x = elm) + member ls'
    end%type.

Adam Chlipala's avatar
Adam Chlipala committed
111 112 113 114 115
  Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
    inl _ pf.
  Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
    inr _ m.

Adam Chlipala's avatar
Adam Chlipala committed
116 117 118 119 120 121 122 123 124 125 126
  Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
    match ls return hlist ls -> member ls -> B elm with
      | nil => fun _ idx => match idx with end
      | _ :: ls' => fun mls idx =>
        match idx with
          | inl pf => match pf with
                        | refl_equal => fst mls
                      end
          | inr idx' => hget ls' (snd mls) idx'
        end
    end.
127 128 129 130 131 132

  Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
    match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
      | nil => fun _ hls2 => hls2
      | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
    end.
Adam Chlipala's avatar
Adam Chlipala committed
133 134
End hlist.

135 136
Implicit Arguments hnil [A B].
Implicit Arguments hcons [A B x ls].
Adam Chlipala's avatar
Adam Chlipala committed
137
Implicit Arguments hget [A B elm ls].
138 139
Implicit Arguments happ [A B ls1 ls2].

Adam Chlipala's avatar
Adam Chlipala committed
140 141 142
Implicit Arguments hfirst [A elm x ls].
Implicit Arguments hnext [A elm x ls].

143 144
Infix ":::" := hcons (right associativity, at level 60).
Infix "+++" := happ (right associativity, at level 60).
Adam Chlipala's avatar
Adam Chlipala committed
145 146 147 148 149 150 151 152 153 154 155 156 157 158 159

Section hmap.
  Variable A : Type.
  Variables B1 B2 : A -> Type.

  Variable f : forall x, B1 x -> B2 x.

  Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
    match ls return hlist B1 ls -> hlist B2 ls with
      | nil => fun _ => hnil
      | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
    end.
End hmap.

Implicit Arguments hmap [A B1 B2 ls].