This file implements a type for functions with a finite domain:
- {ffun aT -> rT} where aT should have a finType structure.
+ {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.
- For f : {ffun aT -> rT}, we define
+ 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)
- fgraph f == the graph of f, i.e., the #|aT|.-tuple rT of the
- values of f over enum aT.
- finfun lam == the f such that f =1 lam; this is the RECOMMENDED
- interface to build an element of {ffun aT -> rT}.
- [ffun x => expr] == finfun (fun x => expr)
- [ffun => expr] == finfun (fun _ => expr)
- f \in ffun_on R == the range of f is a subset of R
+> 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 addidional 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.
@@ -60,143 +89,262 @@
Section Def.
-
Variables (
aT :
finType) (
rT :
Type).
+
Variables (
aT :
finType) (
rT :
aT → Type).
-
Inductive finfun_type :
predArgType :=
Finfun of #|aT|.-tuple rT.
+
Inductive finfun_on :
seq aT → Type :=
+|
finfun_nil :
finfun_on [::]
+|
finfun_cons x s of rT x &
finfun_on s :
finfun_on (
x :: s).
-
Definition finfun_of of phant (
aT → rT) :=
finfun_type.
-
Identity Coercion type_of_finfun :
finfun_of >->
finfun_type.
-
Definition fgraph f :=
let:
Finfun t :=
f in t.
+
Variant finfun_of (
ph :
phant (
∀ x,
rT x)) :
predArgType :=
+
FinfunOf of finfun_on (
enum aT).
-
Canonical finfun_subType :=
Eval hnf in [newType for fgraph].
+
Definition dfinfun_of ph :=
finfun_of ph.
+
+
+
Definition fun_of_fin ph (
f :
finfun_of ph)
x :=
+
let:
FinfunOf f_aT :=
f in fun_of_fin_rec f_aT (
mem_enum aT x).
End Def.
-
Notation "{ 'ffun' fT }" := (
finfun_of (
Phant fT))
+
Coercion fun_of_fin : finfun_of >-> Funclass.
+
Identity Coercion unfold_dfinfun_of :
dfinfun_of >->
finfun_of.
+
+
+
Notation "{ 'ffun' fT }" := (
finfun_of (
Phant fT))
(
at level 0,
format "{ 'ffun' '[hv' fT ']' }") :
type_scope.
-
Definition exp_finIndexType n :=
ordinal_finType n.
-
Notation "T ^ n" := (@
finfun_of (
exp_finIndexType n)
T (
Phant _)) :
type_scope.
+
Notation "{ 'dffun' fT }" := (
dfinfun_of (
Phant fT))
+ (
at level 0,
format "{ 'dffun' '[hv' fT ']' }") :
type_scope.
+
+
+
Definition exp_finIndexType :=
ordinal_finType.
+
Notation "T ^ n" :=
+ (@
finfun_of (
exp_finIndexType n) (
fun⇒ T) (
Phant _)) :
type_scope.
-
Module Type FunFinfunSig.
-
Parameter fun_of_fin :
∀ aT rT,
finfun_type aT rT → aT → rT.
-
Parameter finfun :
∀ (
aT :
finType)
rT,
(aT → rT) → {ffun aT → rT}.
-
Axiom fun_of_finE :
fun_of_fin = fun_of_fin_def.
-
Axiom finfunE :
finfun = finfun_def.
-
End FunFinfunSig.
+
Module Type FinfunDefSig.
+
Parameter finfun :
∀ aT rT,
finPi aT rT → {ffun finPi aT rT}.
+
Axiom finfunE :
finfun = finfun_def.
+
End FinfunDefSig.
-
Module FunFinfun :
FunFinfunSig.
-
Definition fun_of_fin :=
fun_of_fin_def.
-
Definition finfun :=
finfun_def.
-
Lemma fun_of_finE :
fun_of_fin = fun_of_fin_def.
-
Lemma finfunE :
finfun = finfun_def.
-
End FunFinfun.
+
Module FinfunDef :
FinfunDefSig.
+
Definition finfun :=
finfun_def.
+
Lemma finfunE :
finfun = finfun_def.
+
End FinfunDef.
-
Notation fun_of_fin :=
FunFinfun.fun_of_fin.
-
Notation finfun :=
FunFinfun.finfun.
-
Coercion fun_of_fin : finfun_type >-> Funclass.
-
Canonical fun_of_fin_unlock :=
Unlockable FunFinfun.fun_of_finE.
-
Canonical finfun_unlock :=
Unlockable FunFinfun.finfunE.
+
Notation finfun :=
FinfunDef.finfun.
+
Canonical finfun_unlock :=
Unlockable FinfunDef.finfunE.
-
Notation "[ 'ffun' x : aT => F ]" := (
finfun (
fun x :
aT ⇒
F))
- (
at level 0,
x ident,
only parsing) :
fun_scope.
+
Notation "[ 'ffun' x : aT => E ]" := (
finfun (
fun x :
aT ⇒
E))
+ (
at level 0,
x ident) :
fun_scope.
-
Notation "[ 'ffun' : aT => F ]" := (
finfun (
fun _ :
aT ⇒
F))
- (
at level 0,
only parsing) :
fun_scope.
+
Notation "[ 'ffun' x => E ]" := (@
finfun _ (
fun⇒ _) (
fun x ⇒
E))
+ (
at level 0,
x ident,
format "[ 'ffun' x => E ]") :
fun_scope.
-
Notation "[ 'ffun' x => F ]" :=
[ffun x : _ ⇒ F]
- (
at level 0,
x ident,
format "[ 'ffun' x => F ]") :
fun_scope.
+
Notation "[ 'ffun' => E ]" :=
[ffun _ ⇒ E]
+ (
at level 0,
format "[ 'ffun' => E ]") :
fun_scope.
-
Notation "[ 'ffun' => F ]" :=
[ffun : _ ⇒ F]
- (
at level 0,
format "[ 'ffun' => F ]") :
fun_scope.
+
- Helper for defining notation for function families.
+ The correspondance between finfun_of and CiC dependent functions.
- Lemmas on the correspondance between finfun_type and CiC functions.
+ Helper for defining notation for function families.