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.

#[short (type ="finType")]
HB.structure Definition Finite := {T of isFinite T & Countable T }.

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.

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

Section WithCountType.
Variable (T : countType) (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.

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

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

Definition fin_pred_sort (T : finType) (pT : predType T) := pred_sort pT.
Identity Coercion pred_sort_of_fin : fin_pred_sort >-> pred_sort.

Definition enum_mem T (mA : mem_pred _) := filter mA (Finite.enum T).
Notation enum A := (enum_mem (mem A)).
Definition pick (T : finType) (P : pred T) := ohead (enum P).

Notation "[ 'pick' x | P ]" := (pick (fun x ⇒ P%B))
  (at level 0, x name, format "[ 'pick' x | P ]") : form_scope.
Notation "[ 'pick' x : T | P ]" := (pick (fun x : T ⇒ P%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.

Canonical card_unlock := Unlockable card.unlock.

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).
#[warning="-notation-incompatible-prefix"]
Notation "F ^~" := (~~ F) (at level 2).

Section Definitions.

Variable T : finType.
Implicit Types (B : quantified) (x y : T).

Definition quant0b Bp := pred0b [pred x : T | let: F^* := Bp x x in F].

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

Definition ex B x y := B.

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

Definition all B x y := let: F^* := B in F^~^*.
Definition all_in C B x y := let: F^* := B in (C ==> F)^~^*.
Definition ex_in C B x y := let: F^* := B in (C && F)^*.

End Definitions.

Notation "[ x | B ]" := (quant0b (fun x ⇒ B x)) (at level 0, x name).
Notation "[ x : T | B ]" := (quant0b (fun x : T ⇒ B 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 x ⇒ F) 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 x ⇒ I) 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 in pred_of_simpl (@pred_of_argType T)]
  (at level 0, F at level 99, x binder, 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.

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.

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.

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.

Section SeqSubType.

Variables (T : eqType) (s : seq T).

Record seq_sub : Type := SeqSub {ssval : T; ssvalP : in_mem ssval (@mem T _ s)}.

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

Lemma mem_seq_sub_enum x : x \in seq_sub_enum.

Lemma val_seq_sub_enum : uniq s → map val seq_sub_enum = s.

Definition seq_sub_pickle x := index x seq_sub_enum.
Definition seq_sub_unpickle n := nth None (map some seq_sub_enum) n.
Lemma seq_sub_pickleK : pcancel seq_sub_pickle seq_sub_unpickle.

Definition seq_sub_isCountable := isCountable.Build seq_sub seq_sub_pickleK.
Fact seq_sub_axiom : Finite.axiom seq_sub_enum.
Definition seq_sub_isFinite := isFinite.Build seq_sub seq_sub_axiom.

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

Definition adhoc_seq_sub_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 i ⇒ P%B) (fun i ⇒ F))
  (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 i ⇒ P%B) (fun i ⇒ F))
  (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 i ⇒ P%B) (fun i ⇒ F))
  (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_m ⇒ inl _ (Ordinal lt_i_m)
  | GeqNotLtn ge_i_m ⇒ inr _ (Ordinal (split_subproof ge_i_m))
  end.

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

Lemma splitP m n (i : 'I_(m + n )) : split_spec i (split i) (i < m).

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 j ⇒ lshift n j | inr k ⇒ rshift m k end.

Lemma ltn_unsplit m n (jk : 'I_m + 'I_n) : (unsplit jk < m ) = jk.

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

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

Section OrdinalPos.

Variable n' : nat.
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.