hlist.v 2.07 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From stdpp Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
6
7
8
9

(* Not using [list Type] in order to avoid universe inconsistencies *)
Inductive tlist := tnil : tlist | tcons : Type  tlist  tlist.

Inductive hlist : tlist  Type :=
  | hnil : hlist tnil
  | hcons {A As} : A  hlist As  hlist (tcons A As).

Robbert Krebbers's avatar
Robbert Krebbers committed
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
Fixpoint tapp (As Bs : tlist) : tlist :=
  match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
  match xs with hnil => ys | hcons _ _ x xs => hcons x (happ xs ys) end.

Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
  match xs with hnil => () | hcons _ _ x _ => x end.
Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
  match xs with hnil => () | hcons _ _ _ xs => xs end.

Fixpoint hheads {As Bs} : hlist (tapp As Bs)  hlist As :=
  match As with
  | tnil => λ _, hnil
  | tcons A As => λ xs, hcons (hhead xs) (hheads (htail xs))
  end.
Fixpoint htails {As Bs} : hlist (tapp As Bs)  hlist Bs :=
  match As with
  | tnil => id
  | tcons A As => λ xs, htails (htail xs)
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
Fixpoint himpl (As : tlist) (B : Type) : Type :=
  match As with tnil => B | tcons A As => A  himpl As B end.

Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
37
38
Definition hinit {B} (y : B) : himpl tnil B := y.
Definition hlam {A As B} (f : A  himpl As B) : himpl (tcons A As) B := f.
Arguments hlam _ _ _ _ _/.

Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
41
42
43
  (fix go As xs :=
    match xs in hlist As return himpl As B  B with
    | hnil => λ f, f
    | hcons A As x xs => λ f, go As xs (f x)
    end) _ xs f.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
46
47
48
49
50
51
52
53
Coercion hcurry : himpl >-> Funclass.

Fixpoint huncurry {As B} : (hlist As  B)  himpl As B :=
  match As with
  | tnil => λ f, f hnil
  | tcons x xs => λ f, hlam (λ x, huncurry (f  hcons x))
  end.

Lemma hcurry_uncurry {As B} (f : hlist As  B) xs : huncurry f xs = f xs.
Proof. by induction xs as [|A As x xs IH]; simpl; rewrite ?IH. Qed.
54
55
56
57

Fixpoint hcompose {As B C} (f : B  C) {struct As} : himpl As B  himpl As C :=
  match As with
  | tnil => f
Robbert Krebbers's avatar
Robbert Krebbers committed
58
  | tcons A As => λ g, hlam (λ x, hcompose f (g x))
59
  end.