Merge branch 'robbert/issue127' into 'master'

Consistent handling of pure implication and forall

Closes #127

See merge request FP/iris-coq!104

theories/proofmode/class_instances.v

@@ -327,6 +327,13 @@ Global Instance into_wand_iff_r p P P' Q Q' :
   WandWeaken p Q P Q' P' → IntoWand p (P ↔ Q) Q' P'.
 Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand_1. Qed.
 
+Global Instance into_wand_forall_prop p (φ : Prop) P :
+  IntoWand p (∀ _ : φ, P) ⌜ φ ⌝ P.
+Proof.
+  rewrite /FromAssumption /IntoWand persistently_if_pure -pure_impl_forall.
+  by apply impl_wand_1.
+Qed.
+
 Global Instance into_wand_forall {A} p (Φ : A → uPred M) P Q x :
   IntoWand p (Φ x) P Q → IntoWand p (∀ x, Φ x) P Q.
 Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
@@ -775,6 +782,18 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP later_forall. Qed.
 Global Instance into_forall_except_0 {A} P (Φ : A → uPred M) :
   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 :
+  FromPureT P φ → IntoForall (P -∗ Q) (λ _ : φ, Q).
+Proof.
+  rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]].
+  by rewrite -pure_impl_forall -impl_wand.
+Qed.
 
 (* FromForall *)
 Global Instance from_forall_forall {A} (Φ : A → uPred M) :

theories/proofmode/classes.v

@@ -54,6 +54,13 @@ Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
 Arguments from_pure {_} _ _ {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
+Class FromPureT {M} (P : uPred M) (φ : Type) :=
+  from_pureT : ∃ ψ : Prop, φ = ψ ∧ FromPure P ψ.
+Lemma from_pureT_hint {M} (P : uPred M) (φ : Prop) : FromPure P φ → FromPureT P φ.
+Proof. by exists φ. Qed.
+Hint Extern 0 (FromPureT _ _) =>
+  notypeclasses refine (from_pureT_hint _ _ _) : typeclass_instances.
+
 Class IntoInternalEq {M} {A : ofeT} (P : uPred M) (x y : A) :=
   into_internal_eq : P ⊢ x ≡ y.
 Arguments into_internal_eq {_ _} _ _ _ {_}.

theories/proofmode/tactics.v

@@ -396,8 +396,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

@@ -234,6 +234,50 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. 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 : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
+Lemma test_forall_nondep_2 (φ : Prop) :
+  φ → (∀ _ : φ, False : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
+Lemma test_forall_nondep_3 (φ : Prop) :
+  φ → (∀ _ : φ, False : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
+Lemma test_forall_nondep_4 (φ : Prop) :
+  φ → (∀ _ : φ, False : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ); done. Qed.
+
+Lemma test_pure_impl_1 (φ : Prop) :
+  φ → (⌜φ⌝ → False : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". by iApply "Hφ". Qed.
+Lemma test_pure_impl_2 (φ : Prop) :
+  φ → (⌜φ⌝ → False : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" with "[% //]"). done. Qed.
+Lemma test_pure_impl_3 (φ : Prop) :
+  φ → (⌜φ⌝ → False : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". unshelve iSpecialize ("Hφ" $! _). done. done. Qed.
+Lemma test_pure_impl_4 (φ : Prop) :
+  φ → (⌜φ⌝ → False : uPred M) -∗ False.
+Proof. iIntros (Hφ) "Hφ". iSpecialize ("Hφ" $! Hφ). done. Qed.
+
+Lemma test_forall_nondep_impl2 (φ : Prop) P :
+  φ → P -∗ (∀ _ : φ, P -∗ False : uPred M) -∗ 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 : uPred M) -∗ False.
+Proof.
+  iIntros (Hφ) "HP Hφ".
+  Fail iSpecialize ("Hφ" with "HP").
+  iSpecialize ("Hφ" with "[% //] HP"). done.
+Qed.
+
 (* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
 8.6 support. See also issue #108. *)
 (*