Library finfun
This file implements a type for functions with a finite domain:
{ffun aT -> rT} where aT should have a finType structure.
Any eqType, choiceType, countType and finType structures on rT extend to
{ffun aT -> rT} as Leibnitz equality and extensional equalities coincide.
For f : {ffun 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)
ffun_on R f == the range of f is a subset of R
family F f == f belongs to the family F (f x \in F x for all x)
support y f x == x is in the y-support of f (i.e., f x != y)
pffun_on y D R f == f is a (y,D)-partial function with range R, i.e., the
y-support of f is a subset of D, and f x \in R for
all x \in D.
pfamily y D pF f == f belongs to the partial family <y, D, pF>, i.e., the
y-support of f is a subset of D, and f x \in pF x for
all x \in D.
powerset D f == f is a sub-predicate of D (when rT == bool)
Import Prenex Implicits.
Section Def.
Variables (aT : finType) (rT : Type).
Inductive finfun_type : predArgType := Finfun of #|aT|.-tuple rT.
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.
Canonical Structure finfun_subType :=
Eval hnf in [newType for fgraph by finfun_type_rect].
End Def.
Notation "{ 'ffun' fT }" := (finfun_of (Phant fT))
(at level 0, format "{ 'ffun' '[hv' fT ']' }") : type_scope.
Notation Local fun_of_fin_def :=
(fun aT rT f x => tnth (@fgraph aT rT f) (enum_rank x)).
Notation Local finfun_def :=
(fun aT rT f => @Finfun aT rT [tuple of map f (enum aT)]).
Module Type FunFinfunSig.
Parameter fun_of_fin : forall aT rT, finfun_type aT rT -> aT -> rT.
Coercion fun_of_fin : finfun_type >-> Funclass.
Parameter finfun : forall (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 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.
Notation fun_of_fin := FunFinfun.fun_of_fin.
Notation finfun := FunFinfun.finfun.
Canonical Structure fun_of_fin_unlock := Unlockable FunFinfun.fun_of_finE.
Canonical Structure finfun_unlock := Unlockable FunFinfun.finfunE.
Notation "[ 'ffun' x : aT => F ]" := (finfun (fun x : aT => F))
(at level 0, x ident, only parsing) : fun_scope.
Notation "[ 'ffun' : aT => F ]" := (finfun (fun _ : aT => F))
(at level 0, only parsing) : fun_scope.
Notation "[ 'ffun' x => F ]" := [ffun x : _ => F]
(at level 0, x ident, format "[ 'ffun' x => F ]") : fun_scope.
Notation "[ 'ffun' => F ]" := [ffun : _ => F]
(at level 0, format "[ 'ffun' => F ]") : fun_scope.
Lemma on the correspondance between finfun_type and finite domain function
Section PlainTheory.
Variables (aT : finType) (rT : Type).
Notation fT := {ffun aT -> rT}.
Canonical Structure finfun_of_subType := Eval hnf in [subType of fT].
Lemma tnth_fgraph : forall (f : fT) i, tnth (fgraph f) i = f (enum_val i).
Lemma ffunE : forall f : aT -> rT, finfun f =1 f.
Lemma fgraph_map : forall f : fT, fgraph f = [tuple of map f (enum aT)].
Lemma map_ffun_enum : forall f : fT, map f (enum aT) = val f.
Lemma ffunP : forall f1 f2 : fT, f1 =1 f2 <-> f1 = f2.
Lemma ffunK : cancel (@fun_of_fin aT rT) (@finfun aT rT).
Section Family.
Variable F : aT -> pred rT.
Definition family : pred fT := fun f => forallb x, F x (f x).
Lemma familyP : forall f : fT, reflect (forall x, F x (f x)) (family f).
End Family.
Definition ffun_on r := family (fun _ => r).
Lemma ffun_onP : forall (r : pred rT) (f : fT),
reflect (forall x, r (f x)) (ffun_on r f).
End PlainTheory.
Lemma nth_fgraph_ord : forall T n (x0 : T) (i : 'I_n) f,
nth x0 (fgraph f) i = f i.
Section EqTheory.
Variables (aT : finType) (rT : eqType).
Notation fT := {ffun aT -> rT}.
Definition finfun_eqMixin :=
Eval hnf in [eqMixin of finfun_type aT rT by <:].
Canonical Structure finfun_eqType := Eval hnf in EqType _ finfun_eqMixin.
Canonical Structure finfun_of_eqType := Eval hnf in [eqType of fT].
Section Partial.
Variables (y0 : rT) (d : pred aT).
Definition support T f : pred T := fun x => f x != y0.
Definition pfamily F :=
family (fun i => if d i then F i else pred1 y0 : pred _).
Lemma pfamilyP : forall (F : aT -> pred rT) (f : fT),
reflect (subpred (support f) d /\ forall x, d x -> F x (f x)) (pfamily F f).
Definition pffun_on r := pfamily (fun _ => r).
Lemma pffun_onP : forall r (f : fT),
reflect (subpred (support f) d /\ subpred (image f d) r) (pffun_on r f).
End Partial.
End EqTheory.
Definition finfun_choiceMixin aT (rT : choiceType) :=
[choiceMixin of finfun_type aT rT by <:].
Canonical Structure finfun_choiceType aT rT :=
Eval hnf in ChoiceType _ (finfun_choiceMixin aT rT).
Canonical Structure finfun_of_choiceType (aT : finType) (rT : choiceType) :=
Eval hnf in [choiceType of {ffun aT -> rT}].
Definition finfun_countMixin aT (rT : countType) :=
[countMixin of finfun_type aT rT by <:].
Canonical Structure finfun_countType aT (rT : countType) :=
Eval hnf in CountType _ (finfun_countMixin aT rT).
Canonical Structure finfun_of_countType (aT : finType) (rT : countType) :=
Eval hnf in [countType of {ffun aT -> rT}].
Canonical Structure finfun_subCountType aT (rT : countType) :=
Eval hnf in [subCountType of finfun_type aT rT].
Canonical Structure finfun_of_subCountType (aT : finType) (rT : countType) :=
Eval hnf in [subCountType of {ffun aT -> rT}].
Section FinTheory.
Variables aT rT : finType.
Notation fT := {ffun aT -> rT}.
Notation ffT := (finfun_type aT rT).
Definition finfun_finMixin := [finMixin of ffT by <:].
Canonical Structure finfun_finType := Eval hnf in FinType ffT finfun_finMixin.
Canonical Structure finfun_subFinType := Eval hnf in [subFinType of ffT].
Canonical Structure finfun_of_finType := Eval hnf in [finType of fT for finfun_finType].
Canonical Structure finfun_of_subFinType := Eval hnf in [subFinType of fT].
Lemma card_pfamily : forall y0 d (F : aT -> pred rT),
#|pfamily y0 d F| = foldr (fun x m => #|F x| * m) 1 (enum d).
Lemma card_family : forall F : aT -> pred rT,
#|family F| = foldr (fun x m => #|F x| * m) 1 (enum aT).
Lemma card_pffun_on : forall y0 d r, #|pffun_on y0 d r| = #|r| ^ #|d|.
Lemma card_ffun_on : forall r, #|ffun_on r| = #|r| ^ #|aT|.
Lemma card_ffun : #|fT| = #|rT| ^ #|aT|.
End FinTheory.
Section FinPowerSet.
Variable eT : finType.
Variable A : pred eT.
Definition powerset := pffun_on false A predT.
Lemma card_powerset : #|powerset| = 2 ^ #|A|.
End FinPowerSet.
Variables (aT : finType) (rT : Type).
Notation fT := {ffun aT -> rT}.
Canonical Structure finfun_of_subType := Eval hnf in [subType of fT].
Lemma tnth_fgraph : forall (f : fT) i, tnth (fgraph f) i = f (enum_val i).
Lemma ffunE : forall f : aT -> rT, finfun f =1 f.
Lemma fgraph_map : forall f : fT, fgraph f = [tuple of map f (enum aT)].
Lemma map_ffun_enum : forall f : fT, map f (enum aT) = val f.
Lemma ffunP : forall f1 f2 : fT, f1 =1 f2 <-> f1 = f2.
Lemma ffunK : cancel (@fun_of_fin aT rT) (@finfun aT rT).
Section Family.
Variable F : aT -> pred rT.
Definition family : pred fT := fun f => forallb x, F x (f x).
Lemma familyP : forall f : fT, reflect (forall x, F x (f x)) (family f).
End Family.
Definition ffun_on r := family (fun _ => r).
Lemma ffun_onP : forall (r : pred rT) (f : fT),
reflect (forall x, r (f x)) (ffun_on r f).
End PlainTheory.
Lemma nth_fgraph_ord : forall T n (x0 : T) (i : 'I_n) f,
nth x0 (fgraph f) i = f i.
Section EqTheory.
Variables (aT : finType) (rT : eqType).
Notation fT := {ffun aT -> rT}.
Definition finfun_eqMixin :=
Eval hnf in [eqMixin of finfun_type aT rT by <:].
Canonical Structure finfun_eqType := Eval hnf in EqType _ finfun_eqMixin.
Canonical Structure finfun_of_eqType := Eval hnf in [eqType of fT].
Section Partial.
Variables (y0 : rT) (d : pred aT).
Definition support T f : pred T := fun x => f x != y0.
Definition pfamily F :=
family (fun i => if d i then F i else pred1 y0 : pred _).
Lemma pfamilyP : forall (F : aT -> pred rT) (f : fT),
reflect (subpred (support f) d /\ forall x, d x -> F x (f x)) (pfamily F f).
Definition pffun_on r := pfamily (fun _ => r).
Lemma pffun_onP : forall r (f : fT),
reflect (subpred (support f) d /\ subpred (image f d) r) (pffun_on r f).
End Partial.
End EqTheory.
Definition finfun_choiceMixin aT (rT : choiceType) :=
[choiceMixin of finfun_type aT rT by <:].
Canonical Structure finfun_choiceType aT rT :=
Eval hnf in ChoiceType _ (finfun_choiceMixin aT rT).
Canonical Structure finfun_of_choiceType (aT : finType) (rT : choiceType) :=
Eval hnf in [choiceType of {ffun aT -> rT}].
Definition finfun_countMixin aT (rT : countType) :=
[countMixin of finfun_type aT rT by <:].
Canonical Structure finfun_countType aT (rT : countType) :=
Eval hnf in CountType _ (finfun_countMixin aT rT).
Canonical Structure finfun_of_countType (aT : finType) (rT : countType) :=
Eval hnf in [countType of {ffun aT -> rT}].
Canonical Structure finfun_subCountType aT (rT : countType) :=
Eval hnf in [subCountType of finfun_type aT rT].
Canonical Structure finfun_of_subCountType (aT : finType) (rT : countType) :=
Eval hnf in [subCountType of {ffun aT -> rT}].
Section FinTheory.
Variables aT rT : finType.
Notation fT := {ffun aT -> rT}.
Notation ffT := (finfun_type aT rT).
Definition finfun_finMixin := [finMixin of ffT by <:].
Canonical Structure finfun_finType := Eval hnf in FinType ffT finfun_finMixin.
Canonical Structure finfun_subFinType := Eval hnf in [subFinType of ffT].
Canonical Structure finfun_of_finType := Eval hnf in [finType of fT for finfun_finType].
Canonical Structure finfun_of_subFinType := Eval hnf in [subFinType of fT].
Lemma card_pfamily : forall y0 d (F : aT -> pred rT),
#|pfamily y0 d F| = foldr (fun x m => #|F x| * m) 1 (enum d).
Lemma card_family : forall F : aT -> pred rT,
#|family F| = foldr (fun x m => #|F x| * m) 1 (enum aT).
Lemma card_pffun_on : forall y0 d r, #|pffun_on y0 d r| = #|r| ^ #|d|.
Lemma card_ffun_on : forall r, #|ffun_on r| = #|r| ^ #|aT|.
Lemma card_ffun : #|fT| = #|rT| ^ #|aT|.
End FinTheory.
Section FinPowerSet.
Variable eT : finType.
Variable A : pred eT.
Definition powerset := pffun_on false A predT.
Lemma card_powerset : #|powerset| = 2 ^ #|A|.
End FinPowerSet.