Commit 34bc7b6a authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' into iris3.0

parents 9c600c8b a095bb8a
......@@ -70,7 +70,11 @@ Elimination of logical connectives
Separating logic specific tactics
---------------------------------
- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal.
- `iFrame "H0 ... Hn"` : cancel the hypotheses `H0 ... Hn` in the goal. The
symbol `★` can be used to frame as much of the spatial context as possible,
and the symbol `#` can be used to repeatedly frame as much of the persistent
context as possible. When without arguments, it attempts to frame all spatial
hypotheses.
- `iCombine "H1" "H2" as "H"` : turns `H1 : P1` and `H2 : P2` into
`H : P1 ★ P2`.
......
......@@ -85,6 +85,7 @@ program_logic/auth.v
program_logic/sts.v
program_logic/namespaces.v
program_logic/boxes.v
program_logic/counter_examples.v
heap_lang/lang.v
heap_lang/tactics.v
heap_lang/wp_tactics.v
......@@ -96,6 +97,7 @@ heap_lang/lib/spawn.v
heap_lang/lib/par.v
heap_lang/lib/assert.v
heap_lang/lib/lock.v
heap_lang/lib/ticket_lock.v
heap_lang/lib/counter.v
heap_lang/lib/barrier/barrier.v
heap_lang/lib/barrier/specification.v
......
......@@ -241,6 +241,28 @@ Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
Program Definition authRF (F : urFunctor) : rFunctor := {|
rFunctor_car A B := authR (urFunctor_car F A B);
rFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(auth_map_id x).
apply auth_map_ext=>y; apply urFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -auth_map_compose.
apply auth_map_ext=>y; apply urFunctor_compose.
Qed.
Instance authRF_contractive F :
urFunctorContractive F rFunctorContractive (authRF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply authC_map_ne, urFunctor_contractive.
Qed.
Program Definition authURF (F : urFunctor) : urFunctor := {|
urFunctor_car A B := authUR (urFunctor_car F A B);
urFunctor_map A1 A2 B1 B2 fg := authC_map (urFunctor_map F fg)
......
......@@ -54,7 +54,6 @@ Section gset.
Canonical Structure gset_disjUR :=
discreteUR (gset_disj K) gset_disj_ra_mixin gset_disj_ucmra_mixin.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Arguments op _ _ _ _ : simpl never.
Lemma gset_alloc_updateP_strong P (Q : gset_disj K Prop) X :
......@@ -68,18 +67,10 @@ Section gset.
- apply HQ; set_solver by eauto.
- apply gset_disj_valid_op. set_solver by eauto.
Qed.
Lemma gset_alloc_updateP (Q : gset_disj K Prop) X :
( i, i X Q (GSet ({[i]} X))) GSet X ~~>: Q.
Proof.
intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
intros Y ?; exists (fresh Y); eauto using is_fresh.
Qed.
Lemma gset_alloc_updateP_strong' P X :
( Y, X Y j, j Y P j)
GSet X ~~>: λ Y, i, Y = GSet ({[ i ]} X) i X P i.
Proof. eauto using gset_alloc_updateP_strong. Qed.
Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, i, Y = GSet ({[ i ]} X) i X.
Proof. eauto using gset_alloc_updateP. Qed.
Lemma gset_alloc_empty_updateP_strong P (Q : gset_disj K Prop) :
( Y : gset K, j, j Y P j)
......@@ -88,15 +79,29 @@ Section gset.
intros. apply (gset_alloc_updateP_strong P); eauto.
intros i; rewrite right_id_L; auto.
Qed.
Lemma gset_alloc_empty_updateP (Q : gset_disj K Prop) :
( i, Q (GSet {[i]})) GSet ~~>: Q.
Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
Lemma gset_alloc_empty_updateP_strong' P :
( Y : gset K, j, j Y P j)
GSet ~~>: λ Y, i, Y = GSet {[ i ]} P i.
Proof. eauto using gset_alloc_empty_updateP_strong. Qed.
Lemma gset_alloc_empty_updateP' : GSet ~~>: λ Y, i, Y = GSet {[ i ]}.
Proof. eauto using gset_alloc_empty_updateP. Qed.
Section fresh_updates.
Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
Lemma gset_alloc_updateP (Q : gset_disj K Prop) X :
( i, i X Q (GSet ({[i]} X))) GSet X ~~>: Q.
Proof.
intro; eapply gset_alloc_updateP_strong with (λ _, True); eauto.
intros Y ?; exists (fresh Y); eauto using is_fresh.
Qed.
Lemma gset_alloc_updateP' X : GSet X ~~>: λ Y, i, Y = GSet ({[ i ]} X) i X.
Proof. eauto using gset_alloc_updateP. Qed.
Lemma gset_alloc_empty_updateP (Q : gset_disj K Prop) :
( i, Q (GSet {[i]})) GSet ~~>: Q.
Proof. intro. apply gset_alloc_updateP. intros i; rewrite right_id_L; auto. Qed.
Lemma gset_alloc_empty_updateP' : GSet ~~>: λ Y, i, Y = GSet {[ i ]}.
Proof. eauto using gset_alloc_empty_updateP. Qed.
End fresh_updates.
Lemma gset_alloc_local_update X i Xf :
i X i Xf GSet X ~l~> GSet ({[i]} X) @ Some (GSet Xf).
......
......@@ -371,11 +371,26 @@ Proof.
Qed.
Global Instance: AntiSymm () (@uPred_entails M).
Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
Lemma soundness_later n : ¬ (True ^n False).
Proof.
unseal. intros [H].
assert ((^n @uPred_pure_def M False) n )%I as Hn.
(* So Coq still has no nice way to say "make this precondition of that lemma a goal"?!? *)
{ apply H; by auto using ucmra_unit_validN. }
clear H. induction n.
- done.
- move: Hn. simpl. unseal. done.
Qed.
Theorem soundness : ¬ (True False).
Proof. exact (soundness_later 0). Qed.
Lemma equiv_spec P Q : (P Q) (P Q) (Q P).
Proof.
split; [|by intros [??]; apply (anti_symm ())].
intros HPQ; split; split=> x i; apply HPQ.
Qed.
Lemma equiv_entails P Q : (P Q) (P Q).
Proof. apply equiv_spec. Qed.
Lemma equiv_entails_sym P Q : (Q P) (P Q).
......
......@@ -15,7 +15,7 @@ This definition varies slightly from the original one in~\cite{catlogic}.
\All n. (\nequiv{n}) ~& \text{is an equivalence relation} \tagH{cofe-equiv} \\
\All n, m.& n \geq m \Ra (\nequiv{n}) \subseteq (\nequiv{m}) \tagH{cofe-mono} \\
\All x, y.& x = y \Lra (\All n. x \nequiv{n} y) \tagH{cofe-limit} \\
\All n, c.& \lim(c) \nequiv{n} c(n+1) \tagH{cofe-compl}
\All n, c.& \lim(c) \nequiv{n} c(n) \tagH{cofe-compl}
\end{align*}
\end{defn}
......@@ -35,7 +35,7 @@ In order to solve the recursive domain equation in \Sref{sec:model} it is also e
A function $f : \cofe \to \cofeB$ between two COFEs is \emph{non-expansive} (written $f : \cofe \nfn \cofeB$) if
\[\All n, x \in \cofe, y \in \cofe. x \nequiv{n} y \Ra f(x) \nequiv{n} f(y) \]
It is \emph{contractive} if
\[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(x) \]
\[ \All n, x \in \cofe, y \in \cofe. (\All m < n. x \nequiv{m} y) \Ra f(x) \nequiv{n} f(y) \]
\end{defn}
Intuitively, applying a non-expansive function to some data will not suddenly introduce differences between seemingly equal data.
Elements that cannot be distinguished by programs within $n$ steps remain indistinguishable after applying $f$.
......@@ -211,7 +211,7 @@ Furthermore, discrete CMRAs can be turned into RAs by ignoring their COFE struct
\end{defn}
Note that every object/arrow in $\CMRAs$ is also an object/arrow of $\COFEs$.
The notion of a locally non-expansive (or contractive) bifunctor naturally generalizes to bifunctors between these categories.
\ralf{Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.}
%TODO: Discuss how we probably have a commuting square of functors between Set, RA, CMRA, COFE.
%%% Local Variables:
%%% mode: latex
......
......@@ -135,7 +135,7 @@ Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable
Note that $\always$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
We will write $\pvs[\term] \prop$ for $\pvs[\term][\term] \prop$.
If we omit the mask, then it is $\top$ for weakest precondition $\wpre\expr{\Ret\var.\prop}$ and $\emptyset$ for primitive view shifts $\pvs \prop$.
\ralf{$\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.}
%FIXME $\top$ is not a term in the logic. Neither is any of the operations on masks that we use in the rules for weakestpre.
Some propositions are \emph{timeless}, which intuitively means that step-indexing does not affect them.
This is a \emph{meta-level} assertion about propositions, defined as follows:
......
......@@ -144,8 +144,17 @@ Section heap.
by apply pure_elim_r.
Qed.
Lemma heap_mapsto_op_split l q v : l {q} v (l {q/2} v l {q/2} v).
Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
Lemma heap_mapsto_op_1 l q1 q2 v1 v2 :
l {q1} v1 l {q2} v2 v1 = v2 l {q1+q2} v1.
Proof. by rewrite heap_mapsto_op. Qed.
Lemma heap_mapsto_op_half l q v1 v2 :
l {q/2} v1 l {q/2} v2 v1 = v2 l {q} v1.
Proof. by rewrite heap_mapsto_op Qp_div_2. Qed.
Lemma heap_mapsto_op_half_1 l q v1 v2 :
l {q/2} v1 l {q/2} v2 v1 = v2 l {q} v1.
Proof. by rewrite heap_mapsto_op_half. Qed.
(** Weakest precondition *)
(* FIXME: try to reduce usage of wp_pvs. We're losing view shifts here. *)
......
......@@ -99,7 +99,7 @@ Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
Proof.
iIntros (HN) "[#? HΦ]".
rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
iApply "HΦ".
iApply ("HΦ" with "|==>[-]").
iPvs (saved_prop_alloc (F:=idCF) _ P) as (γ) "#?".
iPvs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
as (γ') "[#? Hγ']"; eauto.
......
From iris.program_logic Require Export global_functor auth.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import gset.
Import uPred.
Definition wait_loop: val :=
rec: "wait_loop" "x" "l" :=
let: "o" := Fst !"l" in
if: "x" = "o"
then #() (* my turn *)
else "wait_loop" "x" "l".
Definition newlock : val := λ: <>, ref((* owner *) #0, (* next *) #0).
Definition acquire : val :=
rec: "acquire" "l" :=
let: "oldl" := !"l" in
if: CAS "l" "oldl" (Fst "oldl", Snd "oldl" + #1)
then wait_loop (Snd "oldl") "l"
else "acquire" "l".
Definition release : val :=
rec: "release" "l" :=
let: "oldl" := !"l" in
if: CAS "l" "oldl" (Fst "oldl" + #1, Snd "oldl")
then #()
else "release" "l".
Global Opaque newlock acquire release wait_loop.
(** The CMRAs we need. *)
Class tlockG Σ := TlockG {
tlock_G :> authG heap_lang Σ (gset_disjUR nat);
tlock_exclG :> inG heap_lang Σ (exclR unitC)
}.
Definition tlockGF : gFunctorList :=
[authGF (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
Instance inGF_tlockG `{H : inGFs heap_lang Σ tlockGF} : tlockG Σ.
Proof. destruct H as (? & ? & ?). split. apply _. apply: inGF_inG. Qed.
Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace).
Local Notation iProp := (iPropG heap_lang Σ).
Definition tickets_inv (n: nat) (gs: gset_disjUR nat) : iProp :=
(gs = GSet (seq_set 0 n))%I.
Definition lock_inv (γ1 γ2: gname) (l : loc) (R : iProp) : iProp :=
( o n: nat, l (#o, #n)
auth_inv γ1 (tickets_inv n)
((own γ2 (Excl ()) R) auth_own γ1 (GSet {[ o ]})))%I.
Definition is_lock (l: loc) (R: iProp) : iProp :=
( γ1 γ2, heapN N heap_ctx inv N (lock_inv γ1 γ2 l R))%I.
Definition issued (l : loc) (x: nat) (R : iProp) : iProp :=
( γ1 γ2, heapN N heap_ctx inv N (lock_inv γ1 γ2 l R)
auth_own γ1 (GSet {[ x ]}))%I.
Definition locked (l : loc) (R : iProp) : iProp :=
( γ1 γ2, heapN N heap_ctx inv N (lock_inv γ1 γ2 l R)
own γ2 (Excl ()))%I.
Global Instance lock_inv_ne n γ1 γ2 l : Proper (dist n ==> dist n) (lock_inv γ1 γ2 l).
Proof. solve_proper. Qed.
Global Instance is_lock_ne n l: Proper (dist n ==> dist n) (is_lock l).
Proof. solve_proper. Qed.
Global Instance locked_ne n l: Proper (dist n ==> dist n) (locked l).
Proof. solve_proper. Qed.
Global Instance is_lock_persistent l R : PersistentP (is_lock l R).
Proof. apply _. Qed.
Lemma newlock_spec (R : iProp) Φ :
heapN N
heap_ctx R ( l, is_lock l R - Φ #l) WP newlock #() {{ Φ }}.
Proof.
iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
wp_seq. wp_alloc l as "Hl".
iPvs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
iPvs (own_alloc_strong (Auth (Excl' ) ) _ {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.
iPvs (inv_alloc N _ (lock_inv γ1 γ2 l R) with "[-HΦ]"); first done.
{ iNext. rewrite /lock_inv.
iExists 0%nat, 0%nat.
iFrame.
iSplitL "Hγ1".
{ rewrite /auth_inv.
iExists (GSet ).
by iFrame. }
iLeft.
by iFrame. }
iPvsIntro.
iApply "HΦ".
iExists γ1, γ2.
iSplit; by auto.
Qed.
Lemma wait_loop_spec l x R (Φ : val iProp) :
issued l x R ( l, locked l R - R - Φ #()) WP wait_loop #x #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Ht)".
iLöb as "IH". wp_rec. wp_let. wp_focus (! _)%E.
iInv N as (o n) "[Hl Ha]".
wp_load. iPvsIntro.
destruct (decide (x = o)) as [Heq|Hneq].
- subst.
iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+ iSplitL "Hl Hainv Ht".
* iNext.
iExists o, n.
iFrame.
by iRight.
* wp_proj. wp_let. wp_op=>[_|[]] //.
wp_if. iPvsIntro.
iApply ("HΦ" with "[-HR] HR"). iExists γ1, γ2; eauto.
+ iExFalso. iCombine "Ht" "Haown" as "Haown".
iDestruct (auth_own_valid with "Haown") as % ?%gset_disj_valid_op.
set_solver.
- iSplitL "Hl Ha".
+ iNext. iExists o, n. by iFrame.
+ wp_proj. wp_let. wp_op=>?; first omega.
wp_if. by iApply ("IH" with "Ht").
Qed.
Lemma acquire_spec l R (Φ : val iProp) :
is_lock l R ( l, locked l R - R - Φ #()) WP acquire #l {{ Φ }}.
Proof.
iIntros "[Hl HΦ]". iDestruct "Hl" as (γ1 γ2) "(% & #? & #?)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iInv N as (o n) "[Hl Ha]".
wp_load. iPvsIntro.
iSplitL "Hl Ha".
- iNext. iExists o, n. by iFrame.
- wp_let. wp_proj. wp_proj. wp_op.
wp_focus (CAS _ _ _).
iInv N as (o' n') "[Hl [Hainv Haown]]".
destruct (decide ((#o', #n') = (#o, #n)))%V
as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
+ wp_cas_suc.
iDestruct "Hainv" as (s) "[Ho %]"; subst.
iPvs (own_update with "Ho") as "Ho".
{ eapply auth_update_no_frag, (gset_alloc_empty_local_update n).
rewrite elem_of_seq_set; omega. }
iDestruct "Ho" as "[Hofull Hofrag]".
iSplitL "Hl Haown Hofull".
* rewrite gset_disj_union; last by apply (seq_set_S_disjoint 0).
rewrite -(seq_set_S_union_L 0).
iPvsIntro. iNext.
iExists o, (S n)%nat.
rewrite Nat2Z.inj_succ -Z.add_1_r.
iFrame. iExists (GSet (seq_set 0 (S n))).
by iFrame.
* iPvsIntro. wp_if. wp_proj.
iApply wait_loop_spec.
iSplitR "HΦ"; last by done.
rewrite /issued /auth_own; eauto 10.
+ wp_cas_fail.
iPvsIntro.
iSplitL "Hl Hainv Haown".
{ iNext. iExists o', n'. by iFrame. }
{ wp_if. by iApply "IH". }
Qed.
Lemma release_spec R l (Φ : val iProp):
locked l R R Φ #() WP release #l {{ Φ }}.
Proof.
iIntros "(Hl & HR & HΦ)"; iDestruct "Hl" as (γ1 γ2) "(% & #? & #? & Hγ)".
iLöb as "IH". wp_rec. wp_focus (! _)%E.
iInv N as (o n) "[Hl Hr]".
wp_load. iPvsIntro.
iSplitL "Hl Hr".
- iNext. iExists o, n. by iFrame.
- wp_let. wp_focus (CAS _ _ _ ).
wp_proj. wp_op. wp_proj.
iInv N as (o' n') "[Hl Hr]".
destruct (decide ((#o', #n') = (#o, #n)))%V
as [[= ->%Nat2Z.inj ->%Nat2Z.inj] | Hneq].
+ wp_cas_suc.
iDestruct "Hr" as "[Hainv [[Ho _] | Hown]]".
* iExFalso. iCombine "Hγ" "Ho" as "Ho".
iDestruct (own_valid with "#Ho") as %[].
* iSplitL "Hl HR Hγ Hainv".
{ iPvsIntro. iNext. iExists (o + 1)%nat, n%nat.
iFrame. rewrite Nat2Z.inj_add.
iFrame. iLeft; by iFrame. }
{ iPvsIntro. by wp_if. }
+ wp_cas_fail.
iPvsIntro.
iSplitL "Hl Hr".
* iNext. iExists o', n'. by iFrame.
* wp_if. by iApply ("IH" with "Hγ HR").
Qed.
End proof.
Typeclasses Opaque is_lock issued locked.
......@@ -13,7 +13,7 @@ Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
Global Instance into_sep_mapsto l q v :
IntoSep false (l {q} v) (l {q/2} v) (l {q/2} v).
Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
Proof. by rewrite /IntoSep heap_mapsto_op_eq Qp_div_2. Qed.
Lemma tac_wp_alloc Δ Δ' E j e v Φ :
to_val e = Some v
......
......@@ -948,3 +948,38 @@ Section more_finite.
intros x ?; destruct (decide (x Y)); rewrite elem_of_app; set_solver.
Qed.
End more_finite.
(** Sets of sequences of natural numbers *)
(* The set [seq_seq start len] of natural numbers contains the sequence
[start, start + 1, ..., start + (len-1)]. *)
Fixpoint seq_set `{Singleton nat C, Union C, Empty C} (start len : nat) : C :=
match len with
| O =>
| S len' => {[ start ]} seq_set (S start) len'
end.
Section seq_set.
Context `{SimpleCollection nat C}.
Implicit Types start len x : nat.
Lemma elem_of_seq_set start len x :
x seq_set start len start x < start + len.
Proof.
revert start. induction len as [|len IH]; intros start; simpl.
- rewrite elem_of_empty. omega.
- rewrite elem_of_union, elem_of_singleton, IH. omega.
Qed.
Lemma seq_set_S_disjoint start len : {[ start + len ]} seq_set start len.
Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
Lemma seq_set_S_union start len :
seq_set start (C:=C) (S len) {[ start + len ]} seq_set start len.
Proof.
intros x. rewrite elem_of_union, elem_of_singleton, !elem_of_seq_set. omega.
Qed.
Lemma seq_set_S_union_L `{!LeibnizEquiv C} start len :
seq_set start (S len) = {[ start + len ]} seq_set start len.
Proof. unfold_leibniz. apply seq_set_S_union. Qed.
End seq_set.
......@@ -82,7 +82,7 @@ Proof. intros. destruct (Nat_mul_split_l n x2 x1 y2 y1); auto with lia. Qed.
Notation lcm := Nat.lcm.
Notation divide := Nat.divide.
Notation "( x | y )" := (divide x y) : nat_scope.
Instance divide_dec x y : Decision (x | y).
Instance Nat_divide_dec x y : Decision (x | y).
Proof.
refine (cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
Defined.
......@@ -94,6 +94,11 @@ Hint Extern 0 (_ | _) => reflexivity.
Lemma Nat_divide_ne_0 x y : (x | y) y 0 x 0.
Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
Lemma Nat_iter_S {A} n (f: A A) x : Nat.iter (S n) f x = f (Nat.iter n f x).
Proof. done. Qed.
Lemma Nat_iter_S_r {A} n (f: A A) x : Nat.iter (S n) f x = Nat.iter n f (f x).
Proof. induction n; f_equal/=; auto. Qed.
(** * Notations and properties of [positive] *)
Open Scope positive_scope.
......@@ -226,16 +231,19 @@ Infix "`rem`" := Z.rem (at level 35) : Z_scope.
Infix "≪" := Z.shiftl (at level 35) : Z_scope.
Infix "≫" := Z.shiftr (at level 35) : Z_scope.
Instance: Inj (=) (=) Zpos.
Instance Zpos_inj : Inj (=) (=) Zpos.
Proof. by injection 1. Qed.
Instance: Inj (=) (=) Zneg.
Instance Zneg_inj : Inj (=) (=) Zneg.
Proof. by injection 1. Qed.
Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.
Instance Z_eq_dec: x y : Z, Decision (x = y) := Z.eq_dec.
Instance Z_le_dec: x y : Z, Decision (x y) := Z_le_dec.
Instance Z_lt_dec: x y : Z, Decision (x < y) := Z_lt_dec.
Instance Z_inhabited: Inhabited Z := populate 1.
Instance: PartialOrder ().
Instance Z_le_order : PartialOrder ().
Proof.
repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
Qed.
......
......@@ -56,6 +56,10 @@ Section auth.
Lemma auth_own_op γ a b : auth_own γ (a b) auth_own γ a auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Global Instance from_sep_own_authM γ a b :
FromSep (auth_own γ (a b)) (auth_own γ a) (auth_own γ b) | 90.
Proof. by rewrite /FromSep auth_own_op. Qed.
Lemma auth_own_mono γ a b : a b auth_own γ b auth_own γ a.
Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
......
From iris.algebra Require Import upred.
From iris.proofmode Require Import tactics.
(** This proves that we need the ▷ in a "Saved Proposition" construction with
name-dependend allocation. *)
(** We fork in [uPred M] for any M, but the proof would work in any BI. *)
Section savedprop.
Context (M : ucmraT).
Notation iProp := (uPred M).
Notation "¬ P" := ( (P False))%I : uPred_scope.
Implicit Types P : iProp.
(* Saved Propositions and view shifts. *)
Context (sprop : Type) (saved : sprop iProp iProp) (pvs : iProp iProp).
Hypothesis pvs_mono : P Q, (P Q) pvs P pvs Q.
Hypothesis sprop_persistent : i P, PersistentP (saved i P).
Hypothesis sprop_alloc_dep :
(P : sprop iProp), True pvs ( i, saved i (P i)).
Hypothesis sprop_agree : i P Q, saved i P saved i Q P Q.
(* Self-contradicting assertions are inconsistent *)
Lemma no_self_contradiction P `{!PersistentP P} : (P ¬ P) False.
Proof.
iIntros "#[H1 H2]".
iAssert P as "#HP".
{ iApply "H2". iIntros "! #HP". by iApply ("H1" with "[#]"). }
by iApply ("H1" with "[#]").
Qed.
(* "Assertion with name [i]" is equivalent to any assertion P s.t. [saved i P] *)
Definition A (i : sprop) : iProp := P, saved i P P.
Lemma saved_is_A i P `{!PersistentP P} : saved i P (A i P).
Proof.
iIntros "#HS !". iSplit.
- iDestruct 1 as (Q) "[#HSQ HQ]".
iApply (sprop_agree i P Q with "[]"); eauto.
- iIntros "#HP". iExists P. by iSplit.
Qed.
(* Define [Q i] to be "negated assertion with name [i]". Show that this
implies that assertion with name [i] is equivalent to its own negation. *)
Definition Q i := saved i (¬ A i).
Lemma Q_self_contradiction i : Q i (A i ¬ A i).
Proof. iIntros "#HQ !". by iApply (saved_is_A i (¬A i)). Qed.
(* We can obtain such a [Q i]. *)
Lemma make_Q : True pvs ( i, Q i).
Proof. apply sprop_alloc_dep. Qed.
(* Put together all the pieces to derive a contradiction. *)
(* TODO: Have a lemma in upred.v that says that we cannot view shift to False. *)
Lemma contradiction : True pvs False.
Proof.
rewrite make_Q. apply pvs_mono. iDestruct 1 as (i) "HQ".
iApply (no_self_contradiction (A i)). by iApply Q_self_contradiction.
Qed.
End savedprop.
......@@ -92,10 +92,12 @@ Global Instance from_later_sep P1 P2 Q1 Q2 :
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
(* IntoWand *)
Global Instance into_wand_wand P Q : IntoWand (P - Q) P Q.
Proof. done. Qed.
Global Instance into_wand_impl P Q : IntoWand (P Q) P Q.
Proof. apply impl_wand. Qed.
Global Instance into_wand_wand P Q Q' :
FromAssumption false Q Q' IntoWand (P - Q) P Q'.
Proof. by rewrite /FromAssumption /IntoWand /= => ->. Qed.
Global Instance into_wand_impl P Q Q' :
FromAssumption false Q Q' IntoWand (P Q) P Q'.
Proof. rewrite /FromAssumption /IntoWand /= => ->. by rewrite impl_wand. Qed.
Global Instance into_wand_iff_l P Q : IntoWand (P Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance into_wand_iff_r P Q : IntoWand (P Q) Q P.
......@@ -230,7 +232,7 @@ Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed.
Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed.
Global Instance make_and_default P Q : MakeSep P Q (P Q) | 100.
Global Instance make_and_default P Q : MakeAnd P Q (P Q) | 100.
Proof. done. Qed.
Global Instance frame_and_l R P1 P2 Q Q' :