Commit e60b556f authored by Ralf Jung's avatar Ralf Jung

bump std++, use the new [default] notation

parent df1feae2
Pipeline #9087 passed with stage
in 14 minutes and 35 seconds
......@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
"coq-stdpp" { (= "dev.2018-05-24.0.de797b31") | (= "dev") }
"coq-stdpp" { (= "dev.2018-05-29.0.4014c929") | (= "dev") }
]
......@@ -179,7 +179,7 @@ Class Core (A : Type) := core : A → A.
Hint Mode Core ! : typeclass_instances.
Instance: Params (@core) 2.
Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
Arguments core' _ _ _ /.
(** * CMRAs with a unit element *)
......
......@@ -46,7 +46,7 @@ Section coPset.
Proof. split. done. intros X. by rewrite coPset_op_union left_id_L. done. Qed.
Canonical Structure coPsetUR := UcmraT coPset coPset_ucmra_mixin.
Lemma coPset_opM X mY : X ? mY = X from_option id mY.
Lemma coPset_opM X mY : X ? mY = X default mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
Lemma coPset_update X Y : X ~~> Y.
......
......@@ -55,7 +55,7 @@ Section gmultiset.
apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X )).
Qed.
Lemma gmultiset_opM X mY : X ? mY = X from_option id mY.
Lemma gmultiset_opM X mY : X ? mY = X default mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
Lemma gmultiset_update X Y : X ~~> Y.
......
......@@ -45,7 +45,7 @@ Section gset.
Proof. split. done. intros X. by rewrite gset_op_union left_id_L. done. Qed.
Canonical Structure gsetUR := UcmraT (gset K) gset_ucmra_mixin.
Lemma gset_opM X mY : X ? mY = X from_option id mY.
Lemma gset_opM X mY : X ? mY = X default mY.
Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
Lemma gset_update X Y : X ~~> Y.
......
......@@ -56,7 +56,7 @@ Canonical Structure listC := OfeT (list A) list_ofe_mixin.
Program Definition list_chain
(c : chain listC) (x : A) (k : nat) : chain A :=
{| chain_car n := from_option id x (c n !! k) |}.
{| chain_car n := default x (c n !! k) |}.
Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
Definition list_compl `{Cofe A} : Compl listC := λ c,
match c 0 with
......@@ -354,7 +354,7 @@ Section properties.
x ~~>: P ( y, P y Q [y]) [x] ~~>: Q.
Proof.
rewrite !cmra_total_updateP=> Hup HQ n lf /list_lookup_validN Hv.
destruct (Hup n (from_option id ε (lf !! 0))) as (y&?&Hv').
destruct (Hup n (default ε (lf !! 0))) as (y&?&Hv').
{ move: (Hv 0). by destruct lf; rewrite /= ?right_id. }
exists [y]; split; first by auto.
apply list_lookup_validN=> i.
......
......@@ -905,7 +905,7 @@ Section option.
Canonical Structure optionC := OfeT (option A) option_ofe_mixin.
Program Definition option_chain (c : chain optionC) (x : A) : chain A :=
{| chain_car n := from_option id x (c n) |}.
{| chain_car n := default x (c n) |}.
Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Definition option_compl `{Cofe A} : Compl optionC := λ c,
match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
......
......@@ -13,7 +13,7 @@ Module bi_reflection. Section bi_reflection.
Fixpoint eval (Σ : list PROP) (e : expr) : PROP :=
match e with
| EEmp => emp
| EVar n => from_option id emp (Σ !! n)
| EVar n => default emp (Σ !! n)
| ESep e1 e2 => eval Σ e1 eval Σ e2
end%I.
Fixpoint flatten (e : expr) : list nat :=
......@@ -23,7 +23,7 @@ Module bi_reflection. Section bi_reflection.
| ESep e1 e2 => flatten e1 ++ flatten e2
end.
Notation eval_list Σ l := ([ list] n l, from_option id emp (Σ !! n))%I.
Notation eval_list Σ l := ([ list] n l, default emp (Σ !! n))%I.
Lemma eval_flatten Σ e : eval Σ e eval_list Σ (flatten e).
Proof.
......
......@@ -526,7 +526,7 @@ Hint Mode IntoInv + ! - : typeclass_instances.
instances to recognize the [emp] case and make it look nicer. *)
Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP PROP)
(α β : X PROP) (mγ : X option PROP) : PROP :=
M1 ( x, α x (β x - M2 (from_option id emp (mγ x))))%I.
M1 ( x, α x (β x - M2 (default emp (mγ x))))%I.
(* Typeclass for assertions around which accessors can be elliminated.
Inputs: [Q], [E1], [E2], [α], [β], [γ]
......@@ -582,7 +582,7 @@ Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
(Pinv Pin : PROP) (Pout : X PROP) (mPclose : option (X PROP))
(Q : PROP) (Q' : X PROP) :=
elim_inv : φ Pinv Pin ( x, Pout x (from_option id (λ _, emp) mPclose) x - Q' x) Q.
elim_inv : φ Pinv Pin ( x, Pout x (default (λ _, emp) mPclose) x - Q' x) Q.
Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
......
......@@ -445,7 +445,7 @@ Proof.
Qed.
Lemma maybe_wand_sound (mP : option PROP) Q :
maybe_wand mP Q (from_option id emp mP - Q).
maybe_wand mP Q (default emp mP - Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
Global Instance envs_Forall2_refl (R : relation PROP) :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment