From c6685a3e1b5accc8fec42952660c7b2b40aff141 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 14:49:15 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20that=20Countable=20A=20gives=20Countabl?=
 =?UTF-8?q?e=20B=20for=20an=20injection=20B=20=E2=86=92=20A.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 prelude/countable.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/prelude/countable.v b/prelude/countable.v
index 6267748cf..a2aad6cc5 100644
--- a/prelude/countable.v
+++ b/prelude/countable.v
@@ -78,6 +78,16 @@ Proof.
 Qed.
 
 (** * Instances *)
+(** ** Injection *)
+Section injective_countable.
+  Context `{Countable A, ∀ x y : B, Decision (x = y)}.
+  Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x).
+
+  Program Instance injective_countable : Countable B :=
+    {| encode y := encode (f y); decode p := x ← decode p; g x |}.
+  Next Obligation. intros y; simpl; rewrite decode_encode; eauto. Qed.
+End injective_countable.
+
 (** ** Option *)
 Program Instance option_countable `{Countable A} : Countable (option A) := {|
   encode o := match o with None => 1 | Some x => Pos.succ (encode x) end;
-- 
GitLab