Commit 6d849e7d authored by Ralf Jung's avatar Ralf Jung

introduce [default] as abbreviation for [from_option id], and use it

parent de797b31
......@@ -251,7 +251,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 id 1 (coPpick_raw (`X)).
Definition coPpick (X : coPset) : positive := default 1 (coPpick_raw (`X)).
Lemma coPpick_raw_elem_of t i : coPpick_raw t = Some i e_of i t.
Proof.
......
......@@ -17,7 +17,7 @@ Definition card A `{Finite A} := length (enum A).
Program Definition finite_countable `{Finite A} : Countable A := {|
encode := λ x,
Pos.of_nat $ S $ from_option id 0 $ fst <$> list_find (x =) (enum A);
Pos.of_nat $ S $ default 0 $ fst <$> list_find (x =) (enum A);
decode := λ p, enum A !! pred (Pos.to_nat p)
|}.
Arguments Pos.of_nat : simpl never.
......@@ -134,7 +134,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 id x' (decode_nat (encode_nat y))).
exists (λ y : B, default 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.
......
......@@ -131,7 +131,7 @@ Definition gmap_curry `{Countable K1, Countable K2} {A} :
Definition gmap_uncurry `{Countable K1, Countable K2} {A} :
gmap (K1 * K2) A gmap K1 (gmap K2 A) :=
map_fold (λ ii x, let '(i1,i2) := ii in
partial_alter (Some <[i2:=x]> from_option id ) i1) .
partial_alter (Some <[i2:=x]> default ) i1) .
Section curry_uncurry.
Context `{Countable K1, Countable K2} {A : Type}.
......
......@@ -484,7 +484,7 @@ Lemma list_lookup_middle l1 l2 x n :
n = length l1 (l1 ++ x :: l2) !! n = Some x.
Proof. intros ->. by induction l1. Qed.
Lemma nth_lookup l i d : nth i l d = from_option id d (l !! i).
Lemma nth_lookup l i d : nth i l d = default d (l !! i).
Proof. revert i. induction l as [|x l IH]; intros [|i]; simpl; auto. Qed.
Lemma nth_lookup_Some l i d x : l !! i = Some x nth i l d = x.
Proof. rewrite nth_lookup. by intros ->. Qed.
......@@ -3561,7 +3561,7 @@ Definition eval {A} (E : env A) : rlist nat → list A :=
fix go t :=
match t with
| rnil => []
| rnode i => from_option id [] (E !! i)
| rnode i => default [] (E !! i)
| rapp t1 t2 => go t1 ++ go t2
end.
......@@ -3595,7 +3595,7 @@ End quote.
Section eval.
Context {A} (E : env A).
Lemma eval_alt t : eval E t = to_list t = from_option id [] (E !!).
Lemma eval_alt t : eval E t = to_list t = default [] (E !!).
Proof.
induction t; csimpl.
- done.
......
......@@ -26,6 +26,9 @@ Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
Instance: Params (@from_option) 3.
Arguments from_option {_ _} _ _ !_ / : assert.
(* The eliminator with the identity function. *)
Notation default := (from_option id).
(** An alternative, but equivalent, definition of equality on the option
data type. This theorem is useful to prove that two options are the same. *)
Lemma option_eq {A} (mx my: option A): mx = my x, mx = Some x my = Some x.
......
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