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
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) :=
Ralf Jung's avatar
Ralf Jung committed
17
  match xs with hnil => ys | hcons x xs => hcons x (happ xs ys) end.
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19

Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
Ralf Jung's avatar
Ralf Jung committed
20
  match xs with hnil => () | hcons x _ => x end.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
Ralf Jung's avatar
Ralf Jung committed
22
  match xs with hnil => () | hcons _ xs => xs end.
Robbert Krebbers's avatar
Robbert Krebbers committed
23 24 25 26 27 28 29 30 31 32 33 34

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
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.
40
Arguments hlam _ _ _ _ _ / : assert.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42

Definition hcurry {As B} (f : himpl As B) (xs : hlist As) : B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45
  (fix go As xs :=
    match xs in hlist As return himpl As B  B with
    | hnil => λ f, f
Ralf Jung's avatar
Ralf Jung committed
46
    | @hcons A As x xs => λ f, go As xs (f x)
Robbert Krebbers's avatar
Robbert Krebbers committed
47
    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.