diff --git a/proofmode/classes.v b/proofmode/classes.v index b84436e8ef4529a1b40bdb29c11142facd3c44af..a88e3daf7589a50410093919cddc839a0d754576 100644 --- a/proofmode/classes.v +++ b/proofmode/classes.v @@ -301,10 +301,6 @@ Global Arguments from_exist {_} _ _ {_}. Global Instance from_exist_exist {A} (Φ: A → uPred M): FromExist (∃ a, Φ a) Φ. Proof. done. Qed. -Lemma tac_exist {A} Δ P (Φ : A → uPred M) : - FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P. -Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed. - Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) := into_exist : P ⊢ ∃ x, Φ x. Global Arguments into_exist {_} _ _ {_}. diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v index 311a4d0ce2b143ed8934463438206045f17d5245..1ac516bbdb8313132fb8a765750b5d36be08700b 100644 --- a/proofmode/coq_tactics.v +++ b/proofmode/coq_tactics.v @@ -719,6 +719,10 @@ Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) : Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed. (** * Existential *) +Lemma tac_exist {A} Δ P (Φ : A → uPred M) : + FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P. +Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed. + Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q : envs_lookup i Δ = Some (p, P) → IntoExist P Φ → (∀ a, ∃ Δ',