Commit 5c38c76b authored by Joseph Tassarotti's avatar Joseph Tassarotti

Delete some context duplication in iInv.

parent bc677d5e
......@@ -668,26 +668,23 @@ 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, Δ')
ElimInv φ Pinv Pin Pout Pclose Q Q'
φ
( R, Δ'',
envs_app false (Esnoc Enil j
( R,
match envs_app false (Esnoc Enil j
(Pin -
( x, Pout x - pm_option_fun Pclose x -? Q' x) -
R
)%I) Δ'
= Some Δ''
envs_entails Δ'' R)
with Some Δ'' => envs_entails Δ'' R | None => False end)
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) [Δ'' [? <-]].
rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) Hmatch.
destruct (envs_app _ _ _) eqn:?; last done.
rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
rewrite intuitionistically_if_elim -assoc. destruct Pclose; simpl in *.
- setoid_rewrite wand_curry. auto.
......
......@@ -2302,7 +2302,7 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" open_constr(H
let I := match goal with |- ElimInv _ ?I _ _ _ _ _ => I end in
fail "iInv: cannot eliminate invariant" I
|iSolveSideCondition
|let R := fresh in intros R; eexists; split; [pm_reflexivity|];
|let R := fresh in intros R; pm_reduce;
(* Now we are left proving [envs_entails Δ'' R]. *)
iSpecializePat H pats; last (
iApplyHyp H; clear R; pm_reduce;
......
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