[Iris-Club] Frame-preserving update and double-negation

[Joseph Tassarotti]

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
>