From 57a1a2075f0936a5e09b64eb6cb1eb87179dc6e8 Mon Sep 17 00:00:00 2001
From: Alix Trieu <alix.trieu@cs.au.dk>
Date: Fri, 19 Mar 2021 19:10:48 +0100
Subject: [PATCH] surjective_finite

---
 theories/finite.v | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/theories/finite.v b/theories/finite.v
index 0afae8a1..4297363d 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -220,15 +220,25 @@ Section enc_finite.
   Proof. unfold card. simpl. by rewrite fmap_length, seq_length. Qed.
 End enc_finite.
 
+Section surjective_finite.
+  Context `{Finite A, EqDecision B} (f : A → B).
+  Context `{!Surj (=) f}.
+
+  Program Instance surjective_finite: Finite B := {| enum := remove_dups (f <$> enum A) |}.
+  Next Obligation. apply NoDup_remove_dups. Qed.
+  Next Obligation.
+    intros y. rewrite elem_of_remove_dups, elem_of_list_fmap.
+    destruct (Surj0 y). eauto using elem_of_enum.
+  Qed.
+End surjective_finite.
+
 Section bijective_finite.
   Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
-  Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
-  Next Obligation. apply (NoDup_fmap_2 _), NoDup_enum. Qed.
-  Next Obligation.
-    intros y. rewrite elem_of_list_fmap. eauto using elem_of_enum.
-  Qed.
+  Program Instance bijective_finite: Finite B := _.
+  Next Obligation. eapply surjective_finite. eapply cancel_surj.
+                   Unshelve. all: eapply _. Qed.
 End bijective_finite.
 
 Program Instance option_finite `{Finite A} : Finite (option A) :=
-- 
GitLab