From fba969b6e84f231db5b4f637f178e5d19ae08ac5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Feb 2019 23:10:27 +0100
Subject: [PATCH] Infinite instances for prod/sum.

---
 theories/infinite.v | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/theories/infinite.v b/theories/infinite.v
index 32575064..ecd3d501 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -11,17 +11,27 @@ Class Infinite A := {
   inject_injective :> Inj (=) (=) inject;
 }.
 
+(** Instances *)
+Program Definition inj_infinite `{Infinite A} {B} (f : A → B) `{!Inj (=) (=) f} :
+  Infinite B := {| inject := f ∘ inject |}.
+
 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 positive_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 |}.
+Instance option_infinite `{Infinite A} : Infinite (option A) := inj_infinite Some.
+Instance sum_infinite_l `{Infinite A} {B} : Infinite (A + B) := inj_infinite inl.
+Instance sum_infinite_r {A} `{Infinite B} : Infinite (A + B) := inj_infinite inr.
+Instance prod_infinite_l `{Infinite A, Inhabited B} : Infinite (A * B) :=
+  inj_infinite (,inhabitant).
+Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
+  inj_infinite (inhabitant,).
+
 Program Instance list_infinite `{Inhabited A}: Infinite (list A) :=
   {| inject := λ i, replicate i inhabitant |}.
 Next Obligation.
-Proof.
   intros A * i j Heqrep%(f_equal length).
   rewrite !replicate_length in Heqrep; done.
 Qed.
-- 
GitLab