diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v index 2cbea3f72278e1e5832151c8786b71019d609b10..31cb222db7aa2b5497b5e3732b3b8a4462c9633a 100644 --- a/theories/proofmode/coq_tactics.v +++ b/theories/proofmode/coq_tactics.v @@ -791,12 +791,14 @@ Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) : (∀ a, Δ ⊢ ⌜φ a⌝) → Δ ⊢ ⌜∀ a, φ a⌝. Proof. intros. rewrite pure_forall. by apply forall_intro. Qed. -Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q x : +Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q : envs_lookup i Δ = Some (p, P) → IntoForall P Φ → - envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' → - (Δ' ⊢ Q) → Δ ⊢ Q. + (∃ x : A, + envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' ∧ + (Δ' ⊢ Q)) → + Δ ⊢ Q. Proof. - intros. rewrite envs_simple_replace_sound //; simpl. + intros ?? (x&?&?). rewrite envs_simple_replace_sound //; simpl. by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r. Qed. diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v index b1d0ffd9746445c09fb2402fb69aba2045f7dede..84f4d999de9809d819bf4477f35d4c6647fdc749 100644 --- a/theories/proofmode/tactics.v +++ b/theories/proofmode/tactics.v @@ -272,11 +272,11 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) := match xs with | hnil => idtac | hcons ?x ?xs => - eapply tac_forall_specialize with _ H _ _ _ x; (* (i:=H) (a:=x) *) + eapply tac_forall_specialize with _ H _ _ _; (* (i:=H) (a:=x) *) [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found" |let P := match goal with |- IntoForall ?P _ => P end in apply _ || fail 1 "iSpecialize: cannot instantiate" P "with" x - |env_cbv; reflexivity|go xs] + |exists x; split; [env_cbv; reflexivity|go xs]] end in go xs. diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v index 28e5da973fabe6091e337a04d4edacb6beae5eb7..459e3198d0c9f6228b709a77ba4734194ea28af0 100644 --- a/theories/tests/proofmode.v +++ b/theories/tests/proofmode.v @@ -120,3 +120,7 @@ Qed. Lemma demo_11 (M : ucmraT) (P Q R : uPred M) : (P -∗ True -∗ True -∗ Q -∗ R) -∗ P -∗ Q -∗ R. Proof. iIntros "H HP HQ". by iApply ("H" with "[HP]"). Qed. + +(* Check coercions *) +Lemma demo_12 (M : ucmraT) (P : Z → uPred M) : (∀ x, P x) -∗ ∃ x, P x. +Proof. iIntros "HP". iExists (0:nat). iApply ("HP" \$! (0:nat)). Qed.