Merge branch 'robbert/encode_Z' into 'master'

Add `encode_Z` function to encode element of countable type as `Z`.

See merge request iris/stdpp!145

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`):

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).