Commit 353be255 authored by Joseph Tassarotti's avatar Joseph Tassarotti

Convert remaining simple tactics.

parent edd00d9a
......@@ -523,16 +523,19 @@ Qed.
(* Using this tactic, one can destruct a (non-separating) conjunction in the
spatial context as long as one of the conjuncts is thrown away. It corresponds
to the principle of "external choice" in linear logic. *)
Lemma tac_and_destruct_choice Δ Δ' i p d j P P1 P2 Q :
Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
envs_lookup i Δ = Some (p, P)
(if p then IntoAnd p P P1 P2 : Type else
TCOr (IntoAnd p P P1 P2) (TCAnd (IntoSep P P1 P2)
(if d is Left then TCOr (Affine P2) (Absorbing Q)
else TCOr (Affine P1) (Absorbing Q))))
envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ = Some Δ'
envs_entails Δ' Q envs_entails Δ Q.
match envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ with
| None => False
| Some Δ' => envs_entails Δ' Q
end envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ? HP ? HQ.
destruct (envs_simple_replace) as [Δ'|] eqn:Hrep; last by (intros; exfalso).
rewrite envs_entails_eq => ? HP HQ.
rewrite envs_simple_replace_singleton_sound //=. destruct p.
{ rewrite (into_and _ P) HQ. destruct d; simpl.
- by rewrite and_elim_l wand_elim_r.
......@@ -668,6 +671,9 @@ Proof.
Qed.
(** * Invariants *)
(* TODO: this duplicates the context, but it is harder to avoid doing so
given the way that that invariants can be selected based on namespace or hypothesis
name. *)
Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X PROP))
Q (Q' : X PROP) :
envs_lookup_delete false i Δ = Some (p, Pinv, Δ')
......@@ -991,12 +997,16 @@ Proof.
- by rewrite Hs //= right_id.
Qed.
Lemma tac_löb Δ Δ' i Q :
Lemma tac_löb Δ i Q :
env_spatial_is_nil Δ = true
envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ'
envs_entails Δ' Q envs_entails Δ Q.
match envs_app true (Esnoc Enil i ( Q)%I) Δ with
| None => False
| Some Δ' => envs_entails Δ' Q
end
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq => ?? HQ.
destruct (envs_app) eqn:?; last by (intros; exfalso).
rewrite envs_entails_eq => ? HQ.
rewrite (env_spatial_is_nil_intuitionistically Δ) //.
rewrite -(persistently_and_emp_elim Q). apply and_intro; first apply: affine.
rewrite -(löb (<pers> Q)%I) later_persistently. apply impl_intro_l.
......
......@@ -1176,15 +1176,18 @@ Local Tactic Notation "iAndDestruct" constr(H) "as" constr(H1) constr(H2) :=
end].
Local Tactic Notation "iAndDestructChoice" constr(H) "as" constr(d) constr(H') :=
eapply tac_and_destruct_choice with _ H _ d H' _ _ _;
eapply tac_and_destruct_choice with H _ d H' _ _ _;
[pm_reflexivity || fail "iAndDestructChoice:" H "not found"
|pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (IntoAnd _ ?P _ _) _ => P end in
fail "iAndDestructChoice: cannot destruct" P
|pm_reflexivity ||
let H' := pretty_ident H' in
fail "iAndDestructChoice:" H' "not fresh"
|(* subgoal *)].
|pm_reduce;
lazymatch goal with
| |- False =>
let H' := pretty_ident H' in
fail "iAndDestructChoice:" H' "not fresh"
| _ => idtac (* subgoal *)
end].
(** * Existential *)
Tactic Notation "iExists" uconstr(x1) :=
......@@ -2025,11 +2028,15 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
(* apply is sometimes confused wrt. canonical structures search.
refine should use the other unification algorithm, which should
not have this issue. *)
notypeclasses refine (tac_löb _ _ IH _ _ _ _);
notypeclasses refine (tac_löb _ IH _ _ _);
[reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|pm_reflexivity ||
let IH := pretty_ident IH in
fail "iLöb:" IH "not fresh"|].
|pm_reduce;
lazymatch goal with
| |- False =>
let IH := pretty_ident IH in
fail "iLöb:" IH "not fresh"
| _ => idtac
end].
Tactic Notation "iLöbRevert" constr(Hs) "with" tactic(tac) :=
iRevertIntros Hs with (
......
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