Commit 0b8de700 authored by Robbert Krebbers's avatar Robbert Krebbers

Some general option_Forall2 properties.

parent 251ab0d5
......@@ -80,9 +80,9 @@ Lemma not_eq_None_Some {A} (mx : option A) : mx ≠ None ↔ is_Some mx.
Proof. rewrite eq_None_not_Some; apply dec_stable; tauto. Qed.
(** Lifting a relation point-wise to option *)
Inductive option_Forall2 {A B} (P: A B Prop) : option A option B Prop :=
| Some_Forall2 x y : P x y option_Forall2 P (Some x) (Some y)
| None_Forall2 : option_Forall2 P None None.
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.
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
......@@ -92,22 +92,30 @@ Definition option_relation {A B} (R: A → B → Prop) (P: A → Prop) (Q: B →
| None, None => True
end.
Section Forall2.
Context {A} (R : relation A).
Global Instance option_Forall2_refl : Reflexive R Reflexive (option_Forall2 R).
Proof. intros ? [?|]; by constructor. Qed.
Global Instance option_Forall2_sym : Symmetric R Symmetric (option_Forall2 R).
Proof. destruct 2; by constructor. Qed.
Global Instance option_Forall2_trans : Transitive R Transitive (option_Forall2 R).
Proof. destruct 2; inversion_clear 1; constructor; etrans; eauto. Qed.
Global Instance option_Forall2_equiv : Equivalence R Equivalence (option_Forall2 R).
Proof. destruct 1; split; apply _. Qed.
End Forall2.
(** Setoids *)
Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 ().
Section setoids.
Context `{Equiv A} `{!Equivalence (() : relation A)}.
Global Instance option_equiv : Equiv (option A) := option_Forall2 ().
Lemma equiv_option_Forall2 mx my : mx my option_Forall2 () mx my.
Proof. split; destruct 1; constructor; auto. Qed.
Proof. done. Qed.
Global Instance option_equivalence : Equivalence (() : relation (option A)).
Proof.
split.
- by intros []; constructor.
- by destruct 1; constructor.
- destruct 1; inversion 1; constructor; etrans; eauto.
Qed.
Proof. apply _. Qed.
Global Instance Some_proper : Proper (() ==> ()) (@Some A).
Proof. by constructor. Qed.
Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
......@@ -129,6 +137,8 @@ Section setoids.
Proof. by destruct 2. Qed.
End setoids.
Typeclasses Opaque option_equiv.
(** 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.
......
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