Commit 9365ea8b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Generalize from_option and define default using it.

parent e36e7f99
...@@ -225,7 +225,7 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive := ...@@ -225,7 +225,7 @@ Fixpoint coPpick_raw (t : coPset_raw) : option positive :=
| Some i => Some (i~0) | None => (~1) <$> coPpick_raw r | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r
end end
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. Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i e_of i t.
Proof. Proof.
......
...@@ -12,7 +12,7 @@ Arguments NoDup_enum _ {_ _} : clear implicits. ...@@ -12,7 +12,7 @@ Arguments NoDup_enum _ {_ _} : clear implicits.
Definition card A `{Finite A} := length (enum A). Definition card A `{Finite A} := length (enum A).
Program Instance finite_countable `{Finite A} : Countable A := {| Program Instance finite_countable `{Finite A} : Countable A := {|
encode := λ x, 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) decode := λ p, enum A !! pred (Pos.to_nat p)
|}. |}.
Arguments Pos.of_nat _ : simpl never. Arguments Pos.of_nat _ : simpl never.
...@@ -127,7 +127,7 @@ Lemma finite_surj A `{Finite A} B `{Finite B} : ...@@ -127,7 +127,7 @@ Lemma finite_surj A `{Finite A} B `{Finite B} :
0 < card A card B g : B A, Surj (=) g. 0 < card A card B g : B A, Surj (=) g.
Proof. Proof.
intros [??]. destruct (finite_inhabited A) as [x']; auto with lia. 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). intros x. destruct (encode_decode B (encode_nat x)) as (y&Hy1&Hy2).
{ pose proof (encode_lt_card x); lia. } { pose proof (encode_lt_card x); lia. }
exists y. by rewrite Hy2, decode_encode_nat. exists y. by rewrite Hy2, decode_encode_nat.
......
...@@ -3393,7 +3393,7 @@ Definition eval {A} (E : env A) : rlist nat → list A := ...@@ -3393,7 +3393,7 @@ Definition eval {A} (E : env A) : rlist nat → list A :=
fix go t := fix go t :=
match t with match t with
| rnil => [] | rnil => []
| rnode i => from_option [] (E !! i) | rnode i => from_option id [] (E !! i)
| rapp t1 t2 => go t1 ++ go t2 | rapp t1 t2 => go t1 ++ go t2
end. end.
...@@ -3427,7 +3427,7 @@ End quote. ...@@ -3427,7 +3427,7 @@ End quote.
Section eval. Section eval.
Context {A} (E : env A). 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. Proof.
induction t; csimpl. induction t; csimpl.
- done. - done.
......
...@@ -19,16 +19,15 @@ Proof. congruence. Qed. ...@@ -19,16 +19,15 @@ Proof. congruence. Qed.
Instance Some_inj {A} : Inj (=) (=) (@Some A). Instance Some_inj {A} : Inj (=) (=) (@Some A).
Proof. congruence. Qed. Proof. congruence. Qed.
(** The non dependent elimination principle on the option type. *) (** The [from_option] is the eliminator for option. *)
Definition default {A B} (y : B) (mx : option A) (f : A B) : B := Definition from_option {A B} (f : A B) (y : B) (mx : option A) : B :=
match mx with None => y | Some x => f x end. 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 (* The eliminator again, but with the arguments in different order, which is
type by specifying a default value. *) sometimes more convenient. *)
Definition from_option {A} (x : A) (mx : option A) : A := Notation default y mx f := (from_option f y mx) (only parsing).
match mx with None => x | Some y => y end.
Instance: Params (@from_option) 1.
(** An alternative, but equivalent, definition of equality on the option (** An alternative, but equivalent, definition of equality on the option
data type. This theorem is useful to prove that two options are the same. *) data type. This theorem is useful to prove that two options are the same. *)
...@@ -137,9 +136,9 @@ Section setoids. ...@@ -137,9 +136,9 @@ Section setoids.
Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A). Global Instance is_Some_proper : Proper (() ==> iff) (@is_Some A).
Proof. inversion_clear 1; split; eauto. Qed. Proof. inversion_clear 1; split; eauto. Qed.
Global Instance from_option_proper : Global Instance from_option_proper {B} (R : relation B) (f : A B) :
Proper (() ==> () ==> ()) (@from_option A). Proper (() ==> R) f Proper (R ==> () ==> R) (from_option f).
Proof. by destruct 2. Qed. Proof. destruct 3; simpl; auto. Qed.
End setoids. End setoids.
Typeclasses Opaque option_equiv. Typeclasses Opaque option_equiv.
...@@ -323,9 +322,7 @@ Tactic Notation "simpl_option" "by" tactic3(tac) := ...@@ -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 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] |- _ => | 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 let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
| H : context [default (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 [from_option (A:=?A) _ ?mx] |- _ =>
let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
| H : context [ match ?mx with _ => _ end ] |- _ => | H : context [ match ?mx with _ => _ end ] |- _ =>
match type of mx with match type of mx with
...@@ -336,9 +333,7 @@ Tactic Notation "simpl_option" "by" tactic3(tac) := ...@@ -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 let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
| |- context [fmap (M:=option) (A:=?A) ?f ?mx] => | |- context [fmap (M:=option) (A:=?A) ?f ?mx] =>
let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
| |- context [default (A:=?A) _ ?mx _] => | |- context [from_option (A:=?A) _ _ ?mx] =>
let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
| |- context [from_option (A:=?A) _ ?mx] =>
let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
| |- context [ match ?mx with _ => _ end ] => | |- context [ match ?mx with _ => _ end ] =>
match type of mx with match type of mx with
......
Supports Markdown
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