From 91d50c60d2d773250b2379096323c8175b8ff1ae Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Jun 2016 22:13:16 +0200
Subject: [PATCH] More hlist stuff.

---
 algebra/upred_hlist.v |  4 ++--
 prelude/hlist.v       | 45 ++++++++++++++++++++++++++++++++++++-------
 proofmode/tactics.v   |  3 +--
 3 files changed, 41 insertions(+), 11 deletions(-)

diff --git a/algebra/upred_hlist.v b/algebra/upred_hlist.v
index ba779b523..82d0e55aa 100644
--- a/algebra/upred_hlist.v
+++ b/algebra/upred_hlist.v
@@ -25,7 +25,7 @@ Proof.
     + apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
       by rewrite -(exist_intro (hcons x xs)).
   - apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite -(exist_intro x).
+    by rewrite -(exist_intro x) IH.
 Qed.
 
 Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
@@ -33,7 +33,7 @@ Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
 Proof.
   apply (anti_symm _).
   - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite (forall_elim x).
+    by rewrite (forall_elim x) IH.
   - induction As as [|A As IH]; simpl.
     + by rewrite (forall_elim hnil) .
     + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
diff --git a/prelude/hlist.v b/prelude/hlist.v
index 7821ef941..8c888c732 100644
--- a/prelude/hlist.v
+++ b/prelude/hlist.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import base.
+From iris.prelude Require Import tactics.
 
 (* Not using [list Type] in order to avoid universe inconsistencies *)
 Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.
@@ -7,22 +7,53 @@ 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 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.
+
 Fixpoint himpl (As : tlist) (B : Type) : Type :=
   match As with tnil => B | tcons A As => A → himpl As B end.
 
-Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
+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 :=
   (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.
-Coercion happly : himpl >-> Funclass.
+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.
 
 Fixpoint hcompose {As B C} (f : B → C) {struct As} : himpl As B → himpl As C :=
   match As with
   | tnil => f
-  | tcons A As => λ g x, hcompose f (g x)
+  | tcons A As => λ g, hlam (λ x, hcompose f (g x))
   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.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 882c35f4c..21bd9cbab 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -11,7 +11,6 @@ Declare Reduction env_cbv := cbv [
   bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
   assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
   string_eq_dec string_rec string_rect (* strings *)
-  himpl happly
   env_persistent env_spatial envs_persistent
   envs_lookup envs_lookup_delete envs_delete envs_app
     envs_simple_replace envs_replace envs_split envs_clear_spatial].
@@ -135,7 +134,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
     eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
       [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
       |apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type"
-      |env_cbv; reflexivity|]
+      |cbn [himpl hcurry]; reflexivity|]
   end.
 
 Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
-- 
GitLab