(Joint Center)Library Ssreflect.fintype

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.

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 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 and T has a choiceType structure; the seq_sub s type has a canonical finType structure. 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 ee =i Taxiom 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 emixin_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)).
Local Coercion base : class_of >-> Choice.class_of.

Structure type : Type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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 mPack (@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 cTmixin_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 xP%B))
  (at level 0, x ident, format "[ 'pick' x | P ]") : form_scope.
Notation "[ 'pick' x : T | P ]" := (pick (fun x : TP%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.

Local Notation card_type := ( T : finType, mem_pred Tnat).
Local Notation card_def := (fun T mAsize (enum_mem mA)).
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 xB x)) (at level 0, x ident).
Notation "[ x : T | B ]" := (quant0b (fun x : TB 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.

Notation Local subset_type := ( (T : finType) (A B : mem_pred T), bool).
Notation Local subset_def := (fun T A Bpred0b (predD A B)).
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 TType :=
  | 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 Qenum P = enum Q.

Lemma eq_pick P Q : P =1 Qpick 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| = nB =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.
Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA.

Lemma eq_subset A1 A2 : A1 =i A2subset (mem A1) =1 subset (mem A2).

Lemma eq_subset_r B1 B2 : B1 =i B2
  (@subset T)^~ (mem B1) =1 (@subset T)^~ (mem B2).

Lemma eq_subxx A B : A =i BA \subset B.

Lemma subset_predT A : A \subset T.

Lemma predT_subset A : T \subset A x, x \in A.

Lemma subset_pred1 A x : (pred1 x \subset A) = (x \in A).

Lemma subset_eqP A B : reflect (A =i B) ((A \subset B) && (B \subset A)).

Lemma subset_cardP A B : #|A| = #|B|reflect (A =i B) (A \subset B).

Lemma subset_leqif_card A B : A \subset B#|A| #|B| ?= iff (B \subset A).

Lemma subset_trans A B C : A \subset BB \subset CA \subset C.

Lemma subset_all s A : (s \subset A) = all (mem A) s.

Lemma properE A B : A \proper B = (A \subset B) && ~~(B \subset A).

Lemma properP A B :
  reflect (A \subset B (exists2 x, x \in B & x \notin A)) (A \proper B).

Lemma proper_sub A B : A \proper BA \subset B.

Lemma proper_subn A B : A \proper B~~ (B \subset A).

Lemma proper_trans A B C : A \proper BB \proper CA \proper C.

Lemma proper_sub_trans A B C : A \proper BB \subset CA \proper C.

Lemma sub_proper_trans A B C : A \subset BB \proper CA \proper C.

Lemma proper_card A B : A \proper B#|A| < #|B|.

Lemma proper_irrefl A : ~~ (A \proper A).

Lemma properxx A : (A \proper A) = false.

Lemma eq_proper A B : A =i Bproper (mem A) =1 proper (mem B).

Lemma eq_proper_r A B : A =i B
  (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B).

Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A].

Lemma eq_disjoint A1 A2 : A1 =i A2disjoint (mem A1) =1 disjoint (mem A2).

Lemma eq_disjoint_r B1 B2 : B1 =i B2
  (@disjoint T)^~ (mem B1) =1 (@disjoint T)^~ (mem B2).

Lemma subset_disjoint A B : (A \subset B) = [disjoint A & [predC B]].

Lemma disjoint_subset A B : [disjoint A & B] = (A \subset [predC B]).

Lemma disjoint_trans A B C :
   A \subset B[disjoint B & C][disjoint A & C].

Lemma disjoint0 A : [disjoint pred0 & A].

Lemma eq_disjoint0 A B : A =i pred0[disjoint A & B].

Lemma disjoint1 x A : [disjoint pred1 x & A] = (x \notin A).

Lemma eq_disjoint1 x A B :
  A =i pred1 x[disjoint A & B] = (x \notin B).

Lemma disjointU A B C :
  [disjoint predU A B & C] = [disjoint A & C] && [disjoint B & C].

Lemma disjointU1 x A B :
  [disjoint predU1 x A & B] = (x \notin B) && [disjoint A & B].

Lemma disjoint_cons x s B :
  [disjoint x :: s & B] = (x \notin B) && [disjoint s & B].

Lemma disjoint_has s A : [disjoint s & A] = ~~ has (mem A) s.

Lemma disjoint_cat s1 s2 A :
  [disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A].

End OpsTheory.

Hint Resolve subxx_hint.

Implicit Arguments pred0P [T P].
Implicit Arguments pred0Pn [T P].
Implicit Arguments subsetP [T A B].
Implicit Arguments subsetPn [T A B].
Implicit Arguments subset_eqP [T A B].
Implicit Arguments card_uniqP [T s].
Implicit Arguments properP [T A B].

Boolean quantifiers for finType

Section QuantifierCombinators.

Variables (T : finType) (P : pred T) (PP : TProp).
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 : TeqType).
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 xP 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 xP1 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 xP1 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.

Implicit Arguments forallP [T P].
Implicit Arguments eqfunP [T rT f1 f2].
Implicit Arguments forall_inP [T D P].
Implicit Arguments eqfun_inP [T rT D f1 f2].
Implicit Arguments existsP [T P].
Implicit Arguments exists_eqP [T rT f1 f2].
Implicit Arguments exists_inP [T D P].
Implicit Arguments exists_eq_inP [T rT D f1 f2].

Section Extrema.

Variables (I : finType) (i0 : I) (P : pred I) (F : Inat).

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) : IType :=
  ExtremumSpec i of P i & ( j, P jord (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 iFP (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 iP%B) (fun iF))
  (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 iP%B) (fun iF))
  (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 : aTrT).
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 xF) 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 : TF) 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 : TT').

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 : TT').

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 Af 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.

Implicit Arguments imageP [T T' f A y].
Implicit Arguments codomP [T T' f y].

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]).
Implicit Arguments flatten_imageP [aT rT A P y].

Section CardFunImage.

Variables (T T' : finType) (f : TT').
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.

Implicit Arguments image_injP [T T' f A].

Section FinCancel.

Variables (T : finType) (f g : TT).

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 yf x = y.

Lemma canF_RL x y : g x = yx = 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 : TT') :
  A =i Bf =1 gimage f A = image g B.

Lemma eq_codom (f g : TT') : f =1 gcodom 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

Section SeqFinType.

Variables (T : choiceType) (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_choiceMixin := [choiceMixin of seq_sub by <:].
Canonical seq_sub_choiceType :=
  Eval hnf in ChoiceType seq_sub seq_sub_choiceMixin.

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 smap 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.
Canonical seq_sub_countType := Eval hnf in CountType seq_sub seq_sub_countMixin.
Canonical seq_sub_subCountType := Eval hnf in [subCountType of seq_sub].
Definition seq_sub_finMixin :=
  Eval hnf in UniqFinMixin (undup_uniq _) mem_seq_sub_enum.
Canonical seq_sub_finType := Eval hnf in FinType seq_sub seq_sub_finMixin.

Lemma card_seq_sub : uniq s#|{:seq_sub}| = size s.

End SeqFinType.

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.

Local Notation enumF T := (Finite.enum T).

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 : eTfT).

Lemma pcan_enumP g : pcancel f gFinite.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 : sTT)) = 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.

Canonical seq_sub_subFinType T s :=
  Eval hnf in [subFinType of @seq_sub T s].

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.
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.

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 < nnth 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 mi < 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 = mi < 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 : TT') A (i : 'I_#|A|) :
  nth y0 (image f A) i = f (enum_val i).

Lemma nth_codom T' y0 (f : TT') (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 xProp) :
  ( x, u, P x u) → ( u, x, P x (u x)).

Lemma fin_all_exists2 U (P Q : x : T, U xProp) :
    ( x, exists2 u, P x u & Q x u) →
  (exists2 u, x, P x (u x) & x, Q x (u x)).

End EnumRank.

Implicit Arguments enum_val_inj [[T] [A] x1 x2].
Implicit Arguments enum_rank_inj [[T] x1 x2].

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.-1Type :=
  | 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 mi - m < n.

Definition split m n (i : 'I_(m + n)) : 'I_m + 'I_n :=
  match ltnP (i) m with
  | LtnNotGeq lt_i_minl _ (Ordinal lt_i_m)
  | GeqNotLtn ge_i_minr _ (Ordinal (split_subproof ge_i_m))
  end.

CoInductive split_spec m n (i : 'I_(m + n)) : 'I_m + 'I_nboolType :=
  | 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 jlshift n j | inr krshift 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.
Local Notation n := n'.+1.

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 < ninord 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.

Implicit Arguments ord0 [[n']].
Implicit Arguments ord_max [[n']].
Implicit Arguments inord [[n']].
Implicit Arguments sub_ord [[n']].

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_ : IfinType).

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.