phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/numbers.v *)
Lemma rotate_nat_sub_add base len offset:
  offset < len →
  rotate_nat_sub base (rotate_nat_add base offset len) len = offset.
Proof.
  intros ?. unfold rotate_nat_add, rotate_nat_sub.
  rewrite Z2Nat.id by (apply Z.mod_pos; lia).
  assert (∀ n, (Z.of_nat len + n - Z.of_nat base) = ((Z.of_nat len - Z.of_nat base) + n))%Z
    as -> by naive_solver lia.
  rewrite Zplus_mod_idemp_r.
  replace (Z.of_nat len - Z.of_nat base + (Z.of_nat base + Z.of_nat offset))%Z with
    (Z.of_nat len + Z.of_nat offset)%Z by lia.
  rewrite (Z.mod_in_range 1) by lia.
  rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_add_add base offset len n:
  0 < len →
  rotate_nat_add base (offset + n) len =
  (rotate_nat_add base offset len + n) `mod` len.
Proof.
  intros ?. unfold rotate_nat_add.
  rewrite !Z2Nat.inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia.
  by rewrite Nat.add_assoc, Nat.Div0.add_mod_idemp_l by lia.
Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_add_S base offset len:
  0 < len →
  rotate_nat_add base (S offset) len =
  S (rotate_nat_add base offset len) `mod` len.
Proof. intros ?. by rewrite <-Nat.add_1_r, rotate_nat_add_add, Nat.add_1_r. Qed.
(* stdpp/option.v *)
Inductive option_reflect {A} (P : A → Prop) (Q : Prop) : option A → Type
:=
  | ReflectSome x : P x → option_reflect P Q (Some x)
  | ReflectNone : Q → option_reflect P Q None.
(* stdpp/option.v *)
(* Basic properties about equality. *)
Lemma None_ne_Some {A} (x : A) : None ≠ Some x.
Proof. congruence. Qed.
(* stdpp/option.v *)
Lemma Some_ne_None {A} (x : A) : Some x ≠ None.
Proof. congruence. Qed.
(* stdpp/option.v *)
Lemma eq_None_ne_Some {A} (mx : option A) : (∀ x, mx ≠ Some x) ↔ mx = None.
Proof. destruct mx; split; congruence. Qed.
(* stdpp/option.v *)
Lemma eq_None_ne_Some_1 {A} (mx : option A) x : mx = None → mx ≠ Some x.
Proof. intros ?. by apply eq_None_ne_Some. Qed.
(* stdpp/option.v *)
Lemma eq_None_ne_Some_2 {A} (mx : option A) : (∀ x, mx ≠ Some x) → mx = None.
Proof. intros ?. by apply eq_None_ne_Some. Qed.
(* stdpp/option.v *)
Instance Some_inj {A} : Inj (=) (=) (@Some A).
Proof. congruence. Qed.
(* stdpp/option.v *)
(* 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.
(* stdpp/option.v *)
Instance : Params (@from_option) 2
:= {}.
(* stdpp/option.v *)
(* Predicate over member of [option A].
We define it with [Inductive] to allow [option_Forall] to be used in other
inductively defined predicates. *)
Inductive option_Forall {A} (P : A → Prop) : option A → Prop
:=
  | Forall_None : option_Forall P None
  | Forall_Some x : P x → option_Forall P (Some x).
(* stdpp/option.v *)
Instance : Params (@option_Forall) 1
:= {}.
(* stdpp/option.v *)
Lemma option_Forall_from_option P mx :
    option_Forall P mx ↔ from_option P True mx.
Proof. split; [by destruct 1|]. destruct mx; by constructor. Qed.
(* stdpp/option.v *)
Lemma option_Forall_true P mx : (∀ x, P x) → option_Forall P mx.
Proof. destruct mx; constructor; auto. Qed.
(* stdpp/option.v *)
Lemma option_Forall_impl P1 P2 mx :
    option_Forall P1 mx → (∀ x, P1 x → P2 x) → option_Forall P2 mx.
Proof. rewrite !option_Forall_from_option. destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma option_Forall_iff P1 P2 mx :
    (∀ a, P1 a ↔ P2 a) → (option_Forall P1 mx ↔ option_Forall P2 mx).
Proof. rewrite !option_Forall_from_option. destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma option_Forall_and P1 P2 mx :
    option_Forall (λ a, P1 a ∧ P2 a) mx
    ↔ option_Forall P1 mx ∧ option_Forall P2 mx.
Proof. rewrite !option_Forall_from_option. destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Instance option_Forall_proper :
    Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@option_Forall A).
Proof.
    intros P1 P2 HP [x|] ? <-; rewrite !option_Forall_from_option; simpl; auto.
  Qed.
(* stdpp/option.v *)
(* The eliminator with the identity function. *)
Notation default
:= (from_option id).
(* stdpp/option.v *)
(* 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.
Proof. split; [by intros; by subst |]. destruct mx, my; naive_solver. Qed.
(* stdpp/option.v *)
Lemma option_eq_1 {A} (mx my: option A) x : mx = my → mx = Some x → my = Some x.
Proof. congruence. Qed.
(* stdpp/option.v *)
Lemma option_eq_1_alt {A} (mx my : option A) x :
  mx = my → my = Some x → mx = Some x.
Proof. congruence. Qed.
(* stdpp/option.v *)
Lemma is_Some_alt {A} (mx : option A) :
  is_Some mx ↔ match mx with Some _ => True | None => False end.
Proof. unfold is_Some. destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma mk_is_Some {A} (mx : option A) x : mx = Some x → is_Some mx.
Proof. by intros ->. Qed.
(* stdpp/option.v *)
Lemma is_Some_None {A} : ¬is_Some (@None A).
Proof. by destruct 1. Qed.
(* stdpp/option.v *)
Lemma eq_None_not_Some {A} (mx : option A) : mx = None ↔ ¬is_Some mx.
Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma not_eq_None_Some {A} (mx : option A) : mx ≠ None ↔ is_Some mx.
Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Instance is_Some_pi {A} (mx : option A) : ProofIrrel (is_Some mx).
Proof.
  set (P (mx : option A) := match mx with Some _ => True | _ => False end).
  set (f mx := match mx return P mx → is_Some mx with
    Some _ => λ _, ex_intro _ _ eq_refl | None => False_rect _ end).
  set (g mx (H : is_Some mx) :=
    match H return P mx with ex_intro _ _ p => eq_rect _ _ I _ (eq_sym p) end).
  assert (∀ mx H, f mx (g mx H) = H) as f_g by (by intros ? [??]; subst).
  intros p1 p2. rewrite <-(f_g _ p1), <-(f_g _ p2). by destruct mx, p1.
Qed.
(* stdpp/option.v *)
Instance is_Some_dec {A} (mx : option A) : Decision (is_Some mx)
:=
  match mx with
  | Some x => left (ex_intro _ x eq_refl)
  | None => right is_Some_None
  end.
(* stdpp/option.v *)
Definition is_Some_proj {A} {mx : option A} : is_Some mx → A
:=
  match mx with Some x => λ _, x | None => False_rect _ ∘ is_Some_None end.
(* stdpp/option.v *)
Definition Some_dec {A} (mx : option A) : { x | mx = Some x } + { mx = None }
:=
  match mx return { x | mx = Some x } + { mx = None } with
  | Some x => inleft (x ↾ eq_refl _)
  | None => inright eq_refl
  end.
(* stdpp/option.v *)
(* Lifting a relation point-wise to option *)
Inductive option_Forall2 {A B} (R: A → B → Prop) : option A → option B → Prop
:=
  | Some_Forall2 x y : R x y → option_Forall2 R (Some x) (Some y)
  | None_Forall2 : option_Forall2 R None None.
(* stdpp/option.v *)
Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B → Prop)
    (mx : option A) (my : option B) : Prop
:=
  match mx, my with
  | Some x, Some y => R x y
  | Some x, None => P x
  | None, Some y => Q y
  | None, None => True
  end.
(* stdpp/option.v *)
Instance option_Forall2_refl : Reflexive R → Reflexive (option_Forall2 R).
Proof. intros ? [?|]; by constructor. Qed.
(* stdpp/option.v *)
Instance option_Forall2_sym : Symmetric R → Symmetric (option_Forall2 R).
Proof. destruct 2; by constructor. Qed.
(* stdpp/option.v *)
Instance option_Forall2_trans : Transitive R → Transitive (option_Forall2 R).
Proof. destruct 2; inv 1; constructor; etrans; eauto. Qed.
(* stdpp/option.v *)
Instance option_Forall2_equiv : Equivalence R → Equivalence (option_Forall2 R).
Proof. destruct 1; split; apply _. Qed.
(* stdpp/option.v *)
Lemma option_eq_Forall2 (mx my : option A) :
    mx = my ↔ option_Forall2 eq mx my.
Proof.
    split.
    - intros ->. destruct my; constructor; done.
    - intros [|]; naive_solver.
  Qed.
(* stdpp/option.v *)
Lemma option_Forall2_flip {A B} (R : A → B → Prop) (mx : option A) my :
  option_Forall2 (flip R) my mx ↔ option_Forall2 R mx my.
Proof. split; destruct 1; constructor; auto. Qed.
(* stdpp/option.v *)
(* Setoids *)
Instance option_equiv `{Equiv A} : Equiv (option A)
:= option_Forall2 (≡).
(* stdpp/option.v *)
Lemma option_equiv_Forall2 mx my : mx ≡ my ↔ option_Forall2 (≡) mx my.
Proof. done. Qed.
(* stdpp/option.v *)
Instance option_equivalence :
    Equivalence (≡@{A}) → Equivalence (≡@{option A}).
Proof. apply _. Qed.
(* stdpp/option.v *)
Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed.
(* stdpp/option.v *)
Instance Some_proper : Proper ((≡) ==> (≡@{option A})) Some.
Proof. by constructor. Qed.
(* stdpp/option.v *)
Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some.
Proof. by inv 1. Qed.
(* stdpp/option.v *)
Lemma None_equiv_eq mx : mx ≡ None ↔ mx = None.
Proof. split; [by inv 1|intros ->; constructor]. Qed.
(* stdpp/option.v *)
Lemma Some_equiv_eq mx y : mx ≡ Some y ↔ ∃ y', mx = Some y' ∧ y' ≡ y.
Proof. split; [inv 1; naive_solver|naive_solver (by constructor)]. Qed.
(* stdpp/option.v *)
Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
Proof. by inv 1. Qed.
(* stdpp/option.v *)
Instance from_option_proper {B} (R : relation B) :
    Proper (((≡@{A}) ==> R) ==> R ==> (≡) ==> R) from_option.
Proof. destruct 3; simpl; auto. Qed.
(* stdpp/option.v *)
(* Equality on [option] is decidable. *)
Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None)
:=
  match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end.
(* stdpp/option.v *)
Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx)
:=
  match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end.
(* stdpp/option.v *)
Instance option_eq_dec `{dec : EqDecision A} : EqDecision (option A).
Proof.
 refine (λ mx my,
  match mx, my with
  | Some x, Some y => cast_if (decide (x = y))
  | None, None => left _ | _, _ => right _
  end); clear dec; abstract congruence.
Defined.
(* stdpp/option.v *)
(* * Monadic operations *)
Instance option_ret: MRet option
:= @Some.
(* stdpp/option.v *)
Instance option_bind: MBind option
:= λ A B f mx,
  match mx with Some x => f x | None => None end.
(* stdpp/option.v *)
Instance option_join: MJoin option
:= λ A mmx,
  match mmx with Some mx => mx | None => None end.
(* stdpp/option.v *)
Instance option_fmap: FMap option
:= @option_map.
(* stdpp/option.v *)
Instance option_mfail: MFail option
:= λ _ _, None.
(* stdpp/option.v *)
Lemma option_fmap_inj {A B} (R1 : A → A → Prop) (R2 : B → B → Prop) (f : A → B) :
  Inj R1 R2 f → Inj (option_Forall2 R1) (option_Forall2 R2) (fmap f).
Proof. intros ? [?|] [?|]; inv 1; constructor; auto. Qed.
(* stdpp/option.v *)
Instance option_fmap_eq_inj {A B} (f : A → B) :
  Inj (=) (=) f → Inj (=@{option A}) (=@{option B}) (fmap f).
Proof.
  intros ?%option_fmap_inj ?? ?%option_eq_Forall2%(inj _).
  by apply option_eq_Forall2.
Qed.
(* stdpp/option.v *)
Instance option_fmap_equiv_inj `{Equiv A, Equiv B} (f : A → B) :
  Inj (≡) (≡) f → Inj (≡@{option A}) (≡@{option B}) (fmap f).
Proof. apply option_fmap_inj. Qed.
(* stdpp/option.v *)
Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <$> mx) ↔ is_Some mx.
Proof. unfold is_Some; destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma fmap_Some {A B} (f : A → B) mx y :
  f <$> mx = Some y ↔ ∃ x, mx = Some x ∧ y = f x.
Proof. destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma fmap_Some_1 {A B} (f : A → B) mx y :
  f <$> mx = Some y → ∃ x, mx = Some x ∧ y = f x.
Proof. apply fmap_Some. Qed.
(* stdpp/option.v *)
Lemma fmap_Some_2 {A B} (f : A → B) mx x : mx = Some x → f <$> mx = Some (f x).
Proof. intros. apply fmap_Some; eauto. Qed.
(* stdpp/option.v *)
Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y :
  f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
Proof.
  destruct mx; simpl; split.
  - intros ?%(inj Some). eauto.
  - intros (? & ->%(inj Some) & ?). constructor. done.
  - intros [=]%symmetry%None_equiv_eq.
  - intros (? & [=] & ?).
Qed.
(* stdpp/option.v *)
Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y :
  f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x.
Proof. by rewrite fmap_Some_equiv. Qed.
(* stdpp/option.v *)
Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None.
Proof. by destruct mx. Qed.
(* stdpp/option.v *)
Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
Proof. by destruct mx. Qed.
(* stdpp/option.v *)
Lemma option_fmap_compose {A B} (f : A → B) {C} (g : B → C) (mx : option A) :
  g ∘ f <$> mx = g <$> (f <$> mx).
Proof. by destruct mx. Qed.
(* stdpp/option.v *)
Lemma option_fmap_ext {A B} (f g : A → B) (mx : option A) :
  (∀ x, f x = g x) → f <$> mx = g <$> mx.
Proof. intros; destruct mx; f_equal/=; auto. Qed.
(* stdpp/option.v *)
Lemma option_fmap_equiv_ext {A} `{Equiv B} (f g : A → B) (mx : option A) :
  (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
Proof. destruct mx; constructor; auto. Qed.
(* stdpp/option.v *)
Lemma from_option_fmap {A B C} (f : A → B) (g : B → C) z (mx : option A) :
  from_option g z (f <$> mx) = from_option (g ∘ f) z mx.
Proof. by destruct mx. Qed.
(* stdpp/option.v *)
Lemma option_Forall_fmap {A B} (P : B → Prop) (f : A → B) (mx : option A) :
  option_Forall P (f <$> mx) ↔ option_Forall (P ∘ f) mx.
Proof. by rewrite !option_Forall_from_option, from_option_fmap. Qed.
(* stdpp/option.v *)
Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :
  (f <$> mx) ≫= g = mx ≫= g ∘ f.
Proof. by destruct mx. Qed.
(* stdpp/option.v *)
Lemma option_bind_assoc {A B C} (f : A → option B)
  (g : B → option C) (mx : option A) : (mx ≫= f) ≫= g = mx ≫= (mbind g ∘ f).
Proof. by destruct mx; simpl. Qed.
(* stdpp/option.v *)
Lemma option_bind_ext {A B} (f g : A → option B) mx my :
  (∀ x, f x = g x) → mx = my → mx ≫= f = my ≫= g.
Proof. destruct mx, my; naive_solver. Qed.
(* stdpp/option.v *)
Lemma option_bind_ext_fun {A B} (f g : A → option B) mx :
  (∀ x, f x = g x) → mx ≫= f = mx ≫= g.
Proof. intros. by apply option_bind_ext. Qed.
(* stdpp/option.v *)
Lemma bind_Some {A B} (f : A → option B) (mx : option A) y :
  mx ≫= f = Some y ↔ ∃ x, mx = Some x ∧ f x = Some y.
Proof. destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma bind_Some_equiv {A} `{Equiv B} (f : A → option B) (mx : option A) y :
  mx ≫= f ≡ Some y ↔ ∃ x, mx = Some x ∧ f x ≡ Some y.
Proof. destruct mx; split; first [by inv 1|naive_solver]. Qed.
(* stdpp/option.v *)
Lemma bind_None {A B} (f : A → option B) (mx : option A) :
  mx ≫= f = None ↔ mx = None ∨ ∃ x, mx = Some x ∧ f x = None.
Proof. destruct mx; naive_solver. Qed.
(* stdpp/option.v *)
Lemma bind_with_Some {A} (mx : option A) : mx ≫= Some = mx.
Proof. by destruct mx. Qed.
(* stdpp/option.v *)
Instance option_fmap_proper `{Equiv A, Equiv B} :
  Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) fmap.
Proof. destruct 2; constructor; auto. Qed.
(* stdpp/option.v *)
Instance option_bind_proper `{Equiv A, Equiv B} :
  Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) mbind.
Proof. destruct 2; simpl; try constructor; auto. Qed.
(* stdpp/option.v *)
Instance option_join_proper `{Equiv A} :
  Proper ((≡) ==> (≡@{option (option A)})) mjoin.
Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
(* stdpp/option.v *)
(* We can do this in a fancy way using dependent types, but rewrite does
not particularly like type level reductions. *)
Class Maybe {A B : Type} (c : A → B)
:=
  maybe : B → option A.
(* stdpp/option.v *)
Class Maybe2 {A1 A2 B : Type} (c : A1 → A2 → B)
:=
  maybe2 : B → option (A1 * A2).
(* stdpp/option.v *)
Class Maybe3 {A1 A2 A3 B : Type} (c : A1 → A2 → A3 → B)
:=
  maybe3 : B → option (A1 * A2 * A3).
(* stdpp/option.v *)
Class Maybe4 {A1 A2 A3 A4 B : Type} (c : A1 → A2 → A3 → A4 → B)
:=
  maybe4 : B → option (A1 * A2 * A3 * A4).
(* stdpp/option.v *)
Instance maybe_comp `{Maybe B C c1, Maybe A B c2} : Maybe (c1 ∘ c2)
:= λ x,
  maybe c1 x ≫= maybe c2.
(* stdpp/option.v *)
Instance maybe_inl {A B} : Maybe (@inl A B)
:= λ xy,
  match xy with inl x => Some x | _ => None end.
(* stdpp/option.v *)
Instance maybe_inr {A B} : Maybe (@inr A B)
:= λ xy,
  match xy with inr y => Some y | _ => None end.
(* stdpp/option.v *)
Instance maybe_Some {A} : Maybe (@Some A)
:= id.
(* stdpp/option.v *)
(* * Union, intersection and difference *)
Instance option_union_with {A} : UnionWith A (option A)
:= λ f mx my,
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
  | None, Some y => Some y
  | None, None => None
  end.
(* stdpp/option.v *)
Instance option_intersection_with {A} : IntersectionWith A (option A)
:=
  λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
(* stdpp/option.v *)
Instance option_difference_with {A} : DifferenceWith A (option A)
:= λ f mx my,
  match mx, my with
  | Some x, Some y => f x y
  | Some x, None => Some x
  | None, _ => None
  end.
(* stdpp/option.v *)
Instance option_union {A} : Union (option A)
:= union_with (λ x _, Some x).
(* stdpp/option.v *)
Lemma union_Some {A} (mx my : option A) z :
  mx ∪ my = Some z ↔ mx = Some z ∨ (mx = None ∧ my = Some z).
Proof. destruct mx, my; naive_solver. Qed.
(* stdpp/option.v *)
Lemma union_Some_l {A} x (my : option A) :
  Some x ∪ my = Some x.
Proof. destruct my; done. Qed.
(* stdpp/option.v *)
Lemma union_Some_r {A} (mx : option A) y :
  mx ∪ Some y = Some (default y mx).
Proof. destruct mx; done. Qed.
(* stdpp/option.v *)
Lemma union_None {A} (mx my : option A) :
  mx ∪ my = None ↔ mx = None ∧ my = None.
Proof. destruct mx, my; naive_solver. Qed.
(* stdpp/option.v *)
Lemma union_is_Some {A} (mx my : option A) :
  is_Some (mx ∪ my) ↔ is_Some mx ∨ is_Some my.
Proof. destruct mx, my; naive_solver. Qed.
(* stdpp/option.v *)
Instance option_union_left_id {A} : LeftId (=@{option A}) None union.
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance option_union_right_id {A} : RightId (=@{option A}) None union.
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance option_intersection {A} : Intersection (option A)
:=
  intersection_with (λ x _, Some x).
(* stdpp/option.v *)
Lemma intersection_Some {A} (mx my : option A) x :
  mx ∩ my = Some x ↔ mx = Some x ∧ is_Some my.
Proof. destruct mx, my; unfold is_Some; naive_solver. Qed.
(* stdpp/option.v *)
Lemma intersection_is_Some {A} (mx my : option A) :
  is_Some (mx ∩ my) ↔ is_Some mx ∧ is_Some my.
Proof. destruct mx, my; unfold is_Some; naive_solver. Qed.
(* stdpp/option.v *)
Lemma intersection_Some_r {A} (mx : option A) (y : A) :
  mx ∩ Some y = mx.
Proof. by destruct mx. Qed.
(* stdpp/option.v *)
Lemma intersection_None {A} (mx my : option A) :
  mx ∩ my = None ↔ mx = None ∨ my = None.
Proof. destruct mx, my; naive_solver. Qed.
(* stdpp/option.v *)
Lemma intersection_None_l {A} (my : option A) :
  None ∩ my = None.
Proof. destruct my; done. Qed.
(* stdpp/option.v *)
Lemma intersection_None_r {A} (mx : option A) :
  mx ∩ None = None.
Proof. destruct mx; done. Qed.
(* stdpp/option.v *)
Instance option_intersection_right_absorb {A} :
  RightAbsorb (=@{option A}) None intersection.
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance option_intersection_left_absorb {A} :
  LeftAbsorb (=@{option A}) None intersection.
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance union_with_left_id : LeftId (=) None (union_with f).
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance union_with_right_id : RightId (=) None (union_with f).
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance union_with_comm :
    Comm (=) f → Comm (=@{option A}) (union_with f).
Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
(* stdpp/option.v *)
(* These are duplicates of the above [LeftId]/[RightId] instances, but easier to
  find with [SearchAbout]. *)
Lemma union_with_None_l my : union_with f None my = my.
Proof. destruct my; done. Qed.
(* stdpp/option.v *)
Lemma union_with_None_r mx : union_with f mx None = mx.
Proof. destruct mx; done. Qed.
(* stdpp/option.v *)
Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance intersection_with_comm :
    Comm (=) f → Comm (=@{option A}) (intersection_with f).
Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
(* stdpp/option.v *)
(* These are duplicates of the above [LeftAbsorb]/[RightAbsorb] instances, but
  easier to find with [SearchAbout]. *)
Lemma intersection_with_None_l my : intersection_with f None my = None.
Proof. destruct my; done. Qed.
(* stdpp/option.v *)
Lemma intersection_with_None_r mx : intersection_with f mx None = None.
Proof. destruct mx; done. Qed.
(* stdpp/option.v *)
Instance difference_with_comm :
    Comm (=) f → Comm (=@{option A}) (intersection_with f).
Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
(* stdpp/option.v *)
Instance difference_with_right_id : RightId (=) None (difference_with f).
Proof. by intros [?|]. Qed.
(* stdpp/option.v *)
Instance union_with_proper `{Equiv A} :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) union_with.
Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
(* stdpp/option.v *)
Instance intersection_with_proper `{Equiv A} :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) intersection_with.
Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
(* stdpp/option.v *)
Instance difference_with_proper `{Equiv A} :
    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) difference_with.
Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
(* stdpp/option.v *)
Instance union_proper `{Equiv A} :
    Proper ((≡@{option A}) ==> (≡) ==> (≡)) union.
Proof. apply union_with_proper. by constructor. Qed.
(* stdpp/option.v *)
(* This lemma includes a bind, to avoid equalities of proofs. We cannot have
[guard P = Some p ↔ P] unless [P] is proof irrelant. The best (but less usable)
self-contained alternative would be [guard P = Some p ↔ decide P = left p]. *)
Lemma option_guard_True {A} P `{Decision P} (mx : option A) :
  P → (guard P;; mx) = mx.
Proof. intros. by case_guard. Qed.
(* stdpp/option.v *)
Lemma option_guard_True_pi P `{Decision P, ProofIrrel P} (HP : P) :
  guard P = Some HP.
Proof. case_guard; [|done]. f_equal; apply proof_irrel. Qed.
(* stdpp/option.v *)
Lemma option_guard_False P `{Decision P} :
  ¬P → guard P = None.
Proof. intros. by case_guard. Qed.
(* stdpp/option.v *)
Lemma option_guard_iff {A} P Q `{Decision P, Decision Q} (mx : option A) :
  (P ↔ Q) → (guard P;; mx) = (guard Q;; mx).
Proof. intros [??]. repeat case_guard; intuition. Qed.
(* stdpp/option.v *)
Lemma option_guard_decide {A} P `{Decision P} (mx : option A) :
  (guard P;; mx) = if decide P then mx else None.
Proof. by case_guard. Qed.
(* stdpp/option.v *)
Lemma option_guard_bool_decide {A} P `{Decision P} (mx : option A) :
  (guard P;; mx) = if bool_decide P then mx else None.
Proof. by rewrite option_guard_decide, decide_bool_decide. Qed.
(* stdpp/orders.v *)
Notation "X ⊈ Y"
:= (¬X ⊆ Y).
(* stdpp/orders.v *)
Lemma reflexive_eq `{!Reflexive R} X Y : X = Y → X ⊆ Y.
Proof. by intros <-. Qed.
(* stdpp/orders.v *)
Lemma anti_symm_iff `{!PartialOrder R} X Y : X = Y ↔ R X Y ∧ R Y X.
Proof. split; [by intros ->|]. by intros [??]; apply (anti_symm R). Qed.
(* stdpp/orders.v *)
Lemma strict_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
Proof. done. Qed.
(* stdpp/orders.v *)
Lemma strict_include X Y : X ⊂ Y → X ⊆ Y.
Proof. by intros [? _]. Qed.
(* stdpp/orders.v *)
Lemma strict_ne X Y : X ⊂ Y → X ≠ Y.
Proof. by intros [??] <-. Qed.
(* stdpp/orders.v *)
Lemma strict_ne_sym X Y : X ⊂ Y → Y ≠ X.
Proof. by intros [??] <-. Qed.
(* stdpp/orders.v *)
Lemma strict_trans_l `{!Transitive R} X Y Z : X ⊂ Y → Y ⊆ Z → X ⊂ Z.
Proof.
    intros [? HXY] ?. split; [by trans Y|].
    contradict HXY. by trans Z.
  Qed.
(* stdpp/orders.v *)
Lemma strict_trans_r `{!Transitive R} X Y Z : X ⊆ Y → Y ⊂ Z → X ⊂ Z.
Proof.
    intros ? [? HYZ]. split; [by trans Y|].
    contradict HYZ. by trans X.
  Qed.
(* stdpp/orders.v *)
Instance : Irreflexive (strict R).
Proof. firstorder. Qed.
(* stdpp/orders.v *)
Instance : Transitive R → StrictOrder (strict R).
Proof.
    split; try apply _.
    eauto using strict_trans_r, strict_include.
  Qed.