Instances for empty type. (#393)

* Add notation and instances for empty type.

* Update change log.

* Mention void in fintype header.

* Remove unnecessary explicit argument.

* Documentation header for void.

5 files changed, 33 insertions, 2 deletions

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index a1b0b78..6bb0e3f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
+- Added a `void` notation for the `Empty_set` type of the standard library, the
+  canonical injection `of_void` and its cancellation lemma `of_voidK`, and
+  `eq`, `choice`, `count` and `fin` instances.
+
 - Added fixpoint and cofixpoint constructions to `finset`: `fixset`,
   `cofixset` and `fix_order`, with a few theorems about them
 
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index b42580a..49d50fe 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -480,6 +480,9 @@ Canonical bitseq_choiceType := Eval hnf in [choiceType of bitseq].
 Definition unit_choiceMixin := CanChoiceMixin bool_of_unitK.
 Canonical unit_choiceType := Eval hnf in ChoiceType unit unit_choiceMixin.
 
+Definition void_choiceMixin := PcanChoiceMixin (of_voidK unit).
+Canonical void_choiceType := Eval hnf in ChoiceType void void_choiceMixin.
+
 Definition option_choiceMixin T := CanChoiceMixin (@seq_of_optK T).
 Canonical option_choiceType T :=
   Eval hnf in ChoiceType (option T) (option_choiceMixin T).
@@ -674,6 +677,9 @@ Canonical bitseq_countType :=  Eval hnf in [countType of bitseq].
 Definition unit_countMixin := CanCountMixin bool_of_unitK.
 Canonical unit_countType := Eval hnf in CountType unit unit_countMixin.
 
+Definition void_countMixin := PcanCountMixin (of_voidK unit).
+Canonical void_countType := Eval hnf in CountType void void_countMixin.
+
 Definition option_countMixin T := CanCountMixin (@seq_of_optK T).
 Canonical option_countType T :=
   Eval hnf in CountType (option T) (option_countMixin T).
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 7e1cdc8..e9da3ec 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -765,6 +765,9 @@ Arguments val_eqP {T P sT x y}.
 Notation "[ 'eqMixin' 'of' T 'by' <: ]" := (SubEqMixin _ : Equality.class_of T)
   (at level 0, format "[ 'eqMixin'  'of'  T  'by'  <: ]") : form_scope.
 
+Definition void_eqMixin := PcanEqMixin (of_voidK unit).
+Canonical void_eqType := EqType void void_eqMixin.
+
 Section SigEqType.
 
 Variables (T : eqType) (P : pred T).
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index fdaf98f..32d2898 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -36,8 +36,8 @@ From mathcomp Require Import path.
 (* [finMixin of T by <:] == a finType structure for T, when T has a subType   *)
 (*                   structure over an existing finType.                      *)
 (*   We define or propagate the finType structure appropriately for all basic *)
-(* types : unit, bool, option, prod, sum, sig and sigT. We also define a      *)
-(* generic type constructor for finite subtypes based on an explicit          *)
+(* types : unit, bool, void, option, prod, sum, sig and sigT. We also define  *)
+(* a generic type constructor for finite subtypes based on an explicit        *)
 (* enumeration:                                                               *)
 (*          seq_sub s == the subType of all x \in s, where s : seq T for some *)
 (*                       eqType T; seq_sub s has a canonical finType instance *)
@@ -1400,6 +1400,11 @@ Definition bool_finMixin := Eval hnf in FinMixin bool_enumP.
 Canonical bool_finType := Eval hnf in FinType bool bool_finMixin.
 Lemma card_bool : #|{: bool}| = 2. Proof. by rewrite cardT enumT unlock. Qed.
 
+Lemma void_enumP : Finite.axiom (Nil void). Proof. by case. Qed.
+Definition void_finMixin := Eval hnf in FinMixin void_enumP.
+Canonical void_finType := Eval hnf in FinType void void_finMixin.
+Lemma card_void : #|{: void}| = 0. Proof. by rewrite cardT enumT unlock. Qed.
+
 Local Notation enumF T := (Finite.enum T).
 
 Section OptionFinType.
diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index 1c1b557..de917a9 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -2,5 +2,18 @@ From mathcomp Require Import ssreflect.
 From Coq Require Export ssrfun.
 From mathcomp Require Export ssrnotations.
 
+(******************************************************************************)
+(* Local additions:                                                           *)
+(*        void == a notation for the Empty_set type of the standard library.  *)
+(*   of_void T == the canonical injection void -> T.                          *)
+(******************************************************************************)
+
 Lemma Some_inj {T : nonPropType} : injective (@Some T).
 Proof. by move=> x y []. Qed.
+
+Notation void := Empty_set.
+
+Definition of_void T (x : void) : T := match x with end.
+
+Lemma of_voidK T : pcancel (of_void T) [fun _ => None].
+Proof. by case. Qed.