+ +

Library mathcomp.ssreflect.fintype

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+

+ +

+ The Finite interface describes Types with finitely many elements, + supplying a duplicate-free sequence of all the elements. It is a subclass + of Countable and thus of Choice and Equality. As with Countable, the + interface explicitly includes these somewhat redundant superclasses to + ensure that Canonical instance inference remains consistent. Finiteness + could be stated more simply by bounding the range of the pickle function + supplied by the Countable interface, but this would yield a useless + computational interpretation due to the wasteful Peano integer encodings. + Because the Countable interface is closely tied to the Finite interface + and is not much used on its own, the Countable mixin is included inside + the Finite mixin; this makes it much easier to derive Finite variants of + interfaces, in this file for subFinType, and in the finalg library. + We define the following interfaces and structures: + finType == the packed class type of the Finite interface. + FinType m == the packed class for the Finite mixin m. + Finite.axiom e <-> every x : T occurs exactly once in e : seq T. + FinMixin ax_e == the Finite mixin for T, encapsulating + ax_e : Finite.axiom e for some e : seq T. + UniqFinMixin uniq_e total_e == an alternative mixin constructor that uses + uniq_e : uniq e and total_e : e =i xpredT. + PcanFinMixin fK == the Finite mixin for T, given f : T -> fT and g with fT + a finType and fK : pcancel f g. + CanFinMixin fK == the Finite mixin for T, given f : T -> fT and g with fT + a finType and fK : cancel f g. + subFinType == the join interface type for subType and finType. + [finType of T for fT] == clone for T of the finType fT. + [finType of T] == clone for T of the finType inferred for T. + [subFinType of T] == a subFinType structure for T, when T already has both + finType and subType structures. + [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 + 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 + when T is a choiceType. + adhoc_seq_sub_choiceType s, adhoc_seq_sub_finType s == + non-canonical instances for seq_sub s, s : seq T, + which can be used when T is not a choiceType. + Bounded integers are supported by the following type and operations: + 'I_n, ordinal n == the finite subType of integers i < n, whose + enumeration is {0, ..., n.-1}. 'I_n coerces to nat, + so all the integer arithmetic functions can be used + with 'I_n. + Ordinal lt_i_n == the element of 'I_n with (nat) value i, given + lt_i_n : i < n. + nat_of_ord i == the nat value of i : 'I_n (this function is a + coercion so it is not usually displayed). + ord_enum n == the explicit increasing sequence of the i : 'I_n. + cast_ord eq_n_m i == the element j : 'I_m with the same value as i : 'I_n + given eq_n_m : n = m (indeed, i : nat and j : nat + are convertible). + widen_ord le_n_m i == a j : 'I_m with the same value as i : 'I_n, given + le_n_m : n <= m. + rev_ord i == the complement to n.-1 of i : 'I_n, such that + i + rev_ord i = n.-1. + inord k == the i : 'I_n.+1 with value k (n is inferred from the + context). + sub_ord k == the i : 'I_n.+1 with value n - k (n is inferred from + the context). + ord0 == the i : 'I_n.+1 with value 0 (n is inferred from the + context). + ord_max == the i : 'I_n.+1 with value n (n is inferred from the + context). + bump h k == k.+1 if k >= h, else k (this is a nat function). + unbump h k == k.-1 if k > h, else k (this is a nat function). + lift i j == the j' : 'I_n with value bump i j, where i : 'I_n + and j : 'I_n.-1. + unlift i j == None if i = j, else Some j', where j' : 'I_n.-1 has + value unbump i j, given i, j : 'I_n. + lshift n j == the i : 'I(m + n) with value j : 'I_m. + rshift m k == the i : 'I(m + n) with value m + k, k : 'I_n. + unsplit u == either lshift n j or rshift m k, depending on + whether if u : 'I_m + 'I_n is inl j or inr k. + split i == the u : 'I_m + 'I_n such that i = unsplit u; the + type 'I(m + n) of i determines the split. + Finally, every type T with a finType structure supports the following + operations: + enum A == a duplicate-free list of all the x \in A, where A is a + collective predicate over T. + #|A| == the cardinal of A, i.e., the number of x \in A. + enum_val i == the i'th item of enum A, where i : 'I(#|A|). + enum_rank x == the i : 'I(#|T|) such that enum_val i = x. + enum_rank_in Ax0 x == some i : 'I(#|A|) such that enum_val i = x if + x \in A, given Ax0 : x0 \in A. + A \subset B == all x \in A satisfy x \in B. + A \proper B == all x \in A satisfy x \in B but not the converse. + [disjoint A & B] == no x \in A satisfies x \in B. + image f A == the sequence of f x for all x : T such that x \in A + (where a is an applicative predicate), of length #|P|. + The codomain of F can be any type, but image f A can + only be used as a collective predicate is it is an + eqType. + codom f == a sequence spanning the codomain of f (:= image f T). + [seq F | x : T in A] := image (fun x : T => F) A. + [seq F | x : T] := [seq F | x <- {: T} ]. + [seq F | x in A], [seq F | x] == variants without casts. + iinv im_y == some x such that P x holds and f x = y, given + im_y : y \in image f P. + invF inj_f y == the x such that f x = y, for inj_j : injective f with + f : T -> T. + dinjectiveb A f == the restriction of f : T -> R to A is injective + (this is a bolean predicate, R must be an eqType). + injectiveb f == f : T -> R is injective (boolean predicate). + pred0b A == no x : T satisfies x \in A. + [forall x, P] == P (in which x can appear) is true for all values of x; + x must range over a finType. + [exists x, P] == P is true for some value of x. + [forall (x | C), P] := [forall x, C ==> P]. + [forall x in A, P] := [forall (x | x \in A), P]. + [exists (x | C), P] := [exists x, C && P]. + [exists x in A, P] := [exists (x | x \in A), P]. + and typed variants [forall x : T, P], [forall (x : T | C), P], + [exists x : T, P], [exists x : T in A, P], etc. +

> The outer brackets can be omitted when nesting finitary quantifiers, + e.g., [forall i in I, forall j in J, exists a, f i j == a]. + 'forall_pP == view for [forall x, p _ ], for pP : reflect .. (p _). + 'exists_pP == view for [exists x, p _ ], for pP : reflect .. (p _). + [pick x | P] == Some x, for an x such that P holds, or None if there + is no such x. + [pick x : T] == Some x with x : T, provided T is nonempty, else None. + [pick x in A] == Some x, with x \in A, or None if A is empty. + +

+ [pick x in A | P] == Some x, with x \in A s.t. P holds, else None. + [pick x | P & Q] := [pick x | P & Q]. + [pick x in A | P & Q] := [pick x | P & Q]. + and (un)typed variants [pick x : T | P], [pick x : T in A], [pick x], etc. + [arg min(i < i0 | P) M] == a value of i : T minimizing M : nat, subject + to the condition P (i may appear in P and M), and + provided P holds for i0. + [arg max(i > i0 | P) M] == a value of i maximizing M subject to P and + provided P holds for i0. + [arg min(i < i0 in A) M] == an i \in A minimizing M if i0 \in A. + [arg max(i > i0 in A) M] == an i \in A maximizing M if i0 \in A. + [arg min(i < i0) M] == an i : T minimizing M, given i0 : T. + [arg max(i > i0) M] == an i : T maximizing M, given i0 : T. +

+ +
+Set Implicit Arguments.
+ +
+Module Finite.
+ +
+Section RawMixin.
+ +
+Variable T : eqType.
+ +
+Definition axiom e := ∀ x : T, count_mem x e = 1.
+ +
+Lemma uniq_enumP e : uniq e → e =i T → axiom e.
+ +
+Record mixin_of := Mixin {
+  mixin_base : Countable.mixin_of T;
+  mixin_enum : seq T;
+  _ : axiom mixin_enum
+}.
+ +
+End RawMixin.
+ +
+Section Mixins.
+ +
+Variable T : countType.
+ +
+Definition EnumMixin :=
+  let: Countable.Pack _ (Countable.Class _ m) _ as cT := T
+    return ∀ e : seq cT, axiom e → mixin_of cT in
+  @Mixin (EqType _ _) m.
+ +
+Definition UniqMixin e Ue eT := @EnumMixin e (uniq_enumP Ue eT).
+ +
+Variable n : nat.
+ +
+Definition count_enum := pmap (@pickle_inv T) (iota 0 n).
+ +
+Hypothesis ubT : ∀ x : T, pickle x < n.
+ +
+Lemma count_enumP : axiom count_enum.
+ +
+Definition CountMixin := EnumMixin count_enumP.
+ +
+End Mixins.
+ +
+Section ClassDef.
+ +
+Record class_of T := Class {
+  base : Choice.class_of T;
+  mixin : mixin_of (Equality.Pack base T)
+}.
+Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)).
+ +
+Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
+Variables (T : Type) (cT : type).
+Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
+Definition clone c of phant_id class c := @Pack T c T.
+Let xT := let: Pack T _ _ := cT in T.
+Notation xclass := (class : class_of xT).
+ +
+Definition pack b0 (m0 : mixin_of (EqType T b0)) :=
+  fun bT b & phant_id (Choice.class bT) b ⇒
+  fun m & phant_id m0 m ⇒ Pack (@Class T b m) T.
+ +
+Definition eqType := @Equality.Pack cT xclass xT.
+Definition choiceType := @Choice.Pack cT xclass xT.
+Definition countType := @Countable.Pack cT (base2 xclass) xT.
+ +
+End ClassDef.
+ +
+Module Import Exports.
+Coercion mixin_base : mixin_of >-> Countable.mixin_of.
+Coercion base : class_of >-> Choice.class_of.
+Coercion mixin : class_of >-> mixin_of.
+Coercion base2 : class_of >-> Countable.class_of.
+Coercion sort : type >-> Sortclass.
+Coercion eqType : type >-> Equality.type.
+Canonical eqType.
+Coercion choiceType : type >-> Choice.type.
+Canonical choiceType.
+Coercion countType : type >-> Countable.type.
+Canonical countType.
+Notation finType := type.
+Notation FinType T m := (@pack T _ m _ _ id _ id).
+Notation FinMixin := EnumMixin.
+Notation UniqFinMixin := UniqMixin.
+Notation "[ 'finType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
+  (at level 0, format "[ 'finType' 'of' T 'for' cT ]") : form_scope.
+Notation "[ 'finType' 'of' T ]" := (@clone T _ _ id)
+  (at level 0, format "[ 'finType' 'of' T ]") : form_scope.
+End Exports.
+ +
+Module Type EnumSig.
+Parameter enum : ∀ cT : type, seq cT.
+Axiom enumDef : enum = fun cT ⇒ mixin_enum (class cT).
+End EnumSig.
+ +
+Module EnumDef : EnumSig.
+Definition enum cT := mixin_enum (class cT).
+Definition enumDef := erefl enum.
+End EnumDef.
+ +
+Notation enum := EnumDef.enum.
+ +
+End Finite.
+Export Finite.Exports.
+ +
+Canonical finEnum_unlock := Unlockable Finite.EnumDef.enumDef.
+ +
+

+ +

+ Workaround for the silly syntactic uniformity restriction on coercions; + this avoids a cross-dependency between finset.v and prime.v for the + definition of the \pi(A) notation. +

+Definition fin_pred_sort (T : finType) (pT : predType T) := pred_sort pT.
+Identity Coercion pred_sort_of_fin : fin_pred_sort >-> pred_sort.
+ +
+Definition enum_mem T (mA : mem_pred _) := filter mA (Finite.enum T).
+Notation enum A := (enum_mem (mem A)).
+Definition pick (T : finType) (P : pred T) := ohead (enum P).
+ +
+Notation "[ 'pick' x | P ]" := (pick (fun x ⇒ P%B))
+  (at level 0, x ident, format "[ 'pick' x | P ]") : form_scope.
+Notation "[ 'pick' x : T | P ]" := (pick (fun x : T ⇒ P%B))
+  (at level 0, x ident, only parsing) : form_scope.
+Definition pick_true T (x : T) := true.
+Notation "[ 'pick' x : T ]" := [pick x : T | pick_true x]
+  (at level 0, x ident, only parsing).
+Notation "[ 'pick' x ]" := [pick x : _]
+  (at level 0, x ident, only parsing) : form_scope.
+Notation "[ 'pic' 'k' x : T ]" := [pick x : T | pick_true _]
+  (at level 0, x ident, format "[ 'pic' 'k' x : T ]") : form_scope.
+Notation "[ 'pick' x | P & Q ]" := [pick x | P && Q ]
+  (at level 0, x ident,
+   format "[ '[hv ' 'pick' x | P '/ ' & Q ] ']'") : form_scope.
+Notation "[ 'pick' x : T | P & Q ]" := [pick x : T | P && Q ]
+  (at level 0, x ident, only parsing) : form_scope.
+Notation "[ 'pick' x 'in' A ]" := [pick x | x \in A]
+  (at level 0, x ident, format "[ 'pick' x 'in' A ]") : form_scope.
+Notation "[ 'pick' x : T 'in' A ]" := [pick x : T | x \in A]
+  (at level 0, x ident, only parsing) : form_scope.
+Notation "[ 'pick' x 'in' A | P ]" := [pick x | x \in A & P ]
+  (at level 0, x ident,
+   format "[ '[hv ' 'pick' x 'in' A '/ ' | P ] ']'") : form_scope.
+Notation "[ 'pick' x : T 'in' A | P ]" := [pick x : T | x \in A & P ]
+  (at level 0, x ident, only parsing) : form_scope.
+Notation "[ 'pick' x 'in' A | P & Q ]" := [pick x in A | P && Q]
+  (at level 0, x ident, format
+  "[ '[hv ' 'pick' x 'in' A '/ ' | P '/ ' & Q ] ']'") : form_scope.
+Notation "[ 'pick' x : T 'in' A | P & Q ]" := [pick x : T in A | P && Q]
+  (at level 0, x ident, only parsing) : form_scope.
+ +
+

+ +

+ We lock the definitions of card and subset to mitigate divergence of the + Coq term comparison algorithm. +

+ +
+Module Type CardDefSig.
+Parameter card : card_type. Axiom cardEdef : card = card_def.
+End CardDefSig.
+Module CardDef : CardDefSig.
+Definition card : card_type := card_def. Definition cardEdef := erefl card.
+End CardDef.
+

+ +

+ Should be Include, but for a silly restriction: can't Include at toplevel! +

+Export CardDef.
+ +
+Canonical card_unlock := Unlockable cardEdef.
+

+ +

+ A is at level 99 to allow the notation #|G : H| in groups. +

+Notation "#| A |" := (card (mem A))
+ (at level 0, A at level 99, format "#| A |") : nat_scope.
+ +
+Definition pred0b (T : finType) (P : pred T) := #|P | == 0.
+ +
+Module FiniteQuant.
+ +
+CoInductive quantified := Quantified of bool.
+ +
+Delimit Scope fin_quant_scope with Q. (* Bogus, only used to declare scope. *)
+ +
+Notation "F ^*" := (Quantified F) (at level 2).
+Notation "F ^~" := (~~ F) (at level 2).
+ +
+Section Definitions.
+ +
+Variable T : finType.
+Implicit Types (B : quantified) (x y : T).
+ +
+Definition quant0b Bp := pred0b [pred x : T | let: F^* := Bp x x in F].
+

+ +

+ The first redundant argument protects the notation from Coq's K-term + display kludge; the second protects it from simpl and /=. +

+Definition ex B x y := B.
+

+ +

+ Binding the predicate value rather than projecting it prevents spurious + unfolding of the boolean connectives by unification. +

+Definition all B x y := let: F^* := B in F^~^*.
+Definition all_in C B x y := let: F^* := B in (C ==> F)^~^*.
+Definition ex_in C B x y := let: F^* := B in (C && F)^*.
+ +
+End Definitions.
+ +
+Notation "[ x | B ]" := (quant0b (fun x ⇒ B x)) (at level 0, x ident).
+Notation "[ x : T | B ]" := (quant0b (fun x : T ⇒ B x)) (at level 0, x ident).
+ +
+Module Exports.
+ +
+Notation ", F" := F^* (at level 200, format ", '/ ' F") : fin_quant_scope.
+ +
+Notation "[ 'forall' x B ]" := [x | all B]
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' 'forall' x B ] ']'") : bool_scope.
+ +
+Notation "[ 'forall' x : T B ]" := [x : T | all B]
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'forall' ( x | C ) B ]" := [x | all_in C B]
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'forall' ( x '/ ' | C ) ']' B ] ']'") : bool_scope.
+Notation "[ 'forall' ( x : T | C ) B ]" := [x : T | all_in C B]
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'forall' x 'in' A B ]" := [x | all_in (x \in A) B]
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'forall' x '/ ' 'in' A ']' B ] ']'") : bool_scope.
+Notation "[ 'forall' x : T 'in' A B ]" := [x : T | all_in (x \in A) B]
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation ", 'forall' x B" := [x | all B]^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ ' 'forall' x B") : fin_quant_scope.
+Notation ", 'forall' x : T B" := [x : T | all B]^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'forall' ( x | C ) B" := [x | all_in C B]^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ ' '[' 'forall' ( x '/ ' | C ) ']' B") : fin_quant_scope.
+Notation ", 'forall' ( x : T | C ) B" := [x : T | all_in C B]^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'forall' x 'in' A B" := [x | all_in (x \in A) B]^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ ' '[' 'forall' x '/ ' 'in' A ']' B") : bool_scope.
+Notation ", 'forall' x : T 'in' A B" := [x : T | all_in (x \in A) B]^*
+  (at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
+ +
+Notation "[ 'exists' x B ]" := [x | ex B]^~
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' 'exists' x B ] ']'") : bool_scope.
+Notation "[ 'exists' x : T B ]" := [x : T | ex B]^~
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'exists' ( x | C ) B ]" := [x | ex_in C B]^~
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'exists' ( x '/ ' | C ) ']' B ] ']'") : bool_scope.
+Notation "[ 'exists' ( x : T | C ) B ]" := [x : T | ex_in C B]^~
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation "[ 'exists' x 'in' A B ]" := [x | ex_in (x \in A) B]^~
+  (at level 0, x at level 99, B at level 200,
+   format "[ '[hv' '[' 'exists' x '/ ' 'in' A ']' B ] ']'") : bool_scope.
+Notation "[ 'exists' x : T 'in' A B ]" := [x : T | ex_in (x \in A) B]^~
+  (at level 0, x at level 99, B at level 200, only parsing) : bool_scope.
+Notation ", 'exists' x B" := [x | ex B]^~^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ ' 'exists' x B") : fin_quant_scope.
+Notation ", 'exists' x : T B" := [x : T | ex B]^~^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'exists' ( x | C ) B" := [x | ex_in C B]^~^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ ' '[' 'exists' ( x '/ ' | C ) ']' B") : fin_quant_scope.
+Notation ", 'exists' ( x : T | C ) B" := [x : T | ex_in C B]^~^*
+  (at level 200, x at level 99, B at level 200, only parsing) : fin_quant_scope.
+Notation ", 'exists' x 'in' A B" := [x | ex_in (x \in A) B]^~^*
+  (at level 200, x at level 99, B at level 200,
+   format ", '/ ' '[' 'exists' x '/ ' 'in' A ']' B") : bool_scope.
+Notation ", 'exists' x : T 'in' A B" := [x : T | ex_in (x \in A) B]^~^*
+  (at level 200, x at level 99, B at level 200, only parsing) : bool_scope.
+ +
+End Exports.
+ +
+End FiniteQuant.
+Export FiniteQuant.Exports.
+ +
+Definition disjoint T (A B : mem_pred _) := @pred0b T (predI A B).
+Notation "[ 'disjoint' A & B ]" := (disjoint (mem A) (mem B))
+  (at level 0,
+   format "'[hv' [ 'disjoint' '/ ' A '/' & B ] ']'") : bool_scope.
+ +
+Module Type SubsetDefSig.
+Parameter subset : subset_type. Axiom subsetEdef : subset = subset_def.
+End SubsetDefSig.
+Module Export SubsetDef : SubsetDefSig.
+Definition subset : subset_type := subset_def.
+Definition subsetEdef := erefl subset.
+End SubsetDef.
+Canonical subset_unlock := Unlockable subsetEdef.
+Notation "A \subset B" := (subset (mem A) (mem B))
+  (at level 70, no associativity) : bool_scope.
+ +
+Definition proper T A B := @subset T A B && ~~ subset B A.
+Notation "A \proper B" := (proper (mem A) (mem B))
+  (at level 70, no associativity) : bool_scope.
+ +
+

+ +

+ image, xinv, inv, and ordinal operations will be defined later. +

+ +
+Section OpsTheory.
+ +
+Variable T : finType.
+ +
+Implicit Types A B C P Q : pred T.
+Implicit Types x y : T.
+Implicit Type s : seq T.
+ +
+Lemma enumP : Finite.axiom (Finite.enum T).
+ +
+Section EnumPick.
+ +
+Variable P : pred T.
+ +
+Lemma enumT : enum T = Finite.enum T.
+ +
+Lemma mem_enum A : enum A =i A.
+ +
+Lemma enum_uniq : uniq (enum P).
+ +
+Lemma enum0 : enum pred0 = Nil T.
+ +
+Lemma enum1 x : enum (pred1 x) = [:: x ].
+ +
+CoInductive pick_spec : option T → Type :=
+  | Pick x of P x : pick_spec (Some x)
+  | Nopick of P =1 xpred0 : pick_spec None.
+ +
+Lemma pickP : pick_spec (pick P).
+ +
+End EnumPick.
+ +
+Lemma eq_enum P Q : P =i Q → enum P = enum Q.
+ +
+Lemma eq_pick P Q : P =1 Q → pick P = pick Q.
+ +
+Lemma cardE A : #|A | = size (enum A).
+ +
+Lemma eq_card A B : A =i B → #|A | = #|B |.
+ +
+Lemma eq_card_trans A B n : #|A | = n → B =i A → #|B | = n.
+ +
+Lemma card0 : #|@pred0 T | = 0.
+ +
+Lemma cardT : #|T | = size (enum T).
+ +
+Lemma card1 x : #|pred1 x | = 1.
+ +
+Lemma eq_card0 A : A =i pred0 → #|A | = 0.
+ +
+Lemma eq_cardT A : A =i predT → #|A | = size (enum T).
+ +
+Lemma eq_card1 x A : A =i pred1 x → #|A | = 1.
+ +
+Lemma cardUI A B : #|[predU A & B ]| + #|[predI A & B ]| = #|A | + #|B |.
+ +
+Lemma cardID B A : #|[predI A & B ]| + #|[predD A & B ]| = #|A |.
+ +
+Lemma cardC A : #|A | + #|[predC A ]| = #|T |.
+ +
+Lemma cardU1 x A : #|[predU1 x & A ]| = (x \notin A ) + #|A |.
+ +
+Lemma card2 x y : #|pred2 x y | = (x != y ).+1.
+ +
+Lemma cardC1 x : #|predC1 x | = #|T |.-1.
+ +
+Lemma cardD1 x A : #|A | = (x \in A ) + #|[predD1 A & x ]|.
+ +
+Lemma max_card A : #|A | ≤ #|T |.
+ +
+Lemma card_size s : #|s | ≤ size s.
+ +
+Lemma card_uniqP s : reflect (#|s | = size s) (uniq s).
+ +
+Lemma card0_eq A : #|A | = 0 → A =i pred0.
+ +
+Lemma pred0P P : reflect (P =1 pred0) (pred0b P).
+ +
+Lemma pred0Pn P : reflect (∃ x, P x) (~~ pred0b P).
+ +
+Lemma card_gt0P A : reflect (∃ i, i \in A) (#|A | > 0).
+ +
+Lemma subsetE A B : (A \subset B ) = pred0b [predD A & B ].
+ +
+Lemma subsetP A B : reflect {subset A ≤ B } (A \subset B).
+ +
+Lemma subsetPn A B :
+  reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B )).
+ +
+Lemma subset_leq_card A B : A \subset B → #|A | ≤ #|B |.
+ +
+Lemma subxx_hint (mA : mem_pred T) : subset mA mA.
+Hint Resolve subxx_hint.
+ +
+

+ +

+ The parametrization by predType makes it easier to apply subxx. +

+ +

+ + Boolean quantifiers for finType + +

+ +
+Section QuantifierCombinators.
+ +
+Variables (T : finType) (P : pred T) (PP : T → Prop).
+Hypothesis viewP : ∀ x, reflect (PP x) (P x).
+ +
+Lemma existsPP : reflect (∃ x, PP x) [∃ x, P x ].
+ +
+Lemma forallPP : reflect (∀ x, PP x) [∀ x, P x ].
+ +
+End QuantifierCombinators.
+ +
+Notation "'exists_ view" := (existsPP (fun _ ⇒ view))
+  (at level 4, right associativity, format "''exists_' view").
+Notation "'forall_ view" := (forallPP (fun _ ⇒ view))
+  (at level 4, right associativity, format "''forall_' view").
+ +
+Section Quantifiers.
+ +
+Variables (T : finType) (rT : T → eqType).
+Implicit Type (D P : pred T) (f : ∀ x, rT x).
+ +
+Lemma forallP P : reflect (∀ x, P x) [∀ x, P x ].
+ +
+Lemma eqfunP f1 f2 : reflect (∀ x, f1 x = f2 x) [∀ x, f1 x == f2 x ].
+ +
+Lemma forall_inP D P : reflect (∀ x, D x → P x) [∀ (x | D x ), P x ].
+ +
+Lemma eqfun_inP D f1 f2 :
+  reflect {in D , ∀ x, f1 x = f2 x } [∀ (x | x \in D ), f1 x == f2 x ].
+ +
+Lemma existsP P : reflect (∃ x, P x) [∃ x, P x ].
+ +
+Lemma exists_eqP f1 f2 :
+  reflect (∃ x, f1 x = f2 x) [∃ x, f1 x == f2 x ].
+ +
+Lemma exists_inP D P : reflect (exists2 x, D x & P x) [∃ (x | D x ), P x ].
+ +
+Lemma exists_eq_inP D f1 f2 :
+  reflect (exists2 x, D x & f1 x = f2 x) [∃ (x | D x ), f1 x == f2 x ].
+ +
+Lemma eq_existsb P1 P2 : P1 =1 P2 → [∃ x, P1 x ] = [∃ x, P2 x ].
+ +
+Lemma eq_existsb_in D P1 P2 :
+    (∀ x, D x → P1 x = P2 x ) →
+  [∃ (x | D x ), P1 x ] = [∃ (x | D x ), P2 x ].
+ +
+Lemma eq_forallb P1 P2 : P1 =1 P2 → [∀ x, P1 x ] = [∀ x, P2 x ].
+ +
+Lemma eq_forallb_in D P1 P2 :
+    (∀ x, D x → P1 x = P2 x ) →
+  [∀ (x | D x ), P1 x ] = [∀ (x | D x ), P2 x ].
+ +
+Lemma negb_forall P : ~~ [∀ x, P x ] = [∃ x, ~~ P x ].
+ +
+Lemma negb_forall_in D P :
+  ~~ [∀ (x | D x ), P x ] = [∃ (x | D x ), ~~ P x ].
+ +
+Lemma negb_exists P : ~~ [∃ x, P x ] = [∀ x, ~~ P x ].
+ +
+Lemma negb_exists_in D P :
+  ~~ [∃ (x | D x ), P x ] = [∀ (x | D x ), ~~ P x ].
+ +
+End Quantifiers.
+ +
+ +
+Section Extrema.
+ +
+Variables (I : finType) (i0 : I) (P : pred I) (F : I → nat).
+ +
+Let arg_pred ord := [pred i | P i & [∀ (j | P j ), ord (F i) (F j)]].
+ +
+Definition arg_min := odflt i0 (pick (arg_pred leq)).
+ +
+Definition arg_max := odflt i0 (pick (arg_pred geq)).
+ +
+CoInductive extremum_spec (ord : rel nat) : I → Type :=
+  ExtremumSpec i of P i & (∀ j, P j → ord (F i) (F j))
+    : extremum_spec ord i.
+ +
+Hypothesis Pi0 : P i0.
+ +
+Let FP n := [∃ (i | P i ), F i == n ].
+Let FP_F i : P i → FP (F i).
+ Let exFP : ∃ n, FP n.
+ +
+Lemma arg_minP : extremum_spec leq arg_min.
+ +
+Lemma arg_maxP : extremum_spec geq arg_max.
+ +
+End Extrema.
+ +
+Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
+    (arg_min i0 (fun i ⇒ P%B) (fun i ⇒ F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg' 'min_' ( i < i0 | P ) F ]") : form_scope.
+ +
+Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
+    [arg min_(i < i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") : form_scope.
+ +
+Notation "[ 'arg' 'min_' ( i < i0 ) F ]" := [arg min_(i < i0 | true ) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg' 'min_' ( i < i0 ) F ]") : form_scope.
+ +
+Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
+     (arg_max i0 (fun i ⇒ P%B) (fun i ⇒ F))
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg' 'max_' ( i > i0 | P ) F ]") : form_scope.
+ +
+Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
+    [arg max_(i > i0 | i \in A) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") : form_scope.
+ +
+Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true ) F]
+  (at level 0, i, i0 at level 10,
+   format "[ 'arg' 'max_' ( i > i0 ) F ]") : form_scope.
+ +
+

+ +

+ + Boolean injectivity test for functions with a finType domain + +

+ +
+Section Injectiveb.
+ +
+Variables (aT : finType) (rT : eqType) (f : aT → rT).
+Implicit Type D : pred aT.
+ +
+Definition dinjectiveb D := uniq (map f (enum D)).
+ +
+Definition injectiveb := dinjectiveb aT.
+ +
+Lemma dinjectivePn D :
+  reflect (exists2 x, x \in D & exists2 y, y \in [predD1 D & x ] & f x = f y)
+          (~~ dinjectiveb D).
+ +
+Lemma dinjectiveP D : reflect {in D &, injective f } (dinjectiveb D).
+ +
+Lemma injectivePn :
+  reflect (∃ x, exists2 y, x != y & f x = f y) (~~ injectiveb).
+ +
+Lemma injectiveP : reflect (injective f) injectiveb.
+ +
+End Injectiveb.
+ +
+Definition image_mem T T' f mA : seq T' := map f (@enum_mem T mA).
+Notation image f A := (image_mem f (mem A)).
+Notation "[ 'seq' F | x 'in' A ]" := (image (fun x ⇒ F) A)
+  (at level 0, F at level 99, x ident,
+   format "'[hv' [ 'seq' F '/ ' | x 'in' A ] ']'") : seq_scope.
+Notation "[ 'seq' F | x : T 'in' A ]" := (image (fun x : T ⇒ F) A)
+  (at level 0, F at level 99, x ident, only parsing) : seq_scope.
+Notation "[ 'seq' F | x : T ]" :=
+  [seq F | x : T in sort_of_simpl_pred (@pred_of_argType T)]
+  (at level 0, F at level 99, x ident,
+   format "'[hv' [ 'seq' F '/ ' | x : T ] ']'") : seq_scope.
+Notation "[ 'seq' F , x ]" := [seq F | x : _ ]
+  (at level 0, F at level 99, x ident, only parsing) : seq_scope.
+ +
+Definition codom T T' f := @image_mem T T' f (mem T).
+ +
+Section Image.
+ +
+Variable T : finType.
+Implicit Type A : pred T.
+ +
+Section SizeImage.
+ +
+Variables (T' : Type) (f : T → T').
+ +
+Lemma size_image A : size (image f A) = #|A |.
+ +
+Lemma size_codom : size (codom f) = #|T |.
+ +
+Lemma codomE : codom f = map f (enum T).
+ +
+End SizeImage.
+ +
+Variables (T' : eqType) (f : T → T').
+ +
+Lemma imageP A y : reflect (exists2 x, x \in A & y = f x) (y \in image f A).
+ +
+Lemma codomP y : reflect (∃ x, y = f x) (y \in codom f).
+ +
+Remark iinv_proof A y : y \in image f A → {x | x \in A & f x = y }.
+ +
+Definition iinv A y fAy := s2val (@iinv_proof A y fAy).
+ +
+Lemma f_iinv A y fAy : f (@iinv A y fAy) = y.
+ +
+Lemma mem_iinv A y fAy : @iinv A y fAy \in A.
+ +
+Lemma in_iinv_f A : {in A &, injective f } →
+  ∀ x fAfx, x \in A → @iinv A (f x) fAfx = x.
+ +
+Lemma preim_iinv A B y fAy : preim f B (@iinv A y fAy) = B y.
+ +
+Lemma image_f A x : x \in A → f x \in image f A.
+ +
+Lemma codom_f x : f x \in codom f.
+ +
+Lemma image_codom A : {subset image f A ≤ codom f }.
+ +
+Lemma image_pred0 : image f pred0 =i pred0.
+ +
+Section Injective.
+ +
+Hypothesis injf : injective f.
+ +
+Lemma mem_image A x : (f x \in image f A ) = (x \in A ).
+ +
+Lemma pre_image A : [preim f of image f A ] =i A.
+ +
+Lemma image_iinv A y (fTy : y \in codom f) :
+  (y \in image f A ) = (iinv fTy \in A ).
+ +
+Lemma iinv_f x fTfx : @iinv T (f x) fTfx = x.
+ +
+Lemma image_pre (B : pred T') : image f [preim f of B ] =i [predI B & codom f ].
+ +
+Lemma bij_on_codom (x0 : T) : {on [pred y in codom f ], bijective f }.
+ +
+Lemma bij_on_image A (x0 : T) : {on [pred y in image f A ], bijective f }.
+ +
+End Injective.
+ +
+Fixpoint preim_seq s :=
+  if s is y :: s' then
+    (if pick (preim f (pred1 y)) is Some x then cons x else id) (preim_seq s')
+    else [::].
+ +
+Lemma map_preim (s : seq T') : {subset s ≤ codom f } → map f (preim_seq s) = s.
+ +
+End Image.
+ +
+ +
+Lemma flatten_imageP (aT : finType) (rT : eqType) A (P : pred aT) (y : rT) :
+  reflect (exists2 x, x \in P & y \in A x) (y \in flatten [seq A x | x in P ]).
+ +
+Section CardFunImage.
+ +
+Variables (T T' : finType) (f : T → T').
+Implicit Type A : pred T.
+ +
+Lemma leq_image_card A : #|image f A | ≤ #|A |.
+ +
+Lemma card_in_image A : {in A &, injective f } → #|image f A | = #|A |.
+ +
+Lemma image_injP A : reflect {in A &, injective f } (#|image f A | == #|A |).
+ +
+Hypothesis injf : injective f.
+ +
+Lemma card_image A : #|image f A | = #|A |.
+ +
+Lemma card_codom : #|codom f | = #|T |.
+ +
+Lemma card_preim (B : pred T') : #|[preim f of B ]| = #|[predI codom f & B ]|.
+ +
+Hypothesis card_range : #|T | = #|T'|.
+ +
+Lemma inj_card_onto y : y \in codom f.
+ +
+Lemma inj_card_bij : bijective f.
+ +
+End CardFunImage.
+ +
+ +
+Section FinCancel.
+ +
+Variables (T : finType) (f g : T → T).
+ +
+Section Inv.
+ +
+Hypothesis injf : injective f.
+ +
+Lemma injF_onto y : y \in codom f.
+Definition invF y := iinv (injF_onto y).
+Lemma invF_f : cancel f invF.
+Lemma f_invF : cancel invF f.
+Lemma injF_bij : bijective f.
+ +
+End Inv.
+ +
+Hypothesis fK : cancel f g.
+ +
+Lemma canF_sym : cancel g f.
+ +
+Lemma canF_LR x y : x = g y → f x = y.
+ +
+Lemma canF_RL x y : g x = y → x = f y.
+ +
+Lemma canF_eq x y : (f x == y ) = (x == g y ).
+ +
+Lemma canF_invF : g =1 invF (can_inj fK).
+ +
+End FinCancel.
+ +
+Section EqImage.
+ +
+Variables (T : finType) (T' : Type).
+ +
+Lemma eq_image (A B : pred T) (f g : T → T') :
+  A =i B → f =1 g → image f A = image g B.
+ +
+Lemma eq_codom (f g : T → T') : f =1 g → codom f = codom g.
+ +
+Lemma eq_invF f g injf injg : f =1 g → @invF T f injf =1 @invF T g injg.
+ +
+End EqImage.
+ +
+

+ +

+ Standard finTypes +

+ +
+Lemma unit_enumP : Finite.axiom [::tt ].
+Definition unit_finMixin := Eval hnf in FinMixin unit_enumP.
+Canonical unit_finType := Eval hnf in FinType unit unit_finMixin.
+Lemma card_unit : #|{: unit }| = 1.
+ +
+Lemma bool_enumP : Finite.axiom [:: true ; false ].
+Definition bool_finMixin := Eval hnf in FinMixin bool_enumP.
+Canonical bool_finType := Eval hnf in FinType bool bool_finMixin.
+Lemma card_bool : #|{: bool }| = 2.
+ +
+ +
+Section OptionFinType.
+ +
+Variable T : finType.
+ +
+Definition option_enum := None :: map some (enumF T).
+ +
+Lemma option_enumP : Finite.axiom option_enum.
+ +
+Definition option_finMixin := Eval hnf in FinMixin option_enumP.
+Canonical option_finType := Eval hnf in FinType (option T) option_finMixin.
+ +
+Lemma card_option : #|{: option T }| = #|T |.+1.
+ +
+End OptionFinType.
+ +
+Section TransferFinType.
+ +
+Variables (eT : countType) (fT : finType) (f : eT → fT).
+ +
+Lemma pcan_enumP g : pcancel f g → Finite.axiom (undup (pmap g (enumF fT))).
+ +
+Definition PcanFinMixin g fK := FinMixin (@pcan_enumP g fK).
+ +
+Definition CanFinMixin g (fK : cancel f g) := PcanFinMixin (can_pcan fK).
+ +
+End TransferFinType.
+ +
+Section SubFinType.
+ +
+Variables (T : choiceType) (P : pred T).
+Import Finite.
+ +
+Structure subFinType := SubFinType {
+  subFin_sort :> subType P;
+  _ : mixin_of (sub_eqType subFin_sort)
+}.
+ +
+Definition pack_subFinType U :=
+  fun cT b m & phant_id (class cT) (@Class U b m) ⇒
+  fun sT m' & phant_id m' m ⇒ @SubFinType sT m'.
+ +
+Implicit Type sT : subFinType.
+ +
+Definition subFin_mixin sT :=
+  let: SubFinType _ m := sT return mixin_of (sub_eqType sT) in m.
+ +
+Coercion subFinType_subCountType sT := @SubCountType _ _ sT (subFin_mixin sT).
+Canonical subFinType_subCountType.
+ +
+Coercion subFinType_finType sT :=
+  Pack (@Class sT (sub_choiceClass sT) (subFin_mixin sT)) sT.
+Canonical subFinType_finType.
+ +
+Lemma codom_val sT x : (x \in codom (val : sT → T)) = P x.
+ +
+End SubFinType.
+ +
+

+ +

+ This assumes that T has both finType and subCountType structures. +

+Notation "[ 'subFinType' 'of' T ]" := (@pack_subFinType _ _ T _ _ _ id _ _ id)
+ (at level 0, format "[ 'subFinType' 'of' T ]") : form_scope.
+ +
+Section FinTypeForSub.
+ +
+Variables (T : finType) (P : pred T) (sT : subCountType P).
+ +
+Definition sub_enum : seq sT := pmap insub (enumF T).
+ +
+Lemma mem_sub_enum u : u \in sub_enum.
+ +
+Lemma sub_enum_uniq : uniq sub_enum.
+ +
+Lemma val_sub_enum : map val sub_enum = enum P.
+ +
+

+ +

+ We can't declare a canonical structure here because we've already + stated that subType_sort and FinType.sort unify via to the + subType_finType structure. +

+ +
+Definition SubFinMixin := UniqFinMixin sub_enum_uniq mem_sub_enum.
+Definition SubFinMixin_for (eT : eqType) of phant eT :=
+ eq_rect _ Finite.mixin_of SubFinMixin eT.
+ +
+Variable sfT : subFinType P.
+ +
+Lemma card_sub : #|sfT | = #|[pred x | P x ]|.
+ +
+Lemma eq_card_sub (A : pred sfT) : A =i predT → #|A | = #|[pred x | P x ]|.
+ +
+End FinTypeForSub.
+ +
+

+ +

+ This assumes that T has a subCountType structure over a type that + has a finType structure. +

+Notation "[ 'finMixin' 'of' T 'by' <: ]" :=
+ (SubFinMixin_for (Phant T) (erefl _))
+ (at level 0, format "[ 'finMixin' 'of' T 'by' <: ]") : form_scope.
+ +
+

+ +

+ Regression for the subFinType stack +Record myb : Type := MyB {myv : bool; _ : ~~ myv}. +Canonical myb_sub := Eval hnf in [subType for myv]. +Definition myb_eqm := Eval hnf in [eqMixin of myb by <: ]. +Canonical myb_eq := Eval hnf in EqType myb myb_eqm. +Definition myb_chm := [choiceMixin of myb by <: ]. +Canonical myb_ch := Eval hnf in ChoiceType myb myb_chm. +Definition myb_cntm := [countMixin of myb by <: ]. +Canonical myb_cnt := Eval hnf in CountType myb myb_cntm. +Canonical myb_scnt := Eval hnf in [subCountType of myb]. +Definition myb_finm := [finMixin of myb by <: ]. +Canonical myb_fin := Eval hnf in FinType myb myb_finm. +Canonical myb_sfin := Eval hnf in [subFinType of myb]. +Print Canonical Projections. +Print myb_finm. +Print myb_cntm. + +

+ +
+Section CardSig.
+ +
+Variables (T : finType) (P : pred T).
+ +
+Definition sig_finMixin := [finMixin of {x | P x } by <:].
+Canonical sig_finType := Eval hnf in FinType {x | P x } sig_finMixin.
+Canonical sig_subFinType := Eval hnf in [subFinType of {x | P x }].
+ +
+Lemma card_sig : #|{: {x | P x }}| = #|[pred x | P x ]|.
+ +
+End CardSig.
+ +
+

+ +

+ Subtype for an explicit enumeration. +

+Section SeqSubType.
+ +
+Variables (T : eqType) (s : seq T).
+ +
+Record seq_sub : Type := SeqSub {ssval : T; ssvalP : in_mem ssval (@mem T _ s)}.
+ +
+Canonical seq_sub_subType := Eval hnf in [subType for ssval ].
+Definition seq_sub_eqMixin := Eval hnf in [eqMixin of seq_sub by <:].
+Canonical seq_sub_eqType := Eval hnf in EqType seq_sub seq_sub_eqMixin.
+ +
+Definition seq_sub_enum : seq seq_sub := undup (pmap insub s).
+ +
+Lemma mem_seq_sub_enum x : x \in seq_sub_enum.
+ +
+Lemma val_seq_sub_enum : uniq s → map val seq_sub_enum = s.
+ +
+Definition seq_sub_pickle x := index x seq_sub_enum.
+Definition seq_sub_unpickle n := nth None (map some seq_sub_enum) n.
+Lemma seq_sub_pickleK : pcancel seq_sub_pickle seq_sub_unpickle.
+ +
+Definition seq_sub_countMixin := CountMixin seq_sub_pickleK.
+Fact seq_sub_axiom : Finite.axiom seq_sub_enum.
+ Definition seq_sub_finMixin := Finite.Mixin seq_sub_countMixin seq_sub_axiom.
+ +
+

+ +

+ Beware: these are not the canonical instances, as they are not consistent + with the generic sub_choiceType canonical instance. +

+Definition adhoc_seq_sub_choiceMixin := PcanChoiceMixin seq_sub_pickleK.
+Definition adhoc_seq_sub_choiceType :=
+ Eval hnf in ChoiceType seq_sub adhoc_seq_sub_choiceMixin.
+Definition adhoc_seq_sub_finType :=
+ [finType of seq_sub for FinType adhoc_seq_sub_choiceType seq_sub_finMixin ].
+ +
+End SeqSubType.
+ +
+Section SeqFinType.
+ +
+Variables (T : choiceType) (s : seq T).
+ +
+Definition seq_sub_choiceMixin := [choiceMixin of sT by <:].
+Canonical seq_sub_choiceType := Eval hnf in ChoiceType sT seq_sub_choiceMixin.
+ +
+Canonical seq_sub_countType := Eval hnf in CountType sT (seq_sub_countMixin s).
+Canonical seq_sub_subCountType := Eval hnf in [subCountType of sT ].
+Canonical seq_sub_finType := Eval hnf in FinType sT (seq_sub_finMixin s).
+Canonical seq_sub_subFinType := Eval hnf in [subFinType of sT ].
+ +
+Lemma card_seq_sub : uniq s → #|{:sT }| = size s.
+ +
+End SeqFinType.
+ +
+

+ +

+ + Ordinal finType : {0, ... , n-1} + +

+ +
+Section OrdinalSub.
+ +
+Variable n : nat.
+ +
+Inductive ordinal : predArgType := Ordinal m of m < n.
+ +
+Coercion nat_of_ord i := let: Ordinal m _ := i in m.
+ +
+Canonical ordinal_subType := [subType for nat_of_ord ].
+Definition ordinal_eqMixin := Eval hnf in [eqMixin of ordinal by <:].
+Canonical ordinal_eqType := Eval hnf in EqType ordinal ordinal_eqMixin.
+Definition ordinal_choiceMixin := [choiceMixin of ordinal by <:].
+Canonical ordinal_choiceType :=
+  Eval hnf in ChoiceType ordinal ordinal_choiceMixin.
+Definition ordinal_countMixin := [countMixin of ordinal by <:].
+Canonical ordinal_countType := Eval hnf in CountType ordinal ordinal_countMixin.
+Canonical ordinal_subCountType := [subCountType of ordinal ].
+ +
+Lemma ltn_ord (i : ordinal) : i < n.
+ +
+Lemma ord_inj : injective nat_of_ord.
+ +
+Definition ord_enum : seq ordinal := pmap insub (iota 0 n).
+ +
+Lemma val_ord_enum : map val ord_enum = iota 0 n.
+ +
+Lemma ord_enum_uniq : uniq ord_enum.
+ +
+Lemma mem_ord_enum i : i \in ord_enum.
+ +
+Definition ordinal_finMixin :=
+  Eval hnf in UniqFinMixin ord_enum_uniq mem_ord_enum.
+Canonical ordinal_finType := Eval hnf in FinType ordinal ordinal_finMixin.
+Canonical ordinal_subFinType := Eval hnf in [subFinType of ordinal ].
+ +
+End OrdinalSub.
+ +
+Notation "''I_' n" := (ordinal n)
+  (at level 8, n at level 2, format "''I_' n").
+ +
+Hint Resolve ltn_ord.
+ +
+Section OrdinalEnum.
+ +
+Variable n : nat.
+ +
+Lemma val_enum_ord : map val (enum 'I_n) = iota 0 n.
+ +
+Lemma size_enum_ord : size (enum 'I_n) = n.
+ +
+Lemma card_ord : #|'I_n | = n.
+ +
+Lemma nth_enum_ord i0 m : m < n → nth i0 (enum 'I_n) m = m :> nat.
+ +
+Lemma nth_ord_enum (i0 i : 'I_n) : nth i0 (enum 'I_n) i = i.
+ +
+Lemma index_enum_ord (i : 'I_n) : index i (enum 'I_n) = i.
+ +
+End OrdinalEnum.
+ +
+Lemma widen_ord_proof n m (i : 'I_n) : n ≤ m → i < m.
+ Definition widen_ord n m le_n_m i := Ordinal (@widen_ord_proof n m i le_n_m).
+ +
+Lemma cast_ord_proof n m (i : 'I_n) : n = m → i < m.
+ Definition cast_ord n m eq_n_m i := Ordinal (@cast_ord_proof n m i eq_n_m).
+ +
+Lemma cast_ord_id n eq_n i : cast_ord eq_n i = i :> 'I_n.
+ +
+Lemma cast_ord_comp n1 n2 n3 eq_n2 eq_n3 i :
+  @cast_ord n2 n3 eq_n3 (@cast_ord n1 n2 eq_n2 i) =
+    cast_ord (etrans eq_n2 eq_n3) i.
+ +
+Lemma cast_ordK n1 n2 eq_n :
+  cancel (@cast_ord n1 n2 eq_n) (cast_ord (esym eq_n)).
+ +
+Lemma cast_ordKV n1 n2 eq_n :
+  cancel (cast_ord (esym eq_n)) (@cast_ord n1 n2 eq_n).
+ +
+Lemma cast_ord_inj n1 n2 eq_n : injective (@cast_ord n1 n2 eq_n).
+ +
+Lemma rev_ord_proof n (i : 'I_n) : n - i .+1 < n.
+ Definition rev_ord n i := Ordinal (@rev_ord_proof n i).
+ +
+Lemma rev_ordK n : involutive (@rev_ord n).
+ +
+Lemma rev_ord_inj {n} : injective (@rev_ord n).
+ +
+

+ +

+ bijection between any finType T and the Ordinal finType of its cardinal +

+Section EnumRank.
+ +
+Variable T : finType.
+Implicit Type A : pred T.
+ +
+Lemma enum_rank_subproof x0 A : x0 \in A → 0 < #|A |.
+ +
+Definition enum_rank_in x0 A (Ax0 : x0 \in A) x :=
+  insubd (Ordinal (@enum_rank_subproof x0 [eta A ] Ax0)) (index x (enum A)).
+ +
+Definition enum_rank x := @enum_rank_in x T (erefl true) x.
+ +
+Lemma enum_default A : 'I_(#|A |) → T.
+ +
+Definition enum_val A i := nth (@enum_default [eta A ] i) (enum A) i.
+ +
+Lemma enum_valP A i : @enum_val A i \in A.
+ +
+Lemma enum_val_nth A x i : @enum_val A i = nth x (enum A) i.
+ +
+Lemma nth_image T' y0 (f : T → T') A (i : 'I_#|A |) :
+  nth y0 (image f A) i = f (enum_val i).
+ +
+Lemma nth_codom T' y0 (f : T → T') (i : 'I_#|T |) :
+  nth y0 (codom f) i = f (enum_val i).
+ +
+Lemma nth_enum_rank_in x00 x0 A Ax0 :
+  {in A , cancel (@enum_rank_in x0 A Ax0) (nth x00 (enum A))}.
+ +
+Lemma nth_enum_rank x0 : cancel enum_rank (nth x0 (enum T)).
+ +
+Lemma enum_rankK_in x0 A Ax0 :
+   {in A , cancel (@enum_rank_in x0 A Ax0) enum_val }.
+ +
+Lemma enum_rankK : cancel enum_rank enum_val.
+ +
+Lemma enum_valK_in x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0).
+ +
+Lemma enum_valK : cancel enum_val enum_rank.
+ +
+Lemma enum_rank_inj : injective enum_rank.
+ +
+Lemma enum_val_inj A : injective (@enum_val A).
+ +
+Lemma enum_val_bij_in x0 A : x0 \in A → {on A , bijective (@enum_val A )}.
+ +
+Lemma enum_rank_bij : bijective enum_rank.
+ +
+Lemma enum_val_bij : bijective (@enum_val T).
+ +
+

+ +

+ Due to the limitations of the Coq unification patterns, P can only be + inferred from the premise of this lemma, not its conclusion. As a result + this lemma will only be usable in forward chaining style. +

+Lemma fin_all_exists U (P : ∀ x : T, U x → Prop) :
+  (∀ x, ∃ u, P x u ) → (∃ u, ∀ x, P x (u x)).
+ +
+Lemma fin_all_exists2 U (P Q : ∀ x : T, U x → Prop) :
+    (∀ x, exists2 u, P x u & Q x u ) →
+  (exists2 u, ∀ x, P x (u x) & ∀ x, Q x (u x)).
+ +
+End EnumRank.
+ +
+ +
+Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i.
+ +
+Lemma enum_val_ord n i : enum_val i = cast_ord (card_ord n) i.
+ +
+

+ +

+ The integer bump / unbump operations. +

+ +
+Definition bump h i := (h ≤ i ) + i.
+Definition unbump h i := i - (h < i ).
+ +
+Lemma bumpK h : cancel (bump h) (unbump h).
+ +
+Lemma neq_bump h i : h != bump h i.
+ +
+Lemma unbumpKcond h i : bump h (unbump h i) = (i == h ) + i.
+ +
+Lemma unbumpK h : {in predC1 h , cancel (unbump h) (bump h)}.
+ +
+Lemma bump_addl h i k : bump (k + h) (k + i) = k + bump h i.
+ +
+Lemma bumpS h i : bump h .+1 i .+1 = (bump h i ).+1.
+ +
+Lemma unbump_addl h i k : unbump (k + h) (k + i) = k + unbump h i.
+ +
+Lemma unbumpS h i : unbump h .+1 i .+1 = (unbump h i ).+1.
+ +
+Lemma leq_bump h i j : (i ≤ bump h j ) = (unbump h i ≤ j ).
+ +
+Lemma leq_bump2 h i j : (bump h i ≤ bump h j ) = (i ≤ j ).
+ +
+Lemma bumpC h1 h2 i :
+ bump h1 (bump h2 i) = bump (bump h1 h2) (bump (unbump h2 h1) i).
+ +
+

+ +

+ The lift operations on ordinals; to avoid a messy dependent type, + unlift is a partial operation (returns an option). +

+ +
+Lemma lift_subproof n h (i : 'I_n .-1) : bump h i < n.
+ +
+Definition lift n (h : 'I_n) (i : 'I_n .-1) := Ordinal (lift_subproof h i).
+ +
+Lemma unlift_subproof n (h : 'I_n) (u : {j | j != h }) : unbump h (val u) < n .-1.
+ +
+Definition unlift n (h i : 'I_n) :=
+  omap (fun u : {j | j != h } ⇒ Ordinal (unlift_subproof u)) (insub i).
+ +
+CoInductive unlift_spec n h i : option 'I_n .-1 → Type :=
+  | UnliftSome j of i = lift h j : unlift_spec h i (Some j)
+  | UnliftNone of i = h : unlift_spec h i None.
+ +
+Lemma unliftP n (h i : 'I_n) : unlift_spec h i (unlift h i).
+ +
+Lemma neq_lift n (h : 'I_n) i : h != lift h i.
+ +
+Lemma unlift_none n (h : 'I_n) : unlift h h = None.
+ +
+Lemma unlift_some n (h i : 'I_n) :
+  h != i → {j | i = lift h j & unlift h i = Some j }.
+ +
+Lemma lift_inj n (h : 'I_n) : injective (lift h).
+ +
+Lemma liftK n (h : 'I_n) : pcancel (lift h) (unlift h).
+ +
+

+ +

+ Shifting and splitting indices, for cutting and pasting arrays +

+ +
+Lemma lshift_subproof m n (i : 'I_m) : i < m + n.
+ +
+Lemma rshift_subproof m n (i : 'I_n) : m + i < m + n.
+ +
+Definition lshift m n (i : 'I_m) := Ordinal (lshift_subproof n i).
+Definition rshift m n (i : 'I_n) := Ordinal (rshift_subproof m i).
+ +
+Lemma split_subproof m n (i : 'I_(m + n )) : i ≥ m → i - m < n.
+ +
+Definition split m n (i : 'I_(m + n )) : 'I_m + 'I_n :=
+  match ltnP (i) m with
+  | LtnNotGeq lt_i_m ⇒ inl _ (Ordinal lt_i_m)
+  | GeqNotLtn ge_i_m ⇒ inr _ (Ordinal (split_subproof ge_i_m))
+  end.
+ +
+CoInductive split_spec m n (i : 'I_(m + n )) : 'I_m + 'I_n → bool → Type :=
+  | SplitLo (j : 'I_m) of i = j :> nat : split_spec i (inl _ j) true
+  | SplitHi (k : 'I_n) of i = m + k :> nat : split_spec i (inr _ k) false.
+ +
+Lemma splitP m n (i : 'I_(m + n )) : split_spec i (split i) (i < m).
+ +
+Definition unsplit m n (jk : 'I_m + 'I_n) :=
+  match jk with inl j ⇒ lshift n j | inr k ⇒ rshift m k end.
+ +
+Lemma ltn_unsplit m n (jk : 'I_m + 'I_n) : (unsplit jk < m ) = jk.
+ +
+Lemma splitK m n : cancel (@split m n) (@unsplit m n).
+ +
+Lemma unsplitK m n : cancel (@unsplit m n) (@split m n).
+ +
+Section OrdinalPos.
+ +
+Variable n' : nat.
+ +
+Definition ord0 := Ordinal (ltn0Sn n').
+Definition ord_max := Ordinal (ltnSn n').
+ +
+Lemma leq_ord (i : 'I_n) : i ≤ n'.
+ +
+Lemma sub_ord_proof m : n' - m < n.
+ Definition sub_ord m := Ordinal (sub_ord_proof m).
+ +
+Lemma sub_ordK (i : 'I_n) : n' - (n' - i ) = i.
+ +
+Definition inord m : 'I_n := insubd ord0 m.
+ +
+Lemma inordK m : m < n → inord m = m :> nat.
+ +
+Lemma inord_val (i : 'I_n) : inord i = i.
+ +
+Lemma enum_ordS : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n').
+ +
+Lemma lift_max (i : 'I_n') : lift ord_max i = i :> nat.
+ +
+Lemma lift0 (i : 'I_n') : lift ord0 i = i .+1 :> nat.
+ +
+End OrdinalPos.
+ +
+ +
+

+ +

+ Product of two fintypes which is a fintype +

+Section ProdFinType.
+ +
+Variable T1 T2 : finType.
+ +
+Definition prod_enum := [seq (x1 , x2 ) | x1 <- enum T1 , x2 <- enum T2 ].
+ +
+Lemma predX_prod_enum (A1 : pred T1) (A2 : pred T2) :
+  count [predX A1 & A2 ] prod_enum = #|A1 | × #|A2 |.
+ +
+Lemma prod_enumP : Finite.axiom prod_enum.
+ +
+Definition prod_finMixin := Eval hnf in FinMixin prod_enumP.
+Canonical prod_finType := Eval hnf in FinType (T1 × T2) prod_finMixin.
+ +
+Lemma cardX (A1 : pred T1) (A2 : pred T2) : #|[predX A1 & A2 ]| = #|A1 | × #|A2 |.
+ +
+Lemma card_prod : #|{: T1 × T2 }| = #|T1 | × #|T2 |.
+ +
+Lemma eq_card_prod (A : pred (T1 × T2)) : A =i predT → #|A | = #|T1 | × #|T2 |.
+ +
+End ProdFinType.
+ +
+Section TagFinType.
+ +
+Variables (I : finType) (T_ : I → finType).
+ +
+Definition tag_enum :=
+  flatten [seq [seq Tagged T_ x | x <- enumF (T_ i)] | i <- enumF I ].
+ +
+Lemma tag_enumP : Finite.axiom tag_enum.
+ +
+Definition tag_finMixin := Eval hnf in FinMixin tag_enumP.
+Canonical tag_finType := Eval hnf in FinType {i : I & T_ i } tag_finMixin.
+ +
+Lemma card_tagged :
+  #|{: {i : I & T_ i }}| = sumn (map (fun i ⇒ #|T_ i |) (enum I)).
+ +
+End TagFinType.
+ +
+Section SumFinType.
+ +
+Variables T1 T2 : finType.
+ +
+Definition sum_enum :=
+  [seq inl _ x | x <- enumF T1 ] ++ [seq inr _ y | y <- enumF T2 ].
+ +
+Lemma sum_enum_uniq : uniq sum_enum.
+ +
+Lemma mem_sum_enum u : u \in sum_enum.
+ +
+Definition sum_finMixin := Eval hnf in UniqFinMixin sum_enum_uniq mem_sum_enum.
+Canonical sum_finType := Eval hnf in FinType (T1 + T2) sum_finMixin.
+ +
+Lemma card_sum : #|{: T1 + T2 }| = #|T1 | + #|T2 |.
+ +
+End SumFinType.
+