Skip to content
Snippets Groups Projects
Commit 3a07f8f1 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies

parent b2a159cb
No related branches found
No related tags found
No related merge requests found
Pipeline #86990 failed
Stage: build
Hide whitespace changes
Inline Side-by-side
coq-tutorial-popl20.opam
+ 1
− 1
View file @ 3a07f8f1
...@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl20.git" ...@@ -8,7 +8,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/tutorial-popl20.git"
synopsis: "The Iris tutorial at POPL 2020" synopsis: "The Iris tutorial at POPL 2020"
depends: [ depends: [
"coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") } "coq-iris-heap-lang" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
exercises/symbol_ghost.v
+ 2
− 2
View file @ 3a07f8f1
...@@ -44,13 +44,13 @@ Section symbol_ghost. ...@@ -44,13 +44,13 @@ Section symbol_ghost.
Lemma counter_exclusive γ n1 n2 : counter γ n1 -∗ counter γ n2 -∗ False. Lemma counter_exclusive γ n1 n2 : counter γ n1 -∗ counter γ n2 -∗ False.
Proof. Proof.
apply bi.wand_intro_r. rewrite -own_op own_valid /=. by iDestruct 1 as %[]. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_op own_valid /=. by iDestruct 1 as %[].
Qed. Qed.
Lemma counter_inc γ n : counter γ n ==∗ counter γ (S n) ∗ symbol γ n. Lemma counter_inc γ n : counter γ n ==∗ counter γ (S n) ∗ symbol γ n.
Proof. Proof.
rewrite -own_op. rewrite -own_op.
apply own_update, auth_update_alloc, max_nat_local_update. apply bi.entails_wand, own_update, auth_update_alloc, max_nat_local_update.
simpl. lia. simpl. lia.
Qed. Qed.
......
solutions/parametricity.v
+ 1
− 1
View file @ 3a07f8f1
...@@ -102,7 +102,7 @@ Section parametricity. ...@@ -102,7 +102,7 @@ Section parametricity.
intros He. intros He.
apply (sem_gen_type_safety _ _ φ)=> ?. apply (sem_gen_type_safety _ _ φ)=> ?.
set (T := SemTy (λ w, ⌜ φ w ⌝)%I : sem_ty Σ). set (T := SemTy (λ w, ⌜ φ w ⌝)%I : sem_ty Σ).
exists T. split; first done. exists T. split; first by auto.
specialize (He _) as (Φ & He & Hvf & Hvz & Hφ). specialize (He _) as (Φ & He & Hvf & Hvz & Hφ).
iIntros (vs) "!# #Hvs". iIntros (vs) "!# #Hvs".
iPoseProof (He with "Hvs") as "He /=". iPoseProof (He with "Hvs") as "He /=".
......
solutions/symbol_ghost.v
+ 2
− 2
View file @ 3a07f8f1
...@@ -44,13 +44,13 @@ Section symbol_ghost. ...@@ -44,13 +44,13 @@ Section symbol_ghost.
Lemma counter_exclusive γ n1 n2 : counter γ n1 -∗ counter γ n2 -∗ False. Lemma counter_exclusive γ n1 n2 : counter γ n1 -∗ counter γ n2 -∗ False.
Proof. Proof.
apply bi.wand_intro_r. rewrite -own_op own_valid /=. by iDestruct 1 as %[]. apply bi.entails_wand, bi.wand_intro_r. rewrite -own_op own_valid /=. by iDestruct 1 as %[].
Qed. Qed.
Lemma counter_inc γ n : counter γ n ==∗ counter γ (S n) ∗ symbol γ n. Lemma counter_inc γ n : counter γ n ==∗ counter γ (S n) ∗ symbol γ n.
Proof. Proof.
rewrite -own_op. rewrite -own_op.
apply own_update, auth_update_alloc, max_nat_local_update. apply bi.entails_wand, own_update, auth_update_alloc, max_nat_local_update.
simpl. lia. simpl. lia.
Qed. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment