- -

Library mathcomp.ssreflect.fintype

- -

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

- -

- 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 T m == the packed finType class for type T and 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 _). - 'forall_in_pP <-> view for [forall x in .., p _ ], for pP as above. - 'exists_in_pP <-> view for [exists x in .., p _ ], for pP as above. - [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 such that 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 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 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. - These are special instances of - [arg[ord](i < i0 | P) F] == a value i : I, minimizing F wrt ord : rel T - such that for all j : T, ord (F i) (F j) - subject to the condition P, and provided P i0 - where I : finType, T : eqType and F : I -> T - [arg[ord](i < i0 in A) F] == an i \in A minimizing F wrt ord, if i0 \in A. - [arg[ord](i < i0) F] == an i : T minimizing F wrt ord, 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)
-}.
-Definition base2 T c := Countable.Class (@base T c) (mixin_base (mixin c)).
- -
-Structure type : Type := Pack {sort; _ : class_of sort}.
-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.
-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).
- -
-Definition eqType := @Equality.Pack cT xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition countType := @Countable.Pack cT (base2 xclass).
- -
-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.
- -
-Variant 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 : {pred T }) (P Q : pred T) (x y : T) (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 A : uniq (enum A).
- -
-Lemma enum0 : enum pred0 = Nil T.
- -
-Lemma enum1 x : enum (pred1 x) = [:: x ].
- -
-Variant 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 A B : A =i B → enum A = enum B.
- -
-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 : core.
- -
-

- -

- 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 Types (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 forall_inPP D P PP : (∀ x, reflect (PP x) (P x)) →
-  reflect (∀ x, D x → PP 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_inPP D P PP : (∀ x, reflect (PP x) (P x)) →
-  reflect (exists2 x, D x & PP 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.
- -
- -
-Notation "'exists_in_ view" := (exists_inPP _ (fun _ ⇒ view))
-  (at level 4, right associativity, format "''exists_in_' view").
-Notation "'forall_in_ view" := (forall_inPP _ (fun _ ⇒ view))
-  (at level 4, right associativity, format "''forall_in_' view").
- -
-Section Extrema.
- -
-Variant extremum_spec {T : eqType} (ord : rel T) {I : finType}
-  (P : pred I) (F : I → T) : I → Type :=
-  ExtremumSpec (i : I) of P i & (∀ j : I, P j → ord (F i) (F j)) :
-                   extremum_spec ord P F i.
- -
-Let arg_pred {T : eqType} ord {I : finType} (P : pred I) (F : I → T) :=
-  [pred i | P i & [∀ (j | P j ), ord (F i) (F j)]].
- -
-Section Extremum.
- -
-Context {T : eqType} {I : finType} (ord : rel T).
-Context (i0 : I) (P : pred I) (F : I → T).
- -
-Hypothesis ord_refl : reflexive ord.
-Hypothesis ord_trans : transitive ord.
-Hypothesis ord_total : total ord.
- -
-Definition extremum := odflt i0 (pick (arg_pred ord P F)).
- -
-Hypothesis Pi0 : P i0.
- -
-Lemma extremumP : extremum_spec ord P F extremum.
- -
-End Extremum.
- -
-Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" :=
-    (extremum ord i0 (fun i ⇒ P%B) (fun i ⇒ F))
-  (at level 0, ord, i, i0 at level 10,
-   format "[ 'arg[' ord ]_( i < i0 | P ) F ]") : form_scope.
- -
-Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" :=
-    [arg [ord]_(i < i0 | i \in A) F]
-  (at level 0, ord, i, i0 at level 10,
-   format "[ 'arg[' ord ]_( i < i0 'in' A ) F ]") : form_scope.
- -
-Notation "[ 'arg[' ord ]_( i < i0 ) F ]" := [arg [ord]_(i < i0 | true ) F]
-  (at level 0, ord, i, i0 at level 10,
-   format "[ 'arg[' ord ]_( i < i0 ) F ]") : form_scope.
- -
-Section ArgMinMax.
- -
-Variables (I : finType) (i0 : I) (P : pred I) (F : I → nat) (Pi0 : P i0).
- -
-Definition arg_min := extremum leq i0 P F.
-Definition arg_max := extremum geq i0 P F.
- -
-Lemma arg_minP : extremum_spec leq P F arg_min.
- -
-Lemma arg_maxP : extremum_spec geq P F arg_max.
- -
-End ArgMinMax.
- -
-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 pred_of_simpl (@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 : aT → seq rT) (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)).
-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 : core.
- -
-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).
- -
-Variant 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.
- -
-Variant 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.
- -
-Lemma unsplitK {m n} : cancel (@unsplit m n) split.
- -
-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.
-