From 94b04a140a72fcd7639f22dce15254f974d107db Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Apr 2020 11:30:55 +0200
Subject: [PATCH] Add `encode_Z` function to encode element of countable type
 as `Z`.

---
 CHANGELOG.md         |  2 ++
 theories/countable.v | 18 ++++++++++++++----
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8c4667d4..0ee29fd5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -60,6 +60,8 @@ Noteworthy additions and changes:
 - Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
   `singletonM` and to avoid overlap with `sets.singleton_proper`.
 - Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
+- Add `encode_Z`/`decode_Z` functions to encode elements of a countable type
+  as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/countable.v b/theories/countable.v
index 9b5373c4..3c87aab9 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -12,15 +12,16 @@ Hint Mode Countable ! - : typeclass_instances.
 Arguments encode : simpl never.
 Arguments decode : simpl never.
 
-Definition encode_nat `{Countable A} (x : A) : nat :=
-  pred (Pos.to_nat (encode x)).
-Definition decode_nat `{Countable A} (i : nat) : option A :=
-  decode (Pos.of_nat (S i)).
 Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
 Proof.
   intros x y Hxy; apply (inj Some).
   by rewrite <-(decode_encode x), Hxy, decode_encode.
 Qed.
+
+Definition encode_nat `{Countable A} (x : A) : nat :=
+  pred (Pos.to_nat (encode x)).
+Definition decode_nat `{Countable A} (i : nat) : option A :=
+  decode (Pos.of_nat (S i)).
 Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
 Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
 Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
@@ -30,6 +31,15 @@ Proof.
   by rewrite Pos2Nat.id, decode_encode.
 Qed.
 
+Definition encode_Z `{Countable A} (x : A) : Z :=
+  Zpos (encode x).
+Definition decode_Z `{Countable A} (i : Z) : option A :=
+  match i with Zpos i => decode i | _ => None end.
+Instance encode_Z_inj `{Countable A} : Inj (=) (=) (encode_Z (A:=A)).
+Proof. unfold encode_Z; intros x y Hxy; apply (inj encode); lia. Qed.
+Lemma decode_encode_Z `{Countable A} (x : A) : decode_Z (encode_Z x) = Some x.
+Proof. apply decode_encode. Qed.
+
 (** * Choice principles *)
 Section choice.
   Context `{Countable A} (P : A → Prop).
-- 
GitLab