hlist.v 2.11 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.prelude Require Import tactics.
2
Local Set Universe Polymorphism.
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4 5 6 7 8 9 10

(* 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
11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31
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
32 33 34
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
35 36 37 38 39
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
40 41 42 43 44
  (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
45 46 47 48 49 50 51 52 53 54
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.
55 56 57 58

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
59
  | tcons A As => λ g, hlam (λ x, hcompose f (g x))
60
  end.