From 8b8d6ae21d2fe9e765c73907a845c06bcfbe9625 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 20 Sep 2016 15:19:23 +0200 Subject: [PATCH] Make iFrame finish the goal if everything has been framed. --- ProofMode.md | 3 +++ proofmode/tactics.v | 11 +++++++++-- 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/ProofMode.md b/ProofMode.md index 9c140467..82c0a5ae 100644 --- a/ProofMode.md +++ b/ProofMode.md @@ -92,6 +92,9 @@ Separating logic specific tactics Notice that framing spatial hypotheses makes them disappear, but framing Coq or persistent hypotheses does not make them disappear. + + This tactic finishes the goal in case everything in the conclusion has been + framed. - `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into `H : P1 ★ P2`. diff --git a/proofmode/tactics.v b/proofmode/tactics.v index ca368e1a..debb4860 100644 --- a/proofmode/tactics.v +++ b/proofmode/tactics.v @@ -432,17 +432,24 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(H) := |env_cbv; reflexivity || fail "iCombine:" H "not fresh"|]. (** Framing *) +Local Ltac iFrameFinish := + lazy iota beta; + try match goal with + | |- _ ⊢ True => exact (uPred.pure_intro _ _ I) + end. + Local Ltac iFramePure t := let φ := type of t in eapply (tac_frame_pure _ _ _ _ t); - [apply _ || fail "iFrame: cannot frame" φ|]. + [apply _ || fail "iFrame: cannot frame" φ + |iFrameFinish]. Local Ltac iFrameHyp H := eapply tac_frame with _ H _ _ _; [env_cbv; reflexivity || fail "iFrame:" H "not found" |let R := match goal with |- Frame ?R _ _ => R end in apply _ || fail "iFrame: cannot frame" R - |lazy iota beta]. + |iFrameFinish]. Local Ltac iFrameAnyPure := repeat match goal with H : _ |- _ => iFramePure H end. -- GitLab