Library finfun

Representation of Finite Functions


Require Import ssreflect.

Require Import ssrbool.

Require Import ssrfun.

Require Import eqtype.

Require Import seq.

Require Import fintype.

Require Import ssrnat.

Require Import general.




Set Implicit Arguments.

Unset Strict Implicit.

Import Prenex Implicits.




Section FGraph.




Variable d1: finType.

Variable d2: eqType.

Represent finite functions by their graphs


Inductive fgraphType: Type := 

  Fgraph (val: seq d2) (fgraph_sizeP: size val = card d1): fgraphType.

This definition was proposed in Gonthier, Mahboubi, Rideau, Tassi, Thery -- A modular formalisation of finite group theory. (The rest of this file is our own development, however, since we did not have access to the sources of their development.)





Implicit Arguments Fgraph [].

Converting functions to their graph


Definition fgraph_of_fun: (d1 -> d2) -> fgraphType.

Proof.

move=> f.

apply: (nosimpl (Fgraph (maps f (enum d1)))); rewrite cardA; apply: size_maps.

Defined.

Reconstructing the function from a graph


Definition fun_of_fgraph: fgraphType -> (d1 -> d2).

Proof.

move => [val H] x.

apply (fun y =>  sub y val (index x (enum d1))).

by rewrite cardA in H; case: val H =>//=; case: (enum d1) (mem_enum x) =>//=.

Defined.




Coercion fun_of_fgraph: fgraphType >-> Funclass.




Definition fval(f:fgraphType):= match f with Fgraph val _ => val end.




Lemma fval_eq: forall f g, (fval f) = (fval g) -> f = g.

Proof.

move => [valf H] [valg K] /=E; elim: E H K => H K.

by rewrite (eq_irrelevance H K).

Qed.

Correctness of the representation


Lemma fgraph_fun_eq: forall f, (fgraph_of_fun f) =1 f.

Proof.

move=>f x//=.

rewrite (fun y:d2 => sub_maps x y f (s:=(enum d1)) (n:=index x (enum d1))).

rewrite sub_index =>//; exact (mem_enum x).

rewrite index_mem; exact (mem_enum x).

Qed.

The next two lemmas show that intensional equality on the representation is the same as extensional equality on functions.


Lemma fgraph_of_fun_congr: forall f g, 

  f =1 g -> (fgraph_of_fun f = fgraph_of_fun g).

Proof.

move=> f g E.

have H:(fval (fgraph_of_fun f) = fval (fgraph_of_fun g)) =>//=.

  elim: (enum d1) =>//=.

  move=> x s H; elim (E x); elim: H=>//=.

apply (fval_eq H).

Qed.




Lemma fgraph_of_fun_inj: forall f g, 

  (fgraph_of_fun f = fgraph_of_fun g) ->  f =1 g.

Proof.

move=> f g E x.

by rewrite -(fgraph_fun_eq f) -(fgraph_fun_eq g) E.

Qed.




End FGraph.

Finite functions have decidable and extensional equality


Section FGraphData.




Variable d1 : finType.

Variable d2 : eqType.




Definition eqfgraph(f g: fgraphType d1 d2) := (fval f) == (fval g).




Lemma eqfgraphPx: reflect_eq eqfgraph.

Proof.

case=>[vf Hf]; case=>[vg Hg]; rewrite /eqfgraph /fval.

elim: (@eqP _ vf vg) Hf Hg => [-> Hf Hg | I Hf Hg]; apply: (iffP idP)=>//.

by rewrite (eq_irrelevance Hf Hg). by case.

Qed.




Canonical Structure funData := EqType eqfgraphPx.




Lemma fgraph_of_fun_surj: forall f, f == fgraph_of_fun (fun_of_fgraph f).

Proof.

move=>f.

apply/eqP; apply: fval_eq.

case U: f=>[v vm]//.

rewrite [fun_of_fgraph]lock /fval /fgraph_of_fun /= -lock /fun_of_fgraph.

apply: (@maps_sub_index d1 d2 v (enum d1) (fun x=>_)).

by rewrite vm cardA.

by move=>x; rewrite FinType.enumP.

Qed.

Two function graphs are equal if and only if the functions induced by them are extensionally equal.


Lemma eq_finfun: forall f g:funData, f =1 g -> f == g.

Proof.

by move=>f g E;

rewrite (eqP (fgraph_of_fun_surj f)) (eqP (fgraph_of_fun_surj g));

apply/eqP; apply: fgraph_of_fun_congr.

Qed.




End FGraphData.




Opaque fgraph_of_fun.

Finite Function Spaces form a Finite Type


Section FinFun.




Variable d1 d2 : finType.

Construct an enumeration of all graphs of function from d1 to d2.





Fixpoint adds_all(ys:seq d2) (ls:seq (seq_eqType d2)) {struct ls}: seq (seq_eqType d2) :=

  match ls with

  | Seq0 => seq0

  | Adds l ls' => cat (maps (fun y=> Adds y l) ys) (adds_all ys ls')

  end.




Lemma count_adds_all: forall ys (y:d2) ls (l:seq_eqType d2), 

   count (pred1 (Adds y l)) (adds_all ys ls) = ((count (pred1 y) ys) * (count (pred1 l) ls)).

Proof.

move=>ys y ls l.

elim: ls=>[|l' ls' IH]/=; first by rewrite muln0.

rewrite count_cat IH; clear IH.

elim: (@eqP _ l l') => [E|I].

have L: count (pred1 y) ys = count (pred1 (Adds y l)) (maps (fun y=> Adds y l) ys)

    by elim: ys=>[|y' ys' IH]//=; rewrite eqseq_adds eq_refl andbT IH.

  by rewrite -E -L muln_addr muln1.

have L:  count (pred1 (Adds y l)) (maps (fun y=> Adds y l') ys) = 0.

  by elim: ys=>[|y' ys' IH]//=; rewrite eqseq_adds; 

     elim: (@eqP _ l l') => [| _ ]//=; rewrite andbF; apply IH.

by rewrite L.

Qed.




Lemma size_adds_all: forall ys ls, size (adds_all ys ls) = ((size ls) * (size ys)).

Proof. by move=>ys; elim=>[|l ls IH]//=;rewrite size_cat size_maps IH. Qed.




Lemma maps_adds_size: forall (ys:seq d2) l l', (maps (fun y=> Adds y l) ys) l' -> (size l') = S (size l).

Proof.

elim=>[|y ys' IH l l' /=H]//=.

elim: (orP H)=>[C1|C2]; first by rewrite -(eqP C1).

by apply IH; apply C2.

Qed.






Fixpoint all_seq(n:nat) {struct n}: seq (seq_eqType d2) :=

  match n with

  | 0 => Adds seq0 seq0

  | S n' => adds_all (enum d2) (all_seq n')

  end.




Lemma size_all_seq: forall n, (size (all_seq n)) = exp (card d2) n.

Proof. by elim=>[|n IH]//=; rewrite size_adds_all IH cardA mulnC. Qed.




Lemma all_seq_elem_size: forall n l, (all_seq n l) -> (size l = n).

elim=>/=[H K|n H l K]; first by elim: (orP K)=>[L|F]//=; rewrite -(eqP L).

elim: (all_seq n) H K=>//=[l' ls' H K].

rewrite mem_cat.

case/orP=>[C1|C2].

  have E: (size l'=n) by apply K; rewrite /predU1 eq_refl.

  by rewrite -E; apply (maps_adds_size C1).

  by apply H=>//U E; apply K; first by case: E=>[E]; by rewrite /predU1 E orbT.

Qed.




Lemma count1_all_seq: forall l, count (pred1 l) (all_seq (size l)) = 1.

Proof. by elim=> //=l' ls' IH;rewrite count_adds_all IH FinType.enumP. Qed.




Definition fgraph_enum_val:= (all_seq (size (enum d1))).




Definition fgraph_enum_lenP: forall l, fgraph_enum_val l -> size l = (size (enum d1)).

move=>l H. by apply all_seq_elem_size.

Defined.




Definition fgraph_enum_dep: { x:seq (funData d1 d2) | maps (@fval d1 d2) x = (all_seq (size (enum d1))) }.

set n:=(size (enum d1)).

have I: forall l, (all_seq n) l -> size l = n by apply all_seq_elem_size.

elim: (all_seq n) I=>[I|vl vls IH I].

  by exists (Seq0 (funData d1 d2)).

  have K: size vl = n. by apply I; rewrite mem_adds /predU1 eq_refl//=.

  have IHa: forall l, vls l -> size l = n.

    by move=>l L; apply I=>//=; rewrite /predU1 L orbT.

  elim: (IH IHa)=>[x xP].

  by exists (Adds (@Fgraph d1 d2 vl K) x); rewrite /= xP.

Defined.




Definition fgraph_enum: seq (funData d1 d2).

elim: fgraph_enum_dep=>[x _]; exact x.

Defined.




Lemma maps_val_fgraph_enum: maps (@fval d1 d2) fgraph_enum = (all_seq (size (enum d1))).

Proof. by rewrite /fgraph_enum; elim fgraph_enum_dep. Qed.




Lemma fgraph_enumP: forall x:fgraphType d1 d2, count (pred1 x) fgraph_enum = 1.

Proof.

move=>x.

have U: (count (pred1 x) fgraph_enum = count (pred1 (@fval d1 d2 x)) (maps (@fval d1 d2) fgraph_enum)).

by rewrite count_maps; apply eq_count=>//=.

have V:(maps (@fval d1 d2) fgraph_enum = (all_seq (size (enum d1)))).

  by rewrite /fgraph_enum; elim fgraph_enum_dep => [y yP].

rewrite V in U.

have W: (size (fval x) = size (enum d1)) by elim x=>//=.

rewrite -W count1_all_seq in U.

apply U.

Qed.




Canonical Structure finFun := FinType fgraph_enumP.




End FinFun.

Cardinality of Finite Function Spaces


Section CardFinFun.




Variable d1 d2 : finType.




Lemma card_finFun: card (finFun d1 d2) = exp (card d2) (card d1).

Proof.

rewrite !cardA /enum =>//=.

have U: (size (maps (@fval d1 d2) (fgraph_enum d1 d2)) =  size (all_seq d2 (size (enum d1)))).

by rewrite maps_val_fgraph_enum.

by rewrite size_maps size_all_seq in U.

Qed.




Lemma card_sub_fin : forall a:pred d1, card (sub_finType a) = card a.

Proof.

move=>a.

by apply: card_sub.

Qed.




End CardFinFun.




Unset Implicit Arguments.