diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/choice.v | 6 | ||||
| -rw-r--r-- | mathcomp/ssreflect/eqtype.v | 3 | ||||
| -rw-r--r-- | mathcomp/ssreflect/fintype.v | 9 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrfun.v | 13 |
4 files changed, 29 insertions, 2 deletions
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. |