[Iris-Club] Frame-preserving update and double-negation
Joseph Tassarotti
jtassaro at andrew.cmu.edu
Wed Aug 24 17:47:32 CEST 2016
Oops, yes, sorry, I should have proof-read my mail more carefully. Thank
you for correcting this. Here are two quick proofs (which work when
placed sufficiently late in the uPred_logic section in uPred.v):
Lemma rvs_nn P: (|=r=> P) ⊢ ((P -★ False) -★ False).
Proof.
split. unseal. intros.
edestruct H0; eauto.
eapply (H3 n' x0); eauto.
- rewrite comm; naive_solver.
- naive_solver.
Qed.
Require Import Coq.Logic.Classical_Pred_Type.
Lemma nn_rvs P (HD: CMRADiscrete M) (HT: TimelessP P): ((P -★ False) -★
False) ⊢ |=r=> P.
Proof.
split. unseal. intros ??? Hnn k yf Hle ?.
apply not_all_not_ex.
intros Hfal. eapply Hnn; eauto.
intros. eapply Hfal; split.
- rewrite comm.
eapply cmra_discrete_valid_iff.
eapply cmra_discrete_valid_iff.
eauto.
- eapply timelessP_spec; eauto.
eapply cmra_discrete_valid_iff.
eapply cmra_discrete_valid_iff.
eapply cmra_validN_op_r. eauto.
eapply uPred_closed; eauto.
eapply cmra_discrete_valid_iff.
eapply cmra_discrete_valid_iff.
eapply cmra_validN_op_r. eauto.
Qed.
On 08/24/2016 11:20 AM, Jacques-Henri Jourdan wrote:
> Hi,
>
> I've been fighting against an apparent paradox: Joe says that (P -*
> False) -* False implies |=r=> P and Robbert said the former is always
> True when used on a later. So, that would mean that |=r=> >P is always
> true, which is rather annoying.
>
>
> The problem is in the following:
>
> > It is not hard to show that (P -* False) -* False implies |=r=> P.
>
> In reality, the easy way is the other one, from |=r=> P to (P -*
> False) -* False. Proving |=r=> P requires many hypotheses
>
More information about the Iris-Club
mailing list