More heterogeneous list stuff.

_CoqProject

@@ -53,6 +53,7 @@ algebra/iprod.v
 algebra/upred.v
 algebra/upred_tactics.v
 algebra/upred_big_op.v
+algebra/upred_hlist.v
 algebra/frac.v
 algebra/csum.v
 algebra/list.v

algebra/upred_hlist.v

+From iris.prelude Require Export hlist.
+From iris.algebra Require Export upred.
+Import uPred.
+
+Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
+  match As return himpl As (uPred M) → uPred M with
+  | tnil => id
+  | tcons A As => λ Φ, ∃ x, uPred_hexist (Φ x)
+  end%I.
+Fixpoint uPred_hforall {M As} : himpl As (uPred M) → uPred M :=
+  match As return himpl As (uPred M) → uPred M with
+  | tnil => id
+  | tcons A As => λ Φ, ∀ x, uPred_hforall (Φ x)
+  end%I.
+
+Section hlist.
+Context {M : ucmraT}.
+
+Lemma hexist_exist {As B} (f : himpl As B) (Φ : B → uPred M) :
+  uPred_hexist (hcompose Φ f) ⊣⊢ ∃ xs : hlist As, Φ (f xs).
+Proof.
+  apply (anti_symm _).
+  - induction As as [|A As IH]; simpl.
+    + by rewrite -(exist_intro hnil) .
+    + 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).
+Qed.
+
+Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
+  uPred_hforall (hcompose Φ f) ⊣⊢ ∀ xs : hlist As, Φ (f xs).
+Proof.
+  apply (anti_symm _).
+  - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
+    by rewrite (forall_elim x).
+  - induction As as [|A As IH]; simpl.
+    + by rewrite (forall_elim hnil) .
+    + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
+      by rewrite (forall_elim (hcons x xs)).
+Qed.
+End hlist.

prelude/hlist.v

@@ -16,3 +16,13 @@ Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
     | hnil => λ f, f
     | hcons A As x xs => λ f, go As xs (f x)
     end) _ xs f.
+Coercion happly : himpl >-> Funclass.
+
+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)
+  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.

proofmode/coq_tactics.v

@@ -895,8 +895,7 @@ Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ
 Proof. apply forall_intro. Qed.
 
 Class ForallSpecialize {As} (xs : hlist As)
-    (P : uPred M) (Φ : himpl As (uPred M)) :=
-  forall_specialize : P ⊢ happly Φ xs.
+  (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P ⊢ Φ xs.
 Arguments forall_specialize {_} _ _ _ {_}.
 
 Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
@@ -908,7 +907,7 @@ Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
 
 Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
   envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ →
-  envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' →
+  envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.