Commit 116b381d authored by Ralf Jung's avatar Ralf Jung

ElimInv generalized to any BI actually works fine

parent b2711d60
......@@ -571,11 +571,8 @@ Hint Mode IntoAcc + - ! - - - - - - - - : typeclass_instances.
still benefit from [iInv].
TODO: Add support for a binder (like accessors have it).
This is defined on sbi instead of bi as typeclass search otherwise
fails (e.g. in the iInv as used in cancelable_invariants.v).
*)
Class ElimInv {PROP : sbi} {X : Type} (φ : Prop)
Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X PROP) (Pclose : option (X PROP))
(Q : PROP) (Q' : X PROP) :=
elim_inv : φ Pinv Pin ( x, Pout x (default (λ _, emp) Pclose id) x - Q' x) Q.
......
......@@ -1093,6 +1093,26 @@ Proof.
rewrite envs_entails_eq => <-. by setoid_rewrite <-envs_incr_counter_equiv.
Qed.
(** * Invariants *)
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
(Pin - ( x, Pout x - default (Q' x) Pclose (λ Pclose, Pclose x - Q' x)) - R)%I) Δ'
= Some Δ''
envs_entails Δ'' R)
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) [Δ'' [? <-]].
rewrite (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.
- setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
Qed.
End bi_tactics.
......@@ -1324,27 +1344,6 @@ Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
(** * Invariants *)
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
(Pin - ( x, Pout x - default (Q' x) Pclose (λ Pclose, Pclose x - Q' x)) - R)%I) Δ'
= Some Δ''
envs_entails Δ'' R)
envs_entails Δ Q.
Proof.
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) [Δ'' [? <-]].
rewrite (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.
- setoid_rewrite <-(right_id emp%I _ (Pout _)). auto.
Qed.
(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy d Q :
envs_lookup i Δ = Some (p, Pxy)
......
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