Commit ec4ac846 authored by Robbert Krebbers's avatar Robbert Krebbers

Allow introduction patterns for result of `iCombine`.

This fixes issue #187.
parent 2c759645
...@@ -108,8 +108,8 @@ Separating logic specific tactics ...@@ -108,8 +108,8 @@ Separating logic specific tactics
This tactic finishes the goal in case everything in the conclusion has been This tactic finishes the goal in case everything in the conclusion has been
framed. framed.
- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into - `iCombine "H1" "H2" as "pat"` : turns `H1 : P1` and `H2 : P2` into
`H : P1 ∗ P2`. `P1 ∗ P2`, on which `iDetruct ... as pat` is called.
Modalities Modalities
---------- ----------
......
...@@ -395,9 +395,14 @@ Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed. ...@@ -395,9 +395,14 @@ Proof. by rewrite /IntoWand /= intuitionistically_persistently_elim. Qed.
Global Instance into_wand_persistently_false q R P Q : Global Instance into_wand_persistently_false q R P Q :
Absorbing R IntoWand false q R P Q IntoWand false q (<pers> R) P Q. Absorbing R IntoWand false q R P Q IntoWand false q (<pers> R) P Q.
Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed. Proof. intros ?. by rewrite /IntoWand persistently_elim. Qed.
Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q R P Q : Global Instance into_wand_embed `{BiEmbed PROP PROP'} p q (PP QQ RR : PROP) (P : PROP') :
IntoWand p q R P Q IntoWand p q R P Q. IntoEmbed P PP
Proof. by rewrite /IntoWand !embed_intuitionistically_if_2 -embed_wand=> ->. Qed. IntoWand p q RR PP QQ IntoWand p q RR P QQ.
Proof.
rewrite /IntoEmbed /IntoWand !embed_intuitionistically_if_2=> -> ->.
apply bi.wand_intro_l.
by rewrite embed_intuitionistically_if_2 -embed_sep bi.wand_elim_r.
Qed.
(* FromWand *) (* FromWand *)
Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2. Global Instance from_wand_wand P1 P2 : FromWand (P1 - P2) P1 P2.
...@@ -880,4 +885,7 @@ Qed. ...@@ -880,4 +885,7 @@ Qed.
Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P : Global Instance into_embed_embed {PROP' : bi} `{BiEmbed PROP PROP'} P :
IntoEmbed P P. IntoEmbed P P.
Proof. by rewrite /IntoEmbed. Qed. Proof. by rewrite /IntoEmbed. Qed.
Global Instance into_embed_affinely `{BiEmbedBUpd PROP PROP'} (P : PROP') (Q : PROP) :
IntoEmbed P Q IntoEmbed (<affine> P) (<affine> Q).
Proof. rewrite /IntoEmbed=> ->. by rewrite embed_affinely_2. Qed.
End bi_instances. End bi_instances.
...@@ -927,20 +927,6 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') : ...@@ -927,20 +927,6 @@ Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :
fail "iAndDestructChoice: cannot destruct" P fail "iAndDestructChoice: cannot destruct" P
|env_reflexivity || fail "iAndDestructChoice:" H' " not fresh"|]. |env_reflexivity || fail "iAndDestructChoice:" H' " not fresh"|].
(** * Combinining hypotheses *)
Tactic Notation "iCombine" constr(Hs) "as" constr(H) :=
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
eapply tac_combine with _ _ Hs _ _ H _;
[env_reflexivity ||
let Hs := iMissingHyps Hs in
fail "iCombine: hypotheses" Hs "not found"
|iSolveTC
|env_reflexivity || fail "iCombine:" H "not fresh"|].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) :=
iCombine [H1;H2] as H.
(** * Existential *) (** * Existential *)
Tactic Notation "iExists" uconstr(x1) := Tactic Notation "iExists" uconstr(x1) :=
iStartProof; iStartProof;
...@@ -1098,6 +1084,22 @@ Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1) ...@@ -1098,6 +1084,22 @@ Tactic Notation "iDestructHyp" constr(H) "as" "(" simple_intropattern(x1)
simple_intropattern(x8) ")" constr(pat) := simple_intropattern(x8) ")" constr(pat) :=
iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat. iExistDestruct H as x1 H; iDestructHyp H as ( x2 x3 x4 x5 x6 x7 x8 ) pat.
(** * Combinining hypotheses *)
Tactic Notation "iCombine" constr(Hs) "as" constr(pat) :=
let Hs := words Hs in
let Hs := eval vm_compute in (INamed <$> Hs) in
let H := iFresh in
eapply tac_combine with _ _ Hs _ _ H _;
[env_reflexivity ||
let Hs := iMissingHyps Hs in
fail "iCombine: hypotheses" Hs "not found"
|iSolveTC
|env_reflexivity || fail "iCombine:" H "not fresh"
|iDestructHyp H as pat].
Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) :=
iCombine [H1;H2] as pat.
(** * Introduction tactic *) (** * Introduction tactic *)
Tactic Notation "iIntros" constr(pat) := Tactic Notation "iIntros" constr(pat) :=
let rec go pats startproof := let rec go pats startproof :=
......
...@@ -197,6 +197,10 @@ Lemma test_iCombine_persistent P Q R `{!Persistent R} : ...@@ -197,6 +197,10 @@ Lemma test_iCombine_persistent P Q R `{!Persistent R} :
P - Q - R R Q P R False. P - Q - R R Q P R False.
Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed. Proof. iIntros "HP HQ #HR". iCombine "HR HQ HP HR" as "H". auto. Qed.
Lemma test_iCombine_frame P Q R `{!Persistent R} :
P - Q - R R Q P R.
Proof. iIntros "HP HQ #HR". iCombine "HQ HP HR" as "$". by iFrame. Qed.
Lemma test_iNext_evar P : P - True. Lemma test_iNext_evar P : P - True.
Proof. Proof.
iIntros "HP". iAssert ( _ - P)%I as "?"; last done. iIntros "HP". iAssert ( _ - P)%I as "?"; last done.
......
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