Commit 37675f7b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Make iPureIntro also work with uPred_valid and uPred_eq.

parent 677c3e3a
...@@ -292,10 +292,7 @@ Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q. ...@@ -292,10 +292,7 @@ Lemma tac_ex_falso Δ Q : Δ ⊢ False → Δ ⊢ Q.
Proof. by rewrite -(False_elim Q). Qed. Proof. by rewrite -(False_elim Q). Qed.
(** * Pure *) (** * Pure *)
Lemma tac_pure_intro Δ (φ : Prop) : φ Δ φ. Class ToPure (P : uPred M) (φ : Prop) := to_pure : P φ.
Proof. apply const_intro. Qed.
Class ToPure (P : uPred M) (φ : Prop) := to_pure : P φ.
Arguments to_pure : clear implicits. Arguments to_pure : clear implicits.
Global Instance to_pure_const φ : ToPure ( φ) φ. Global Instance to_pure_const φ : ToPure ( φ) φ.
Proof. done. Qed. Proof. done. Qed.
...@@ -305,6 +302,9 @@ Proof. intros; red. by rewrite timeless_eq. Qed. ...@@ -305,6 +302,9 @@ Proof. intros; red. by rewrite timeless_eq. Qed.
Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure ( a) ( a). Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure ( a) ( a).
Proof. intros; red. by rewrite discrete_valid. Qed. Proof. intros; red. by rewrite discrete_valid. Qed.
Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ φ Δ Q.
Proof. intros ->. apply const_intro. Qed.
Lemma tac_pure Δ Δ' i p P φ Q : Lemma tac_pure Δ Δ' i p P φ Q :
envs_lookup_delete i Δ = Some (p, P, Δ') ToPure P φ envs_lookup_delete i Δ = Some (p, P, Δ') ToPure P φ
(φ Δ' Q) Δ Q. (φ Δ' Q) Δ Q.
......
...@@ -113,7 +113,10 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := ...@@ -113,7 +113,10 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
apply _ || fail "iPure:" H ":" P "not pure" apply _ || fail "iPure:" H ":" P "not pure"
|intros pat]. |intros pat].
Tactic Notation "iPureIntro" := apply uPred.const_intro. Tactic Notation "iPureIntro" :=
eapply tac_pure_intro;
[let P := match goal with |- ToPure ?P _ => P end in
apply _ || fail "iPureIntro:" P "not pure"|].
(** * Specialize *) (** * Specialize *)
Record iTrm {X As} := Record iTrm {X As} :=
...@@ -751,5 +754,5 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) := ...@@ -751,5 +754,5 @@ Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
iRewriteCore true t in H. iRewriteCore true t in H.
(* Make sure that by and done solve trivial things in proof mode *) (* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (of_envs _ _) => by apply tac_pure_intro. Hint Extern 0 (of_envs _ _) => by iPureIntro.
Hint Extern 0 (of_envs _ _) => iAssumption. Hint Extern 0 (of_envs _ _) => iAssumption.
...@@ -72,9 +72,10 @@ Proof. ...@@ -72,9 +72,10 @@ Proof.
Qed. Qed.
Lemma demo_6 (M : cmraT) (P Q : uPred M) : Lemma demo_6 (M : cmraT) (P Q : uPred M) :
True ( x y z, x = 0 y = 0 z = 0 P Q foo False). True ( x y z : nat,
x = plus 0 x y = 0 z = 0 P Q foo (x x)).
Proof. Proof.
iIntros {a} "*". iIntros {a} "*".
iIntros "#Hfoo **". iIntros "#Hfoo **".
by iIntros "%". by iIntros "# _".
Qed. Qed.
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