(Joint Center)Library MathComp.finfun

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple.

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 ot 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 (aTrT) := 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 finexp_domFinType n := ordinal_finType n.
Notation "T ^ n" := (@finfun_of (finexp_domFinType n) T (Phant _)) : type_scope.

Notation Local fun_of_fin_def :=
  (fun aT rT f xtnth (@fgraph aT rT f) (enum_rank x)).

Notation Local finfun_def := (fun aT rT f ⇒ @Finfun aT rT (codom_tuple f)).

Module Type FunFinfunSig.
Parameter fun_of_fin : aT rT, finfun_type aT rTaTrT.
Parameter finfun : (aT : finType) rT, (aTrT) → {ffun aTrT}.
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 : aTF))
  (at level 0, x ident, only parsing) : fun_scope.

Notation "[ 'ffun' : aT => F ]" := (finfun (fun _ : aTF))
  (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.
Definition fmem aT rT (pT : predType rT) (f : aTpT) := [fun x mem (f x)].

Lemmas on the correspondance between finfun_type and CiC functions.
Section PlainTheory.

Variables (aT : finType) (rT : Type).
Notation fT := {ffun aTrT}.
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 : aTrT) : 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 : aTpT) 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)).

Implicit Arguments familyP [aT rT pT F f].
Implicit Arguments ffun_onP [aT rT R f].

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 : aTrT) := [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 aTrT}.
Implicit Types (y : rT) (D : pred aT) (R : pred rT) (f : fT).

Lemma supportP y D g :
  reflect ( x, x \notin Dg 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 : aTmem_pred rT) :=
  family (fun i : aTif in_mem i mD then pred_of_simpl (mF i) else pred1 y).

Lemma pfamilyP (pT : predType rT) y D (F : aTpT) 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.
Canonical exp_eqType (T : eqType) n := [eqType of T ^ n].

Implicit Arguments supportP [aT rT y D g].
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 aTrT}].
Canonical exp_choiceType (T : choiceType) n := [choiceType of T ^ n].

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 aTrT}].
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 aTrT}].

Section FinTheory.

Variables aT rT : finType.
Notation fT := {ffun aTrT}.
Notation ffT := (finfun_type aT rT).
Implicit Types (D : pred aT) (R : pred rT) (F : aTpred 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.
Canonical exp_finType (T : finType) n := [finType of T ^ n].