From d68e31c7c63c669580eadecad9efc2eea751763f Mon Sep 17 00:00:00 2001
From: Daniil Iaitskov <dyaitskov@gmail.com>
Date: Thu, 26 Dec 2024 13:07:06 -0900
Subject: [PATCH] EqDecOption EqDec instance for option

---
 .../19949-option-eqdec.rst                    |  3 +++
 stdlib/test-suite/success/EquivDec.v          |  6 ++++++
 stdlib/theories/Classes/EquivDec.v            | 19 +++++++++++++++++++
 3 files changed, 28 insertions(+)
 create mode 100644 doc/changelog/11-standard-library/19949-option-eqdec.rst
 create mode 100644 stdlib/test-suite/success/EquivDec.v

diff --git a/doc/changelog/11-standard-library/19949-option-eqdec.rst b/doc/changelog/11-standard-library/19949-option-eqdec.rst
new file mode 100644
index 000000000000..8ac2f2c24327
--- /dev/null
+++ 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
new file mode 100644
index 000000000000..1a7ce5ad2594
--- /dev/null
+++ 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
index 9bffbba8ab73..bd8ae905aa08 100644
--- 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).