Library Coq.ssr.ssrfun
This file contains the basic definitions and notations for working with
functions. The definitions provide for:
- Pair projections:
p.1 == first element of a pair
p.2 == second element of a pair
These notations also apply to p : P /\ Q, via an and >-> pair coercion.
- Simplifying functions, beta-reduced by /= and simpl:
[fun : T => E] == constant function from type T that returns E
[fun x => E] == unary function
[fun x : T => E] == unary function with explicit domain type
[fun x y => E] == binary function
[fun x y : T => E] == binary function with common domain type
[fun (x : T) y => E] \
[fun (x : xT) (y : yT) => E] | == binary function with (some) explicit,
[fun x (y : T) => E] / independent domain types for each argument
- Partial functions using option type:
oapp f d ox == if ox is Some x returns f x, d otherwise
odflt d ox == if ox is Some x returns x, d otherwise
obind f ox == if ox is Some x returns f x, None otherwise
omap f ox == if ox is Some x returns Some (f x), None otherwise
- Singleton types:
all_equal_to x0 == x0 is the only value in its type, so any such value
can be rewritten to x0.
- A generic wrapper type:
wrapped T == the inductive type with values Wrap x for x : T.
unwrap w == the projection of w : wrapped T on T.
wrap x == the canonical injection of x : T into wrapped T; it is
equivalent to Wrap x, but is declared as a (default)
Canonical Structure, which lets the Coq HO unification
automatically expand x into unwrap (wrap x). The delta
reduction of wrap x to Wrap can be exploited to
introduce controlled nondeterminism in Canonical
Structure inference, as in the implementation of
the mxdirect predicate in matrix.v.
- The empty type:
void == a notation for the Empty_set type of the standard library.
of_void T == the canonical injection void -> T.
- Sigma types:
tag w == the i of w : {i : I & T i}.
tagged w == the T i component of w : {i : I & T i}.
Tagged T x == the {i : I & T i} with component x : T i.
tag2 w == the i of w : {i : I & T i & U i}.
tagged2 w == the T i component of w : {i : I & T i & U i}.
tagged2' w == the U i component of w : {i : I & T i & U i}.
Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i.
sval u == the x of u : {x : T | P x}.
s2val u == the x of u : {x : T | P x & Q x}.
The properties of sval u, s2val u are given by lemmas svalP, s2valP, and
s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT.
A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2
and pair, e.g.,
have /all_sig[f fP] (x : T): {y : U | P y} by ...
yields an f : T -> U such that fP : forall x, P (f x).
- Identity functions:
id == NOTATION for the explicit identity function fun x => x.
@id T == notation for the explicit identity at type T.
idfun == an expression with a head constant, convertible to id;
idfun x simplifies to x.
@idfun T == the expression above, specialized to type T.
phant_id x y == the function type phantom _ x -> phantom _ y.
*** In addition to their casual use in functional programming, identity
functions are often used to trigger static unification as part of the
construction of dependent Records and Structures. For example, if we need
a structure sT over a type T, we take as arguments T, sT, and a "dummy"
function T -> sort sT:
Definition foo T sT & T -> sort sT := ...
We can avoid specifying sT directly by calling foo (@id T), or specify
the call completely while still ensuring the consistency of T and sT, by
calling @foo T sT idfun. The phant_id type allows us to extend this trick
to non-Type canonical projections. It also allows us to sidestep
dependent type constraints when building explicit records, e.g., given
Record r := R {x; y : T(x)}.
if we need to build an r from a given y0 while inferring some x0, such
that y0 : T(x0), we pose
Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'.
Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking
the dependent type constraint y0 : T(x0).
- Extensional equality for functions and relations (i.e. functions of two
arguments):
f1 =1 f2 == f1 x is equal to f2 x for all x.
f1 =1 f2 :> A == ... and f2 is explicitly typed.
f1 =2 f2 == f1 x y is equal to f2 x y for all x y.
f1 =2 f2 :> A == ... and f2 is explicitly typed.
- Composition for total and partial functions:
f^~ y == function f with second argument specialised to y,
i.e., fun x => f x y
CAVEAT: conditional (non-maximal) implicit arguments
of f are NOT inserted in this context
@^~ x == application at x, i.e., fun f => f x
[eta f] == the explicit eta-expansion of f, i.e., fun x => f x
CAVEAT: conditional (non-maximal) implicit arguments
of f are NOT inserted in this context.
fun=> v := the constant function fun _ => v.
f1 \o f2 == composition of f1 and f2.
Note: (f1 \o f2) x simplifies to f1 (f2 x).
f1 \; f2 == categorical composition of f1 and f2. This expands to
to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x).
pcomp f1 f2 == composition of partial functions f1 and f2.
- Properties of functions:
injective f <-> f is injective.
cancel f g <-> g is a left inverse of f / f is a right inverse of g.
pcancel f g <-> g is a left inverse of f where g is partial.
ocancel f g <-> g is a left inverse of f where f is partial.
bijective f <-> f is bijective (has a left and right inverse).
involutive f <-> f is involutive.
- Properties for operations.
left_id e op <-> e is a left identity for op (e op x = x).
right_id e op <-> e is a right identity for op (x op e = x).
left_inverse e inv op <-> inv is a left inverse for op wrt identity e,
i.e., (inv x) op x = e.
right_inverse e inv op <-> inv is a right inverse for op wrt identity e
i.e., x op (i x) = e.
self_inverse e op <-> each x is its own op-inverse (x op x = e).
idempotent op <-> op is idempotent for op (x op x = x).
associative op <-> op is associative, i.e.,
x op (y op z) = (x op y) op z.
commutative op <-> op is commutative (x op y = y op x).
left_commutative op <-> op is left commutative, i.e.,
x op (y op z) = y op (x op z).
right_commutative op <-> op is right commutative, i.e.,
(x op y) op z = (x op z) op y.
left_zero z op <-> z is a left zero for op (z op x = z).
right_zero z op <-> z is a right zero for op (x op z = z).
left_distributive op1 op2 <-> op1 distributes over op2 to the left:
(x op2 y) op1 z = (x op1 z) op2 (y op1 z).
right_distributive op1 op2 <-> op distributes over add to the right:
x op1 (y op2 z) = (x op1 z) op2 (x op1 z).
interchange op1 op2 <-> op1 and op2 satisfy an interchange law:
(x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t).
Note that interchange op op is a commutativity property.
left_injective op <-> op is injective in its left argument:
x op y = z op y -> x = z.
right_injective op <-> op is injective in its right argument:
x op y = x op z -> y = z.
left_loop inv op <-> op, inv obey the inverse loop left axiom:
(inv x) op (x op y) = y for all x, y, i.e.,
op (inv x) is always a left inverse of op x
rev_left_loop inv op <-> op, inv obey the inverse loop reverse left
axiom: x op ((inv x) op y) = y, for all x, y.
right_loop inv op <-> op, inv obey the inverse loop right axiom:
(x op y) op (inv y) = x for all x, y.
rev_right_loop inv op <-> op, inv obey the inverse loop reverse right
axiom: (x op (inv y)) op y = x for all x, y.
Note that familiar "cancellation" identities like x + y - y = x or
x - y + y = x are respectively instances of right_loop and rev_right_loop
The corresponding lemmas will use the K and NK/VK suffixes, respectively.
- Morphisms for functions and relations:
{morph f : x / a >-> r} <-> f is a morphism with respect to functions
(fun x => a) and (fun x => r); if r == R[x],
this states that f a = R[f x] for all x.
{morph f : x / a} <-> f is a morphism with respect to the
function expression (fun x => a). This is
shorthand for {morph f : x / a >-> a}; note
that the two instances of a are often
interpreted at different types.
{morph f : x y / a >-> r} <-> f is a morphism with respect to functions
(fun x y => a) and (fun x y => r).
{morph f : x y / a} <-> f is a morphism with respect to the
function expression (fun x y => a).
{homo f : x / a >-> r} <-> f is a homomorphism with respect to the
predicates (fun x => a) and (fun x => r);
if r == R[x], this states that a -> R[f x]
for all x.
{homo f : x / a} <-> f is a homomorphism with respect to the
predicate expression (fun x => a).
{homo f : x y / a >-> r} <-> f is a homomorphism with respect to the
relations (fun x y => a) and (fun x y => r).
{homo f : x y / a} <-> f is a homomorphism with respect to the
relation expression (fun x y => a).
{mono f : x / a >-> r} <-> f is monotone with respect to projectors
(fun x => a) and (fun x => r); if r == R[x],
this states that R[f x] = a for all x.
{mono f : x / a} <-> f is monotone with respect to the projector
expression (fun x => a).
{mono f : x y / a >-> r} <-> f is monotone with respect to relators
(fun x y => a) and (fun x y => r).
{mono f : x y / a} <-> f is monotone with respect to the relator
expression (fun x y => a).
The file also contains some basic lemmas for the above concepts.
Lemmas relative to cancellation laws use some abbreviated suffixes:
K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x).
LR - a lemma moving an operation from the left hand side of a relation to
the right hand side, like canLR: cancel g f -> x = g y -> f x = y.
RL - a lemma moving an operation from the right to the left, e.g., canRL.
Beware that the LR and RL orientations refer to an "apply" (back chaining)
usage; when using the same lemmas with "have" or "move" (forward chaining)
the directions will be reversed!.
Set Implicit Arguments.
Parsing / printing declarations.
Reserved Notation "p .1" (at level 2, left associativity, format "p .1").
Reserved Notation "p .2" (at level 2, left associativity, format "p .2").
Reserved Notation "f ^~ y" (at level 10, y at level 8, no associativity,
format "f ^~ y").
Reserved Notation "@^~ x" (at level 10, x at level 8, no associativity,
format "@^~ x").
Reserved Notation "[ 'eta' f ]" (at level 0, format "[ 'eta' f ]").
Reserved Notation "'fun' => E" (at level 200, format "'fun' => E").
Reserved Notation "[ 'fun' : T => E ]" (at level 0,
format "'[hv' [ 'fun' : T => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x => E ]" (at level 0,
x ident, format "'[hv' [ 'fun' x => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x : T => E ]" (at level 0,
x ident, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x y => E ]" (at level 0,
x ident, y ident, format "'[hv' [ 'fun' x y => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x y : T => E ]" (at level 0,
x ident, y ident, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'").
Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0,
x ident, y ident, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0,
x ident, y ident, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'").
Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0,
x ident, y ident, format "[ 'fun' ( x : T ) ( y : U ) => E ]" ).
Reserved Notation "f =1 g" (at level 70, no associativity).
Reserved Notation "f =1 g :> A" (at level 70, g at next level, A at level 90).
Reserved Notation "f =2 g" (at level 70, no associativity).
Reserved Notation "f =2 g :> A" (at level 70, g at next level, A at level 90).
Reserved Notation "f \o g" (at level 50, format "f \o '/ ' g").
Reserved Notation "f \; g" (at level 60, right associativity,
format "f \; '/ ' g").
Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99,
x ident, format "{ 'morph' f : x / a >-> r }").
Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99,
x ident, format "{ 'morph' f : x / a }").
Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
x ident, y ident, format "{ 'morph' f : x y / a >-> r }").
Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99,
x ident, y ident, format "{ 'morph' f : x y / a }").
Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
x ident, format "{ 'homo' f : x / a >-> r }").
Reserved Notation "{ 'homo' f : x / a }" (at level 0, f at level 99,
x ident, format "{ 'homo' f : x / a }").
Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
x ident, y ident, format "{ 'homo' f : x y / a >-> r }").
Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99,
x ident, y ident, format "{ 'homo' f : x y / a }").
Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99,
x ident, y ident, format "{ 'homo' f : x y /~ a }").
Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
x ident, format "{ 'mono' f : x / a >-> r }").
Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99,
x ident, format "{ 'mono' f : x / a }").
Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
x ident, y ident, format "{ 'mono' f : x y / a >-> r }").
Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99,
x ident, y ident, format "{ 'mono' f : x y / a }").
Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99,
x ident, y ident, format "{ 'mono' f : x y /~ a }").
Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id' T").
Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'").
Syntax for defining auxiliary recursive function.
Usage:
Section FooDefinition.
Variables (g1 : T1) (g2 : T2). (globals)
Fixoint foo_auxiliary (a3 : T3) ... :=
body, using [rec e3, ... ] for recursive calls
where " [ 'rec' a3 , a4 , ... ]" := foo_auxiliary.
Definition foo x y .. := [rec e1, ... ].
+ proofs about foo
End FooDefinition.
Reserved Notation "[ 'rec' a ]" (at level 0,
format "[ 'rec' a ]").
Reserved Notation "[ 'rec' a , b ]" (at level 0,
format "[ 'rec' a , b ]").
Reserved Notation "[ 'rec' a , b , c ]" (at level 0,
format "[ 'rec' a , b , c ]").
Reserved Notation "[ 'rec' a , b , c , d ]" (at level 0,
format "[ 'rec' a , b , c , d ]").
Reserved Notation "[ 'rec' a , b , c , d , e ]" (at level 0,
format "[ 'rec' a , b , c , d , e ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f ]" (at level 0,
format "[ 'rec' a , b , c , d , e , f ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g ]" (at level 0,
format "[ 'rec' a , b , c , d , e , f , g ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h ]" (at level 0,
format "[ 'rec' a , b , c , d , e , f , g , h ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h , i ]" (at level 0,
format "[ 'rec' a , b , c , d , e , f , g , h , i ]").
Reserved Notation "[ 'rec' a , b , c , d , e , f , g , h , i , j ]" (at level 0,
format "[ 'rec' a , b , c , d , e , f , g , h , i , j ]").
Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.
Notations for pair/conjunction projections
Complements on the option type constructor, used below to
encode partial functions.
Shorthand for some basic equality lemmas.
Force at least one implicit when used as a view.
A predicate for singleton types.
A generic wrapper type
Notations for argument transpose
Notation "f ^~ y" := (
fun x =>
f x y) :
fun_scope.
Notation "@^~ x" := (
fun f =>
f x) :
fun_scope.
Definitions and notation for explicit functions with simplification,
i.e., which simpl and /= beta expand (this is complementary to nosimpl).
For delta functions in eqtype.v.
Extensional equality, for unary and binary functions, including syntactic
sugar.
The empty type.
Strong sigma types.
Refinement types.
Prenex Implicits and renaming.
Morphism property for unary and binary functions
Homomorphism property for unary and binary relations
Stability property for unary and binary relations
In an intuitionistic setting, we have two degrees of injectivity. The
weaker one gives only simplification, and the strong one provides a left
inverse (we show in `fintype' that they coincide for finite types).
We also define an intermediate version where the left inverse is only a
partial function.
cancellation lemmas for dependent type casts.
Lemma esymK T x y :
cancel (@
esym T x y) (@
esym T y x).
Lemma etrans_id T x y (
eqxy :
x = y :> T) :
etrans (
erefl x)
eqxy = eqxy.
Section InjectionsTheory.
Variables (
A B C :
Type) (
f g :
B -> A) (
h :
C -> B).
Lemma inj_id :
injective (
@id A).
Lemma inj_can_sym f' :
cancel f f' -> injective f' -> cancel f' f.
Lemma inj_comp :
injective f -> injective h -> injective (
f \o h).
Lemma inj_compr :
injective (
f \o h)
-> injective h.
Lemma can_comp f' h' :
cancel f f' -> cancel h h' -> cancel (
f \o h) (
h' \o f').
Lemma pcan_pcomp f' h' :
pcancel f f' -> pcancel h h' -> pcancel (
f \o h) (
pcomp h' f').
Lemma eq_inj :
injective f -> f =1 g -> injective g.
Lemma eq_can f' g' :
cancel f f' -> f =1 g -> f' =1 g' -> cancel g g'.
Lemma inj_can_eq f' :
cancel f f' -> injective f' -> cancel g f' -> f =1 g.
End InjectionsTheory.
Section Bijections.
Variables (
A B :
Type) (
f :
B -> A).
Variant bijective :
Prop :=
Bijective g of cancel f g &
cancel g f.
Hypothesis bijf :
bijective.
Lemma bij_inj :
injective f.
Lemma bij_can_sym f' :
cancel f' f <-> cancel f f'.
Lemma bij_can_eq f' f'' :
cancel f f' -> cancel f f'' -> f' =1 f''.
End Bijections.
Section BijectionsTheory.
Variables (
A B C :
Type) (
f :
B -> A) (
h :
C -> B).
Lemma eq_bij :
bijective f -> forall g,
f =1 g -> bijective g.
Lemma bij_comp :
bijective f -> bijective h -> bijective (
f \o h).
Lemma bij_can_bij :
bijective f -> forall f',
cancel f f' -> bijective f'.
End BijectionsTheory.
Section Involutions.
Variables (
A :
Type) (
f :
A -> A).
Definition involutive :=
cancel f f.
Hypothesis Hf :
involutive.
Lemma inv_inj :
injective f.
Lemma inv_bij :
bijective f.
End Involutions.
Section OperationProperties.
Variables S T R :
Type.
Section SopTisR.
Implicit Type op :
S -> T -> R.
Definition left_inverse e inv op :=
forall x,
op (
inv x)
x = e.
Definition right_inverse e inv op :=
forall x,
op x (
inv x)
= e.
Definition left_injective op :=
forall x,
injective (
op^~ x).
Definition right_injective op :=
forall y,
injective (
op y).
End SopTisR.
Section SopTisS.
Implicit Type op :
S -> T -> S.
Definition right_id e op :=
forall x,
op x e = x.
Definition left_zero z op :=
forall x,
op z x = z.
Definition right_commutative op :=
forall x y z,
op (
op x y)
z = op (
op x z)
y.
Definition left_distributive op add :=
forall x y z,
op (
add x y)
z = add (
op x z) (
op y z).
Definition right_loop inv op :=
forall y,
cancel (
op^~ y) (
op^~ (inv y)).
Definition rev_right_loop inv op :=
forall y,
cancel (
op^~ (inv y)) (
op^~ y).
End SopTisS.
Section SopTisT.
Implicit Type op :
S -> T -> T.
Definition left_id e op :=
forall x,
op e x = x.
Definition right_zero z op :=
forall x,
op x z = z.
Definition left_commutative op :=
forall x y z,
op x (
op y z)
= op y (
op x z).
Definition right_distributive op add :=
forall x y z,
op x (
add y z)
= add (
op x y) (
op x z).
Definition left_loop inv op :=
forall x,
cancel (
op x) (
op (
inv x)).
Definition rev_left_loop inv op :=
forall x,
cancel (
op (
inv x)) (
op x).
End SopTisT.
Section SopSisT.
Implicit Type op :
S -> S -> T.
Definition self_inverse e op :=
forall x,
op x x = e.
Definition commutative op :=
forall x y,
op x y = op y x.
End SopSisT.
Section SopSisS.
Implicit Type op :
S -> S -> S.
Definition idempotent op :=
forall x,
op x x = x.
Definition associative op :=
forall x y z,
op x (
op y z)
= op (
op x y)
z.
Definition interchange op1 op2 :=
forall x y z t,
op1 (
op2 x y) (
op2 z t)
= op2 (
op1 x z) (
op1 y t).
End SopSisS.
End OperationProperties.