From 3a262d020c0181ca5f390464ec01b7a478c88f86 Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Tue, 31 Oct 2017 11:40:58 +0100
Subject: [PATCH] Proofs of infinity and Fresh instances.

We prove that various types are infinite, notably:
- nat, N, positive and Z;
- string (using pretty-printing of nat);
- option, with an infinite element type;
- list, with an inhabited element type.

Furthermore, we instantiate Fresh for strings.
---
 _CoqProject         |  1 +
 theories/infinite.v | 24 ++++++++++++++++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 theories/infinite.v

diff --git a/_CoqProject b/_CoqProject
index 9c07436c..2fdb39c7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -39,4 +39,5 @@ theories/list.v
 theories/functions.v
 theories/hlist.v
 theories/sorting.v
+theories/infinite.v
 
diff --git a/theories/infinite.v b/theories/infinite.v
new file mode 100644
index 00000000..79739fbc
--- /dev/null
+++ b/theories/infinite.v
@@ -0,0 +1,24 @@
+(* Copyright (c) 2012-2017, Coq-std++ developers. *)
+(* This file is distributed under the terms of the BSD license. *)
+From stdpp Require Import pretty fin_collections.
+
+Instance string_infinite: Infinite string := {| inject := λ x, "~" +:+ pretty x |}.
+Instance nat_infinite: Infinite nat := {| inject := id |}.
+Instance N_infinite: Infinite N := {| inject_injective := Nat2N.inj |}.
+Instance pos_infinite: Infinite positive := {| inject_injective := SuccNat2Pos.inj |}.
+Instance Z_infinite: Infinite Z := {| inject_injective := Nat2Z.inj |}.
+Instance option_infinite `{Infinite A}: Infinite (option A) := {| inject := Some ∘ inject |}.
+Program Instance list_infinite `{Inhabited A}: Infinite (list A) :=
+  {| inject := λ i, replicate i inhabitant |}.
+Next Obligation.
+Proof.
+  intros * i j eqrep%(f_equal length).
+  rewrite !replicate_length in eqrep; done.
+Qed.
+
+(** Derive fresh instances. *)
+Section StringFresh.
+  Context `{FinCollection string C, ∀ (x: string) (s: C), Decision (x ∈ s)}.
+  Global Instance string_fresh: Fresh string C := fresh_generic.
+  Global Instance string_fresh_spec: FreshSpec string C := _.
+End StringFresh.
\ No newline at end of file
-- 
GitLab