- -

Library mathcomp.ssreflect.finfun

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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 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. - 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 : aT → Type).
- -
-Inductive finfun_on : seq aT → Type :=
-| finfun_nil : finfun_on [::]
-| finfun_cons x s of rT x & finfun_on s : finfun_on (x :: s).
- -
- -
- -
-Variant finfun_of (ph : phant (∀ x, rT x)) : predArgType :=
-  FinfunOf of finfun_on (enum aT).
- -
-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.
- -
-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.
- -
-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 FinfunDefSig.
-Parameter finfun : ∀ aT rT, finPi aT rT → {ffun finPi aT rT }.
-Axiom finfunE : finfun = finfun_def.
-End FinfunDefSig.
- -
-Module FinfunDef : FinfunDefSig.
-Definition finfun := finfun_def.
-Lemma finfunE : finfun = finfun_def.
-End FinfunDef.
- -
-Notation finfun := FinfunDef.finfun.
-Canonical finfun_unlock := Unlockable FinfunDef.finfunE.
- -
-Notation "[ 'ffun' x : aT => E ]" := (finfun (fun x : aT ⇒ E))
-  (at level 0, x ident) : fun_scope.
- -
-Notation "[ 'ffun' x => E ]" := (@finfun _ (fun ⇒ _) (fun x ⇒ E))
-  (at level 0, x ident, format "[ 'ffun' x => E ]") : fun_scope.
- -
-Notation "[ 'ffun' => E ]" := [ffun _ ⇒ E]
-  (at level 0, format "[ 'ffun' => E ]") : fun_scope.
- -
-(* Example outcommented.
-(**  Examples of using finite functions as containers in recursive inductive
- types, and making use of the fact that the type and accessor are
- structurally positive and decreasing, respectively.                         **)
-Unset Elimination Schemes.
-Inductive tree := node n of tree ^ n.
-Fixpoint size t := let: node n f := t in sumn (codom (size \o f)) + 1.
-Example tree_step (K : tree -> Type) :=
-  forall n st (t := node st) & forall i : 'I_n, K (st i), K t.
-Example tree_rect K (Kstep : tree_step K) : forall t, K t.
-Proof. by fix IHt 1 => -n st; apply/Kstep=> i; apply: IHt. Defined.
-
-(**  An artificial example use of dependent functions.                           **)
-Inductive tri_tree n := tri_row of {ffun forall i : 'I_n, tri_tree i}.
-Fixpoint tri_size n (t : tri_tree n) :=
-  let: tri_row f := t in sumn seq tri_size (f i) | i : 'I_n + 1.
-Example tri_tree_step (K : forall n, tri_tree n -> Type) :=
-  forall n st (t := tri_row st) & forall i : 'I_n, K i (st i), K n t.
-Example tri_tree_rect K (Kstep : tri_tree_step K) : forall n t, K n t.
-Proof. by fix IHt 2 => n st; apply/Kstep=> i; apply: IHt. Defined.
-Set Elimination Schemes.
-(**  End example. *)  **)
- -
-

- -

- The correspondance between finfun_of and CiC dependent functions. -

-Section DepPlainTheory.
-Variables (aT : finType) (rT : aT → Type).
-Notation fT := {ffun finPi aT rT }.
-Implicit Type f : fT.
- -
-Fact ffun0 (aT0 : #|aT | = 0) : fT.
- -
-Lemma ffunE g x : (finfun g : fT) x = g x.
- -
-Lemma ffunP (f1 f2 : fT) : (∀ x, f1 x = f2 x ) ↔ f1 = f2.
- -
-Lemma ffunK : @cancel (finPi aT rT) fT fun_of_fin finfun.
- -
-Lemma eq_dffun (g1 g2 : ∀ x, rT x) :
- (∀ x, g1 x = g2 x ) → finfun g1 = finfun g2.
- -
-Definition total_fun g x := Tagged rT (g x : rT x).
- -
-Definition tfgraph f := codom_tuple (total_fun f).
- -
-Lemma codom_tffun f : codom (total_fun f) = tfgraph f.
- -
- -
- -
-Lemma tfgraph_inj : injective tfgraph.
- -
-Definition family_mem mF := [pred f : fT | [∀ x, in_mem (f x) (mF x)]].
- -
-Variables (pT : ∀ x, predType (rT x)) (F : ∀ x, pT x).
- -
-

- -

- Helper for defining notation for function families. -

- -
-Lemma familyP f : reflect (∀ x, f x \in F x) (f \in family_mem (fmem F)).
- -
-End DepPlainTheory.
- -
- -
-Notation family F := (family_mem (fmem F)).
- -
-Section InheritedStructures.
- -
-Variable aT : finType.
-Notation dffun_aT rT rS := {dffun ∀ x : aT, rT x : rS}.
- -
- Canonical finfun_eqType (rT : eqType) :=
-  EqType {ffun aT → rT } (eqMixin (fun ⇒ rT)).
-Canonical dfinfun_eqType rT :=
-  EqType (dffun_aT rT eqType) (eqMixin rT).
- -
- Canonical finfun_choiceType (rT : choiceType) :=
-  ChoiceType {ffun aT → rT } (choiceMixin (fun ⇒ rT)).
-Canonical dfinfun_choiceType rT :=
-  ChoiceType (dffun_aT rT choiceType) (choiceMixin rT).
- -
- Canonical finfun_countType (rT : countType) :=
-  CountType {ffun aT → rT } (countMixin (fun ⇒ rT)).
-Canonical dfinfun_countType rT :=
-  CountType (dffun_aT rT countType) (countMixin rT).
- -
-Canonical finfun_finType (rT : finType) :=
-  FinType {ffun aT → rT } (finMixin (fun ⇒ rT)).
-Canonical dfinfun_finType rT :=
-  FinType (dffun_aT rT finType) (finMixin rT).
- -
-End InheritedStructures.
- -
-Section FunPlainTheory.
- -
-Variables (aT : finType) (rT : Type).
-Notation fT := {ffun aT → rT }.
-Implicit Types (f : fT) (R : pred rT).
- -
-Definition fgraph f := codom_tuple f.
- -
-Definition Finfun (G : #|aT |.-tuple rT) := [ffun x ⇒ tnth G (enum_rank x)].
- -
-Lemma tnth_fgraph f i : tnth (fgraph f) i = f (enum_val i).
- -
-Lemma FinfunK : cancel Finfun fgraph.
- -
-Lemma fgraphK : cancel fgraph Finfun.
- -
-Lemma fgraph_ffun0 aT0 : fgraph (ffun0 aT0) = nil :> seq rT.
- -
-Lemma codom_ffun f : codom f = fgraph f.
- -
-Lemma tagged_tfgraph f : @map _ rT tagged (tfgraph f) = fgraph f.
- -
-Lemma eq_ffun (g1 g2 : aT → rT) : g1 =1 g2 → finfun g1 = finfun g2.
- -
-Lemma fgraph_codom f : fgraph f = codom_tuple f.
- -
-Definition ffun_on_mem (mR : mem_pred rT) := family_mem (fun _ : aT ⇒ mR).
- -
-Lemma ffun_onP R f : reflect (∀ x, f x \in R) (f \in ffun_on_mem (mem R)).
- -
-End FunPlainTheory.
- -
- -
-Notation ffun_on R := (ffun_on_mem _ (mem R)).
-Notation "@ 'ffun_on' aT R" :=
-  (ffun_on R : simpl_pred (finfun_of (Phant (aT → id _))))
-  (at level 10, aT, R at level 9).
- -
-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 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) (fmem F)).
-Notation pffun_on y D R := (pffun_on_mem y (mem D) (mem R)).
- -
-Section FinDepTheory.
- -
-Variables (aT : finType) (rT : aT → finType).
-Notation fT := {dffun ∀ x : aT, rT x }.
- -
-Lemma card_family (F : ∀ x, pred (rT x)) :
-  #|(family F : simpl_pred fT )| = foldr muln 1 [seq #|F x | | x : aT ].
- -
-Lemma card_dep_ffun : #|fT | = foldr muln 1 [seq #|rT x | | x : aT ].
- -
-End FinDepTheory.
- -
-Section FinFunTheory.
- -
-Variables aT rT : finType.
-Notation fT := {ffun aT → rT }.
-Implicit Types (D : {pred aT }) (R : {pred rT }) (F : aT → pred rT).
- -
-Lemma card_pfamily y0 D F :
-  #|pfamily y0 D F | = foldr muln 1 [seq #|F x | | x in D ].
- -
-Lemma card_pffun_on y0 D R : #|pffun_on y0 D R | = #|R | ^ #|D |.
- -
-Lemma card_ffun_on R : #|@ffun_on aT R | = #|R | ^ #|aT |.
- -
-Lemma card_ffun : #|fT | = #|rT | ^ #|aT |.
- -
-End FinFunTheory.
-