Commit a113503b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Revert "Merge branch 'fix-idestruct-specialize' into 'master'"

This reverts merge request !591
parent 550fea78
......@@ -247,7 +247,7 @@ Lemma slice_iff E q f P Q Q' γ b :
Proof.
iIntros (??) "#HQQ' #Hs Hb". destruct b.
- iMod (slice_delete_full with "Hs Hb") as (P') "(HQ & Heq & Hb)"; try done.
iPoseProof ("HQQ'" with "HQ") as "HQ'".
iDestruct ("HQQ'" with "HQ") as "HQ'".
iMod (slice_insert_full with "HQ' Hb") as (γ' ?) "[#Hs' Hb]"; try done.
iExists γ', _. iIntros "{$∗ $# $%} !>". do 2 iNext. iRewrite "Heq".
iIntros "!>". by iSplit; iIntros "[? $]"; iApply "HQQ'".
......
......@@ -1992,12 +1992,6 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15) "" with tac.
(** * Destruct tactic *)
(** [CopyDestruct] is an internal class used by the [iDestruct] tactic to
identify universally quantified hypotheses that should be copied and not be
consumed when they are specialized in proofmode terms.
Not intended for user extensibility. *)
Class CopyDestruct {PROP : bi} (P : PROP).
Arguments CopyDestruct {_} _%I.
Hint Mode CopyDestruct + ! : typeclass_instances.
......@@ -2019,8 +2013,8 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic3(tac) :=
| string => constr:(Some (INamed lem))
| iTrm =>
lazymatch lem with
| @ITrm ident _ _?H _ _ => constr:(Some H)
| @ITrm string _ _ ?H _ _ => constr:(Some (INamed H))
| @iTrm ident ?H _ _ => constr:(Some H)
| @iTrm string ?H _ _ => constr:(Some (INamed H))
| _ => constr:(@None ident)
end
| _ => constr:(@None ident)
......
......@@ -93,32 +93,6 @@ Lemma test_iDestruct_intuitionistic_2 P Q `{!Persistent P, !Affine P}:
Q (Q - P) - P.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". done. Qed.
Lemma test_iDestruct_specialize_wand P Q :
Q (Q - P) - P.
Proof.
iIntros "[HQ #HQP]".
(* iDestruct specializes, consuming the hypothesis *)
iDestruct ("HQP" with "HQ") as "HQP". done.
Qed.
Lemma test_iPoseProof_copy_wand P Q :
Q (Q - P) - P (Q - P).
Proof.
iIntros "[HQ #HQP]".
(* in contrast with [iDestruct], [iPoseProof] leaves "HQP" alone *)
iPoseProof ("HQP" with "HQ") as "HP".
iFrame "HP HQP".
Qed.
Lemma test_iDestruct_pose_forall (Φ: nat PROP) :
( (x:nat), Φ x) - Φ 0 Φ 1.
Proof.
iIntros "#H".
(* iDestruct does not consume "H" because it's a [∀] *)
iDestruct ("H" $! 0) as "$".
iDestruct ("H" $! 1) as "$".
Qed.
Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persistent P}:
Q (Q - P) - P Q.
Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. 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