### Bump Iris (⊢ changes).

parent 339a19a1
Pipeline #28849 failed with stage
in 15 minutes and 12 seconds
 ... @@ -73,7 +73,7 @@ Section proof2. ... @@ -73,7 +73,7 @@ Section proof2. proofs we tend to inline simple lemmas like these, but they are here to proofs we tend to inline simple lemmas like these, but they are here to make things easier to understand. *) make things easier to understand. *) Lemma ghost_var_alloc n : Lemma ghost_var_alloc n : (|==> ∃ γ, own γ (●E n) ∗ own γ (◯E n))%I. ⊢ |==> ∃ γ, own γ (●E n) ∗ own γ (◯E n). Proof. Proof. iMod (own_alloc (●E n ⋅ ◯E n)) as (γ) "[??]". iMod (own_alloc (●E n ⋅ ◯E n)) as (γ) "[??]". - by apply excl_auth_valid. - by apply excl_auth_valid. ... ...
 ... @@ -31,7 +31,7 @@ Section proof. ... @@ -31,7 +31,7 @@ Section proof. (** The same helping lemmas for ghost variables that we have already seen in (** The same helping lemmas for ghost variables that we have already seen in the previous exercise. *) the previous exercise. *) Lemma ghost_var_alloc b : Lemma ghost_var_alloc b : (|==> ∃ γ, own γ (●E b) ∗ own γ (◯E b))%I. ⊢ |==> ∃ γ, own γ (●E b) ∗ own γ (◯E b). Proof. Proof. iMod (own_alloc (●E b ⋅ ◯E b)) as (γ) "[??]". iMod (own_alloc (●E b ⋅ ◯E b)) as (γ) "[??]". - by apply excl_auth_valid. - by apply excl_auth_valid. ... ...
 ... @@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl18.git" ... @@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl18.git" synopsis: "The Iris tutorial at POPL 2018" synopsis: "The Iris tutorial at POPL 2018" depends: [ depends: [ "coq-iris" { (= "dev.2020-03-10.6.79f576aa") | (= "dev") } "coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") } ] ] build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"] ... ...
 ... @@ -77,7 +77,7 @@ Section proof2. ... @@ -77,7 +77,7 @@ Section proof2. proofs we tend to inline simple lemmas like these, but they are here to proofs we tend to inline simple lemmas like these, but they are here to make things easier to understand. *) make things easier to understand. *) Lemma ghost_var_alloc n : Lemma ghost_var_alloc n : (|==> ∃ γ, own γ (●E n) ∗ own γ (◯E n))%I. ⊢ |==> ∃ γ, own γ (●E n) ∗ own γ (◯E n). Proof. Proof. iMod (own_alloc (●E n ⋅ ◯E n)) as (γ) "[??]". iMod (own_alloc (●E n ⋅ ◯E n)) as (γ) "[??]". - by apply excl_auth_valid. - by apply excl_auth_valid. ... ...
 ... @@ -31,7 +31,7 @@ Section proof. ... @@ -31,7 +31,7 @@ Section proof. (** The same helping lemmas for ghost variables that we have already seen in (** The same helping lemmas for ghost variables that we have already seen in the previous exercise. *) the previous exercise. *) Lemma ghost_var_alloc b : Lemma ghost_var_alloc b : (|==> ∃ γ, own γ (●E b) ∗ own γ (◯E b))%I. ⊢ |==> ∃ γ, own γ (●E b) ∗ own γ (◯E b). Proof. Proof. iMod (own_alloc (●E b ⋅ ◯E b)) as (γ) "[??]". iMod (own_alloc (●E b ⋅ ◯E b)) as (γ) "[??]". - by apply excl_auth_valid. - by apply excl_auth_valid. ... ...
 ... @@ -54,7 +54,7 @@ Section proof2. ... @@ -54,7 +54,7 @@ Section proof2. (* Rules for fractional ghost variables (* Rules for fractional ghost variables (proved from generic principles) *) (proved from generic principles) *) Lemma frac_auth_alloc n : Lemma frac_auth_alloc n : (|==> ∃ γ, own γ (●F n) ∗ own γ (◯F{1} n))%I. ⊢ |==> ∃ γ, own γ (●F n) ∗ own γ (◯F{1} n). Proof. Proof. iMod (own_alloc (●F n ⋅ ◯F n)) as (γ) "[??]"; eauto with iFrame. iMod (own_alloc (●F n ⋅ ◯F n)) as (γ) "[??]"; eauto with iFrame. by apply frac_auth_valid. by apply frac_auth_valid. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!