Library mathcomp.ssreflect.finfun
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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.
+ (T ^ n)%type is notation for {ffun 'I_n -> T}, which is isomorphic
+ to n.-tuple T.
+ 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)
+ f \in ffun_on R == the range of f is a subset of R
+ f \in family F == f belongs to the family F (f x \in F x for all x)
+ 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.
+
+
+
+
+Set Implicit Arguments.
+ +
+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 finfun_subType := Eval hnf in [newType for fgraph].
+ +
+End Def.
+ +
+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.
+ +
+ +
+ +
+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 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.
+Coercion fun_of_fin : finfun_type >-> Funclass.
+Canonical fun_of_fin_unlock := Unlockable FunFinfun.fun_of_finE.
+Canonical 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.
+ +
+
+
++Set Implicit Arguments.
+ +
+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 finfun_subType := Eval hnf in [newType for fgraph].
+ +
+End Def.
+ +
+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.
+ +
+ +
+ +
+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 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.
+Coercion fun_of_fin : finfun_type >-> Funclass.
+Canonical fun_of_fin_unlock := Unlockable FunFinfun.fun_of_finE.
+Canonical 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.
+ +
+
+ Helper for defining notation for function families.
+
+
+
+
+ Lemmas on the correspondance between finfun_type and CiC functions.
+
+
+Section PlainTheory.
+ +
+Variables (aT : finType) (rT : Type).
+Notation fT := {ffun aT → rT}.
+Implicit Types (f : fT) (R : pred rT).
+ +
+Canonical finfun_of_subType := Eval hnf in [subType of fT].
+ +
+Lemma tnth_fgraph f i : tnth (fgraph f) i = f (enum_val i).
+ +
+Lemma ffunE (g : aT → rT) : finfun g =1 g.
+ +
+Lemma fgraph_codom f : fgraph f = codom_tuple f.
+ +
+Lemma codom_ffun f : codom f = val f.
+ +
+Lemma ffunP f1 f2 : f1 =1 f2 ↔ f1 = f2.
+ +
+Lemma ffunK : cancel (@fun_of_fin aT rT) (@finfun aT rT).
+ +
+Definition family_mem mF := [pred f : fT | [∀ x, in_mem (f x) (mF x)]].
+ +
+Lemma familyP (pT : predType rT) (F : aT → pT) f :
+ reflect (∀ x, f x \in F x) (f \in family_mem (fmem F)).
+ +
+Definition ffun_on_mem mR := family_mem (fun _ ⇒ mR).
+ +
+Lemma ffun_onP R f : reflect (∀ x, f x \in R) (f \in ffun_on_mem (mem R)).
+ +
+End PlainTheory.
+ +
+Notation family F := (family_mem (fun_of_simpl (fmem F))).
+Notation ffun_on R := (ffun_on_mem _ (mem R)).
+ +
+ +
+Lemma nth_fgraph_ord T n (x0 : T) (i : 'I_n) f : nth x0 (fgraph f) i = f i.
+ +
+Section Support.
+ +
+Variables (aT : Type) (rT : eqType).
+ +
+Definition support_for y (f : aT → rT) := [pred x | f x != y].
+ +
+Lemma supportE x y f : (x \in support_for y f) = (f x != y).
+ +
+End Support.
+ +
+Notation "y .-support" := (support_for y)
+ (at level 2, format "y .-support") : fun_scope.
+ +
+Section EqTheory.
+ +
+Variables (aT : finType) (rT : eqType).
+Notation fT := {ffun aT → rT}.
+Implicit Types (y : rT) (D : pred aT) (R : pred rT) (f : fT).
+ +
+Lemma supportP y D g :
+ reflect (∀ x, x \notin D → g x = y) (y.-support g \subset D).
+ +
+Definition finfun_eqMixin :=
+ Eval hnf in [eqMixin of finfun_type aT rT by <:].
+Canonical finfun_eqType := Eval hnf in EqType _ finfun_eqMixin.
+Canonical finfun_of_eqType := Eval hnf in [eqType of fT].
+ +
+Definition pfamily_mem y mD (mF : aT → mem_pred rT) :=
+ family (fun i : aT ⇒ if in_mem i mD then pred_of_simpl (mF i) else pred1 y).
+ +
+Lemma pfamilyP (pT : predType rT) y D (F : aT → pT) f :
+ reflect (y.-support f \subset D ∧ {in D, ∀ x, f x \in F x})
+ (f \in pfamily_mem y (mem D) (fmem F)).
+ +
+Definition pffun_on_mem y mD mR := pfamily_mem y mD (fun _ ⇒ mR).
+ +
+Lemma pffun_onP y D R f :
+ reflect (y.-support f \subset D ∧ {subset image f D ≤ R})
+ (f \in pffun_on_mem y (mem D) (mem R)).
+ +
+End EqTheory.
+ +
+Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))).
+Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)).
+ +
+Definition finfun_choiceMixin aT (rT : choiceType) :=
+ [choiceMixin of finfun_type aT rT by <:].
+Canonical finfun_choiceType aT rT :=
+ Eval hnf in ChoiceType _ (finfun_choiceMixin aT rT).
+Canonical 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 finfun_countType aT (rT : countType) :=
+ Eval hnf in CountType _ (finfun_countMixin aT rT).
+Canonical finfun_of_countType (aT : finType) (rT : countType) :=
+ Eval hnf in [countType of {ffun aT → rT}].
+Canonical finfun_subCountType aT (rT : countType) :=
+ Eval hnf in [subCountType of finfun_type aT rT].
+Canonical 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).
+Implicit Types (D : pred aT) (R : pred rT) (F : aT → pred rT).
+ +
+Definition finfun_finMixin := [finMixin of ffT by <:].
+Canonical finfun_finType := Eval hnf in FinType ffT finfun_finMixin.
+Canonical finfun_subFinType := Eval hnf in [subFinType of ffT].
+Canonical finfun_of_finType := Eval hnf in [finType of fT for finfun_finType].
+Canonical finfun_of_subFinType := Eval hnf in [subFinType of fT].
+ +
+Lemma card_pfamily y0 D F :
+ #|pfamily y0 D F| = foldr muln 1 [seq #|F x| | x in D].
+ +
+Lemma card_family F : #|family F| = foldr muln 1 [seq #|F x| | x : aT].
+ +
+Lemma card_pffun_on y0 D R : #|pffun_on y0 D R| = #|R| ^ #|D|.
+ +
+Lemma card_ffun_on R : #|ffun_on R| = #|R| ^ #|aT|.
+ +
+Lemma card_ffun : #|fT| = #|rT| ^ #|aT|.
+ +
+End FinTheory.
+ +
+
++ +
+Variables (aT : finType) (rT : Type).
+Notation fT := {ffun aT → rT}.
+Implicit Types (f : fT) (R : pred rT).
+ +
+Canonical finfun_of_subType := Eval hnf in [subType of fT].
+ +
+Lemma tnth_fgraph f i : tnth (fgraph f) i = f (enum_val i).
+ +
+Lemma ffunE (g : aT → rT) : finfun g =1 g.
+ +
+Lemma fgraph_codom f : fgraph f = codom_tuple f.
+ +
+Lemma codom_ffun f : codom f = val f.
+ +
+Lemma ffunP f1 f2 : f1 =1 f2 ↔ f1 = f2.
+ +
+Lemma ffunK : cancel (@fun_of_fin aT rT) (@finfun aT rT).
+ +
+Definition family_mem mF := [pred f : fT | [∀ x, in_mem (f x) (mF x)]].
+ +
+Lemma familyP (pT : predType rT) (F : aT → pT) f :
+ reflect (∀ x, f x \in F x) (f \in family_mem (fmem F)).
+ +
+Definition ffun_on_mem mR := family_mem (fun _ ⇒ mR).
+ +
+Lemma ffun_onP R f : reflect (∀ x, f x \in R) (f \in ffun_on_mem (mem R)).
+ +
+End PlainTheory.
+ +
+Notation family F := (family_mem (fun_of_simpl (fmem F))).
+Notation ffun_on R := (ffun_on_mem _ (mem R)).
+ +
+ +
+Lemma nth_fgraph_ord T n (x0 : T) (i : 'I_n) f : nth x0 (fgraph f) i = f i.
+ +
+Section Support.
+ +
+Variables (aT : Type) (rT : eqType).
+ +
+Definition support_for y (f : aT → rT) := [pred x | f x != y].
+ +
+Lemma supportE x y f : (x \in support_for y f) = (f x != y).
+ +
+End Support.
+ +
+Notation "y .-support" := (support_for y)
+ (at level 2, format "y .-support") : fun_scope.
+ +
+Section EqTheory.
+ +
+Variables (aT : finType) (rT : eqType).
+Notation fT := {ffun aT → rT}.
+Implicit Types (y : rT) (D : pred aT) (R : pred rT) (f : fT).
+ +
+Lemma supportP y D g :
+ reflect (∀ x, x \notin D → g x = y) (y.-support g \subset D).
+ +
+Definition finfun_eqMixin :=
+ Eval hnf in [eqMixin of finfun_type aT rT by <:].
+Canonical finfun_eqType := Eval hnf in EqType _ finfun_eqMixin.
+Canonical finfun_of_eqType := Eval hnf in [eqType of fT].
+ +
+Definition pfamily_mem y mD (mF : aT → mem_pred rT) :=
+ family (fun i : aT ⇒ if in_mem i mD then pred_of_simpl (mF i) else pred1 y).
+ +
+Lemma pfamilyP (pT : predType rT) y D (F : aT → pT) f :
+ reflect (y.-support f \subset D ∧ {in D, ∀ x, f x \in F x})
+ (f \in pfamily_mem y (mem D) (fmem F)).
+ +
+Definition pffun_on_mem y mD mR := pfamily_mem y mD (fun _ ⇒ mR).
+ +
+Lemma pffun_onP y D R f :
+ reflect (y.-support f \subset D ∧ {subset image f D ≤ R})
+ (f \in pffun_on_mem y (mem D) (mem R)).
+ +
+End EqTheory.
+ +
+Notation pfamily y D F := (pfamily_mem y (mem D) (fun_of_simpl (fmem F))).
+Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)).
+ +
+Definition finfun_choiceMixin aT (rT : choiceType) :=
+ [choiceMixin of finfun_type aT rT by <:].
+Canonical finfun_choiceType aT rT :=
+ Eval hnf in ChoiceType _ (finfun_choiceMixin aT rT).
+Canonical 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 finfun_countType aT (rT : countType) :=
+ Eval hnf in CountType _ (finfun_countMixin aT rT).
+Canonical finfun_of_countType (aT : finType) (rT : countType) :=
+ Eval hnf in [countType of {ffun aT → rT}].
+Canonical finfun_subCountType aT (rT : countType) :=
+ Eval hnf in [subCountType of finfun_type aT rT].
+Canonical 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).
+Implicit Types (D : pred aT) (R : pred rT) (F : aT → pred rT).
+ +
+Definition finfun_finMixin := [finMixin of ffT by <:].
+Canonical finfun_finType := Eval hnf in FinType ffT finfun_finMixin.
+Canonical finfun_subFinType := Eval hnf in [subFinType of ffT].
+Canonical finfun_of_finType := Eval hnf in [finType of fT for finfun_finType].
+Canonical finfun_of_subFinType := Eval hnf in [subFinType of fT].
+ +
+Lemma card_pfamily y0 D F :
+ #|pfamily y0 D F| = foldr muln 1 [seq #|F x| | x in D].
+ +
+Lemma card_family F : #|family F| = foldr muln 1 [seq #|F x| | x : aT].
+ +
+Lemma card_pffun_on y0 D R : #|pffun_on y0 D R| = #|R| ^ #|D|.
+ +
+Lemma card_ffun_on R : #|ffun_on R| = #|R| ^ #|aT|.
+ +
+Lemma card_ffun : #|fT| = #|rT| ^ #|aT|.
+ +
+End FinTheory.
+ +
+