Library stdpp.hlist

From stdpp Require Import tactics.
From stdpp Require Import options.
Local Set Universe Polymorphism.

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

Fixpoint tapp (As Bs : tlist) : tlist :=
  match As with tnilBs | tcons A Astcons A (tapp As Bs) end.
Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
  match xs with hnilys | hcons x xshcons x (happ xs ys) end.

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

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

Fixpoint himpl (As : tlist) (B : Type) : Type :=
  match As with tnilB | tcons A AsA himpl As B end.

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.
Global Arguments hlam _ _ _ _ _ / : assert.

Definition huncurry {As B} (f : himpl As B) (xs : hlist As) : B :=
  (fix go {As} xs :=
    match xs in hlist As return himpl As B B with
    | hnilλ f, f
    | hcons x xsλ f, go xs (f x)
    end) _ xs f.
Coercion huncurry : himpl >-> Funclass.

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

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

Fixpoint hcompose {As B C} (f : B C) {struct As} : himpl As B himpl As C :=
  match As with
  | tnilf
  | tcons A Asλ g, hlam (λ x, hcompose f (g x))