Merge PR coq#19949: EqDec instance for option

Reviewed-by: andres-erbsen Ack-by: SkySkimmer Ack-by: ppedrot Co-authored-by: andres-erbsen <[email protected]>
SkySkimmer · Dec 27, 2024 · 03dd829 · 03dd829
2 parents 78b2bf4 + d68e31c
commit 03dd829
Show file tree

Hide file tree

Showing 3 changed files with 28 additions and 0 deletions.
diff --git a/doc/changelog/11-standard-library/19949-option-eqdec.rst b/doc/changelog/11-standard-library/19949-option-eqdec.rst
@@ -0,0 +1,3 @@
+- **Added:** :g:`EqDec` instance for :g:`option`
+  (`#19949 <https://github.com/coq/coq/pull/19949>`_,
+  by Daniil Iaitskov).
diff --git a/stdlib/test-suite/success/EquivDec.v b/stdlib/test-suite/success/EquivDec.v
@@ -0,0 +1,6 @@
+From Stdlib Require Import EquivDec.
+
+Example test_None_eqb_None: None ==b None = true. Proof. reflexivity. Qed.
+Example test_None_eqb_Some: None ==b Some true = false. Proof. reflexivity. Qed.
+Example test_Some_eqb_Some: Some 1 ==b Some 1 = true. Proof. reflexivity. Qed.
+Example test_Some_neqb_Some: Some 0 ==b Some 1 = false. Proof. reflexivity. Qed.
diff --git a/stdlib/theories/Classes/EquivDec.v b/stdlib/theories/Classes/EquivDec.v
@@ -157,3 +157,22 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : EqDec (list A) eq :=
 
   Solve Obligations with unfold equiv, complement in * ;
     program_simpl ; intuition (discriminate || eauto).
+
+#[export]
+Program Instance option_eqdec `(eqa : EqDec A eq) : EqDec (option A) eq :=
+  { equiv_dec (x y : option A) :=
+    match x, y with
+      | None, None => in_left
+      | Some s, Some s' =>
+        if s == s' then in_left else in_right
+      | _, _ => in_right
+    end
+  }.
+
+  Next Obligation.
+    match goal with y : option _ |- _ => destruct y end ;
+    unfold not in *; eauto.
+  Defined.
+
+  Solve Obligations with unfold equiv, complement in * ;
+    program_simpl; intuition (discriminate || eauto).