From 9365ea8ba93d571c3b2b06c062540dd767fd1eec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 26 May 2016 14:34:32 +0200
Subject: [PATCH] Generalize from_option and define default using it.

---
 theories/co_pset.v |  2 +-
 theories/finite.v  |  4 ++--
 theories/list.v    |  4 ++--
 theories/option.v  | 29 ++++++++++++-----------------
 4 files changed, 17 insertions(+), 22 deletions(-)

diff --git a/theories/co_pset.v b/theories/co_pset.v
index 19ea8bd7..2d5e38d9 100644
--- a/theories/co_pset.v
+++ b/theories/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.
diff --git a/theories/finite.v b/theories/finite.v
index fd15244b..a091c036 100644
--- a/theories/finite.v
+++ b/theories/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.
diff --git a/theories/list.v b/theories/list.v
index 6060b9e0..0d7f6cea 100644
--- a/theories/list.v
+++ b/theories/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.
diff --git a/theories/option.v b/theories/option.v
index e79e2ef4..24552ced 100644
--- a/theories/option.v
+++ b/theories/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
-- 
GitLab