From af4cedfaa17dc2aa13bcbfae690a5b7237d80150 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Aug 2019 14:29:50 +0200
Subject: [PATCH] more instances for the empty type
---
theories/countable.v | 5 +++++
theories/decidable.v | 2 ++
theories/finite.v | 6 ++++++
3 files changed, 13 insertions(+)
diff --git a/theories/countable.v b/theories/countable.v
index 5f41b827..0d32ba0d 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -102,6 +102,11 @@ Section inj_countable'.
Next Obligation. intros x. by f_equal/=. Qed.
End inj_countable'.
+(** ** Empty *)
+Program Instance Empty_set_countable : Countable Empty_set :=
+ {| encode u := 1; decode p := None |}.
+Next Obligation. by intros []. Qed.
+
(** ** Unit *)
Program Instance unit_countable : Countable unit :=
{| encode u := 1; decode p := Some () |}.
diff --git a/theories/decidable.v b/theories/decidable.v
index c5db311f..2345ab9f 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -184,6 +184,8 @@ Instance bool_eq_dec : EqDecision bool.
Proof. solve_decision. Defined.
Instance unit_eq_dec : EqDecision unit.
Proof. solve_decision. Defined.
+Instance Empty_set_eq_dec : EqDecision Empty_set.
+Proof. solve_decision. Defined.
Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
Proof. solve_decision. Defined.
Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
diff --git a/theories/finite.v b/theories/finite.v
index 4d8aba1f..15414236 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -246,6 +246,12 @@ Qed.
Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
Proof. unfold card. simpl. by rewrite fmap_length. Qed.
+Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
+Next Obligation. by apply NoDup_nil. Qed.
+Next Obligation. intros []. Qed.
+Lemma Empty_set_card : card Empty_set = 0.
+Proof. done. Qed.
+
Program Instance unit_finite : Finite () := {| enum := [tt] |}.
Next Obligation. apply NoDup_singleton. Qed.
Next Obligation. intros []. by apply elem_of_list_singleton. Qed.
--
GitLab