Library mathcomp.ssreflect.finfun

This file implements a type for functions with a finite domain: {ffun aT -> rT} where aT should have a finType structure, {ffun forall x : aT, rT} for dependent functions over a finType aT, and {ffun funT} where funT expands to a product over a finType. Any eqType, choiceType, countType and finType structures on rT extend to {ffun aT -> rT} as Leibnitz equality and extensional equalities coincide. (T ^ n)%type is notation for {ffun 'I_n -> T}, which is isomorphic to n.-tuple T, but is structurally positive and thus can be used to define inductive types, e.g., Inductive tree := node n of tree ^ n (see mid-file for an expanded example). --> More generally, {ffun fT} is always structurally positive. {ffun fT} inherits combinatorial structures of rT, i.e., eqType, choiceType, countType, and finType. However, due to some limitations of the Coq 8.9 unification code the structures are only inherited in the NON dependent case, when rT does not depend on x. For f : {ffun fT} with fT := forall x : aT, rT we define f x == the image of x under f (f coerces to a CiC function) --> The coercion is structurally decreasing, e.g., Coq will accept Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1. as structurally decreasing on t of the inductive tree type above. {dffun fT} == alias for {ffun fT} that inherits combinatorial structures on rT, when rT DOES depend on x. total_fun g == the function induced by a dependent function g of type forall x, rT on the total space {x : aT & rT}. := fun x => Tagged (fun x => rT) (g x). tfgraph f == the total function graph of f, i.e., the #|aT|.-tuple of all the (dependent pair) values of total_fun f. finfun g == the f extensionally equal to g, and the RECOMMENDED interface for building elements of {ffun fT}. [ffun x : aT => E] := finfun (fun x : aT => E). There should be an explicit type constraint on E if type does not depend on x, due to the Coq unification limitations referred to above. ffun0 aT0 == the trivial finfun, from a proof aT0 that #|aT| = 0. f \in family F == f belongs to the family F (f x \in F x for all x) There are additional operations for non-dependent finite functions, i.e., f in {ffun aT -> rT}. [ffun x => E] := finfun (fun x => E). The type of E must not depend on x; this restriction is a mitigation of the aforementioned Coq unification limitations. [ffun=> E] := [ffun _ => E] (E should not have a dependent type). fgraph f == the function graph of f, i.e., the #|aT|.-tuple listing the values of f x, for x ranging over enum aT. Finfun G == the finfun f whose (simple) function graph is G. f \in ffun_on R == the range of f is a subset of R. y.-support f == the y-support of f, i.e., [pred x | f x != y]. Thus, y.-support f \subset D means f has y-support D. We will put Notation support := 0.-support in ssralg. f \in pffun_on y D R == f is a y-partial function from D to R: f has y-support D and f x \in R for all x \in D. f \in pfamily y D F == f belongs to the y-partial family from D to F: f has y-support D and f x \in F x for all x \in D.

The correspondence between finfun_of and CiC dependent functions.

Helper for defining notation for function families.