Merge remote-tracking branch 'origin/master' into gen_proofmode

theories/base_logic/lib/boxes.v

@@ -272,7 +272,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
-    iNext. iApply (internal_eq_rewrite_contractive with "[Heq] Hbox").
+    iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
   - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ -280,7 +280,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
-    iNext. iApply (internal_eq_rewrite_contractive with "[Heq] Hbox").
+    iNext. iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
 Qed.
 
@@ -297,14 +297,14 @@ Proof.
     iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
-    iApply (internal_eq_rewrite_contractive with "[Heq1 Heq2] Hbox").
+    iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
   - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
     iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
     iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
     iExists γ. iIntros "{$% $#} !>". iNext.
-    iApply (internal_eq_rewrite_contractive with "[Heq1 Heq2] Hbox").
+    iApply (internal_eq_rewrite_contractive _ _ (λ P, _) with "[Heq1 Heq2] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
 End box.

theories/bi/fixpoint.v

@@ -67,7 +67,7 @@ Section least.
 End least.
 
 Section greatest.
-  Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BIMonoPred F}.
+  Context {PROP : bi} {A : ofeT} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
   Global Instance greatest_fixpoint_ne : NonExpansive (bi_greatest_fixpoint F).
   Proof. solve_proper. Qed.

theories/proofmode/class_instances.v

@@ -224,10 +224,11 @@ Proof.
   rewrite /FromAssumption /IntoWand=> HP. by rewrite HP affinely_persistently_if_elim.
 Qed.
 
-Global Instance into_wand_impl_false_false `{!BiAffine PROP} P Q P' :
+Global Instance into_wand_impl_false_false P Q P' :
+  Absorbing P' → Absorbing (P' → Q) →
   FromAssumption false P P' → IntoWand false false (P' → Q) P Q.
 Proof.
-  rewrite /FromAssumption /IntoWand /= => ->. apply wand_intro_r.
+  rewrite /FromAssumption /IntoWand /= => ?? ->. apply wand_intro_r.
   by rewrite sep_and impl_elim_l.
 Qed.
 
@@ -264,6 +265,20 @@ Global Instance into_wand_and_r p q R1 R2 P' Q' :
   IntoWand p q R2 Q' P' → IntoWand p q (R1 ∧ R2) Q' P'.
 Proof. rewrite /IntoWand=> ?. by rewrite /bi_wand_iff and_elim_r. Qed.
 
+Global Instance into_wand_forall_prop_true p (φ : Prop) P :
+  IntoWand p true (∀ _ : φ, P) ⌜ φ ⌝ P.
+Proof.
+  rewrite /IntoWand (affinely_persistently_if_elim p) /=
+          -impl_wand_affinely_persistently -pure_impl_forall
+          bi.persistently_elim //.
+Qed.
+Global Instance into_wand_forall_prop_false p (φ : Prop) P :
+  Absorbing P → IntoWand p false (∀ _ : φ, P) ⌜ φ ⌝ P.
+Proof.
+  intros ?.
+  rewrite /IntoWand (affinely_persistently_if_elim p) /= pure_wand_forall //.
+Qed.
+
 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.
@@ -1016,6 +1031,18 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
 Global Instance into_forall_except_0 {A} P (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (◇ P) (λ a, ◇ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
+Global Instance into_forall_impl_pure φ P Q :
+  FromPureT P φ → IntoForall (P → Q) (λ _ : φ, Q).
+Proof.
+  rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]].
+  by rewrite pure_impl_forall.
+Qed.
+Global Instance into_forall_wand_pure φ P Q :
+  Absorbing Q → FromPureT P φ → IntoForall (P -∗ Q) (λ _ : φ, Q).
+Proof.
+  rewrite /FromPureT /FromPure /IntoForall=> ? -[φ' [-> <-]].
+  by rewrite pure_wand_forall.
+Qed.
 
 (* FromForall *)
 Global Instance from_forall_later {A} P (Φ : A → PROP) :

theories/proofmode/classes.v

@@ -49,6 +49,13 @@ Arguments FromPure {_} _%I _%type_scope : simpl never.
 Arguments from_pure {_} _%I _%type_scope {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
+Class FromPureT {PROP : bi} (P : PROP) (φ : Type) :=
+  from_pureT : ∃ ψ : Prop, φ = ψ ∧ FromPure P ψ.
+Lemma from_pureT_hint {PROP : bi} (P : PROP) (φ : Prop) : FromPure P φ → FromPureT P φ.
+Proof. by exists φ. Qed.
+Hint Extern 0 (FromPureT _ _) =>
+  notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.
+
 Class IntoInternalEq {PROP : bi} {A : ofeT} (P : PROP) (x y : A) :=
   into_internal_eq : P ⊢ x ≡ y.
 Arguments IntoInternalEq {_ _} _%I _%type_scope _%type_scope : simpl never.

theories/proofmode/tactics.v

@@ -433,8 +433,11 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
          |typeclasses eauto ||
           let P := match goal with |- IntoForall ?P _ => P end in
           fail "iSpecialize: cannot instantiate" P "with" x
-         |lazymatch goal with (* Force [A] in [ex_intro] to deal with coercions. *)
-          | |- ∃ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _))
+         |match goal with (* Force [A] in [ex_intro] to deal with coercions. *)
+          | |- ∃ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _)); [|]
+          (* If the existentially quantified predicate is non-dependent and [x]
+          is a hole, [refine] will generate an additional goal. *)
+          | |- ∃ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |]
           end; [env_reflexivity|go xs]]
     end in
   go xs.

theories/tests/proofmode.v

@@ -250,4 +250,47 @@ Lemma test_iAlways P Q R :
   □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_affinely (bi_affinely P)) ∗ □ Q.
 Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
 
+(* A bunch of test cases from #127 to establish that tactics behave the same on
+`⌜ φ ⌝ → P` and `∀ _ : φ, P` *)
+Lemma test_forall_nondep_1 (φ : Prop) :
+  φ → (∀ _ : φ, False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
+Lemma test_forall_nondep_2 (φ : Prop) :
+  φ → (∀ _ : φ, False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
+Lemma test_forall_nondep_3 (φ : Prop) :
+  φ → (∀ _ : φ, False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
+Lemma test_forall_nondep_4 (φ : Prop) :
+  φ → (∀ _ : φ, False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.
+
+Lemma test_pure_impl_1 (φ : Prop) :
+  φ → (⌜φ⌝ → False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
+Lemma test_pure_impl_2 (φ : Prop) :
+  φ → (⌜φ⌝ → False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
+Lemma test_pure_impl_3 (φ : Prop) :
+  φ → (⌜φ⌝ → False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
+Lemma test_pure_impl_4 (φ : Prop) :
+  φ → (⌜φ⌝ → False : PROP) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.
+
+Lemma test_forall_nondep_impl2 (φ : Prop) P :
+  φ → P -∗ (∀ _ : φ, P -∗ False : PROP) -∗ False.
+Proof.
+  iIntros (Hφ) "HP Hφ".
+  Fail iSpecialize ("Hφ" with "HP").
+  iSpecialize ("Hφ" with "[% //] HP"). done.
+Qed.
+
+Lemma test_pure_impl2 (φ : Prop) P :
+  φ → P -∗ (⌜φ⌝ → P -∗ False : PROP) -∗ False.
+Proof.
+  iIntros (Hφ) "HP Hφ".
+  Fail iSpecialize ("Hφ" with "HP").
+  iSpecialize ("Hφ" with "[% //] HP"). done.
+Qed.
 End tests.