Library mathcomp.ssreflect.fintype

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

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import path div.

Finite types NB: See CONTRIBUTING.md for an introduction to HB concepts and commands. This file defines an interface for finite types: finType == type with finitely many inhabitants The HB class is called Finite. subFinType P == join of finType and subType P The HB class is called SubFinite. 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. 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) ordS n i == the successor of i : 'I_n along the cyclic structure of 'I_n, reduces in nat to i.+1 %% n ord_pred n i == the predecessor of i : 'I_n along the cyclic structure of 'I_n, reduces in nat to (i + n).-1 %% n 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 boolean 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 We define the following interfaces and structures: Finite.axiom e <-> every x : T occurs exactly once in e : seq T. [Finite 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, void, option, prod, sum, sig and sigT. We also define a generic type constructor for finite subtypes based on an explicit enumeration: seq_sub s == the subType of all x \in s, where s : seq T for some eqType T; seq_sub s has a canonical finType instance 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

Set Implicit Arguments.

Declare Scope fin_quant_scope.

Definition finite_axiom (T : eqType) e :=
   x : T, count_mem x e = 1.

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.
As with Countable, the interface explicitly includes the somewhat redundant Equality, Choice and Countable superclasses to ensure the forgetful inheritance criterion is met.

Module Export FiniteNES.
Module Finite.


Notation axiom := finite_axiom.
#[deprecated(since="mathcomp 2.0.0", note="Use isFinite.Build instead.")]
Notation EnumMixin m := (@isFinite.Build _ _ m).

Lemma uniq_enumP (T : eqType) e : uniq e e =i T axiom e.

Section WithCountType.
Variable (T : countType).

Definition UniqMixin_deprecated e Ue (eT : e =i T) :=
  @isFinite.Build T 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_deprecated := @isFinite.Build _ _ count_enumP.

End WithCountType.
#[deprecated(since="mathcomp 2.0.0",
  note="Use isFinite.Build and Finite.uniq_enumP instead.")]
Notation UniqMixin := UniqMixin_deprecated.
#[deprecated(since="mathcomp 2.0.0",
  note="Use isFinite.Build and Finite.count_enumP instead.")]
Notation CountMixin := CountMixin_deprecated.
End Finite.
Canonical finEnum_unlock := Unlockable Finite.enum.unlock.
End FiniteNES.

Section CanonicalFinType.
Variable (T : eqType) (s : seq T).

Definition fin_type of finite_axiom s : Type := T.

Variable (f : finite_axiom s).
Notation fT := (fin_type f).

Definition fin_pickle (x : fT) : nat := index x s.
Definition fin_unpickle (n : nat) : option fT :=
  nth None (map some s) n.
Lemma fin_pickleK : pcancel fin_pickle fin_unpickle.


End CanonicalFinType.

#[deprecated(since="mathcomp 2.0.0", note="Use isFinite.Build instead.")]
Notation FinMixin x := (@isFinite.Build _ _ x).
#[deprecated(since="mathcomp 2.0.0",
  note="Use isFinite.Build with Finite.uniq_enumP instead.")]
Notation UniqFinMixin := Finite.UniqMixin_deprecated.
#[deprecated(since="mathcomp 2.0.0", note="Use Finite.clone instead.")]
Notation "[ 'finType' 'of' T 'for' cT ]" := (Finite.clone T%type cT)
  (at level 0, format "[ 'finType' 'of' T 'for' cT ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use Finite.clone instead.")]
Notation "[ 'finType' 'of' T ]" := (Finite.clone T%type _)
  (at level 0, format "[ 'finType' 'of' T ]") : form_scope.

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 name, format "[ 'pick' x | P ]") : form_scope.
Notation "[ 'pick' x : T | P ]" := (pick (fun x : TP%B))
  (at level 0, x name, only parsing) : form_scope.
Definition pick_true T (x : T) := true.
Reserved Notation "[ 'pick' x : T ]"
  (at level 0, x name, format "[ 'pick' x : T ]").
Notation "[ 'pick' x : T ]" := [pick x : T | pick_true x]
  (only parsing) : form_scope.
Notation "[ 'pick' x : T ]" := [pick x : T | pick_true _]
  (only printing) : form_scope.
Notation "[ 'pick' x ]" := [pick x : _]
  (at level 0, x name, only parsing) : form_scope.
Notation "[ 'pick' x | P & Q ]" := [pick x | P && Q ]
  (at level 0, x name,
   format "[ '[hv ' 'pick' x | P '/ ' & Q ] ']'") : form_scope.
Notation "[ 'pick' x : T | P & Q ]" := [pick x : T | P && Q ]
  (at level 0, x name, only parsing) : form_scope.
Notation "[ 'pick' x 'in' A ]" := [pick x | x \in A]
  (at level 0, x name, format "[ 'pick' x 'in' A ]") : form_scope.
Notation "[ 'pick' x : T 'in' A ]" := [pick x : T | x \in A]
  (at level 0, x name, only parsing) : form_scope.
Notation "[ 'pick' x 'in' A | P ]" := [pick x | x \in A & P ]
  (at level 0, x name,
   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 name, only parsing) : form_scope.
Notation "[ 'pick' x 'in' A | P & Q ]" := [pick x in A | P && Q]
  (at level 0, x name, 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 name, only parsing) : form_scope.

We lock the definitions of card and subset to mitigate divergence of the Coq term comparison algorithm.
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. *)
Bind Scope fin_quant_scope with quantified.

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 name).
Notation "[ x : T | B ]" := (quant0b (fun x : TB x)) (at level 0, x name).

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.

Canonical subset_unlock := Unlockable subset.unlock.

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 D : {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 fintype0 : T #|T| 0.

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 card_le1P {A} : reflect {in A, x, A =i pred1 x} (#|A| 1).

Lemma mem_card1 A : #|A| = 1 {x | A =i pred1 x}.

Lemma card1P A : reflect ( x, A =i pred1 x) (#|A| == 1).

Lemma card_le1_eqP A :
  reflect {in A &, x, all_equal_to x} (#|A| 1).

Lemma fintype_le1P : reflect ( x : T, all_equal_to x) (#|T| 1).

Lemma fintype1 : #|T| = 1 {x : T | all_equal_to x}.

Lemma fintype1P : reflect ( x, all_equal_to x) (#|T| == 1).

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.
Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA.

Lemma eq_subset A B : A =i B subset (mem A) =1 subset (mem B).

Lemma eq_subset_r A B :
   A =i B (@subset T)^~ (mem A) =1 (@subset T)^~ (mem B).

Lemma eq_subxx A B : A =i B A \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 B B \subset C A \subset C.

Lemma subset_all s A : (s \subset A) = all [in A] s.

Lemma subset_cons s x : s \subset x :: s.

Lemma subset_cons2 s1 s2 x : s1 \subset s2 x :: s1 \subset x :: s2.

Lemma subset_catl s s' : s \subset s ++ s'.

Lemma subset_catr s s' : s \subset s' ++ s.

Lemma subset_cat2 s1 s2 s3 : s1 \subset s2 s3 ++ s1 \subset s3 ++ s2.

Lemma filter_subset p s : [seq a <- s | p a] \subset s.

Lemma subset_filter p s1 s2 :
  s1 \subset s2 [seq a <- s1 | p a] \subset [seq a <- s2 | p a].

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 B A \subset B.

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

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

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

Lemma sub_proper_trans A B C : A \subset B B \proper C A \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 B proper (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 card_geqP {A n} :
  reflect ( s, [/\ uniq s, size s = n & {subset s A}]) (n #|A|).

Lemma card_gt1P A :
  reflect ( x y, [/\ x \in A, y \in A & x != y]) (1 < #|A|).

Lemma card_gt2P A :
  reflect ( x y z,
              [/\ x \in A, y \in A & z \in A] [/\ x != y, y != z & z != x])
          (2 < #|A|).

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

Lemma eq_disjoint A B : A =i B disjoint (mem A) =1 disjoint (mem B).

Lemma eq_disjoint_r A B : A =i B
  (@disjoint T)^~ (mem A) =1 (@disjoint T)^~ (mem B).

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 disjointFr A B x : [disjoint A & B] x \in A x \in B = false.

Lemma disjointFl A B x : [disjoint A & B] x \in B x \in A = false.

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

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

Lemma disjointW A B C D :
  A \subset B C \subset D [disjoint B & D] [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 [in A] s.

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

End OpsTheory.

Lemma map_subset {T T' : finType} (s1 s2 : seq T) (f : T T') :
  s1 \subset s2 [seq f x | x <- s1 ] \subset [seq f x | x <- s2].

#[global] Hint Resolve subxx_hint : core.

Arguments pred0P {T P}.
Arguments pred0Pn {T P}.
Arguments card_le1P {T A}.
Arguments card_le1_eqP {T A}.
Arguments card1P {T A}.
Arguments fintype_le1P {T}.
Arguments fintype1P {T}.
Arguments subsetP {T A B}.
Arguments subsetPn {T A B}.
Arguments subset_eqP {T A B}.
Arguments card_uniqP {T s}.
Arguments card_geqP {T A n}.
Arguments card_gt0P {T A}.
Arguments card_gt1P {T A}.
Arguments card_gt2P {T A}.
Arguments properP {T A B}.

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 existsb P (x : T) : 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_inb D P (x : T) : 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].

Lemma existsPn P :
  reflect ( x, ~~ P x) (~~ [ x, P x]).

Lemma forallPn P :
  reflect ( x, ~~ P x) (~~ [ x, P x]).

Lemma exists_inPn D P :
  reflect ( x, x \in D ~~ P x) (~~ [ x in D, P x]).

Lemma forall_inPn D P :
  reflect (exists2 x, x \in D & ~~ P x) (~~ [ x in D, P x]).

End Quantifiers.

Arguments forallP {T P}.
Arguments eqfunP {T rT f1 f2}.
Arguments forall_inP {T D P}.
Arguments eqfun_inP {T rT D f1 f2}.
Arguments existsP {T P}.
Arguments existsb {T P}.
Arguments exists_eqP {T rT f1 f2}.
Arguments exists_inP {T D P}.
Arguments exists_inb {T D P}.
Arguments exists_eq_inP {T rT D f1 f2}.
Arguments existsPn {T P}.
Arguments exists_inPn {T D P}.
Arguments forallPn {T P}.
Arguments forall_inPn {T D P}.

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

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 xF) A)
  (at level 0, F at level 99, x binder,
   format "'[hv' [ 'seq' F '/ ' | x 'in' A ] ']'") : seq_scope.
Notation "[ 'seq' F | x ]" :=
  [seq F | x in pred_of_simpl (@pred_of_argType
    (* kludge for getting the type of x *)
    match _, (fun xI) with
    | T, f
      ⇒ match match f return T True with f'f' end with
         | _T
         end
    end)]
  (at level 0, F at level 99, x binder, 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 name, only printing,
   format "'[hv' [ 'seq' F '/ ' | x : T ] ']'") : seq_scope.
Notation "[ 'seq' F , x ]" := [seq F | x ]
  (at level 0, F at level 99, x binder, 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.

Arguments imageP {T T' f A y}.
Arguments codomP {T T' f y}.

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

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

Lemma leq_card_in A : {in A &, injective f} #|A| #|T'|.

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

Lemma leq_card : #|T| #|T'|.

Hypothesis card_range : #|T| #|T'|.

Let eq_card : #|T| = #|T'|.

Lemma inj_card_onto y : y \in codom f.

Lemma inj_card_bij : bijective f.

End CardFunImage.

Arguments image_injP {T T' f A}.
Arguments leq_card_in [T T'] f.
Arguments leq_card [T T'] f.

Lemma bij_eq_card (T T' : finType) (f : T T') : bijective f #|T| = #|T'|.

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].
Lemma card_unit : #|{: unit}| = 1.

Lemma bool_enumP : Finite.axiom [:: true; false].
Lemma card_bool : #|{: bool}| = 2.

Lemma void_enumP : Finite.axiom (Nil void).
Lemma card_void : #|{: void}| = 0.

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.


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

End OptionFinType.

Section TransferFinTypeFromCount.

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

Lemma pcan_enumP g : pcancel f g Finite.axiom (undup (pmap g (enumF fT))).

Definition PCanIsFinite g fK := @isFinite.Build _ _ (@pcan_enumP g fK).

Definition CanIsFinite g (fK : cancel f g) := PCanIsFinite (can_pcan fK).

End TransferFinTypeFromCount.

#[deprecated(since="mathcomp 2.0.0",
  note="Use pcan_type instead or PCanIsFInite.")]
Notation PcanFinMixin := PCanIsFinite.
#[deprecated(since="mathcomp 2.0.0",
  note="Use can_type instead or CanIsFinite.")]
Notation CanFinMixin := CanIsFinite.

Section TransferFinType.

Variables (eT : Type) (fT : finType) (f : eT fT).



End TransferFinType.

#[short(type="subFinType")]
HB.structure Definition SubFinite (T : Type) (P : pred T) :=
  { sT of Finite sT & isSub T P sT }.

Section SubFinType.

Variables (T : choiceType) (P : pred T).
Import Finite.

Implicit Type sT : subFinType P.

Lemma codom_val sT x : (x \in codom (val : sT T)) = P x.

End SubFinType.

#[deprecated(since="mathcomp 2.0.0", note="Use SubFinite.clone instead.")]
Notation "[ 'subFinType' 'of' T ]" := (SubFinite.clone _ _ T%type _)
  (at level 0, format "[ 'subFinType' 'of' T ]") : form_scope.



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.


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


Notation "[ 'Finite' 'of' T 'by' <: ]" := (Finite.copy T%type (sub_type T%type))
  (at level 0, format "[ 'Finite' 'of' T 'by' <: ]") : form_scope.
#[deprecated(since="mathcomp 2.0.0", note="Use [Finite of _ by <:] instead.")]
Notation "[ 'finMixin' 'of' T 'by' <: ]" := [Finite of T%type by <:]
  (at level 0, format "[ 'finMixin' 'of' T 'by' <: ]") : form_scope.

Section SubCountable_isFiniteTheory.

Variables (T : finType) (P : pred T) (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 SubCountable_isFiniteTheory.

(* (* Regression for the subFinType stack *)
 Record myb : Type := MyB {myv : bool; _ : ~~ myv}. 
 HB.instance Definition myb_sub : isSub bool (fun x => ~~ x) myb := 
    isSub for myv
 HB.instance Definition _ := Finite of myb by <:
 Check subFinType of myb
 Check finType of myb. *)


Section CardSig.

Variables (T : finType) (P : pred T).


Lemma card_sig : #|{: {x | P x}}| = #|[pred x | P x]|.

End CardSig.

Subtype for an explicit enumeration.
Beware: these are not the canonical instances, as they are not consistent with the generic sub_choiceType canonical instance.
Definition adhoc_seq_sub_choiceType : choiceType := pcan_type seq_sub_pickleK.
Definition adhoc_seq_sub_countType := HB.pack_for countType seq_sub
  seq_sub_isCountable (Choice.class adhoc_seq_sub_choiceType).
Definition adhoc_seq_sub_finType := HB.pack_for finType seq_sub
  seq_sub_isFinite seq_sub_isCountable (Choice.class adhoc_seq_sub_choiceType).

End SeqSubType.

Section SeqReplace.
Variables (T : eqType).
Implicit Types (s : seq T).

Lemma seq_sub_default s : size s > 0 seq_sub s.

Lemma seq_subE s (s_gt0 : size s > 0) :
  s = map val (map (insubd (seq_sub_default s_gt0)) s : seq (seq_sub s)).

End SeqReplace.
Notation in_sub_seq s_gt0 := (insubd (seq_sub_default s_gt0)).

Section SeqFinType.

Variables (T : choiceType) (s : seq T).
Local Notation sT := (seq_sub s).


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

End SeqFinType.

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

Definition extremum := odflt i0 (pick (arg_pred ord P F)).

Hypothesis ord_refl : reflexive ord.
Hypothesis ord_trans : transitive ord.
Hypothesis ord_total : total ord.
Hypothesis Pi0 : P i0.

Lemma extremumP : extremum_spec ord P F extremum.

End Extremum.

Section ExtremumIn.

Context {T : eqType} {I : finType} (ord : rel T).
Context (i0 : I) (P : pred I) (F : I T).

Hypothesis ord_refl : {in P, reflexive (relpre F ord)}.
Hypothesis ord_trans : {in P & P & P, transitive (relpre F ord)}.
Hypothesis ord_total : {in P &, total (relpre F ord)}.
Hypothesis Pi0 : P i0.

Lemma extremum_inP : extremum_spec ord P F (extremum ord i0 P F).

End ExtremumIn.

Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" :=
    (extremum ord i0 (fun iP%B) (fun iF))
  (at level 0, ord, i, i0 at level 10,
   format "[ 'arg[' ord ]_( i < i0 | P ) F ]") : nat_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 ]") : nat_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 ]") : nat_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_minnP : extremum_spec leq P F arg_min.

Lemma arg_maxnP : extremum_spec geq P F arg_max.

End ArgMinMax.

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 ]") : nat_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 ]") : nat_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 ]") : nat_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 ]") : nat_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 ]") : nat_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 ]") : nat_scope.

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.


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.


End OrdinalSub.

Notation "''I_' n" := (ordinal n)
  (at level 8, n at level 2, format "''I_' n").

#[global] 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.

Lemma mask_enum_ord m :
  mask m (enum 'I_n) = [seq i <- enum 'I_n | nth false m (val i)].

End OrdinalEnum.

Lemma enum_ord0 : enum 'I_0 = [::].

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

Fact ordS_subproof n (i : 'I_n) : i.+1 %% n < n.
Definition ordS n (i : 'I_n) := Ordinal (ordS_subproof i).

Fact ord_pred_subproof n (i : 'I_n) : (i + n).-1 %% n < n.
Definition ord_pred n (i : 'I_n) := Ordinal (ord_pred_subproof i).

Lemma ordSK n : cancel (@ordS n) (@ord_pred n).

Lemma ord_predK n : cancel (@ord_pred n) (@ordS n).

Lemma ordS_bij n : bijective (@ordS n).

Lemma ordS_inj n : injective (@ordS n).

Lemma ord_pred_bij n : bijective (@ord_pred n).

Lemma ord_pred_inj n : injective (@ord_pred 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).

Lemma inj_leq m n (f : 'I_m 'I_n) : injective f m n.
Arguments inj_leq [m n] f _.

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

Lemma enum_rank_subproof (T : finType) x0 (A : {pred T}) : x0 \in A 0 < #|A|.

Canonical unlockable_enum_rank_in := Unlockable enum_rank_in.unlock.

Section EnumRank.

Variable T : finType.
Implicit Type A : {pred T}.

Definition enum_rank x := @enum_rank_in T 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 T 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 T 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 T 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 eq_enum_rank_in (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) :
  {in A, enum_rank_in Ax0 =1 enum_rank_in Ay0}.

Lemma enum_rank_in_inj (x0 y0 : T) A (Ax0 : x0 \in A) (Ay0 : y0 \in A) :
  {in A &, x y, enum_rank_in Ax0 x = enum_rank_in Ay0 y x = y}.

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.

Arguments enum_val_inj {T A} [i1 i2] : rename.
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 bumpDl 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 unbumpDl 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 eq_liftF n (h : 'I_n) i : (h == lift h i) = false.

Lemma lift_eqF n (h : 'I_n) i : (lift h i == h) = false.

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).
Arguments lift_inj {n h} [i1 i2] eq_i12h : rename.

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 lshift_inj m n : injective (@lshift m n).

Lemma rshift_inj m n : injective (@rshift m n).

Lemma eq_lshift m n i j : (@lshift m n i == @lshift m n j) = (i == j).

Lemma eq_rshift m n i j : (@rshift m n i == @rshift m n j) = (i == j).

Lemma eq_lrshift m n i j : (@lshift m n i == @rshift m n j) = false.

Lemma eq_rlshift m n i j : (@rshift m n i == @lshift m n j) = false.

Definition eq_shift := (eq_lshift, eq_rshift, eq_lrshift, eq_rlshift).

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_minl _ (Ordinal lt_i_m)
  | GeqNotLtn ge_i_minr _ (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).

Variant split_ord_spec m n (i : 'I_(m + n)) : 'I_m + 'I_n bool Type :=
  | SplitOrdLo (j : 'I_m) of i = lshift _ j : split_ord_spec i (inl _ j) true
  | SplitOrdHi (k : 'I_n) of i = rshift _ k : split_ord_spec i (inr _ k) false.

Lemma split_ordP m n (i : 'I_(m + n)) : split_ord_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.

Lemma unsplitK {m n} : cancel (@unsplit m n) split.

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 < n inord m = m :> nat.

Lemma inord_val (i : 'I_n) : inord i = i.

Lemma enum_ordSl : enum 'I_n = ord0 :: map (lift ord0) (enum 'I_n').

Lemma enum_ordSr :
  enum 'I_n = rcons (map (widen_ord (leqnSn _)) (enum 'I_n')) ord_max.

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.

Arguments ord0 {n'}.
Arguments ord_max {n'}.
Arguments inord {n'}.
Arguments sub_ord {n'}.
Arguments sub_ordK {n'}.
Arguments inord_val {n'}.

Lemma ord1 : all_equal_to (ord0 : 'I_1).

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.


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.


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.


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

End SumFinType.