From 6d15cf3916de8b77bd61d28d98f3dab1fa6884ba Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 9 Jun 2018 11:55:17 +0200
Subject: [PATCH] add general telescopes and telescopic BI binders and
 proofmode support

---
 _CoqProject                             |  1 +
 tests/telescopes.ref                    | 25 ++++++++
 tests/telescopes.v                      | 49 +++++++++++++++
 theories/bi/telescopes.v                | 82 +++++++++++++++++++++++++
 theories/proofmode/class_instances_bi.v | 19 +++++-
 theories/proofmode/ltac_tactics.v       |  5 +-
 theories/proofmode/reduction.v          |  6 +-
 7 files changed, 182 insertions(+), 5 deletions(-)
 create mode 100644 tests/telescopes.ref
 create mode 100644 tests/telescopes.v
 create mode 100644 theories/bi/telescopes.v

diff --git a/_CoqProject b/_CoqProject
index f404e380b..92fc6bd86 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,6 +39,7 @@ theories/bi/tactics.v
 theories/bi/monpred.v
 theories/bi/embedding.v
 theories/bi/weakestpre.v
+theories/bi/telescopes.v
 theories/bi/lib/counter_examples.v
 theories/bi/lib/fixpoint.v
 theories/bi/lib/fractional.v
diff --git a/tests/telescopes.ref b/tests/telescopes.ref
new file mode 100644
index 000000000..d6074925d
--- /dev/null
+++ b/tests/telescopes.ref
@@ -0,0 +1,25 @@
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  X : tele
+  E1, E2 : coPset
+  α, β, γ1, γ2 : X → PROP
+  x' : X
+  ============================
+  "Hγ12" : ∀.. x : X, γ1 x -∗ γ2 x
+  "Hα" : α x'
+  "Hclose" : β x' ={E2,E1}=∗ γ1 x'
+  --------------------------------------∗
+  |={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
+  
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  E1, E2 : coPset
+  ============================
+  "H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝ ∗ (True ={E2,E1}=∗ <affine> ⌜x ≠ x0⌝)
+  --------------------------------------∗
+  |={E2,E1}=> False
+  
diff --git a/tests/telescopes.v b/tests/telescopes.v
new file mode 100644
index 000000000..3313b38c8
--- /dev/null
+++ b/tests/telescopes.v
@@ -0,0 +1,49 @@
+From stdpp Require Import coPset namespaces.
+From iris.proofmode Require Import tactics.
+Set Default Proof Using "Type".
+
+(* Just playing around a bit with a telescope version
+   of accessors with just one binder list. *)
+Definition accessor `{!BiFUpd PROP} {X : tele} (E1 E2 : coPset)
+           (α β γ : X → PROP) : PROP :=
+  (|={E1,E2}=> ∃.. x, α x ∗ (β x -∗ |={E2,E1}=> (γ x)))%I.
+
+Notation "'ACC' @ E1 , E2 {{ ∃ x1 .. xn , α | β | γ } }" :=
+  (accessor (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            E1 E2
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => α%I) ..)
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => β%I) ..)
+            (tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
+                      fun x1 => .. (fun xn => γ%I) ..))
+  (at level 20, α, β, γ at level 200, x1 binder, xn binder, only parsing).
+
+(* Working with abstract telescopes. *)
+Section tests.
+Context `{!BiFUpd PROP} {X : tele}.
+Implicit Types α β γ : X → PROP.
+
+Lemma acc_mono E1 E2 α β γ1 γ2 :
+  (∀.. x, γ1 x -∗ γ2 x) -∗
+  accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β γ2.
+Proof.
+  iIntros "Hγ12 >Hacc". iDestruct "Hacc" as (x') "[Hα Hclose]". Show.
+  iModIntro. iExists x'. iFrame. iIntros "Hβ".
+  iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
+Qed.
+End tests.
+
+Section printing_tests.
+Context `{!BiFUpd PROP}.
+
+(* Working with concrete telescopes: Testing the reduction into normal quantifiers. *)
+Lemma acc_elim_test_1 E1 E2 :
+  ACC @ E1, E2 {{ ∃ a b : nat, <affine> ⌜a = b⌝ | True | <affine> ⌜a ≠ b⌝ }}
+    ⊢@{PROP} |={E1}=> False.
+Proof.
+  iIntros ">H". Show.
+  iDestruct "H" as (a b) "[% Hclose]". iMod ("Hclose" with "[//]") as "%".
+  done.
+Qed.
+End printing_tests.
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
new file mode 100644
index 000000000..554cd0b27
--- /dev/null
+++ b/theories/bi/telescopes.v
@@ -0,0 +1,82 @@
+From stdpp Require Export telescopes.
+From iris.bi Require Export bi.
+Set Default Proof Using "Type*".
+Import bi.
+
+(* This cannot import the proofmode because it is imported by the proofmode! *)
+
+(** Telescopic quantifiers *)
+Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
+  tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
+Arguments bi_texist {_ !_} _ /.
+Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
+  tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
+Arguments bi_tforall {_ !_} _ /.
+
+Notation "'∃..' x .. y , P" := (bi_texist (λ x, .. (bi_texist (λ y, P)) .. )%I)
+  (at level 200, x binder, y binder, right associativity,
+  format "∃..  x  ..  y ,  P") : bi_scope.
+Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) .. )%I)
+  (at level 200, x binder, y binder, right associativity,
+  format "∀..  x  ..  y ,  P") : bi_scope.
+
+Section telescope_quantifiers.
+  Context {PROP : bi} {TT : tele}.
+
+  Lemma bi_tforall_forall (Ψ : TT -> PROP) :
+    (bi_tforall Ψ) ⊣⊢ (bi_forall Ψ).
+  Proof.
+    symmetry. unfold bi_tforall. induction TT as [|X ft IH].
+    - simpl. apply (anti_symm _).
+      + by rewrite (forall_elim TargO).
+      + rewrite -forall_intro; first done.
+        intros p. rewrite (tele_arg_O_inv p) /= //.
+    - simpl. apply (anti_symm _); apply forall_intro; intros a.
+      + rewrite /= -IH. apply forall_intro; intros p.
+        by rewrite (forall_elim (TargS a p)).
+      + move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
+        setoid_rewrite <- IH.
+        do 2 rewrite forall_elim. done.
+  Qed.
+
+  Lemma bi_texist_exist (Ψ : TT -> PROP) :
+    (bi_texist Ψ) ⊣⊢ (bi_exist Ψ).
+  Proof.
+    symmetry. unfold bi_texist. induction TT as [|X ft IH].
+    - simpl. apply (anti_symm _).
+      + apply exist_elim; intros p.
+        rewrite (tele_arg_O_inv p) //.
+      + by rewrite -(exist_intro TargO).
+    - simpl. apply (anti_symm _); apply exist_elim.
+      + intros p. move/tele_arg_inv: (p) => [x [pf ->]] {p} /=.
+        by rewrite -exist_intro -IH -exist_intro.
+      + intros x.
+        rewrite /= -IH. apply exist_elim; intros p.
+        by rewrite -(exist_intro (TargS x p)).
+  Qed.
+
+  Global Instance bi_tforall_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
+  Qed.
+
+  Global Instance bi_tforall_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_tforall PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
+  Qed.
+
+  Global Instance bi_texist_ne n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
+  Qed.
+
+  Global Instance bi_texist_proper :
+    Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@bi_texist PROP TT).
+  Proof.
+    intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
+  Qed.
+
+End telescope_quantifiers.
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 44110484a..0c8a785b1 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -1,5 +1,5 @@
 From stdpp Require Import nat_cancel.
-From iris.bi Require Import bi tactics.
+From iris.bi Require Import bi tactics telescopes.
 From iris.proofmode Require Import base modality_instances classes ltac_tactics.
 Set Default Proof Using "Type".
 Import bi.
@@ -413,6 +413,10 @@ Global Instance into_wand_forall {A} p q (Φ : A → PROP) P Q x :
   IntoWand p q (Φ x) P Q → IntoWand p q (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. by rewrite (forall_elim x). Qed.
 
+Global Instance into_wand_tforall {A} p q (Φ : tele_arg A → PROP) P Q x :
+  IntoWand p q (Φ x) P Q → IntoWand p q (∀.. x, Φ x) P Q.
+Proof. rewrite /IntoWand=> <-. by rewrite bi_tforall_forall (forall_elim x). Qed.
+
 Global Instance into_wand_affine p q R P Q :
   IntoWand p q R P Q → IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
 Proof.
@@ -841,8 +845,11 @@ Global Instance into_or_embed `{BiEmbed PROP PROP'} P Q1 Q2 :
 Proof. by rewrite /IntoOr -embed_or => <-. Qed.
 
 (** FromExist *)
-Global Instance from_exist_exist {A} (Φ : A → PROP): FromExist (∃ a, Φ a) Φ.
+Global Instance from_exist_exist {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
 Proof. by rewrite /FromExist. Qed.
+Global Instance from_exist_texist {A} (Φ : tele_arg A → PROP) :
+  FromExist (∃.. a, Φ a) Φ.
+Proof. by rewrite /FromExist bi_texist_exist. Qed.
 Global Instance from_exist_pure {A} (φ : A → Prop) :
   @FromExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /FromExist pure_exist. Qed.
@@ -871,6 +878,9 @@ Qed.
 (** IntoExist *)
 Global Instance into_exist_exist {A} (Φ : A → PROP) : IntoExist (∃ a, Φ a) Φ.
 Proof. by rewrite /IntoExist. Qed.
+Global Instance into_exist_texist {A} (Φ : tele_arg A → PROP) :
+  IntoExist (∃.. a, Φ a) Φ.
+Proof. by rewrite /IntoExist bi_texist_exist. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
 Proof. by rewrite /IntoExist pure_exist. Qed.
@@ -906,6 +916,8 @@ Proof. by rewrite /IntoExist -embed_exist => <-. Qed.
 (** IntoForall *)
 Global Instance into_forall_forall {A} (Φ : A → PROP) : IntoForall (∀ a, Φ a) Φ.
 Proof. by rewrite /IntoForall. Qed.
+Global Instance into_forall_tforall {A} (Φ : tele_arg A → PROP) : IntoForall (∀.. a, Φ a) Φ.
+Proof. by rewrite /IntoForall bi_tforall_forall. Qed.
 Global Instance into_forall_affinely {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (<affine> P) (λ a, <affine> (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP affinely_forall. Qed.
@@ -946,6 +958,9 @@ Proof. rewrite /IntoForall. apply forall_intro=><-. rewrite -True_emp True_impl
 Global Instance from_forall_forall {A} (Φ : A → PROP) :
   FromForall (∀ x, Φ x)%I Φ.
 Proof. by rewrite /FromForall. Qed.
+Global Instance from_forall_tforall {A} (Φ : tele_arg A → PROP) :
+  FromForall (∀.. x, Φ x)%I Φ.
+Proof. by rewrite /FromForall bi_tforall_forall. Qed.
 Global Instance from_forall_pure {A} (φ : A → Prop) :
   @FromForall PROP A (⌜∀ a : A, φ a⌝)%I (λ a, ⌜ φ a ⌝)%I.
 Proof. by rewrite /FromForall pure_forall. Qed.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 7738772f8..d82ef1bf0 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
-From iris.bi Require Export bi.
+From iris.bi Require Export bi telescopes.
 From stdpp Require Import namespaces.
 From iris.proofmode Require Export classes notation.
 From stdpp Require Import hlist pretty.
@@ -2193,6 +2193,8 @@ Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
 Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros.
 Hint Extern 0 (envs_entails _ (_ → _)) => iIntros.
 Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros.
+(* Multi-intro doesn't work for custom binders. *)
+Hint Extern 0 (envs_entails _ (∀.. _, _)) => iIntros (?).
 
 Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit.
 Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit.
@@ -2202,6 +2204,7 @@ Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways.
 Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways.
 Hint Extern 1 (envs_entails _ (â–¡ _)) => iAlways.
 Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.
+Hint Extern 1 (envs_entails _ (∃.. _, _)) => iExists _.
 Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft.
 Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 7aac9f5e3..839bd78da 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -1,4 +1,4 @@
-From iris.bi Require Import bi.
+From iris.bi Require Import bi telescopes.
 From iris.proofmode Require Import base environments.
 
 Declare Reduction pm_cbv := cbv [
@@ -18,9 +18,11 @@ Declare Reduction pm_cbv := cbv [
 Declare Reduction pm_cbn := cbn [
   (* PM option combinators *)
   pm_option_bind pm_from_option pm_option_fun
+  (* telescope combinators *)
+  tele_fold tele_bind tele_app
   (* BI connectives *)
   bi_persistently_if bi_affinely_if bi_intuitionistically_if
-  bi_wandM
+  bi_wandM bi_tforall bi_texist
 ].
 Ltac pm_eval t :=
   let u := eval pm_cbv in t in
-- 
GitLab