diff --git a/opam b/opam index 825f04ed6b68f69b32f7f69a4b9d686b380019b4..0b17ee15f1cb7d97e73351db0d3e1b1018685061 100644 --- a/opam +++ b/opam @@ -11,5 +11,5 @@ install: [make "install"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"] depends: [ "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") } - "coq-stdpp" { (= "dev.2019-01-24.0.17241997") | (= "dev") } + "coq-stdpp" { (= "dev.2019-01-24.2.b72e1fa8") | (= "dev") } ] diff --git a/tests/telescopes.ref b/tests/telescopes.ref index 0816c1fa580fdb2ee3576d27ddb20c1fdef07ef4..5f4957effb35bbf563ce517031efe2ef366e810f 100644 --- a/tests/telescopes.ref +++ b/tests/telescopes.ref @@ -13,6 +13,41 @@ --------------------------------------∗ |={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x) +1 subgoal + + PROP : sbi + BiFUpd0 : BiFUpd PROP + X : tele + E1, E2 : coPset + α, β, γ1, γ2 : X → PROP + ============================ + accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x : X, γ1 x ∨ γ2 x) +1 subgoal + + PROP : sbi + BiFUpd0 : BiFUpd PROP + X : tele + E1, E2 : coPset + α, β, γ1, γ2 : X → PROP + x : X + ============================ + "Hγ1" : γ1 x + --------------------------------------∗ + (λ.. x0 : X, γ1 x0 ∨ γ2 x0) x + +1 subgoal + + PROP : sbi + BiFUpd0 : BiFUpd PROP + X : tele + E1, E2 : coPset + α, β, γ1, γ2 : X → PROP + x : X + ============================ + "Hγ1" : γ1 x + --------------------------------------∗ + γ1 x ∨ γ2 x + 1 subgoal PROP : sbi diff --git a/tests/telescopes.v b/tests/telescopes.v index 621e086dff47bb7aed49c11191c4f511fe1ad9fd..a60ba91e0b76ab12b315b3c5995c395f63377d7d 100644 --- a/tests/telescopes.v +++ b/tests/telescopes.v @@ -33,6 +33,15 @@ Proof. iModIntro. iExists x'. iFrame. iIntros "Hβ". iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto. Qed. + +Lemma acc_mono_disj E1 E2 α β γ1 γ2 : + accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x, γ1 x ∨ γ2 x). +Proof. + Show. + iApply acc_mono. iIntros (x) "Hγ1". Show. + rewrite ->tele_app_bind. Show. + iLeft. done. +Qed. End tests. Section printing_tests.