Commit fe99f874 authored by Robbert Krebbers's avatar Robbert Krebbers

Move tac_exist from classes to coq_tactics where it belongs.

parent 97e8a9de
...@@ -301,10 +301,6 @@ Global Arguments from_exist {_} _ _ {_}. ...@@ -301,10 +301,6 @@ Global Arguments from_exist {_} _ _ {_}.
Global Instance from_exist_exist {A} (Φ: A uPred M): FromExist ( a, Φ a) Φ. Global Instance from_exist_exist {A} (Φ: A uPred M): FromExist ( a, Φ a) Φ.
Proof. done. Qed. 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) := Class IntoExist {A} (P : uPred M) (Φ : A uPred M) :=
into_exist : P x, Φ x. into_exist : P x, Φ x.
Global Arguments into_exist {_} _ _ {_}. Global Arguments into_exist {_} _ _ {_}.
......
...@@ -719,6 +719,10 @@ Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) : ...@@ -719,6 +719,10 @@ Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed. Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
(** * Existential *) (** * 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 : Lemma tac_exist_destruct {A} Δ i p j P (Φ : A uPred M) Q :
envs_lookup i Δ = Some (p, P) IntoExist P Φ envs_lookup i Δ = Some (p, P) IntoExist P Φ
( a, Δ', ( a, Δ',
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment