Generalize from_option and define default using it.

algebra/cmra.v

@@ -765,7 +765,7 @@ Section option.
     by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
   Qed.
   Lemma option_updateP' (P : A → Prop) x :
-    x ~~>: P → Some x ~~>: λ my, default False my P.
+    x ~~>: P → Some x ~~>: from_option P False.
   Proof. eauto using option_updateP. Qed.
   Lemma option_update x y : x ~~> y → Some x ~~> Some y.
   Proof.

algebra/cmra_tactics.v

@@ -11,7 +11,7 @@ Module ra_reflection. Section ra_reflection.
     | EOp : expr → expr → expr.
   Fixpoint eval (Σ : list A) (e : expr) : A :=
     match e with
-    | EVar n => from_option ∅ (Σ !! n)
+    | EVar n => from_option id ∅ (Σ !! n)
     | EEmpty => ∅
     | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
     end.
@@ -22,7 +22,7 @@ Module ra_reflection. Section ra_reflection.
     | EOp e1 e2 => flatten e1 ++ flatten e2
     end.
   Lemma eval_flatten Σ e :
-    eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
+    eval Σ e ≡ big_op ((λ n, from_option id ∅ (Σ !! n)) <$> flatten e).
   Proof.
     by induction e as [| |e1 IH1 e2 IH2];
       rewrite /= ?right_id ?fmap_app ?big_op_app ?IH1 ?IH2.

algebra/cofe.v

@@ -542,7 +542,7 @@ Section option.
   Proof. done. Qed.
 
   Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
-    {| chain_car n := from_option x (c n) |}.
+    {| chain_car n := from_option id x (c n) |}.
   Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
   Instance option_compl : Compl (option A) := λ c,
     match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
@@ -569,9 +569,6 @@ Section option.
   Proof. destruct 1; split; eauto. Qed.
   Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
   Proof. by inversion_clear 1. Qed.
-  Global Instance from_option_ne n :
-    Proper (dist n ==> dist n ==> dist n) (@from_option A).
-  Proof. by destruct 2. Qed.
 
   Global Instance None_timeless : Timeless (@None A).
   Proof. inversion_clear 1; constructor. Qed.
@@ -595,6 +592,11 @@ End option.
 Typeclasses Opaque option_dist.
 Arguments optionC : clear implicits.
 
+Instance from_option_ne {A B : cofeT} (f : A → B) n :
+  Proper (dist n ==> dist n) f →
+  Proper (dist n ==> dist n ==> dist n) (from_option f).
+Proof. destruct 3; simpl; auto. Qed.
+
 Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
   Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
 Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.

algebra/gmap.v

@@ -270,7 +270,7 @@ Lemma singleton_updateP_empty `{Empty A, !CMRAUnit A}
   ∅ ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
 Proof.
   intros Hx HQ n gf Hg.
-  destruct (Hx n (from_option ∅ (gf !! i))) as (y&?&Hy).
+  destruct (Hx n (from_option id ∅ (gf !! i))) as (y&?&Hy).
   { move:(Hg i). rewrite !left_id.
     case _: (gf !! i); simpl; auto using cmra_unit_validN. }
   exists {[ i := y ]}; split; first by auto.

algebra/list.v

@@ -43,7 +43,7 @@ Global Instance resize_ne n :
 
 Program Definition list_chain
     (c : chain (list A)) (x : A) (k : nat) : chain A :=
-  {| chain_car n := from_option x (c n !! k) |}.
+  {| chain_car n := from_option id x (c n !! k) |}.
 Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
 Instance list_compl : Compl (list A) := λ c,
   match c 0 with

algebra/upred.v

@@ -1202,8 +1202,8 @@ Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
 Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
 Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
 Proof. intros. by rewrite /PersistentP always_ownM. Qed.
-Global Instance default_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
-  PersistentP P → (∀ x, PersistentP (Ψ x)) → PersistentP (default P mx Ψ).
+Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
+  (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx).
 Proof. destruct mx; apply _. Qed.
 
 (* Derived lemmas for persistence *)

algebra/upred_tactics.v

@@ -12,7 +12,7 @@ Module uPred_reflection. Section uPred_reflection.
   Fixpoint eval (Σ : list (uPred M)) (e : expr) : uPred M :=
     match e with
     | ETrue => True
-    | EVar n => from_option True%I (Σ !! n)
+    | EVar n => from_option id True%I (Σ !! n)
     | ESep e1 e2 => eval Σ e1 ★ eval Σ e2
     end.
   Fixpoint flatten (e : expr) : list nat :=
@@ -22,7 +22,7 @@ Module uPred_reflection. Section uPred_reflection.
     | ESep e1 e2 => flatten e1 ++ flatten e2
     end.
 
-  Notation eval_list Σ l := ([★] ((λ n, from_option True%I (Σ !! n)) <$> l))%I.
+  Notation eval_list Σ l := ([★] ((λ n, from_option id True%I (Σ !! n)) <$> l))%I.
   Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
   Proof.
     induction e as [| |e1 IH1 e2 IH2];

prelude/co_pset.v

@@ -225,7 +225,7 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
      | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
      end
   end.
-Definition coPpick (X : coPset) : positive := from_option 1 (coPpick_raw (`X)).
+Definition coPpick (X : coPset) : positive := from_option id 1 (coPpick_raw (`X)).
 
 Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i → e_of i t.
 Proof.

prelude/finite.v

@@ -12,7 +12,7 @@ Arguments NoDup_enum _ {_ _} : clear implicits.
 Definition card A `{Finite A} := length (enum A).
 Program Instance finite_countable `{Finite A} : Countable A := {|
   encode := λ x,
-    Pos.of_nat $ S $ from_option 0 $ fst <$> list_find (x =) (enum A);
+    Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A);
   decode := λ p, enum A !! pred (Pos.to_nat p)
 |}.
 Arguments Pos.of_nat _ : simpl never.
@@ -127,7 +127,7 @@ Lemma finite_surj A `{Finite A} B `{Finite B} :
   0 < card A ≤ card B → ∃ g : B → A, Surj (=) g.
 Proof.
   intros [??]. destruct (finite_inhabited A) as [x']; auto with lia.
-  exists (λ y : B, from_option x' (decode_nat (encode_nat y))).
+  exists (λ y : B, from_option id x' (decode_nat (encode_nat y))).
   intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2).
   { pose proof (encode_lt_card x); lia. }
   exists y. by rewrite Hy2, decode_encode_nat.

prelude/list.v

@@ -3393,7 +3393,7 @@ Definition eval {A} (E : env A) : rlist nat → list A :=
   fix go t :=
   match t with
   | rnil => []
-  | rnode i => from_option [] (E !! i)
+  | rnode i => from_option id [] (E !! i)
   | rapp t1 t2 => go t1 ++ go t2
   end.
 
@@ -3427,7 +3427,7 @@ End quote.
 Section eval.
   Context {A} (E : env A).
 
-  Lemma eval_alt t : eval E t = to_list t ≫= from_option [] ∘ (E !!).
+  Lemma eval_alt t : eval E t = to_list t ≫= from_option id [] ∘ (E !!).
   Proof.
     induction t; csimpl.
     - done.

prelude/option.v

@@ -19,16 +19,15 @@ Proof. congruence. Qed.
 Instance Some_inj {A} : Inj (=) (=) (@Some A).
 Proof. congruence. Qed.
 
-(** The non dependent elimination principle on the option type. *)
-Definition default {A B} (y : B) (mx : option A) (f : A → B)  : B :=
+(** The [from_option] is the eliminator for option. *)
+Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
   match mx with None => y | Some x => f x end.
-Instance: Params (@default) 2.
+Instance: Params (@from_option) 3.
+Arguments from_option {_ _} _ _ !_ /.
 
-(** The [from_option] function allows us to get the value out of the option
-type by specifying a default value. *)
-Definition from_option {A} (x : A) (mx : option A) : A :=
-  match mx with None => x | Some y => y end.
-Instance: Params (@from_option) 1.
+(* The eliminator again, but with the arguments in different order, which is
+sometimes more convenient. *)
+Notation default y mx f := (from_option f y mx) (only parsing).
 
 (** An alternative, but equivalent, definition of equality on the option
 data type. This theorem is useful to prove that two options are the same. *)
@@ -137,9 +136,9 @@ Section setoids.
 
   Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A).
   Proof. inversion_clear 1; split; eauto. Qed.
-  Global Instance from_option_proper :
-    Proper ((≡) ==> (≡) ==> (≡)) (@from_option A).
-  Proof. by destruct 2. Qed.
+  Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
+    Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
+  Proof. destruct 3; simpl; auto. Qed.
 End setoids.
 
 Typeclasses Opaque option_equiv.
@@ -323,9 +322,7 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
   | H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
-  | H : context [default (A:=?A) _ ?mx _] |- _ =>
-    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
-  | H : context [from_option (A:=?A) _ ?mx] |- _ =>
+  | H : context [from_option (A:=?A) _ _ ?mx] |- _ =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
   | H : context [ match ?mx with _ => _ end ] |- _ =>
     match type of mx with
@@ -336,9 +333,7 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
   | |- context [fmap (M:=option) (A:=?A) ?f ?mx] =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
-  | |- context [default (A:=?A) _ ?mx _] =>
-    let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
-  | |- context [from_option (A:=?A) _ ?mx] =>
+  | |- context [from_option (A:=?A) _ _ ?mx] =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
   | |- context [ match ?mx with _ => _ end ] =>
     match type of mx with

proofmode/coq_tactics.v

@@ -752,7 +752,7 @@ Qed.
 (** The [option] is to account for formulas that can be framed entirely, so
 we do not end up with [True]s everywhere. *)
 Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
-  frame : (R ★ from_option True mQ) ⊢ P.
+  frame : (R ★ from_option id True mQ) ⊢ P.
 Arguments frame : clear implicits.
 
 Global Instance frame_here R : Frame R R None.