hlist.v 2.25 KB
Newer Older
1 2
(* Copyright (c) 2012-2017, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From stdpp Require Import tactics.
4
Set Default Proof Using "Type".
5
Local Set Universe Polymorphism.
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11 12 13

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

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