From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.ssreflect.fintype.html | 1043 ++++++++++++++------------
1 file changed, 552 insertions(+), 491 deletions(-)
(limited to 'docs/htmldoc/mathcomp.ssreflect.fintype.html')
diff --git a/docs/htmldoc/mathcomp.ssreflect.fintype.html b/docs/htmldoc/mathcomp.ssreflect.fintype.html
index caca428..a99038e 100644
--- a/docs/htmldoc/mathcomp.ssreflect.fintype.html
+++ b/docs/htmldoc/mathcomp.ssreflect.fintype.html
@@ -21,7 +21,6 @@
@@ -41,7 +40,7 @@
interfaces, in this file for subFinType, and in the finalg library.
We define the following interfaces and structures:
finType == the packed class type of the Finite interface.
- FinType m == the packed class for the Finite mixin m.
+ FinType T m == the packed finType class for type T and Finite mixin m.
Finite.axiom e <-> every x : T occurs exactly once in e : seq T.
FinMixin ax_e == the Finite mixin for T, encapsulating
ax_e : Finite.axiom e for some e : seq T.
@@ -114,9 +113,9 @@
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.
+ 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
@@ -130,13 +129,13 @@
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
+ dinjectiveb A f <=> the restriction of f : T -> R to A is injective
(this is a bolean predicate, R must be an eqType).
- injectiveb f == f : T -> R is injective (boolean predicate).
- pred0b A == no x : T satisfies x \in A.
- [forall x, P] == P (in which x can appear) is true for all values of x;
+ 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.
+ [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].
@@ -146,8 +145,10 @@
- > 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_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.
@@ -155,19 +156,26 @@
- [pick x in A | P] == Some x, with x \in A s.t. P holds, else None.
+ [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 of i : T minimizing M : nat, subject
+ [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 of i maximizing M subject to P and
+ [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.
+ [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.
@@ -184,10 +192,10 @@
Variable T :
eqType.
-
Definition axiom e :=
∀ x :
T,
count_mem x e = 1.
+
Definition axiom e :=
∀ x :
T,
count_mem x e = 1.
-
Lemma uniq_enumP e :
uniq e → e =i T → axiom e.
+
Lemma uniq_enumP e :
uniq e → e =i T → axiom e.
Record mixin_of :=
Mixin {
@@ -207,21 +215,21 @@
Definition EnumMixin :=
-
let:
Countable.Pack _ (
Countable.Class _ m)
_ as cT :=
T
-
return ∀ e :
seq cT,
axiom e → mixin_of cT in
+
let:
Countable.Pack _ (
Countable.Class _ m)
as cT :=
T
+
return ∀ e :
seq cT,
axiom e → mixin_of cT in
@
Mixin (
EqType _ _)
m.
Definition UniqMixin e Ue eT := @
EnumMixin e (
uniq_enumP Ue eT).
-
Variable n :
nat.
+
Variable n :
nat.
Definition count_enum :=
pmap (@
pickle_inv T) (
iota 0
n).
-
Hypothesis ubT :
∀ x :
T,
pickle x < n.
+
Hypothesis ubT :
∀ x :
T,
pickle x < n.
Lemma count_enumP :
axiom count_enum.
@@ -238,27 +246,27 @@
Record class_of T :=
Class {
base :
Choice.class_of T;
-
mixin :
mixin_of (
Equality.Pack base T)
+
mixin :
mixin_of (
Equality.Pack base)
}.
Definition base2 T c :=
Countable.Class (@
base T c) (
mixin_base (
mixin c)).
-
Structure type :
Type :=
Pack {
sort;
_ :
class_of sort;
_ :
Type}.
+
Structure type :
Type :=
Pack {
sort;
_ :
class_of sort}.
Variables (
T :
Type) (
cT :
type).
-
Definition class :=
let:
Pack _ c _ as cT' :=
cT return class_of cT' in c.
-
Definition clone c of phant_id class c := @
Pack T c T.
-
Let xT :=
let:
Pack T _ _ :=
cT in T.
-
Notation xclass := (
class : class_of xT).
+
Definition class :=
let:
Pack _ c as cT' :=
cT return class_of cT' in c.
+
Definition clone c of phant_id class c := @
Pack T c.
+
Let xT :=
let:
Pack T _ :=
cT in T.
+
Notation xclass := (
class : class_of xT).
Definition pack b0 (
m0 :
mixin_of (
EqType T b0)) :=
-
fun bT b &
phant_id (
Choice.class bT)
b ⇒
-
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m)
T.
+
fun bT b &
phant_id (
Choice.class bT)
b ⇒
+
fun m &
phant_id m0 m ⇒
Pack (@
Class T b m).
-
Definition eqType := @
Equality.Pack cT xclass xT.
-
Definition choiceType := @
Choice.Pack cT xclass xT.
-
Definition countType := @
Countable.Pack cT (
base2 xclass)
xT.
+
Definition eqType := @
Equality.Pack cT xclass.
+
Definition choiceType := @
Choice.Pack cT xclass.
+
Definition countType := @
Countable.Pack cT (
base2 xclass).
End ClassDef.
@@ -277,25 +285,25 @@
Coercion countType : type >-> Countable.type.
Canonical countType.
Notation finType :=
type.
-
Notation FinType T m := (@
pack T _ m _ _ id _ id).
+
Notation FinType T m := (@
pack T _ m _ _ id _ id).
Notation FinMixin :=
EnumMixin.
Notation UniqFinMixin :=
UniqMixin.
-
Notation "[ 'finType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
+
Notation "[ 'finType' 'of' T 'for' cT ]" := (@
clone T cT _ idfun)
(
at level 0,
format "[ 'finType' 'of' T 'for' cT ]") :
form_scope.
-
Notation "[ 'finType' 'of' T ]" := (@
clone T _ _ id)
+
Notation "[ 'finType' 'of' T ]" := (@
clone T _ _ id)
(
at level 0,
format "[ 'finType' 'of' T ]") :
form_scope.
End Exports.
Module Type EnumSig.
Parameter enum :
∀ cT :
type,
seq cT.
-
Axiom enumDef :
enum = fun cT ⇒
mixin_enum (
class cT).
+
Axiom enumDef :
enum = fun cT ⇒
mixin_enum (
class cT).
End EnumSig.
Module EnumDef :
EnumSig.
Definition enum cT :=
mixin_enum (
class cT).
-
Definition enumDef :=
erefl enum.
+
Definition enumDef :=
erefl enum.
End EnumDef.
@@ -306,7 +314,7 @@
Export Finite.Exports.
-
Canonical finEnum_unlock :=
Unlockable Finite.EnumDef.enumDef.
+
Canonical finEnum_unlock :=
Unlockable Finite.EnumDef.enumDef.
-
Definition fin_pred_sort (
T :
finType) (
pT :
predType T) :=
pred_sort pT.
+
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).
+
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))
+
Notation "[ 'pick' x | P ]" := (
pick (
fun x ⇒
P%
B))
(
at level 0,
x ident,
format "[ 'pick' x | P ]") :
form_scope.
-
Notation "[ 'pick' x : T | P ]" := (
pick (
fun x :
T ⇒
P%
B))
+
Notation "[ 'pick' x : T | P ]" := (
pick (
fun x :
T ⇒
P%
B))
(
at level 0,
x ident,
only parsing) :
form_scope.
-
Definition pick_true T (
x :
T) :=
true.
-
Notation "[ 'pick' x : T ]" :=
[pick x : T | pick_true x]
+
Definition pick_true T (
x :
T) :=
true.
+
Notation "[ 'pick' x : T ]" :=
[pick x : T | pick_true x]
(
at level 0,
x ident,
only parsing).
-
Notation "[ 'pick' x ]" :=
[pick x : _]
+
Notation "[ 'pick' x ]" :=
[pick x : _]
(
at level 0,
x ident,
only parsing) :
form_scope.
-
Notation "[ 'pic' 'k' x : T ]" :=
[pick x : T | pick_true _]
+
Notation "[ 'pic' 'k' x : T ]" :=
[pick x : T | pick_true _]
(
at level 0,
x ident,
format "[ 'pic' 'k' x : T ]") :
form_scope.
-
Notation "[ 'pick' x | P & Q ]" :=
[pick x | P && Q ]
+
Notation "[ 'pick' x | P & Q ]" :=
[pick x | P && Q ]
(
at level 0,
x ident,
format "[ '[hv ' 'pick' x | P '/ ' & Q ] ']'") :
form_scope.
-
Notation "[ 'pick' x : T | P & Q ]" :=
[pick x : T | P && Q ]
+
Notation "[ 'pick' x : T | P & Q ]" :=
[pick x : T | P && Q ]
(
at level 0,
x ident,
only parsing) :
form_scope.
-
Notation "[ 'pick' x 'in' A ]" :=
[pick x | x \in A]
+
Notation "[ 'pick' x 'in' A ]" :=
[pick x | x \in A]
(
at level 0,
x ident,
format "[ 'pick' x 'in' A ]") :
form_scope.
-
Notation "[ 'pick' x : T 'in' A ]" :=
[pick x : T | x \in A]
+
Notation "[ 'pick' x : T 'in' A ]" :=
[pick x : T | x \in A]
(
at level 0,
x ident,
only parsing) :
form_scope.
-
Notation "[ 'pick' x 'in' A | P ]" :=
[pick x | x \in A & P ]
+
Notation "[ 'pick' x 'in' A | P ]" :=
[pick x | x \in A & P ]
(
at level 0,
x ident,
format "[ '[hv ' 'pick' x 'in' A '/ ' | P ] ']'") :
form_scope.
-
Notation "[ 'pick' x : T 'in' A | P ]" :=
[pick x : T | x \in A & P ]
+
Notation "[ 'pick' x : T 'in' A | P ]" :=
[pick x : T | x \in A & P ]
(
at level 0,
x ident,
only parsing) :
form_scope.
-
Notation "[ 'pick' x 'in' A | P & Q ]" :=
[pick x in A | P && Q]
+
Notation "[ 'pick' x 'in' A | P & Q ]" :=
[pick x in A | P && Q]
(
at level 0,
x ident,
format
"[ '[hv ' 'pick' x 'in' A '/ ' | P '/ ' & Q ] ']'") :
form_scope.
-
Notation "[ 'pick' x : T 'in' A | P & Q ]" :=
[pick x : T in A | P && Q]
+
Notation "[ 'pick' x : T 'in' A | P & Q ]" :=
[pick x : T in A | P && Q]
(
at level 0,
x ident,
only parsing) :
form_scope.
@@ -368,10 +376,10 @@
Module Type CardDefSig.
-
Parameter card :
card_type.
Axiom cardEdef :
card = card_def.
+
Parameter card :
card_type.
Axiom cardEdef :
card = card_def.
End CardDefSig.
Module CardDef :
CardDefSig.
-
Definition card :
card_type :=
card_def.
Definition cardEdef :=
erefl card.
+
Definition card :
card_type :=
card_def.
Definition cardEdef :=
erefl card.
End CardDef.
-Canonical card_unlock := Unlockable cardEdef.
+Canonical card_unlock := Unlockable cardEdef.
A is at level 99 to allow the notation #|G : H| in groups.
@@ -432,87 +440,87 @@
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)^*.
+
Definition all B x y :=
let:
F^* :=
B in F^~^*.
+
Definition all_in C B x y :=
let:
F^* :=
B in (C ==> F)^~^*.
+
Definition ex_in C B x y :=
let:
F^* :=
B in (C && F)^*.
End Definitions.
-
Notation "[ x | B ]" := (
quant0b (
fun x ⇒
B x)) (
at level 0,
x ident).
-
Notation "[ x : T | B ]" := (
quant0b (
fun x :
T ⇒
B x)) (
at level 0,
x ident).
+
Notation "[ x | B ]" := (
quant0b (
fun x ⇒
B x)) (
at level 0,
x ident).
+
Notation "[ x : T | B ]" := (
quant0b (
fun x :
T ⇒
B x)) (
at level 0,
x ident).
Module Exports.
-
Notation ", F" :=
F^* (
at level 200,
format ", '/ ' F") :
fin_quant_scope.
+
Notation ", F" :=
F^* (
at level 200,
format ", '/ ' F") :
fin_quant_scope.
-
Notation "[ 'forall' x B ]" :=
[x | all B]
+
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]
+
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]
+
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]
+
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]
+
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]
+
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]^*
+
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]^*
+
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]^*
+
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]^*
+
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]^*
+
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]^*
+
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]^~
+
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]^~
+
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]^~
+
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]^~
+
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]^~
+
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]^~
+
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]^~^*
+
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]^~^*
+
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]^~^*
+
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]^~^*
+
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]^~^*
+
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]^~^*
+
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.
@@ -523,26 +531,26 @@
Export FiniteQuant.Exports.
-
Definition disjoint T (
A B :
mem_pred _) := @
pred0b T (
predI A B).
-
Notation "[ 'disjoint' A & B ]" := (
disjoint (
mem A) (
mem B))
+
Definition disjoint T (
A B :
mem_pred _) := @
pred0b T (
predI A B).
+
Notation "[ 'disjoint' A & B ]" := (
disjoint (
mem A) (
mem B))
(
at level 0,
format "'[hv' [ 'disjoint' '/ ' A '/' & B ] ']'") :
bool_scope.
Module Type SubsetDefSig.
-
Parameter subset :
subset_type.
Axiom subsetEdef :
subset = subset_def.
+
Parameter subset :
subset_type.
Axiom subsetEdef :
subset = subset_def.
End SubsetDefSig.
Module Export SubsetDef :
SubsetDefSig.
Definition subset :
subset_type :=
subset_def.
-
Definition subsetEdef :=
erefl subset.
+
Definition subsetEdef :=
erefl subset.
End SubsetDef.
-
Canonical subset_unlock :=
Unlockable subsetEdef.
-
Notation "A \subset B" := (
subset (
mem A) (
mem B))
+
Canonical subset_unlock :=
Unlockable subsetEdef.
+
Notation "A \subset B" := (
subset (
mem A) (
mem B))
(
at level 70,
no associativity) :
bool_scope.
-
Definition proper T A B := @
subset T A B && ~~ subset B A.
-
Notation "A \proper B" := (
proper (
mem A) (
mem B))
+
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.
@@ -560,9 +568,7 @@
Variable T :
finType.
-
Implicit Types A B C P Q :
pred T.
-
Implicit Types x y :
T.
-
Implicit Type s :
seq T.
+
Implicit Types (
A B C :
{pred T}) (
P Q :
pred T) (
x y :
T) (
s :
seq T).
Lemma enumP :
Finite.axiom (
Finite.enum T).
@@ -571,27 +577,27 @@
Section EnumPick.
-
Variable P :
pred T.
+
Variable P :
pred T.
-
Lemma enumT :
enum T = Finite.enum T.
+
Lemma enumT :
enum T = Finite.enum T.
-
Lemma mem_enum A :
enum A =i A.
+
Lemma mem_enum A :
enum A =i A.
-
Lemma enum_uniq :
uniq (
enum P).
+
Lemma enum_uniq A :
uniq (
enum A).
-
Lemma enum0 :
enum pred0 = Nil T.
+
Lemma enum0 :
enum pred0 = Nil T.
-
Lemma enum1 x :
enum (
pred1 x)
= [:: x].
+
Lemma enum1 x :
enum (
pred1 x)
= [:: x].
-
CoInductive pick_spec :
option T → Type :=
- |
Pick x of P x :
pick_spec (
Some x)
- |
Nopick of P =1 xpred0 :
pick_spec None.
+
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).
@@ -600,96 +606,96 @@
End EnumPick.
-
Lemma eq_enum P Q :
P =i Q → enum P = enum Q.
+
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 eq_pick P Q :
P =1 Q → pick P = pick Q.
-
Lemma cardE A :
#|A| = size (
enum A).
+
Lemma cardE A :
#|A| = size (
enum A).
-
Lemma eq_card A B :
A =i B → #|A| = #|B|.
+
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 eq_card_trans A B n :
#|A| = n → B =i A → #|B| = n.
-
Lemma card0 :
#|@
pred0 T| = 0.
+
Lemma card0 :
#|@
pred0 T| = 0.
-
Lemma cardT :
#|T| = size (
enum T).
+
Lemma cardT :
#|T| = size (
enum T).
-
Lemma card1 x :
#|pred1 x| = 1.
+
Lemma card1 x :
#|pred1 x| = 1.
-
Lemma eq_card0 A :
A =i pred0 → #|A| = 0.
+
Lemma eq_card0 A :
A =i pred0 → #|A| = 0.
-
Lemma eq_cardT A :
A =i predT → #|A| = size (
enum T).
+
Lemma eq_cardT A :
A =i predT → #|A| = size (
enum T).
-
Lemma eq_card1 x A :
A =i pred1 x → #|A| = 1.
+
Lemma eq_card1 x A :
A =i pred1 x → #|A| = 1.
-
Lemma cardUI A B :
#|[predU A & B]| + #|[predI A & B]| = #|A| + #|B|.
+
Lemma cardUI A B :
#|[predU A & B]| + #|[predI A & B]| = #|A| + #|B|.
-
Lemma cardID B A :
#|[predI A & B]| + #|[predD A & B]| = #|A|.
+
Lemma cardID B A :
#|[predI A & B]| + #|[predD A & B]| = #|A|.
-
Lemma cardC A :
#|A| + #|[predC A]| = #|T|.
+
Lemma cardC A :
#|A| + #|[predC A]| = #|T|.
-
Lemma cardU1 x A :
#|[predU1 x & A]| = (x \notin A) + #|A|.
+
Lemma cardU1 x A :
#|[predU1 x & A]| = (x \notin A) + #|A|.
-
Lemma card2 x y :
#|pred2 x y| = (x != y).+1.
+
Lemma card2 x y :
#|pred2 x y| = (x != y).+1.
-
Lemma cardC1 x :
#|predC1 x| = #|T|.-1.
+
Lemma cardC1 x :
#|predC1 x| = #|T|.-1.
-
Lemma cardD1 x A :
#|A| = (x \in A) + #|[predD1 A & x]|.
+
Lemma cardD1 x A :
#|A| = (x \in A) + #|[predD1 A & x]|.
-
Lemma max_card A :
#|A| ≤ #|T|.
+
Lemma max_card A :
#|A| ≤ #|T|.
-
Lemma card_size s :
#|s| ≤ size s.
+
Lemma card_size s :
#|s| ≤ size s.
-
Lemma card_uniqP s :
reflect (
#|s| = size s) (
uniq s).
+
Lemma card_uniqP s :
reflect (
#|s| = size s) (
uniq s).
-
Lemma card0_eq A :
#|A| = 0
→ A =i pred0.
+
Lemma card0_eq A :
#|A| = 0
→ A =i pred0.
-
Lemma pred0P P :
reflect (
P =1 pred0) (
pred0b P).
+
Lemma pred0P P :
reflect (
P =1 pred0) (
pred0b P).
-
Lemma pred0Pn P :
reflect (
∃ x, P x) (
~~ pred0b P).
+
Lemma pred0Pn P :
reflect (
∃ x, P x) (
~~ pred0b P).
-
Lemma card_gt0P A :
reflect (
∃ i, i \in A) (
#|A| > 0).
+
Lemma card_gt0P A :
reflect (
∃ i, i \in A) (
#|A| > 0).
-
Lemma subsetE A B :
(A \subset B) = pred0b [predD A & B].
+
Lemma subsetE A B :
(A \subset B) = pred0b [predD A & B].
-
Lemma subsetP A B :
reflect {subset A ≤ B} (
A \subset 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)).
+
reflect (
exists2 x, x \in A & x \notin B) (
~~ (A \subset B)).
-
Lemma subset_leq_card A B :
A \subset B → #|A| ≤ #|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.
+
Lemma subxx_hint (
mA :
mem_pred T) :
subset mA mA.
+
Hint Resolve subxx_hint :
core.
-
Lemma subxx (
pT :
predType T) (
pA :
pT) :
pA \subset pA.
+
Lemma subxx (
pT :
predType T) (
pA :
pT) :
pA \subset pA.
-
Lemma eq_subset A1 A2 :
A1 =i A2 → subset (
mem A1)
=1 subset (
mem A2).
+
Lemma eq_subset A B :
A =i B → subset (
mem A)
=1 subset (
mem B).
-
Lemma eq_subset_r B1 B2 :
B1 =i B2 →
-
(@
subset T)^~ (mem B1) =1 (@
subset T)^~ (mem B2).
+
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 eq_subxx A B :
A =i B → A \subset B.
-
Lemma subset_predT A :
A \subset T.
+
Lemma subset_predT A :
A \subset T.
-
Lemma predT_subset A :
T \subset A → ∀ x,
x \in A.
+
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_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_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_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_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_trans A B C :
A \subset B → B \subset C → A \subset C.
-
Lemma subset_all s A :
(s \subset A) = all (
mem A)
s.
+
Lemma subset_all s A :
(s \subset A) = all (
mem A)
s.
-
Lemma properE A B :
A \proper B = (A \subset B) && ~~(B \subset A).
+
Lemma 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).
+
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_sub A B :
A \proper B → A \subset B.
-
Lemma proper_subn A B :
A \proper B → ~~ (B \subset A).
+
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_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 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 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_card A B :
A \proper B → #|A| < #|B|.
-
Lemma proper_irrefl A :
~~ (A \proper A).
+
Lemma proper_irrefl A :
~~ (A \proper A).
-
Lemma properxx A :
(A \proper A) = false.
+
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 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 eq_proper_r A B :
+
A =i B → (@
proper T)^~ (mem A) =1 (@
proper T)^~ (mem B).
-
Lemma disjoint_sym A B :
[disjoint A & B] = [disjoint B & A].
+
Lemma disjoint_sym A B :
[disjoint A & B] = [disjoint B & A].
-
Lemma eq_disjoint A1 A2 :
A1 =i A2 → disjoint (
mem A1)
=1 disjoint (
mem A2).
+
Lemma eq_disjoint A B :
A =i B → disjoint (
mem A)
=1 disjoint (
mem B).
-
Lemma eq_disjoint_r B1 B2 :
B1 =i B2 →
-
(@
disjoint T)^~ (mem B1) =1 (@
disjoint T)^~ (mem B2).
+
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 subset_disjoint A B :
(A \subset B) = [disjoint A & [predC B]].
-
Lemma disjoint_subset A B :
[disjoint A & B] = (A \subset [predC B]).
+
Lemma disjoint_subset A B :
[disjoint A & B] = (A \subset [predC B]).
Lemma disjoint_trans A B C :
-
A \subset B → [disjoint B & C] → [disjoint A & C].
+
A \subset B → [disjoint B & C] → [disjoint A & C].
-
Lemma disjoint0 A :
[disjoint pred0 & A].
+
Lemma disjoint0 A :
[disjoint pred0 & A].
-
Lemma eq_disjoint0 A B :
A =i pred0 → [disjoint A & B].
+
Lemma eq_disjoint0 A B :
A =i pred0 → [disjoint A & B].
-
Lemma disjoint1 x A :
[disjoint pred1 x & A] = (x \notin A).
+
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).
+
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].
+
[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].
+
[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].
+
[disjoint x :: s & B] = (x \notin B) && [disjoint s & B].
-
Lemma disjoint_has s A :
[disjoint s & A] = ~~ has (
mem A)
s.
+
Lemma disjoint_has s A :
[disjoint s & A] = ~~ has (
mem A)
s.
Lemma disjoint_cat s1 s2 A :
-
[disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A].
+
[disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A].
End OpsTheory.
-
Hint Resolve subxx_hint.
+
Hint Resolve subxx_hint :
core.
@@ -848,161 +854,214 @@
Section QuantifierCombinators.
-
Variables (
T :
finType) (
P :
pred T) (
PP :
T → Prop).
-
Hypothesis viewP :
∀ x,
reflect (
PP x) (
P x).
+
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 existsPP :
reflect (
∃ x, PP x)
[∃ x, P x].
-
Lemma forallPP :
reflect (
∀ x,
PP x)
[∀ x, P x].
+
Lemma forallPP :
reflect (
∀ x,
PP x)
[∀ x, P x].
End QuantifierCombinators.
-
Notation "'exists_ view" := (
existsPP (
fun _ ⇒
view))
+
Notation "'exists_ view" := (
existsPP (
fun _ ⇒
view))
(
at level 4,
right associativity,
format "''exists_' view").
-
Notation "'forall_ view" := (
forallPP (
fun _ ⇒
view))
+
Notation "'forall_ view" := (
forallPP (
fun _ ⇒
view))
(
at level 4,
right associativity,
format "''forall_' view").
Section Quantifiers.
-
Variables (
T :
finType) (
rT :
T → eqType).
-
Implicit Type (
D P :
pred T) (
f :
∀ x,
rT x).
+
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 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 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_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].
+
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 existsP P :
reflect (
∃ x, P x)
[∃ x, P x].
Lemma exists_eqP f1 f2 :
-
reflect (
∃ x, f1 x = f2 x)
[∃ x, f1 x == f2 x].
+
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_inP D P :
reflect (
exists2 x, D x & P x)
[∃ (x | D x), P x].
+
Lemma exists_inPP D P PP :
(∀ x,
reflect (
PP x) (
P x)
) →
+
reflect (
exists2 x, D x & PP x)
[∃ (x | D x), P x].
Lemma exists_eq_inP D f1 f2 :
-
reflect (
exists2 x, D x & f1 x = f2 x)
[∃ (x | D x), f1 x == f2 x].
+
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 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].
+
(∀ 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 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].
+
(∀ 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 P :
~~ [∀ x, P x] = [∃ x, ~~ P x].
Lemma negb_forall_in D P :
-
~~ [∀ (x | D x), P x] = [∃ (x | D x), ~~ P x].
+
~~ [∀ (x | D x), P x] = [∃ (x | D x), ~~ P x].
-
Lemma negb_exists P :
~~ [∃ x, P x] = [∀ 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].
+
~~ [∃ (x | D x), P x] = [∀ (x | D x), ~~ P x].
End Quantifiers.
+
+
Notation "'exists_in_ view" := (
exists_inPP _ (
fun _ ⇒
view))
+ (
at level 4,
right associativity,
format "''exists_in_' view").
+
Notation "'forall_in_ view" := (
forall_inPP _ (
fun _ ⇒
view))
+ (
at level 4,
right associativity,
format "''forall_in_' view").
+
Section Extrema.
-
Variables (
I :
finType) (
i0 :
I) (
P :
pred I) (
F :
I → nat).
+
Variant extremum_spec {
T :
eqType} (
ord :
rel T) {
I :
finType}
+ (
P :
pred I) (
F :
I → T) :
I → Type :=
+
ExtremumSpec (
i :
I)
of P i & (
∀ j :
I,
P j → ord (
F i) (
F j)) :
+
extremum_spec ord P F i.
+
+
+
Let arg_pred {
T :
eqType}
ord {
I :
finType} (
P :
pred I) (
F :
I → T) :=
+
[pred i | P i & [∀ (j | P j), ord (
F i) (
F j)
]].
+
+
+
Section Extremum.
+
+
+
Context {
T :
eqType} {
I :
finType} (
ord :
rel T).
+
Context (
i0 :
I) (
P :
pred I) (
F :
I → T).
+
+
+
Hypothesis ord_refl :
reflexive ord.
+
Hypothesis ord_trans :
transitive ord.
+
Hypothesis ord_total :
total ord.
-
Let arg_pred ord :=
[pred i | P i & [∀ (j | P j), ord (
F i) (
F j)
]].
+
Definition extremum :=
odflt i0 (
pick (
arg_pred ord P F)).
-
Definition arg_min :=
odflt i0 (
pick (
arg_pred leq)).
+
Hypothesis Pi0 :
P i0.
-
Definition arg_max :=
odflt i0 (
pick (
arg_pred geq)).
+
Lemma extremumP :
extremum_spec ord P F extremum.
-
CoInductive extremum_spec (
ord :
rel nat) :
I → Type :=
-
ExtremumSpec i of P i & (
∀ j,
P j → ord (
F i) (
F j))
- :
extremum_spec ord i.
+
End Extremum.
-
Hypothesis Pi0 :
P i0.
+
Notation "[ 'arg[' ord ]_( i < i0 | P ) F ]" :=
+ (
extremum ord i0 (
fun i ⇒
P%
B) (
fun i ⇒
F))
+ (
at level 0,
ord,
i,
i0 at level 10,
+
format "[ 'arg[' ord ]_( i < i0 | P ) F ]") :
form_scope.
-
Let FP n :=
[∃ (i | P i), F i == n].
-
Let FP_F i :
P i → FP (
F i).
-
Let exFP :
∃ n, FP n.
+
Notation "[ 'arg[' ord ]_( i < i0 'in' A ) F ]" :=
+
[arg[ord]_(i < i0 | i \in A) F]
+ (
at level 0,
ord,
i,
i0 at level 10,
+
format "[ 'arg[' ord ]_( i < i0 'in' A ) F ]") :
form_scope.
-
Lemma arg_minP :
extremum_spec leq arg_min.
+
Notation "[ 'arg[' ord ]_( i < i0 ) F ]" :=
[arg[ord]_(i < i0 | true) F]
+ (
at level 0,
ord,
i,
i0 at level 10,
+
format "[ 'arg[' ord ]_( i < i0 ) F ]") :
form_scope.
-
Lemma arg_maxP :
extremum_spec geq arg_max.
+
Section ArgMinMax.
+
+
+
Variables (
I :
finType) (
i0 :
I) (
P :
pred I) (
F :
I → nat) (
Pi0 :
P i0).
+
+
+
Definition arg_min :=
extremum leq i0 P F.
+
Definition arg_max :=
extremum geq i0 P F.
+
+
+
Lemma arg_minP :
extremum_spec leq P F arg_min.
+
+
+
Lemma arg_maxP :
extremum_spec geq P F arg_max.
+
+
+
End ArgMinMax.
End Extrema.
-
Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
+
Notation "[ 'arg' 'min_' ( i < i0 | P ) F ]" :=
(
arg_min i0 (
fun i ⇒
P%
B) (
fun i ⇒
F))
(
at level 0,
i,
i0 at level 10,
format "[ 'arg' 'min_' ( i < i0 | P ) F ]") :
form_scope.
-
Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
-
[arg min_(i < i0 | i \in A) F]
+
Notation "[ 'arg' 'min_' ( i < i0 'in' A ) F ]" :=
+
[arg min_(i < i0 | i \in A) F]
(
at level 0,
i,
i0 at level 10,
format "[ 'arg' 'min_' ( i < i0 'in' A ) F ]") :
form_scope.
-
Notation "[ 'arg' 'min_' ( i < i0 ) F ]" :=
[arg min_(i < i0 | true) F]
+
Notation "[ 'arg' 'min_' ( i < i0 ) F ]" :=
[arg min_(i < i0 | true) F]
(
at level 0,
i,
i0 at level 10,
format "[ 'arg' 'min_' ( i < i0 ) F ]") :
form_scope.
-
Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
+
Notation "[ 'arg' 'max_' ( i > i0 | P ) F ]" :=
(
arg_max i0 (
fun i ⇒
P%
B) (
fun i ⇒
F))
(
at level 0,
i,
i0 at level 10,
format "[ 'arg' 'max_' ( i > i0 | P ) F ]") :
form_scope.
-
Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
-
[arg max_(i > i0 | i \in A) F]
+
Notation "[ 'arg' 'max_' ( i > i0 'in' A ) F ]" :=
+
[arg max_(i > i0 | i \in A) F]
(
at level 0,
i,
i0 at level 10,
format "[ 'arg' 'max_' ( i > i0 'in' A ) F ]") :
form_scope.
-
Notation "[ 'arg' 'max_' ( i > i0 ) F ]" :=
[arg max_(i > i0 | true) F]
+
Notation "[ 'arg' 'max_' ( i > i0 ) F ]" :=
[arg max_(i > i0 | true) F]
(
at level 0,
i,
i0 at level 10,
format "[ 'arg' 'max_' ( i > i0 ) F ]") :
form_scope.
@@ -1022,8 +1081,8 @@
Section Injectiveb.
-
Variables (
aT :
finType) (
rT :
eqType) (
f :
aT → rT).
-
Implicit Type D :
pred aT.
+
Variables (
aT :
finType) (
rT :
eqType) (
f :
aT → rT).
+
Implicit Type D :
{pred aT}.
Definition dinjectiveb D :=
uniq (
map f (
enum D)).
@@ -1033,144 +1092,144 @@
Lemma dinjectivePn D :
-
reflect (
exists2 x, x \in D & exists2 y, y \in [predD1 D & x] & f x = f y)
- (
~~ dinjectiveb 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 dinjectiveP D :
reflect {in D &, injective f} (
dinjectiveb D).
Lemma injectivePn :
-
reflect (
∃ x, exists2 y, x != y & f x = f y) (
~~ injectiveb).
+
reflect (
∃ x, exists2 y, x != y & f x = f y) (
~~ injectiveb).
-
Lemma injectiveP :
reflect (
injective f)
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)
+
Notation image f A := (
image_mem f (
mem A)).
+
Notation "[ 'seq' F | x 'in' A ]" := (
image (
fun x ⇒
F)
A)
(
at level 0,
F at level 99,
x ident,
format "'[hv' [ 'seq' F '/ ' | x 'in' A ] ']'") :
seq_scope.
-
Notation "[ 'seq' F | x : T 'in' A ]" := (
image (
fun x :
T ⇒
F)
A)
+
Notation "[ 'seq' F | x : T 'in' A ]" := (
image (
fun x :
T ⇒
F)
A)
(
at level 0,
F at level 99,
x ident,
only parsing) :
seq_scope.
-
Notation "[ 'seq' F | x : T ]" :=
-
[seq F | x : T in sort_of_simpl_pred (@
pred_of_argType T)
]
+
Notation "[ 'seq' F | x : T ]" :=
+
[seq F | x : T in pred_of_simpl (@
pred_of_argType T)
]
(
at level 0,
F at level 99,
x ident,
format "'[hv' [ 'seq' F '/ ' | x : T ] ']'") :
seq_scope.
-
Notation "[ 'seq' F , x ]" :=
[seq F | x : _ ]
+
Notation "[ 'seq' F , x ]" :=
[seq F | x : _ ]
(
at level 0,
F at level 99,
x ident,
only parsing) :
seq_scope.
-
Definition codom T T' f := @
image_mem T T' f (
mem T).
+
Definition codom T T' f := @
image_mem T T' f (
mem T).
Section Image.
Variable T :
finType.
-
Implicit Type A :
pred T.
+
Implicit Type A :
{pred T}.
Section SizeImage.
-
Variables (
T' :
Type) (
f :
T → T').
+
Variables (
T' :
Type) (
f :
T → T').
-
Lemma size_image A :
size (
image f A)
= #|A|.
+
Lemma size_image A :
size (
image f A)
= #|A|.
-
Lemma size_codom :
size (
codom f)
= #|T|.
+
Lemma size_codom :
size (
codom f)
= #|T|.
-
Lemma codomE :
codom f = map f (
enum T).
+
Lemma codomE :
codom f = map f (
enum T).
End SizeImage.
-
Variables (
T' :
eqType) (
f :
T → T').
+
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 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).
+
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}.
+
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 f_iinv A y fAy :
f (@
iinv A y fAy)
= y.
-
Lemma mem_iinv A y fAy : @
iinv A y fAy \in A.
+
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 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 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 image_f A x :
x \in A → f x \in image f A.
-
Lemma codom_f x :
f x \in codom f.
+
Lemma codom_f x :
f x \in codom f.
-
Lemma image_codom A :
{subset image f A ≤ codom f}.
+
Lemma image_codom A :
{subset image f A ≤ codom f}.
-
Lemma image_pred0 :
image f pred0 =i pred0.
+
Lemma image_pred0 :
image f pred0 =i pred0.
Section Injective.
-
Hypothesis injf :
injective f.
+
Hypothesis injf :
injective f.
-
Lemma mem_image A x :
(f x \in image f A) = (x \in A).
+
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 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 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 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 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_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}.
+
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 [::].
+
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.
+
Lemma map_preim (
s :
seq T') :
{subset s ≤ codom f} → map f (
preim_seq s)
= s.
End Image.
@@ -1178,45 +1237,46 @@
-
Lemma flatten_imageP (
aT :
finType) (
rT :
eqType)
A (
P :
pred aT) (
y :
rT) :
-
reflect (
exists2 x, x \in P & y \in A x) (
y \in flatten [seq A x | x in P]).
+
Lemma flatten_imageP (
aT :
finType) (
rT :
eqType)
+ (
A :
aT → seq rT) (
P :
{pred aT}) (
y :
rT) :
+
reflect (
exists2 x, x \in P & y \in A x) (
y \in flatten [seq A x | x in P]).
Section CardFunImage.
-
Variables (
T T' :
finType) (
f :
T → T').
-
Implicit Type A :
pred T.
+
Variables (
T T' :
finType) (
f :
T → T').
+
Implicit Type A :
{pred T}.
-
Lemma leq_image_card A :
#|image f A| ≤ #|A|.
+
Lemma leq_image_card A :
#|image f A| ≤ #|A|.
-
Lemma card_in_image A :
{in A &, injective f} → #|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 image_injP A :
reflect {in A &, injective f} (
#|image f A| == #|A|).
-
Hypothesis injf :
injective f.
+
Hypothesis injf :
injective f.
-
Lemma card_image A :
#|image f A| = #|A|.
+
Lemma card_image A :
#|image f A| = #|A|.
-
Lemma card_codom :
#|codom f| = #|T|.
+
Lemma card_codom :
#|codom f| = #|T|.
-
Lemma card_preim (
B :
pred T') :
#|[preim f of B]| = #|[predI codom f & B]|.
+
Lemma card_preim (
B :
{pred T'}) :
#|[preim f of B]| = #|[predI codom f & B]|.
-
Hypothesis card_range :
#|T| = #|T'|.
+
Hypothesis card_range :
#|T| = #|T'|.
-
Lemma inj_card_onto y :
y \in codom f.
+
Lemma inj_card_onto y :
y \in codom f.
-
Lemma inj_card_bij :
bijective f.
+
Lemma inj_card_bij :
bijective f.
End CardFunImage.
@@ -1227,41 +1287,41 @@
Section FinCancel.
-
Variables (
T :
finType) (
f g :
T → T).
+
Variables (
T :
finType) (
f g :
T → T).
Section Inv.
-
Hypothesis injf :
injective f.
+
Hypothesis injf :
injective f.
-
Lemma injF_onto y :
y \in codom 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.
+
Lemma invF_f :
cancel f invF.
+
Lemma f_invF :
cancel invF f.
+
Lemma injF_bij :
bijective f.
End Inv.
-
Hypothesis fK :
cancel f g.
+
Hypothesis fK :
cancel f g.
-
Lemma canF_sym :
cancel g f.
+
Lemma canF_sym :
cancel g f.
-
Lemma canF_LR x y :
x = g y → f x = y.
+
Lemma canF_LR x y :
x = g y → f x = y.
-
Lemma canF_RL x y :
g x = y → x = f 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_eq x y :
(f x == y) = (x == g y).
-
Lemma canF_invF :
g =1 invF (
can_inj fK).
+
Lemma canF_invF :
g =1 invF (
can_inj fK).
End FinCancel.
@@ -1273,14 +1333,14 @@
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_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_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.
+
Lemma eq_invF f g injf injg :
f =1 g → @
invF T f injf =1 @
invF T g injg.
End EqImage.
@@ -1294,16 +1354,16 @@
-
Lemma unit_enumP :
Finite.axiom [::tt].
+
Lemma unit_enumP :
Finite.axiom [::tt].
Definition unit_finMixin :=
Eval hnf in FinMixin unit_enumP.
-
Canonical unit_finType :=
Eval hnf in FinType unit unit_finMixin.
-
Lemma card_unit :
#|{: unit}| = 1.
+
Canonical unit_finType :=
Eval hnf in FinType unit unit_finMixin.
+
Lemma card_unit :
#|{: unit}| = 1.
-
Lemma bool_enumP :
Finite.axiom [:: true; false].
+
Lemma bool_enumP :
Finite.axiom [:: true; false].
Definition bool_finMixin :=
Eval hnf in FinMixin bool_enumP.
-
Canonical bool_finType :=
Eval hnf in FinType bool bool_finMixin.
-
Lemma card_bool :
#|{: bool}| = 2.
+
Canonical bool_finType :=
Eval hnf in FinType bool bool_finMixin.
+
Lemma card_bool :
#|{: bool}| = 2.
@@ -1314,17 +1374,17 @@
Variable T :
finType.
-
Definition option_enum :=
None :: map some (
enumF T).
+
Definition option_enum :=
None :: map some (
enumF T).
Lemma option_enumP :
Finite.axiom option_enum.
Definition option_finMixin :=
Eval hnf in FinMixin option_enumP.
-
Canonical option_finType :=
Eval hnf in FinType (
option T)
option_finMixin.
+
Canonical option_finType :=
Eval hnf in FinType (
option T)
option_finMixin.
-
Lemma card_option :
#|{: option T}| = #|T|.+1.
+
Lemma card_option :
#|{: option T}| = #|T|.+1.
End OptionFinType.
@@ -1333,16 +1393,16 @@
Section TransferFinType.
-
Variables (
eT :
countType) (
fT :
finType) (
f :
eT → fT).
+
Variables (
eT :
countType) (
fT :
finType) (
f :
eT → fT).
-
Lemma pcan_enumP g :
pcancel f g → Finite.axiom (
undup (
pmap g (
enumF fT))).
+
Lemma pcan_enumP g :
pcancel f g → Finite.axiom (
undup (
pmap g (
enumF fT))).
Definition PcanFinMixin g fK :=
FinMixin (@
pcan_enumP g fK).
-
Definition CanFinMixin g (
fK :
cancel f g) :=
PcanFinMixin (
can_pcan fK).
+
Definition CanFinMixin g (
fK :
cancel f g) :=
PcanFinMixin (
can_pcan fK).
End TransferFinType.
@@ -1351,7 +1411,7 @@
Section SubFinType.
-
Variables (
T :
choiceType) (
P :
pred T).
+
Variables (
T :
choiceType) (
P :
pred T).
Import Finite.
@@ -1362,8 +1422,8 @@
Definition pack_subFinType U :=
-
fun cT b m &
phant_id (
class cT) (@
Class U b m) ⇒
-
fun sT m' &
phant_id m' m ⇒ @
SubFinType sT m'.
+
fun cT b m &
phant_id (
class cT) (@
Class U b m) ⇒
+
fun sT m' &
phant_id m' m ⇒ @
SubFinType sT m'.
Implicit Type sT :
subFinType.
@@ -1378,11 +1438,11 @@
Coercion subFinType_finType sT :=
-
Pack (@
Class sT (
sub_choiceClass sT) (
subFin_mixin sT))
sT.
+
Pack (@
Class sT (
sub_choiceClass sT) (
subFin_mixin sT)).
Canonical subFinType_finType.
-
Lemma codom_val sT x :
(x \in codom (
val : sT → T)
) = P x.
+
Lemma codom_val sT x :
(x \in codom (
val : sT → T)
) = P x.
End SubFinType.
@@ -1394,26 +1454,26 @@
This assumes that T has both finType and subCountType structures.
@@ -1427,17 +1487,17 @@
Definition SubFinMixin :=
UniqFinMixin sub_enum_uniq mem_sub_enum.
-
Definition SubFinMixin_for (
eT :
eqType)
of phant eT :=
-
eq_rect _ Finite.mixin_of SubFinMixin eT.
+
Definition SubFinMixin_for (
eT :
eqType)
of phant eT :=
+
eq_rect _ Finite.mixin_of SubFinMixin eT.
Variable sfT :
subFinType P.
-
Lemma card_sub :
#|sfT| = #|[pred x | P x]|.
+
Lemma card_sub :
#|sfT| = #|[pred x | P x]|.
-
Lemma eq_card_sub (
A :
pred sfT) :
A =i predT → #|A| = #|[pred x | P x]|.
+
Lemma eq_card_sub (
A :
{pred sfT}) :
A =i predT → #|A| = #|[pred x | P x]|.
End FinTypeForSub.
@@ -1450,8 +1510,8 @@
has a finType structure.
-
Notation "[ 'finMixin' 'of' T 'by' <: ]" :=
- (
SubFinMixin_for (
Phant T) (
erefl _))
+
Notation "[ 'finMixin' 'of' T 'by' <: ]" :=
+ (
SubFinMixin_for (
Phant T) (
erefl _))
(
at level 0,
format "[ 'finMixin' 'of' T 'by' <: ]") :
form_scope.
@@ -1482,15 +1542,15 @@ Print myb_cntm.
Section CardSig.
-
Variables (
T :
finType) (
P :
pred T).
+
Variables (
T :
finType) (
P :
pred T).
-
Definition sig_finMixin :=
[finMixin of {x | P x} by <:].
-
Canonical sig_finType :=
Eval hnf in FinType {x | P x} sig_finMixin.
-
Canonical sig_subFinType :=
Eval hnf in [subFinType of {x | P x}].
+
Definition sig_finMixin :=
[finMixin of {x | P x} by <:].
+
Canonical sig_finType :=
Eval hnf in FinType {x | P x} sig_finMixin.
+
Canonical sig_subFinType :=
Eval hnf in [subFinType of {x | P x}].
-
Lemma card_sig :
#|{: {x | P x}}| = #|[pred x | P x]|.
+
Lemma card_sig :
#|{: {x | P x}}| = #|[pred x | P x]|.
End CardSig.
@@ -1508,26 +1568,26 @@ Print myb_cntm.
Variables (
T :
eqType) (
s :
seq T).
-
Record seq_sub :
Type :=
SeqSub {
ssval :
T;
ssvalP :
in_mem ssval (@
mem T _ s)}.
+
Record seq_sub :
Type :=
SeqSub {
ssval :
T;
ssvalP :
in_mem ssval (@
mem T _ s)}.
-
Canonical seq_sub_subType :=
Eval hnf in [subType for ssval].
-
Definition seq_sub_eqMixin :=
Eval hnf in [eqMixin of seq_sub by <:].
+
Canonical seq_sub_subType :=
Eval hnf in [subType for ssval].
+
Definition seq_sub_eqMixin :=
Eval hnf in [eqMixin of seq_sub by <:].
Canonical seq_sub_eqType :=
Eval hnf in EqType seq_sub seq_sub_eqMixin.
Definition seq_sub_enum :
seq seq_sub :=
undup (
pmap insub s).
-
Lemma mem_seq_sub_enum x :
x \in seq_sub_enum.
+
Lemma mem_seq_sub_enum x :
x \in seq_sub_enum.
-
Lemma val_seq_sub_enum :
uniq s → map val seq_sub_enum = s.
+
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_unpickle n :=
nth None (
map some seq_sub_enum)
n.
+
Lemma seq_sub_pickleK :
pcancel seq_sub_pickle seq_sub_unpickle.
Definition seq_sub_countMixin :=
CountMixin seq_sub_pickleK.
@@ -1546,7 +1606,7 @@ Print myb_cntm.
Definition adhoc_seq_sub_choiceType :=
Eval hnf in ChoiceType seq_sub adhoc_seq_sub_choiceMixin.
Definition adhoc_seq_sub_finType :=
-
[finType of seq_sub for FinType adhoc_seq_sub_choiceType seq_sub_finMixin].
+
[finType of seq_sub for FinType adhoc_seq_sub_choiceType seq_sub_finMixin].
End SeqSubType.
@@ -1558,17 +1618,17 @@ Print myb_cntm.
Variables (
T :
choiceType) (
s :
seq T).
-
Definition seq_sub_choiceMixin :=
[choiceMixin of sT by <:].
+
Definition seq_sub_choiceMixin :=
[choiceMixin of sT by <:].
Canonical seq_sub_choiceType :=
Eval hnf in ChoiceType sT seq_sub_choiceMixin.
Canonical seq_sub_countType :=
Eval hnf in CountType sT (
seq_sub_countMixin s).
-
Canonical seq_sub_subCountType :=
Eval hnf in [subCountType of sT].
+
Canonical seq_sub_subCountType :=
Eval hnf in [subCountType of sT].
Canonical seq_sub_finType :=
Eval hnf in FinType sT (
seq_sub_finMixin s).
-
Canonical seq_sub_subFinType :=
Eval hnf in [subFinType of sT].
+
Canonical seq_sub_subFinType :=
Eval hnf in [subFinType of sT].
-
Lemma card_seq_sub :
uniq s → #|{:sT}| = size s.
+
Lemma card_seq_sub :
uniq s → #|{:sT}| = size s.
End SeqFinType.
@@ -1589,122 +1649,122 @@ Print myb_cntm.
Section OrdinalSub.
-
Variable n :
nat.
+
Variable n :
nat.
-
Inductive ordinal :
predArgType :=
Ordinal m of m < n.
+
Inductive ordinal :
predArgType :=
Ordinal m of m < n.
Coercion nat_of_ord i :=
let:
Ordinal m _ :=
i in m.
-
Canonical ordinal_subType :=
[subType for nat_of_ord].
-
Definition ordinal_eqMixin :=
Eval hnf in [eqMixin of ordinal by <:].
+
Canonical ordinal_subType :=
[subType for nat_of_ord].
+
Definition ordinal_eqMixin :=
Eval hnf in [eqMixin of ordinal by <:].
Canonical ordinal_eqType :=
Eval hnf in EqType ordinal ordinal_eqMixin.
-
Definition ordinal_choiceMixin :=
[choiceMixin of ordinal by <:].
+
Definition ordinal_choiceMixin :=
[choiceMixin of ordinal by <:].
Canonical ordinal_choiceType :=
Eval hnf in ChoiceType ordinal ordinal_choiceMixin.
-
Definition ordinal_countMixin :=
[countMixin of ordinal by <:].
+
Definition ordinal_countMixin :=
[countMixin of ordinal by <:].
Canonical ordinal_countType :=
Eval hnf in CountType ordinal ordinal_countMixin.
-
Canonical ordinal_subCountType :=
[subCountType of ordinal].
+
Canonical ordinal_subCountType :=
[subCountType of ordinal].
-
Lemma ltn_ord (
i :
ordinal) :
i < n.
+
Lemma ltn_ord (
i :
ordinal) :
i < n.
-
Lemma ord_inj :
injective nat_of_ord.
+
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 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.
+
Lemma mem_ord_enum i :
i \in ord_enum.
Definition ordinal_finMixin :=
Eval hnf in UniqFinMixin ord_enum_uniq mem_ord_enum.
Canonical ordinal_finType :=
Eval hnf in FinType ordinal ordinal_finMixin.
-
Canonical ordinal_subFinType :=
Eval hnf in [subFinType of ordinal].
+
Canonical ordinal_subFinType :=
Eval hnf in [subFinType of ordinal].
End OrdinalSub.
-
Notation "''I_' n" := (
ordinal n)
+
Notation "''I_' n" := (
ordinal n)
(
at level 8,
n at level 2,
format "''I_' n").
-
Hint Resolve ltn_ord.
+
Hint Resolve ltn_ord :
core.
Section OrdinalEnum.
-
Variable n :
nat.
+
Variable n :
nat.
-
Lemma val_enum_ord :
map val (
enum 'I_n)
= iota 0
n.
+
Lemma val_enum_ord :
map val (
enum 'I_n)
= iota 0
n.
-
Lemma size_enum_ord :
size (
enum 'I_n)
= n.
+
Lemma size_enum_ord :
size (
enum 'I_n)
= n.
-
Lemma card_ord :
#|'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_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 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 index_enum_ord (
i :
'I_n) :
index i (
enum 'I_n)
= i.
End OrdinalEnum.
-
Lemma widen_ord_proof n m (
i :
'I_n) :
n ≤ m → i < m.
+
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.
+
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_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.
+ @
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)).
+
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).
+
cancel (
cast_ord (
esym eq_n)) (@
cast_ord n1 n2 eq_n).
-
Lemma cast_ord_inj n1 n2 eq_n :
injective (@
cast_ord n1 n2 eq_n).
+
Lemma cast_ord_inj n1 n2 eq_n :
injective (@
cast_ord n1 n2 eq_n).
-
Lemma rev_ord_proof n (
i :
'I_n) :
n - i.+1 < n.
+
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_ordK {
n} :
involutive (@
rev_ord n).
-
Lemma rev_ord_inj {
n} :
injective (@
rev_ord n).
+
Lemma rev_ord_inj {
n} :
injective (@
rev_ord n).
Variable T : finType.
-Implicit Type A : pred T.
+Implicit Type A : {pred T}.
-Lemma enum_rank_subproof x0 A : x0 \in A → 0 < #|A|.
+Lemma enum_rank_subproof x0 A : x0 \in A → 0 < #|A|.
-Definition enum_rank_in x0 A (Ax0 : x0 \in A) x :=
- insubd (Ordinal (@enum_rank_subproof x0 [eta A] Ax0)) (index x (enum A)).
+Definition enum_rank_in x0 A (Ax0 : x0 \in A) x :=
+ insubd (Ordinal (@enum_rank_subproof x0 [eta A] Ax0)) (index x (enum A)).
-Definition enum_rank x := @enum_rank_in x T (erefl true) x.
+Definition enum_rank x := @enum_rank_in x T (erefl true) x.
-Lemma enum_default A : 'I_(#|A|) → T.
+Lemma enum_default A : 'I_(#|A|) → T.
-Definition enum_val A i := nth (@enum_default [eta A] i) (enum A) i.
+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_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 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_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_codom T' y0 (f : T → T') (i : 'I_#|T|) :
+ nth y0 (codom f) i = f (enum_val i).
Lemma nth_enum_rank_in x00 x0 A Ax0 :
- {in A, cancel (@enum_rank_in x0 A Ax0) (nth x00 (enum A))}.
+ {in A, cancel (@enum_rank_in x0 A Ax0) (nth x00 (enum A))}.
-Lemma nth_enum_rank x0 : cancel enum_rank (nth x0 (enum T)).
+Lemma nth_enum_rank x0 : cancel enum_rank (nth x0 (enum T)).
Lemma enum_rankK_in x0 A Ax0 :
- {in A, cancel (@enum_rank_in x0 A Ax0) enum_val}.
+ {in A, cancel (@enum_rank_in x0 A Ax0) enum_val}.
-Lemma enum_rankK : cancel enum_rank enum_val.
+Lemma enum_rankK : cancel enum_rank enum_val.
-Lemma enum_valK_in x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0).
+Lemma enum_valK_in x0 A Ax0 : cancel enum_val (@enum_rank_in x0 A Ax0).
-Lemma enum_valK : cancel enum_val enum_rank.
+Lemma enum_valK : cancel enum_val enum_rank.
-Lemma enum_rank_inj : injective enum_rank.
+Lemma enum_rank_inj : injective enum_rank.
-Lemma enum_val_inj A : injective (@enum_val A).
+Lemma enum_val_inj A : injective (@enum_val A).
-Lemma enum_val_bij_in x0 A : x0 \in A → {on A, bijective (@enum_val A)}.
+Lemma enum_val_bij_in x0 A : x0 \in A → {on A, bijective (@enum_val A)}.
-Lemma enum_rank_bij : bijective enum_rank.
+Lemma enum_rank_bij : bijective enum_rank.
-Lemma enum_val_bij : bijective (@enum_val T).
+Lemma enum_val_bij : bijective (@enum_val T).
@@ -1793,13 +1853,13 @@ Print myb_cntm.
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_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)
).
+
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.
@@ -1807,10 +1867,10 @@ Print myb_cntm.
-
Lemma enum_rank_ord n i :
enum_rank i = cast_ord (
esym (
card_ord n))
i.
+
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.
+
Lemma enum_val_ord n i :
enum_val i = cast_ord (
card_ord n)
i.
-
Lemma lshift_subproof m n (
i :
'I_m) :
i < m + n.
+
Lemma lshift_subproof m n (
i :
'I_m) :
i < m + n.
-
Lemma rshift_subproof m n (
i :
'I_n) :
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).
+
Definition lshift m n (
i :
'I_m) :=
Ordinal (
lshift_subproof n i).
+
Definition rshift m n (
i :
'I_n) :=
Ordinal (
rshift_subproof m i).
-
Lemma split_subproof m n (
i :
'I_(m + n)) :
i ≥ m → i - m < n.
+
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 :=
+
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))
+ |
LtnNotGeq lt_i_m ⇒
inl _ (
Ordinal lt_i_m)
+ |
GeqNotLtn ge_i_m ⇒
inr _ (
Ordinal (
split_subproof ge_i_m))
end.
-
CoInductive split_spec m n (
i :
'I_(m + n)) :
'I_m + 'I_n → bool → Type :=
- |
SplitLo (
j :
'I_m)
of i = j :> nat :
split_spec i (
inl _ j)
true
- |
SplitHi (
k :
'I_n)
of i = m + k :> nat :
split_spec i (
inr _ k)
false.
+
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).
+
Lemma splitP m n (
i :
'I_(m + n)) :
split_spec i (
split i) (
i < m).
-
Definition unsplit m n (
jk :
'I_m + 'I_n) :=
-
match jk with inl j ⇒
lshift n j |
inr k ⇒
rshift m k end.
+
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 ltn_unsplit m n (
jk :
'I_m + 'I_n) :
(unsplit jk < m) = jk.
-
Lemma splitK m n :
cancel (@
split m n) (@
unsplit m n).
+
Lemma splitK {
m n} :
cancel (@
split m n)
unsplit.
-
Lemma unsplitK m n :
cancel (@
unsplit m n) (@
split m n).
+
Lemma unsplitK {
m n} :
cancel (@
unsplit m n)
split.
Section OrdinalPos.
-
Variable n' :
nat.
+
Variable n' :
nat.
Definition ord0 :=
Ordinal (
ltn0Sn n').
Definition ord_max :=
Ordinal (
ltnSn n').
-
Lemma leq_ord (
i :
'I_n) :
i ≤ n'.
+
Lemma leq_ord (
i :
'I_n) :
i ≤ n'.
-
Lemma sub_ord_proof m :
n' - m < 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.
+
Lemma sub_ordK (
i :
'I_n) :
n' - (n' - i) = i.
-
Definition inord m :
'I_n :=
insubd ord0 m.
+
Definition inord m :
'I_n :=
insubd ord0 m.
-
Lemma inordK m :
m < n → inord m = m :> nat.
+
Lemma inordK m :
m < n → inord m = m :> nat.
-
Lemma inord_val (
i :
'I_n) :
inord i = i.
+
Lemma inord_val (
i :
'I_n) :
inord i = i.
-
Lemma enum_ordS :
enum 'I_n = ord0 :: map (
lift ord0) (
enum 'I_n').
+
Lemma enum_ordS :
enum 'I_n = ord0 :: map (
lift ord0) (
enum 'I_n').
-
Lemma lift_max (
i :
'I_n') :
lift ord_max i = i :> nat.
+
Lemma lift_max (
i :
'I_n') :
lift ord_max i = i :> nat.
-
Lemma lift0 (
i :
'I_n') :
lift ord0 i = i.+1 :> nat.
+
Lemma lift0 (
i :
'I_n') :
lift ord0 i = i.+1 :> nat.
End OrdinalPos.
@@ -2009,27 +2069,28 @@ Print myb_cntm.
Variable T1 T2 :
finType.
-
Definition prod_enum :=
[seq (x1, x2) | x1 <- enum T1, x2 <- enum T2].
+
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 predX_prod_enum (
A1 :
{pred T1}) (
A2 :
{pred T2}) :
+
count [predX A1 & A2] prod_enum = #|A1| × #|A2|.
Lemma prod_enumP :
Finite.axiom prod_enum.
Definition prod_finMixin :=
Eval hnf in FinMixin prod_enumP.
-
Canonical prod_finType :=
Eval hnf in FinType (
T1 × T2)
prod_finMixin.
+
Canonical prod_finType :=
Eval hnf in FinType (
T1 × T2)
prod_finMixin.
-
Lemma cardX (
A1 :
pred T1) (
A2 :
pred T2) :
#|[predX A1 & A2]| = #|A1| × #|A2|.
+
Lemma cardX (
A1 :
{pred T1}) (
A2 :
{pred T2}) :
+
#|[predX A1 & A2]| = #|A1| × #|A2|.
-
Lemma card_prod :
#|{: T1 × T2}| = #|T1| × #|T2|.
+
Lemma card_prod :
#|{: T1 × T2}| = #|T1| × #|T2|.
-
Lemma eq_card_prod (
A :
pred (
T1 × T2)) :
A =i predT → #|A| = #|T1| × #|T2|.
+
Lemma eq_card_prod (
A :
{pred (T1 × T2)}) :
A =i predT → #|A| = #|T1| × #|T2|.
End ProdFinType.
@@ -2038,22 +2099,22 @@ Print myb_cntm.
Section TagFinType.
-
Variables (
I :
finType) (
T_ :
I → finType).
+
Variables (
I :
finType) (
T_ :
I → finType).
Definition tag_enum :=
-
flatten [seq [seq Tagged T_ x | x <- enumF (
T_ i)
] | i <- enumF I].
+
flatten [seq [seq Tagged T_ x | x <- enumF (
T_ i)
] | i <- enumF I].
Lemma tag_enumP :
Finite.axiom tag_enum.
Definition tag_finMixin :=
Eval hnf in FinMixin tag_enumP.
-
Canonical tag_finType :=
Eval hnf in FinType {i : I & T_ i} tag_finMixin.
+
Canonical tag_finType :=
Eval hnf in FinType {i : I & T_ i} tag_finMixin.
Lemma card_tagged :
-
#|{: {i : I & T_ i}}| = sumn (
map (
fun i ⇒
#|T_ i|) (
enum I)).
+
#|{: {i : I & T_ i}}| = sumn (
map (
fun i ⇒
#|T_ i|) (
enum I)).
End TagFinType.
@@ -2066,20 +2127,20 @@ Print myb_cntm.
Definition sum_enum :=
-
[seq inl _ x | x <- enumF T1] ++ [seq inr _ y | y <- enumF T2].
+
[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 mem_sum_enum u :
u \in sum_enum.
Definition sum_finMixin :=
Eval hnf in UniqFinMixin sum_enum_uniq mem_sum_enum.
-
Canonical sum_finType :=
Eval hnf in FinType (
T1 + T2)
sum_finMixin.
+
Canonical sum_finType :=
Eval hnf in FinType (
T1 + T2)
sum_finMixin.
-
Lemma card_sum :
#|{: T1 + T2}| = #|T1| + #|T2|.
+
Lemma card_sum :
#|{: T1 + T2}| = #|T1| + #|T2|.
End SumFinType.
--
cgit v1.2.3