Library Stdlib.ssr.ssrfun
This file contains the basic definitions and notations for working with
functions. The definitions provide for:
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!.
- 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] \
- 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
olift f := Some \o f
- 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}.
- 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.
- 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).
- 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).
Set Implicit Arguments.
Parsing / printing declarations.
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 name, format "'[hv' [ 'fun' x => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x : T => E ]" (at level 0,
x name, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x y => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' x y => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x y : T => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'").
Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'").
Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0,
x name, y name, 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 name, format "{ 'morph' f : x / a >-> r }").
Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99,
x name, format "{ 'morph' f : x / a }").
Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
x name, y name, format "{ 'morph' f : x y / a >-> r }").
Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99,
x name, y name, format "{ 'morph' f : x y / a }").
Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
x name, format "{ 'homo' f : x / a >-> r }").
Reserved Notation "{ 'homo' f : x / a }" (at level 0, f at level 99,
x name, format "{ 'homo' f : x / a }").
Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
x name, y name, format "{ 'homo' f : x y / a >-> r }").
Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99,
x name, y name, format "{ 'homo' f : x y / a }").
Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99,
x name, y name, format "{ 'homo' f : x y /~ a }").
Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
x name, format "{ 'mono' f : x / a >-> r }").
Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99,
x name, format "{ 'mono' f : x / a }").
Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
x name, y name, format "{ 'mono' f : x y / a >-> r }").
Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99,
x name, y name, format "{ 'mono' f : x y / a }").
Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99,
x name, y name, format "{ 'mono' f : x y /~ a }").
Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id' T").
#[warning="-closed-notation-not-level-0"]
Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'").
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 name, format "'[hv' [ 'fun' x => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x : T => E ]" (at level 0,
x name, format "'[hv' [ 'fun' x : T => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x y => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' x y => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x y : T => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' x y : T => '/ ' E ] ']'").
Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' ( x : T ) y => '/ ' E ] ']'").
Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0,
x name, y name, format "'[hv' [ 'fun' x ( y : T ) => '/ ' E ] ']'").
Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0,
x name, y name, 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 name, format "{ 'morph' f : x / a >-> r }").
Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99,
x name, format "{ 'morph' f : x / a }").
Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
x name, y name, format "{ 'morph' f : x y / a >-> r }").
Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99,
x name, y name, format "{ 'morph' f : x y / a }").
Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
x name, format "{ 'homo' f : x / a >-> r }").
Reserved Notation "{ 'homo' f : x / a }" (at level 0, f at level 99,
x name, format "{ 'homo' f : x / a }").
Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
x name, y name, format "{ 'homo' f : x y / a >-> r }").
Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99,
x name, y name, format "{ 'homo' f : x y / a }").
Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99,
x name, y name, format "{ 'homo' f : x y /~ a }").
Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
x name, format "{ 'mono' f : x / a >-> r }").
Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99,
x name, format "{ 'mono' f : x / a }").
Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
x name, y name, format "{ 'mono' f : x y / a >-> r }").
Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99,
x name, y name, format "{ 'mono' f : x y / a }").
Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99,
x name, y name, format "{ 'mono' f : x y /~ a }").
Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id' T").
#[warning="-closed-notation-not-level-0"]
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 ]").
Declare Scope pair_scope.
Delimit Scope pair_scope with PAIR.
Open Scope pair_scope.
Notations for pair/conjunction projections
Notation "p .1" := (fst p) : pair_scope.
Notation "p .2" := (snd p) : pair_scope.
Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ).
Definition all_pair I T U (w : forall i : I, T i * U i) :=
(fun i => (w i).1, fun i => (w i).2).
Notation "p .2" := (snd p) : pair_scope.
Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ).
Definition all_pair I T U (w : forall i : I, T i * U i) :=
(fun i => (w i).1, fun i => (w i).2).
Complements on the option type constructor, used below to
encode partial functions.
Module Option.
Definition apply aT rT (f : aT -> rT) x u := if u is Some y then f y else x.
Definition default T := apply (fun x : T => x).
Definition bind aT rT (f : aT -> option rT) := apply f None.
Definition map aT rT (f : aT -> rT) := bind (fun x => Some (f x)).
Definition lift aT rT (f : aT -> rT) := fun x => Some (f x).
End Option.
Notation oapp := Option.apply.
Notation odflt := Option.default.
Notation obind := Option.bind.
Notation omap := Option.map.
Notation olift := Option.lift.
Notation some := (@Some _) (only parsing).
Shorthand for some basic equality lemmas.
Notation erefl := refl_equal.
Notation ecast i T e x := (let: erefl in _ = i := e return T in x).
Definition esym := sym_eq.
Definition nesym := sym_not_eq.
Definition etrans := trans_eq.
Definition congr1 := f_equal.
Definition congr2 := f_equal2.
Force at least one implicit when used as a view.
A predicate for singleton types.
A generic wrapper type
fun_scope below is deprecated and should eventually be
removed. Use function_scope instead.
Declare Scope fun_scope.
Delimit Scope fun_scope with FUN.
Open Scope fun_scope.
Open Scope function_scope.
Delimit Scope fun_scope with FUN.
Open Scope fun_scope.
Open Scope function_scope.
Notations for argument transpose
Notation "f ^~ y" := (fun x => f x y) : function_scope.
Notation "@^~ x" := (fun f => f x) : function_scope.
Notation "@^~ x" := (fun f => f x) : function_scope.
Definitions and notation for explicit functions with simplification,
i.e., which simpl and /= beta expand (this is complementary to nosimpl).
#[universes(template)]
Variant simpl_fun (aT rT : Type) := SimplFun of aT -> rT.
Section SimplFun.
Variables aT rT : Type.
Definition fun_of_simpl (f : simpl_fun aT rT) := fun x => let: SimplFun lam := f in lam x.
End SimplFun.
Coercion fun_of_simpl : simpl_fun >-> Funclass.
Notation "[ 'fun' : T => E ]" := (SimplFun (fun _ : T => E)) : function_scope.
Notation "[ 'fun' x => E ]" := (SimplFun (fun x => E)) : function_scope.
Notation "[ 'fun' x y => E ]" := (fun x => [fun y => E]) : function_scope.
Notation "[ 'fun' x : T => E ]" := (SimplFun (fun x : T => E))
(only parsing) : function_scope.
Notation "[ 'fun' x y : T => E ]" := (fun x : T => [fun y : T => E])
(only parsing) : function_scope.
Notation "[ 'fun' ( x : T ) y => E ]" := (fun x : T => [fun y => E])
(only parsing) : function_scope.
Notation "[ 'fun' x ( y : T ) => E ]" := (fun x => [fun y : T => E])
(only parsing) : function_scope.
Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" := (fun x : T => [fun y : U => E])
(only parsing) : function_scope.
For delta functions in eqtype.v.
Extensional equality, for unary and binary functions, including syntactic
sugar.
Section ExtensionalEquality.
Variables A B C : Type.
Definition eqfun (f g : B -> A) : Prop := forall x, f x = g x.
Definition eqrel (r s : C -> B -> A) : Prop := forall x y, r x y = s x y.
Lemma frefl f : eqfun f f.
Lemma fsym f g : eqfun f g -> eqfun g f.
Lemma ftrans f g h : eqfun f g -> eqfun g h -> eqfun f h.
Lemma rrefl r : eqrel r r.
End ExtensionalEquality.
Global Typeclasses Opaque eqfun eqrel.
#[global]
Hint Resolve frefl rrefl : core.
Notation "f1 =1 f2" := (eqfun f1 f2) : type_scope.
Notation "f1 =1 f2 :> A" := (f1 =1 (f2 : A)) : type_scope.
Notation "f1 =2 f2" := (eqrel f1 f2) : type_scope.
Notation "f1 =2 f2 :> A" := (f1 =2 (f2 : A)) : type_scope.
Section Composition.
Variables A B C : Type.
Definition comp (f : B -> A) (g : C -> B) x := f (g x).
Definition catcomp g f := comp f g.
Definition pcomp (f : B -> option A) (g : C -> option B) x := obind f (g x).
Lemma eq_comp f f' g g' : f =1 f' -> g =1 g' -> comp f g =1 comp f' g'.
End Composition.
Arguments comp {A B C} f g x /.
Arguments catcomp {A B C} g f x /.
Notation "f1 \o f2" := (comp f1 f2) : function_scope.
Notation "f1 \; f2" := (catcomp f1 f2) : function_scope.
Lemma compA {A B C D : Type} (f : B -> A) (g : C -> B) (h : D -> C) :
f \o (g \o h) = (f \o g) \o h.
Notation "[ 'eta' f ]" := (fun x => f x) : function_scope.
Notation "'fun' => E" := (fun _ => E) : function_scope.
Notation id := (fun x => x).
Notation "@ 'id' T" := (fun x : T => x) (only parsing) : function_scope.
Definition idfun T x : T := x.
Arguments idfun {T} x /.
Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2.
Section OptionTheory.
Variables (aT rT sT : Type) (f : aT -> rT) (g : rT -> sT).
Lemma obindEapp (fo : aT -> option rT) : obind fo = oapp fo None.
Lemma omapEbind : omap f = obind (olift f).
Lemma omapEapp : omap f = oapp (olift f) None.
Lemma oappEmap (y0 : rT) x : oapp f y0 x = odflt y0 (omap f x).
Lemma omap_comp : omap (g \o f) =1 omap g \o omap f.
Lemma oapp_comp x : oapp (g \o f) x =1 (@oapp _ _)^~ x g \o omap f.
Lemma oapp_comp_f (x : rT) : oapp (g \o f) (g x) =1 g \o oapp f x.
Lemma olift_comp : olift (g \o f) = olift g \o f.
End OptionTheory.
The empty type.
Strong sigma types.
Section Tag.
Variables (I : Type) (i : I) (T_ U_ : I -> Type).
Definition tag := projT1.
Definition tagged : forall w, T_(tag w) := @projT2 I [eta T_].
Definition Tagged x := @existT I [eta T_] i x.
Definition tag2 (w : @sigT2 I T_ U_) := let: existT2 _ _ i _ _ := w in i.
Definition tagged2 w : T_(tag2 w) := let: existT2 _ _ _ x _ := w in x.
Definition tagged2' w : U_(tag2 w) := let: existT2 _ _ _ _ y := w in y.
Definition Tagged2 x y := @existT2 I [eta T_] [eta U_] i x y.
End Tag.
Arguments Tagged [I i].
Arguments Tagged2 [I i].
Coercion tag_of_tag2 I T_ U_ (w : @sigT2 I T_ U_) :=
Tagged (fun i => T_ i * U_ i)%type (tagged2 w, tagged2' w).
Lemma all_tag I T U :
(forall x : I, {y : T x & U x y}) ->
{f : forall x, T x & forall x, U x (f x)}.
Lemma all_tag2 I T U V :
(forall i : I, {y : T i & U i y & V i y}) ->
{f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}.
Refinement types.
Prenex Implicits and renaming.
Notation sval := (@proj1_sig _ _).
Notation "@ 'sval'" := (@proj1_sig) (only parsing) : function_scope.
Section Sig.
Variables (T : Type) (P Q : T -> Prop).
Lemma svalP (u : sig P) : P (sval u).
Definition s2val (u : sig2 P Q) := let: exist2 _ _ x _ _ := u in x.
Lemma s2valP u : P (s2val u).
Lemma s2valP' u : Q (s2val u).
End Sig.
Coercion tag_of_sig I P (u : @sig I P) := Tagged P (svalP u).
Coercion sig_of_sig2 I P Q (u : @sig2 I P Q) :=
exist (fun i => P i /\ Q i) (s2val u) (conj (s2valP u) (s2valP' u)).
Lemma all_sig I T P :
(forall x : I, {y : T x | P x y}) ->
{f : forall x, T x | forall x, P x (f x)}.
Lemma all_sig2 I T P Q :
(forall x : I, {y : T x | P x y & Q x y}) ->
{f : forall x, T x | forall x, P x (f x) & forall x, Q x (f x)}.
Section Morphism.
Variables (aT rT sT : Type) (f : aT -> rT).
Notation "@ 'sval'" := (@proj1_sig) (only parsing) : function_scope.
Section Sig.
Variables (T : Type) (P Q : T -> Prop).
Lemma svalP (u : sig P) : P (sval u).
Definition s2val (u : sig2 P Q) := let: exist2 _ _ x _ _ := u in x.
Lemma s2valP u : P (s2val u).
Lemma s2valP' u : Q (s2val u).
End Sig.
Coercion tag_of_sig I P (u : @sig I P) := Tagged P (svalP u).
Coercion sig_of_sig2 I P Q (u : @sig2 I P Q) :=
exist (fun i => P i /\ Q i) (s2val u) (conj (s2valP u) (s2valP' u)).
Lemma all_sig I T P :
(forall x : I, {y : T x | P x y}) ->
{f : forall x, T x | forall x, P x (f x)}.
Lemma all_sig2 I T P Q :
(forall x : I, {y : T x | P x y & Q x y}) ->
{f : forall x, T x | forall x, P x (f x) & forall x, Q x (f x)}.
Section Morphism.
Variables (aT rT sT : Type) (f : aT -> rT).
Morphism property for unary and binary functions
Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x).
Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y).
Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y).
Homomorphism property for unary and binary relations
Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x).
Definition homomorphism_2 (aR rR : _ -> _ -> Prop) :=
forall x y, aR x y -> rR (f x) (f y).
Definition homomorphism_2 (aR rR : _ -> _ -> Prop) :=
forall x y, aR x y -> rR (f x) (f y).
Stability property for unary and binary relations
Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x.
Definition monomorphism_2 (aR rR : _ -> _ -> sT) :=
forall x y, rR (f x) (f y) = aR x y.
End Morphism.
Notation "{ 'morph' f : x / a >-> r }" :=
(morphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'morph' f : x / a }" :=
(morphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'morph' f : x y / a >-> r }" :=
(morphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'morph' f : x y / a }" :=
(morphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'homo' f : x / a >-> r }" :=
(homomorphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'homo' f : x / a }" :=
(homomorphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'homo' f : x y / a >-> r }" :=
(homomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'homo' f : x y / a }" :=
(homomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'homo' f : x y /~ a }" :=
(homomorphism_2 f (fun y x => a) (fun x y => a)) : type_scope.
Notation "{ 'mono' f : x / a >-> r }" :=
(monomorphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'mono' f : x / a }" :=
(monomorphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'mono' f : x y / a >-> r }" :=
(monomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'mono' f : x y / a }" :=
(monomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'mono' f : x y /~ a }" :=
(monomorphism_2 f (fun y x => a) (fun x y => a)) : type_scope.
Definition monomorphism_2 (aR rR : _ -> _ -> sT) :=
forall x y, rR (f x) (f y) = aR x y.
End Morphism.
Notation "{ 'morph' f : x / a >-> r }" :=
(morphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'morph' f : x / a }" :=
(morphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'morph' f : x y / a >-> r }" :=
(morphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'morph' f : x y / a }" :=
(morphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'homo' f : x / a >-> r }" :=
(homomorphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'homo' f : x / a }" :=
(homomorphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'homo' f : x y / a >-> r }" :=
(homomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'homo' f : x y / a }" :=
(homomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'homo' f : x y /~ a }" :=
(homomorphism_2 f (fun y x => a) (fun x y => a)) : type_scope.
Notation "{ 'mono' f : x / a >-> r }" :=
(monomorphism_1 f (fun x => a) (fun x => r)) : type_scope.
Notation "{ 'mono' f : x / a }" :=
(monomorphism_1 f (fun x => a) (fun x => a)) : type_scope.
Notation "{ 'mono' f : x y / a >-> r }" :=
(monomorphism_2 f (fun x y => a) (fun x y => r)) : type_scope.
Notation "{ 'mono' f : x y / a }" :=
(monomorphism_2 f (fun x y => a) (fun x y => a)) : type_scope.
Notation "{ 'mono' f : x y /~ a }" :=
(monomorphism_2 f (fun y x => a) (fun x y => a)) : type_scope.
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.
Section Injections.
Variables (rT aT : Type) (f : aT -> rT).
Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2.
Definition cancel g := forall x, g (f x) = x.
Definition pcancel g := forall x, g (f x) = Some x.
Definition ocancel (g : aT -> option rT) h := forall x, oapp h x (g x) = x.
Lemma can_pcan g : cancel g -> pcancel (fun y => Some (g y)).
Lemma pcan_inj g : pcancel g -> injective.
Lemma can_inj g : cancel g -> injective.
Lemma canLR g x y : cancel g -> x = f y -> g x = y.
Lemma canRL g x y : cancel g -> f x = y -> x = g y.
End Injections.
Lemma Some_inj {T : nonPropType} : injective (@Some T).
Lemma of_voidK T : pcancel (of_void T) [fun _ => None].
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 ocan_comp [fo : B -> option A] [ho : C -> option B]
[f' : A -> B] [h' : B -> C] :
ocancel fo f' -> ocancel ho h' -> ocancel (obind fo \o ho) (h' \o 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.
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 ocan_comp [fo : B -> option A] [ho : C -> option B]
[f' : A -> B] [h' : B -> C] :
ocancel fo f' -> ocancel ho h' -> ocancel (obind fo \o ho) (h' \o 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.