Library fintype

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
The Finite Structure describes Types with finitely many elements, by   
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 redundancy is needed for the consistency of the         
Canonical structure inference. Also, while finiteness could be stated  
more simply by giving a bound on the range of the pickle function      
provided by the Countable structure, this would yield a useless        
computational interpretation due to the wasteful encoding into Peano   
integers.                                                              
We define operations on Finite Type expecting an applicative predicate 
as argument:                                                           
  - enum to enumerate the elements filtered by pred                    
  - pick, returning the first filtered element; we also give Notations 
  to supply the pred coercion as in [pick x | P]                       
  - boolean quantifiers for finType: forallb x, F  and existsb x, F    
We also define operations card, disjoint, subset and proper expecting  
a mem_pred and  used through notations that supply the mem coercion.   
We provide a serie of lemmas for all these operations on finType       
We define operations on functions on finTypes: the Boolean injectivity,
image (image f of A), inverse function.                                
Finally we define some standard finTypes the ordinals and the product  
and the sum of two finTypes.                                           
  The Ordinal finType I_n : {0, ... , n-1} is provided with a coercion 
nat_of_ord to  natural numbers, and                                    
  -  the lift/unlift operations to avoid a messy dependent type;       
     unlift is a partial operation (returns an option).                
  -  shifting and splitting indices, for cutting and pasting arrays    

Import Prenex Implicits.

Module Finite.

Definition axiom T e := forall x, count (@pred1 T x) e = 1.

Record mixin_of (T : eqType) : Type :=
  Mixin {mixin_enum : seq T; _ : axiom mixin_enum}.

Lemma uniq_enumP : forall T e, @uniq T e -> e =i T -> axiom e.

Definition UniqMixin T e Ue eT := Mixin (@uniq_enumP T e Ue eT).

Section CountAxiom.

Variables (T : countType) (n : nat).
Hypothesis ubT : forall x : T, pickle x < n.

Definition count_enum := pmap (@pickle_inv T) (iota 0 n).

Lemma count_enumP : axiom count_enum.

Definition CountMixin := Mixin count_enumP.

End CountAxiom.

Record class_of (T : Type) : Type := Class {
  base :> Countable.class_of T;
  mixin :> mixin_of (Equality.Pack base T)
}.

Structure type : Type := Pack {sort :> Type; _ : class_of sort; _ : Type}.
Definition class cT := let: Pack _ c _ := cT return class_of cT in c.
Definition unpack K (k : forall T (c : class_of T), K T c) cT :=
  let: Pack T c _ := cT return K _ (class cT) in k _ c.
Definition repack cT : _ -> Type -> type := let k T c p := p c in unpack k cT.

Definition pack := let k T c m := Pack (@Class T c m) T in Countable.unpack k.

Module Type EnumSig.
Parameter enum : forall 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.

Definition eqType cT := Equality.Pack (class cT) cT.
Definition choiceType cT := Choice.Pack (class cT) cT.
Coercion countType cT := Countable.Pack (class cT) cT.

End Finite.

Notation finType := Finite.type.
Notation FinType := Finite.pack.
Notation FinMixin := Finite.Mixin.
Notation UniqFinMixin := Finite.UniqMixin.
Notation "[ 'finType' 'of' T 'for' cT ]" :=
    (@Finite.repack cT (@Finite.Pack T) T)
  (at level 0, format "[ 'finType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'finType' 'of' T ]" :=
    (Finite.repack (fun c => @Finite.Pack T c) T)
  (at level 0, format "[ 'finType' 'of' T ]") : form_scope.
Canonical Structure Finite.eqType.
Canonical Structure Finite.choiceType.
Canonical Structure Finite.countType.

Canonical Structure finEnum_unlock := Unlockable Finite.EnumDef.enumDef.

Definition enum T P := filter P (Finite.enum T).
Definition pick T P := ohead (@enum T P).
Notation "[ 'pick' x | P ]" := (pick [pred x | P])
  (at level 0, x ident, format "[ 'pick' x | P ]") : form_scope.
Notation "[ 'pick' x : T | P ]" := (pick [pred x : T | P])
  (at level 0, x ident, only parsing) : form_scope.
Notation "[ 'pick' x \in A ]" := (pick [pred x | x \in A])
  (at level 0, x ident, format "[ 'pick' x \in A ]") : form_scope.
Notation "[ 'pick' x \in A | P ]" := (pick [pred x | (x \in A) && P])
  (at level 0, x ident, format "[ 'pick' x \in A | P ]") : form_scope.

mitigate divergence in the Coq term comparison algorithm.     

Notation Local card_type := (forall T : finType, mem_pred T -> nat).
Notation Local card_def := (fun T A => size (enum A)).
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.
Export CardDef.
Should become Include in 8.2. 
Canonical Structure 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.
Notation "'forallb' x , F" := (pred0b (fun x => ~~ F))
  (at level 200, x at level 99,
   format "'[hv' 'forallb' x , '/ ' F ']'") : bool_scope.
Notation "'forallb' x : T , F" := (pred0b (fun x : T => ~~ F))
  (at level 200, x at level 99, only parsing) : bool_scope.
Notation "'existsb' x , F" := (~~ pred0b (fun x => F%B))
  (at level 200, x at level 99,
   format "'[hv' 'existsb' x , '/ ' F ']'") : bool_scope.
Notation "'existsb' x : T , F" := (~~ pred0b (fun x : T => F%B))
  (at level 200, x at level 99, only parsing) : bool_scope.

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 := (forall (T : finType) (A B : mem_pred T), bool).
Notation Local subset_def := (fun T A B => pred0b (predD A B)).
Module Type SubsetDefSig.
Parameter subset : subset_type. Axiom subsetEdef : subset = subset_def.
End SubsetDefSig.
Module SubsetDef : SubsetDefSig.
Definition subset : subset_type := subset_def.
Definition subsetEdef := erefl subset.
End SubsetDef.
Export SubsetDef.
Should become Include in 8.2. 
Canonical Structure 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 : forall A, enum A =i A.

Lemma enum_uniq : uniq (enum P).

Lemma enum0 : @enum T pred0 = [::]. Qed.

Lemma enum1 : forall x, enum (pred1 x) = [:: x].

CoInductive pick_spec : option T -> Type :=
  | Pick x of P x : pick_spec (Some x)
  | Nopick of P =1 xpred0 : pick_spec None.

Lemma pickP : pick_spec (pick P).

End EnumPick.

Lemma eq_enum : forall P Q, P =1 Q -> enum P = enum Q.

Lemma eq_pick : forall P Q, P =1 Q -> pick P = pick Q.

Lemma cardE : forall A, #|A| = size (enum (mem A)).

Lemma eq_card : forall A B, A =i B -> #|A| = #|B|.

Lemma eq_card_trans : forall A B n, #|A| = n -> B =i A -> #|B| = n.

Lemma card0 : #|@pred0 T| = 0. Qed.

Lemma cardT : #|T| = size (enum T). Qed.

Lemma card1 : forall x, #|pred1 x| = 1.

Lemma eq_card0 : forall A, A =i pred0 -> #|A| = 0.

Lemma eq_cardT : forall A, A =i predT -> #|A| = size (enum T).

Lemma eq_card1 : forall x A, A =i pred1 x -> #|A| = 1.

Lemma cardUI : forall A B,
  #|[predU A & B]| + #|[predI A & B]| = #|A| + #|B|.

Lemma cardID : forall B A, #|[predI A & B]| + #|[predD A & B]| = #|A|.

Lemma cardC : forall A, #|A| + #|[predC A]| = #|T|.

Lemma cardU1 : forall x A, #|[predU1 x & A]| = (x \notin A) + #|A|.

Lemma card2 : forall x y, #|pred2 x y| = (x != y).+1.

Lemma cardC1 : forall x, #|predC1 x| = #|T|.-1.

Lemma cardD1 : forall x A, #|A| = (x \in A) + #|[predD1 A & x]|.

Lemma max_card : forall A, #|A| <= #|T|.

Lemma card_size : forall s, #|s| <= size s.

Lemma card_uniqP : forall s, reflect (#|s| = size s) (uniq s).

Lemma card0_eq : forall A, #|A| = 0 -> A =i pred0.

Lemma pred0P : forall P, reflect (P =1 pred0) (pred0b P).

Lemma pred0Pn : forall P, reflect (exists x, P x) (~~ pred0b P).

Lemma subsetE : forall A B, (A \subset B) = pred0b [predD A & B].

Lemma subsetP : forall A B, reflect {subset A <= B} (A \subset B).

Lemma subsetPn : forall A B,
  reflect (exists2 x, x \in A & x \notin B) (~~ (A \subset B)).

Lemma subset_leq_card : forall A B, A \subset B -> #|A| <= #|B|.

Lemma subxx_hint : forall mA : mem_pred T, subset mA mA.
Hint Resolve subxx_hint.

The parametrization by predType makes it easier to apply subxx. 
Lemma subxx : forall (pT : predType T) (pA : pT), pA \subset pA.

Lemma eq_subset : forall A1 A2, A1 =i A2 -> subset (mem A1) =1 subset (mem A2).

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

Lemma eq_subxx : forall A B, A =i B -> A \subset B.

Lemma subset_predT : forall A, A \subset T.

Lemma predT_subset : forall A, T \subset A -> forall x, x \in A.

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

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

Lemma subset_cardP : forall A B,
  #|A| = #|B| -> reflect (A =i B) (A \subset B).

Lemma subset_leqif_card : forall A B,
  A \subset B -> #|A| <= #|B| ?= iff (B \subset A).

Lemma subset_trans : forall A B C,
  A \subset B -> B \subset C -> A \subset C.

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

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

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

Lemma proper_sub : forall A B, A \proper B -> A \subset B.

Lemma proper_subn : forall A B, A \proper B -> ~~ (B \subset A).

Lemma proper_trans : forall A B C,
  A \proper B -> B \proper C -> A \proper C.

Lemma proper_sub_trans : forall A B C,
  A \proper B -> B \subset C -> A \proper C.

Lemma sub_proper_trans : forall A B C,
  A \subset B -> B \proper C -> A \proper C.

Lemma proper_card : forall A B, A \proper B -> #|A| < #|B|.

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

Lemma eq_proper : forall A B,
  A =i B -> proper (mem A) =1 proper (mem B).

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

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

Lemma eq_disjoint : forall A1 A2, A1 =i A2 ->
  disjoint (mem A1) =1 disjoint (mem A2).

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

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

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

Lemma disjoint_trans : forall A B C,
  A \subset B -> [disjoint B & C] -> [disjoint A & C].

Lemma disjoint0 : forall A, [disjoint pred0 & A].

Lemma eq_disjoint0 : forall A B, A =i pred0 -> [disjoint A & B].

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

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

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

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

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

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

Lemma disjoint_cat : forall 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].

                                                                   
 Boolean quantifiers for finType                                   
                                                                   

Section Quantifiers.

Variable T : finType.
Implicit Type P : pred T.

Lemma forallP : forall P, reflect (forall x, P x) (forallb x, P x).

Lemma existsP : forall P, reflect (exists x, P x) (existsb x, P x).

Lemma eq_forallb : forall P1 P2,
   P1 =1 P2 -> (forallb x, P1 x) = (forallb x, P2 x).

Lemma eq_existsb : forall P1 P2,
  P1 =1 P2 -> (existsb x, P1 x) = (existsb x, P2 x).

Lemma negb_forall : forall P, ~~ (forallb x, P x) = (existsb x, ~~ P x).

Lemma negb_exists : forall P, ~~ (existsb x, P x) = (forallb x, ~~ P x).

End Quantifiers.

Implicit Arguments forallP [T P].
Implicit Arguments existsP [T P].

                                                                   
 Boolean injective for finType                                     
                                                                   

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 : forall D,
  reflect (exists2 x, x \in D & exists2 y, y \in [predD1 D & x] & f x = f y)
          (~~ dinjectiveb D).

Lemma dinjectiveP : forall D, reflect {in D &, injective f} (dinjectiveb D).

Lemma injectivePn :
  reflect (exists x, exists2 y, x != y & f x = f y) (~~ injectiveb).

Lemma injectiveP : reflect (injective f) injectiveb.

End Injectiveb.

Section Image.

Variables (T : finType) (T' : eqType) (f : T -> T').

Section Def.

Variable A : pred T.

Definition image : pred T' := mem (map f (enum A)).

Lemma imageP : forall y, reflect (exists2 x, A x & y = f x) (image y).

Remark iinv_proof : forall y, image y -> {x : T | A x & f x = y}.

Definition iinv y fAy := s2val (@iinv_proof y fAy).

Lemma f_iinv : forall y fAy, f (@iinv y fAy) = y.

Lemma mem_iinv : forall y fAy, A (@iinv y fAy).

Lemma in_iinv_f : {in A &, injective f} ->
  forall x fAfx, A x -> @iinv (f x) fAfx = x.

Lemma preim_iinv : forall B y fAy, preim f B (@iinv y fAy) = B y.

Lemma mem_image : forall x, A x -> image (f x).

Hypothesis injf : injective f.

Lemma image_f : forall x, image (f x) = A x.

Lemma pre_image : preim f image =1 A.

End Def.

Definition codom := image T.

Lemma codom_f : forall x, codom (f x).

Lemma iinv_f : forall x fTfx, injective f -> @iinv T (f x) fTfx = x.

Lemma image_codom : forall A y, image A y -> codom y.

Lemma image_iinv : injective f ->
 forall A y (fTy : codom y), image A y = A (iinv fTy).

Lemma image_pred0 : image pred0 =1 pred0.

Lemma image_pre : forall B, injective f -> image (preim f B) =1 predI B codom.

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 : forall s : seq T',
  {subset s <= codom} -> map f (preim_seq s) = s.

End Image.


Notation "[ 'image' f 'of' A ]" := (image f [mem A])
  (at level 0, format "[ 'image' f 'of' A ]") : form_scope.

Section CardFunImage.

Variables (T T' : finType) (f : T -> T').
Implicit Type A : pred T.

Lemma leq_image_card : forall A, #|[image f of A]| <= #|A|.

Lemma card_in_image : forall A,
  {in A &, injective f} -> #|[image f of A]| = #|A|.

Hypothesis injf : injective f.

Lemma card_image : forall A, #|[image f of A]| = #|A|.

Lemma card_codom : #|codom f| = #|T|.

Lemma card_preim : forall B, #|preim f B| = #|predI (codom f) B|.

End CardFunImage.

Section FinCancel.

Variables (T : finType) (f g : T -> T).

Section Inv.

Hypothesis injf : injective f.

Lemma injF_codom : forall y, codom f y.

Definition invF y := iinv (injF_codom y).
Lemma invF_f : cancel f invF. Qed.

Lemma f_invF : cancel invF f. Qed.

Lemma injF_bij : bijective f. Qed.

End Inv.

Hypothesis fK : cancel f g.

Lemma canF_sym : cancel g f.

Lemma canF_LR : forall x y, x = g y -> f x = y.

Lemma canF_RL : forall x y, g x = y -> x = f y.

Lemma canF_eq : forall 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' : eqType).

Lemma eq_image : forall (A B : pred T) (f g : T -> T'),
  A =1 B -> f =1 g -> image f A =1 image g B.

Lemma eq_codom : forall f g : T -> T', f =1 g -> codom f =1 codom g.

Lemma eq_invF : forall 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 : ssval \in s }.

Canonical Structure seq_sub_subType :=
  Eval hnf in [subType for ssval by seq_sub_rect].
Definition seq_sub_eqMixin := Eval hnf in [eqMixin of seq_sub by <:].
Canonical Structure seq_sub_eqType := Eval hnf in EqType seq_sub_eqMixin.
Definition seq_sub_choiceMixin := [choiceMixin of seq_sub by <:].
Canonical Structure seq_sub_choiceType :=
  Eval hnf in ChoiceType seq_sub_choiceMixin.

Definition seq_sub_enum : seq seq_sub := undup (pmap insub s).

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

End SeqFinType.

Lemma unit_enumP : Finite.axiom [::tt]. Qed.

Definition unit_finMixin := FinMixin unit_enumP.
Canonical Structure unit_finType := Eval hnf in FinType unit_finMixin.
Lemma card_unit : #|{: unit}| = 1. Qed.

Lemma bool_enumP : Finite.axiom [:: true; false]. Qed.

Definition bool_finMixin := FinMixin bool_enumP.
Canonical Structure bool_finType := Eval hnf in FinType bool_finMixin.
Lemma card_bool : #|{: bool}| = 2. Qed.

Section OptionFinType.

Variable T : finType.

Definition option_enum := None :: map some (Finite.enum T).

Lemma option_enumP : Finite.axiom option_enum.

Definition option_finMixin := FinMixin option_enumP.
Canonical Structure option_finType := Eval hnf in FinType option_finMixin.

Lemma card_option : #|{: option T}| = #|T|.+1.

End OptionFinType.

Section TransferFinType.

Variables (eT : countType) (fT : finType) (f : eT -> fT).

Lemma pcan_enumP : forall g,
  pcancel f g -> Finite.axiom (undup (pmap g (Finite.enum 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 : Type := SubFinType {
  subFin_sort :> subCountType P;
  _ : @mixin_of subFin_sort
}.

Coercion subFinType_finType sT :=
  Eval hnf in pack (let: SubFinType _ m := sT return mixin_of sT in m).
Canonical Structure subFinType_finType.

Definition subFinType_for scT :=
  let k T c of phant T :=
    let: Class _ m := c return _ = Equality.Pack c T -> _ in fun eq_eT =>
    eq_rect _ (fun eT => mixin_of eT -> _) (@SubFinType scT) _ eq_eT m
  in unpack k.

End SubFinType.

This assumes that T has both finType and subCountType structures. 
Notation "[ 'subFinType' 'of' T ]" := (subFinType_for (Phant T) (erefl _))
  (at level 0, format "[ 'subFinType' 'of' T ]") : form_scope.

Canonical Structure 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 (Finite.enum T).

Lemma mem_sub_enum : forall 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.
Let sfT := FinType SubFinMixin.

Lemma card_sub : #|sfT| = #|[pred x | P x]|.

Lemma eq_card_sub : forall 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 Structure myb_sub := Eval hnf in [subType for myv by myb_rect].
Definition myb_eqm := Eval hnf in [eqMixin of myb by <:].
Canonical Structure myb_eq := Eval hnf in EqType myb_eqm.
Definition myb_chm := [choiceMixin of myb by <:].
Canonical Structure myb_ch := Eval hnf in ChoiceType myb_chm.
Definition myb_cntm := [countMixin of myb by <:].
Canonical Structure myb_cnt := Eval hnf in CountType myb_cntm.
Canonical Structure myb_scnt := Eval hnf in [subCountType of myb].
Definition myb_finm := [finMixin of myb by <:].
Canonical Structure myb_fin := Eval hnf in FinType myb_finm.
Canonical Structure 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 Structure sig_finType := Eval hnf in FinType sig_finMixin.
Canonical Structure 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 Structure ordinal_subType :=
  [subType for nat_of_ord by ordinal_rect].
Definition ordinal_eqMixin := Eval hnf in [eqMixin of ordinal by <:].
Canonical Structure ordinal_eqType := Eval hnf in EqType ordinal_eqMixin.
Definition ordinal_choiceMixin := [choiceMixin of ordinal by <:].
Canonical Structure ordinal_choiceType :=
  Eval hnf in ChoiceType ordinal_choiceMixin.
Definition ordinal_countMixin := [countMixin of ordinal by <:].
Canonical Structure ordinal_countType :=
  Eval hnf in CountType ordinal_countMixin.
Canonical Structure ordinal_subCountType := [subCountType of ordinal].

Lemma ltn_ord : forall i : ordinal, i < n. Qed.

Lemma ord_inj : injective nat_of_ord. Qed.

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 : forall i, i \in ord_enum.

Definition ordinal_finMixin := UniqFinMixin ord_enum_uniq mem_ord_enum.
Canonical Structure ordinal_finType := Eval hnf in FinType ordinal_finMixin.
Canonical Structure 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 : forall i0 m, m < n -> nth i0 (enum 'I_n) m = m :> nat.

Lemma nth_ord_enum : forall i0 i : 'I_n, nth i0 (enum 'I_n) i = i.

Lemma index_enum_ord : forall i : 'I_n, index i (enum 'I_n) = i.

End OrdinalEnum.

Lemma widen_ordP : forall n m (i : 'I_n), n <= m -> i < m.
Definition widen_ord n m le_n_m i := Ordinal (@widen_ordP n m i le_n_m).

Lemma cast_ordP : forall n m (i : 'I_n), n = m -> i < m.
Definition cast_ord n m eq_n_m i := Ordinal (@cast_ordP n m i eq_n_m).

bijection between any finType T and the Ordinal finType of its cardinal 
Section EnumRank.

Variable T : finType.

Lemma enum_rank_subproof : forall x : T, index x (enum T) < #|T|.

Definition enum_rank (x : T) := Ordinal (enum_rank_subproof x).

Lemma enum_default : 'I_(#|T|) -> T.

Definition enum_val i := nth (enum_default i) (enum T) i.

Lemma enum_val_nth : forall x i, enum_val i = nth x (enum T) i.

Lemma nth_enum_rank : forall x, cancel enum_rank (nth x (enum T)).

Lemma enum_rankK : cancel enum_rank enum_val.

Lemma enum_valK : cancel enum_val enum_rank.

Lemma enum_rank_inj : injective enum_rank.

Lemma enum_val_inj : injective enum_val.

Lemma enum_rank_bij : bijective enum_rank.

Lemma enum_val_bij : bijective enum_val.

End EnumRank.

Lemma enum_rank_ord : forall n i, enum_rank i = cast_ord (esym (card_ord n)) i.

Lemma enum_val_ord : forall 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 : forall h, cancel (bump h) (unbump h).

Lemma neq_bump : forall h i, h != bump h i.

Lemma unbumpK : forall h, {in predC1 h, cancel (unbump h) (bump h)}.

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

Lemma lift_subproof : forall 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 : forall n (h : 'I_n) (u : {j : 'I_n| 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 : 'I_n) : 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 : forall n (h i : 'I_n), unlift_spec h i (unlift h i).

Lemma neq_lift : forall n (h : 'I_n) i, h != lift h i.

Lemma unlift_none : forall n (h : 'I_n), unlift h h = None.

Lemma unlift_some : forall n (h i : 'I_n),
  h != i -> {j | i = lift h j & unlift h i = Some j}.

Lemma lift_inj : forall n (h : 'I_n), injective (lift h).

Lemma liftK : forall n (h : 'I_n), pcancel (lift h) (unlift h).

Shifting and splitting indices, for cutting and pasting arrays 

Lemma lshift_subproof : forall m n (i : 'I_m), i < m + n.

Lemma rshift_subproof : forall 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 : forall m n (i : 'I_(m + n)), i >= m -> i - m < n.

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

CoInductive split_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n -> bool -> Type :=
  | SplitLo (j : 'I_m) of i = j :> nat : split_spec i (inl _ j) true
  | SplitHi (k : 'I_n) of i = m + k :> nat : split_spec i (inr _ k) false.

Lemma splitP : forall 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 : forall m n (jk : 'I_m + 'I_n), (unsplit jk < m) = jk.

Lemma splitK : forall m n, cancel (@split m n) (@unsplit m n).

Lemma unsplitK : forall m n, cancel (@unsplit m n) (@split m n).

Section OrdinalPos.

Variable n : pos_nat.

Definition ord0 := Ordinal (pos_natP n).

Lemma ord_maxP : n.-1 < n. Qed.

Definition ord_max := Ordinal ord_maxP.

Lemma leq_ord : forall i : 'I_n, i <= n.-1.

Lemma ord_subP : forall m, n.-1 - m < n.
Definition ord_sub m := Ordinal (ord_subP m).

Definition ord_opp (i : 'I_n) := ord_sub i.

Lemma sub_ordK : forall i : 'I_n, n.-1 - (n.-1 - i) = i.

Lemma ord_oppK : involutive ord_opp.

Definition inord m : 'I_n := insubd ord0 m.

Lemma inordK : forall m, m < n -> inord m = m :> nat.

Lemma inord_val : forall i : 'I_n, inord i = i.

Lemma enum_ordS : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_(n.-1)).

End OrdinalPos.

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


Product of two fintypes which is a fintype 
Section ProdFinType.

Variable T1 T2 : finType.

Definition prod_enum :=
  foldr (fun x1 => cat (map (pair x1) (enum T2))) [::] (enum T1).

Lemma predX_prod_enum : forall (A1 : pred T1) (A2 : pred T2),
  count [predX A1 & A2] prod_enum = #|A1| * #|A2|.

Lemma prod_enumP : Finite.axiom prod_enum.

Definition prod_finMixin := FinMixin prod_enumP.
Canonical Structure prod_finType := Eval hnf in FinType prod_finMixin.

Lemma cardX : forall (A1 : pred T1) (A2 : pred T2),
  #|[predX A1 & A2]| = #|A1| * #|A2|.

Lemma card_prod : #|{: T1 * T2}| = #|T1| * #|T2|.

Lemma eq_card_prod : forall A : pred (T1 * T2),
   A =i predT -> #|A| = #|T1| * #|T2|.

End ProdFinType.

Section TagFinType.

Variables (I : finType) (T_ : I -> finType).

Definition tag_enum :=
  let tagged_enum i := map (Tagged T_) (Finite.enum (T_ i)) in
  flatten (map tagged_enum (Finite.enum I)).

Lemma tag_enumP : Finite.axiom tag_enum.

Definition tag_finMixin := FinMixin tag_enumP.
Canonical Structure tag_finType := Eval hnf in FinType 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 :=
  map (@inl _ _) (Finite.enum T1) ++ map (@inr _ _) (Finite.enum T2).

Lemma sum_enum_uniq : uniq sum_enum.

Lemma mem_sum_enum : forall u, u \in sum_enum.

Definition sum_finMixin := UniqFinMixin sum_enum_uniq mem_sum_enum.
Canonical Structure sum_finType := Eval hnf in FinType sum_finMixin.

Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|.

End SumFinType.