test and fix more telescope normalization

tests/telescopes.ref

@@ -23,3 +23,71 @@
   --------------------------------------∗
   |={E2,E1}=> False
   
+"test1_test"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  ▷ False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  ▷ False
+  
+"test2_test"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  ============================
+  "H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ▷ (∃ x0 : nat, <affine> ⌜x = x0⌝)
+  --------------------------------------∗
+  ▷ False
+  
+"test3_test"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
+  --------------------------------------∗
+  ▷ False
+  
+1 subgoal
+  
+  PROP : sbi
+  x : nat
+  ============================
+  "H" : ◇ (∃ x0 : nat, <affine> ⌜x = x0⌝)
+  --------------------------------------∗
+  ▷ False
+  

tests/telescopes.v

@@ -2,6 +2,7 @@ From stdpp Require Import coPset namespaces.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
+Section accessor.
 (* 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)
@@ -47,3 +48,66 @@ Proof.
   done.
 Qed.
 End printing_tests.
+End accessor.
+
+(* Robbert's tests *)
+Section telescopes_and_tactics.
+
+Definition test1 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+  (∃.. x, α x)%I.
+
+Notation "'TEST1' {{ ∃ x1 .. xn , α } }" :=
+  (test1 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            (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).
+
+Definition test2 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+  (▷ ∃.. x, α x)%I.
+
+Notation "'TEST2' {{ ∃ x1 .. xn , α } }" :=
+  (test2 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            (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).
+
+Definition test3 {PROP : sbi} {X : tele} (α : X → PROP) : PROP :=
+  (◇ ∃.. x, α x)%I.
+
+Notation "'TEST3' {{ ∃ x1 .. xn , α } }" :=
+  (test3 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
+            (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).
+
+Check "test1_test".
+Lemma test1_test {PROP : sbi}  :
+  TEST1 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
+Proof.
+  iIntros "H". iDestruct "H" as (x) "H". Show.
+Restart.
+  iIntros "H". unfold test1. iDestruct "H" as (x) "H". Show.
+Abort.
+
+Check "test2_test".
+Lemma test2_test {PROP : sbi}  :
+  TEST2 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
+Proof.
+  iIntros "H". iModIntro. Show.
+  iDestruct "H" as (x) "H". Show.
+Restart.
+  iIntros "H". iDestruct "H" as (x) "H". Show.
+Abort.
+
+Check "test3_test".
+Lemma test3_test {PROP : sbi}  :
+  TEST3 {{ ∃ a b : nat, <affine> ⌜a = b⌝ }} ⊢@{PROP} ▷ False.
+Proof.
+  iIntros "H". iMod "H".
+  iDestruct "H" as (x) "H".
+  Show.
+Restart.
+  iIntros "H". iDestruct "H" as (x) "H". Show.
+Abort.
+
+End telescopes_and_tactics.

theories/proofmode/class_instances_bi.v

@@ -879,7 +879,7 @@ Qed.
 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) Φ.
+  IntoExist (∃.. a, Φ a) Φ | 10.
 Proof. by rewrite /IntoExist bi_texist_exist. Qed.
 Global Instance into_exist_pure {A} (φ : A → Prop) :
   @IntoExist PROP A ⌜∃ x, φ x⌝ (λ a, ⌜φ a⌝)%I.
@@ -916,7 +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) Φ.
+Global Instance into_forall_tforall {A} (Φ : tele_arg A → PROP) :
+  IntoForall (∀.. a, Φ a) Φ | 10.
 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.

theories/proofmode/ltac_tactics.v

@@ -811,7 +811,8 @@ Tactic Notation "iApplyHyp" constr(H) :=
     [eapply tac_apply with _ H _ _ _;
       [pm_reflexivity
       |iSolveTC
-      |pm_reduce (* reduce redexes created by instantiation *)]
+      |pm_prettify (* reduce redexes created by instantiation *)
+      ]
     |iSpecializePat H "[]"; last go H] in
   iExact H ||
   go H ||
@@ -1058,7 +1059,8 @@ Tactic Notation "iModIntro" uconstr(sel) :=
      end
     |pm_reduce; iSolveTC ||
      fail "iModIntro: cannot filter spatial context when goal is not absorbing"
-    |].
+    |pm_prettify (* reduce redexes created by instantiation *)
+    ].
 Tactic Notation "iModIntro" := iModIntro _.
 Tactic Notation "iAlways" := iModIntro.
 

theories/proofmode/reduction.v

@@ -31,3 +31,8 @@ Ltac pm_eval t :=
 Ltac pm_reduce :=
   match goal with |- ?u => let v := pm_eval u in change v end.
 Ltac pm_reflexivity := pm_reduce; exact eq_refl.
+
+(** Called e.g. by iApply for redexes that are created by instantiation.
+    This cannot create any envs redexes so we just to the cbn part. *)
+Ltac pm_prettify :=
+  match goal with |- ?u => let v := eval pm_cbn in u in change v end.