Module mathcomp.boot.finfun

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype tuple.

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.
   fcat f g == concatenation of f : T ^ n and g : T ^ m as a finfun
              of type T ^ (n + m)
  {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 additional 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.
      fprod I T_ == alternative construct to {ffun forall i : I, T_ i} for
                    the finite product of finTypes, in a set-theoretic way
                 := Record fprod I T_ := FProd
                    { fprod_fun : {ffun I -> {i : I & T_ i}} ;
                    fprod_prop : [forall i : I, tag (fprod_fun i) == i] }.
fprod I T_ is endowed with a finType structure and allow these operations:
[fprod i : I => F] == the dependent fprod function built from fun i:I => F
                   := fprod_of_fun (fun i : I => F)
  [fprod : I => F] == [fprod _ : I => F]
    [fprod i => F] == [fprod i : _ => F]
      [fprod => F] == [fprod _ : _ => F]
These fprod terms coerce into vanilla dependent functions via the coercion
       fun_of_fprod I T_ : fprod I T_ -> (forall i : I, T_ i).
We also define the mutual bijections:
          fprod_of_dffun : {dffun forall i : I, T_ i} -> fprod I T_
          dffun_of_fprod : fprod I T_ -> {dffun forall i : I, T_ i}
   of_family_tagged_with : {x in family (tagged_with T_)} -> fprod I T_
   to_family_tagged_with : fprod I T_ -> {x in family (tagged_with T_)}

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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).

Local Fixpoint finfun_rec (g : forall x, rT x) s : finfun_on s :=
  if s is x1 :: s1 then finfun_cons (g x1) (finfun_rec g s1) else finfun_nil.

Local Fixpoint fun_of_fin_rec x s (f_s : finfun_on s) : x \in s -> rT x :=
  if f_s is finfun_cons x1 s1 y1 f_s1 then
    if eqP is ReflectT Dx in reflect _ Dxb return Dxb || (x \in s1) -> rT x then
      fun=> ecast x (rT x) (esym Dx) y1
    else fun_of_fin_rec f_s1
  else fun isF => False_rect (rT x) (notF isF).

Variant finfun_of (ph : phant (forall 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.
Arguments fun_of_fin {aT rT ph} f x.

Notation "{ 'ffun' fT }" := (finfun_of (Phant fT))
  (format "{ 'ffun' '[hv' fT ']' }") : type_scope.

Notation "{ 'dffun' fT }" := (dfinfun_of (Phant fT))
  (format "{ 'dffun' '[hv' fT ']' }") : type_scope.

Definition exp_finIndexType n : finType := 'I_n.
Notation "T ^ n" :=
  (@finfun_of (exp_finIndexType n) (fun=> T) (Phant _)) : type_scope.

Local Notation finPi aT rT := (forall x : Finite.sort aT, rT x) (only parsing).

HB.lock Definition finfun aT rT g :=
  FinfunOf (Phant (finPi aT rT)) (finfun_rec g (enum aT)).
Canonical finfun_unlock := Unlockable finfun.unlock.
Arguments finfun {aT rT} g.

Notation "[ 'ffun' x : aT => E ]" := (finfun (fun x : aT => E))
  (x name) : function_scope.

Notation "[ 'ffun' x => E ]" := (@finfun _ (fun=> _) (fun x => E))
  (x name, format "[ 'ffun' x => E ]") : function_scope.

Notation "[ 'ffun' => E ]" := [ffun _ => E]
  (format "[ 'ffun' => E ]") : function_scope.

Section DepPlainTheory.
Variables (aT : finType) (rT : aT -> Type).
Notation fT := {ffun finPi aT rT}.
Implicit Type f : fT.

Fact ffun0 (aT0 : #|aT| = 0) : fT.

Proof.

by apply/finfun=> x; have:= card0_eq aT0 x. Qed.

Lemma ffunE g x : (finfun g : fT) x = g x.

Proof.

rewrite unlock /=; set s := enum aT; set s_x : mem_seq s x := mem_enum _ _.
by elim: s s_x => //= x1 s IHs; case: eqP => [|_]; [case: x1 / | apply: IHs].
Qed.

Lemma ffunP (f1 f2 : fT) : (forall x, f1 x = f2 x) <-> f1 = f2.

Proof.

suffices ffunK f g: (forall x, f x = g x) -> f = finfun g.
by split=> [/ffunK|] -> //; apply/esym/ffunK.
case: f => f Dg; rewrite unlock; congr FinfunOf.
have{} Dg x (aTx : mem_seq (enum aT) x): g x = fun_of_fin_rec f aTx.
by rewrite -Dg /= (bool_irrelevance (mem_enum _ _) aTx).
elim: (enum aT) / f (enum_uniq aT) => //= x1 s y f IHf /andP[s'x1 Us] in Dg *.
rewrite Dg ?eqxx //=; case: eqP => // /eq_axiomK-> /= _.
rewrite {}IHf // => x s_x; rewrite Dg ?s_x ?orbT //.
by case: eqP (memPn s'x1 x s_x) => // _ _ /(bool_irrelevance s_x) <-.
Qed.

Lemma ffunK : @cancel (finPi aT rT) fT fun_of_fin finfun.

Proof.

by move=> f; apply/ffunP=> x; rewrite ffunE. Qed.

Lemma eq_dffun (g1 g2 : forall x, rT x) :
(forall x, g1 x = g2 x) -> finfun g1 = finfun g2.

Proof.

by move=> eq_g; apply/ffunP => x; rewrite !ffunE eq_g. Qed.

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

Proof.

by []. Qed.

Local Definition tfgraph_inv (G : #|aT|.-tuple {x : aT & rT x}) : option fT :=
if eqfunP isn't ReflectT Dtg then None else
Some [ffun x => ecast x (rT x) (Dtg x) (tagged (tnth G (enum_rank x)))].

Local Lemma tfgraphK : pcancel tfgraph tfgraph_inv.

Proof.

move=> f; have Dg x: tnth (tfgraph f) (enum_rank x) = total_fun f x.
by rewrite tnth_map -[tnth _ _]enum_val_nth enum_rankK.
rewrite /tfgraph_inv; case: eqfunP => /= [Dtg | [] x]; last by rewrite Dg.
congr (Some _); apply/ffunP=> x; rewrite ffunE.
by rewrite Dg in (Dx := Dtg x) *; rewrite eq_axiomK.
Qed.

Lemma tfgraph_inj : injective tfgraph

Proof.

exact: pcan_inj tfgraphK. Qed.

Definition family_mem mF := [pred f : fT | [forall x, in_mem (f x) (mF x)]].

Variables (pT : forall x, predType (rT x)) (F : forall x, pT x).

Local Definition fmem F x := mem (F x : pT x).

Lemma familyP f : reflect (forall x, f x \in F x) (f \in family_mem (fmem F)).

Proof.

exact: forallP. Qed.

Proof.

by move=> t; apply: eq_from_tnth => i; rewrite tnth_map ffunE tnth_ord_tuple.
Qed.

Lemma tuple_of_finfunK : cancel tuple_of_finfun finfun_of_tuple.

Proof.

by move=> f; apply/ffunP => i; rewrite ffunE tnth_map tnth_ord_tuple.
Qed.

End FinFunTuple.

Section FinFunCat.

Context {T : Type} {A B : finType}.

Definition cat_fun (f : A -> T) (g : B -> T) : A + B -> T :=
fun i => match i with inl j => f j | inr j => g j end.

Lemma cat_inl f g j : cat_fun f g (inl j) = f j.

Proof.

by []. Qed.

Lemma cat_inr f g j : cat_fun f g (inr j) = g j.

Proof.

by []. Qed.

End FinFunCat.

Section OrdFunCat.
Context {T : Type} {m n : nat}.

Definition cat_ordfun (f : T ^ m) (g : T ^ n) : T^(m + n) :=
finfun (cat_fun f g \o split).

Lemma cat_lshift f g j : cat_ordfun f g (lshift n j) = f j.

Proof.

by rewrite ffunE/= (unsplitK (inl _ _)). Qed.

Lemma cat_rshift f g j : cat_ordfun f g (rshift m j) = g j.

Proof.

by rewrite ffunE/= (unsplitK (inr _ _)). Qed.

Definition cat_lrshift := (@cat_lshift, @cat_rshift).

End OrdFunCat.

Lemma cat_ordfunK {m n} :
cat_ordfun (finfun (@lshift m n)) (finfun (@rshift _ _)) =1 id.

Proof.

by move=> i; case: (split_ordP i) => //= {}i ->; rewrite ?cat_lrshift ?ffunE.
Qed.

Lemma cat_ordfun_comp {m n S T} (f : S ^ m) (g : S ^ n) (h : S -> T) :
cat_ordfun (finfun (h \o f)) (finfun (h \o g)) =1 h \o cat_ordfun f g.

Proof.

by move=> i; case: (split_ordP i) => //= {}i ->; rewrite ?cat_lrshift ?ffunE.
Qed.

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).

Proof.

by rewrite tnth_map /tnth -enum_val_nth. Qed.

Lemma FinfunK : cancel Finfun fgraph.

Proof.

by move=> G; apply/eq_from_tnth=> i; rewrite tnth_fgraph ffunE enum_valK.
Qed.

Lemma fgraphK : cancel fgraph Finfun.

Proof.

by move=> f; apply/ffunP=> x; rewrite ffunE tnth_fgraph enum_rankK. Qed.

Lemma fgraph_ffun0 aT0 : fgraph (ffun0 aT0) = nil :> seq rT.

Proof.

by apply/nilP/eqP; rewrite size_tuple. Qed.

Lemma codom_ffun f : codom f = fgraph f

Proof.

by []. Qed.

Lemma tagged_tfgraph f : @map _ rT tagged (tfgraph f) = fgraph f.

Proof.

by rewrite -map_comp. Qed.

Lemma eq_ffun (g1 g2 : aT -> rT) : g1 =1 g2 -> finfun g1 = finfun g2.

Proof.

exact: eq_dffun. Qed.

Lemma fgraph_codom f : fgraph f = codom_tuple f.

Proof.

exact/esym/val_inj/codom_ffun. Qed.

Definition ffun_on_mem (mR : mem_pred rT) := family_mem (fun _ : aT => mR).

Lemma ffun_onP R f : reflect (forall x, f x \in R) (f \in ffun_on_mem (mem R)).

Proof.

exact: forallP. Qed.

End FunPlainTheory.

Arguments Finfun {aT rT} G.
Arguments fgraph {aT rT} f.
Arguments FinfunK {aT rT} G : rename.
Arguments fgraphK {aT rT} f : rename.
Arguments eq_ffun {aT rT} [g1] g2 eq_g12.
Arguments ffun_onP {aT rT R f}.

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.

Proof.

by rewrite -[i in RHS]enum_rankK -tnth_fgraph (tnth_nth x0) enum_rank_ord.
Qed.

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). Proof. by []. Qed.
End Support.
Notation "y .-support" := (support_for y)
  (at level 1, format "y .-support") : function_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 (forall x, x \notin D -> g x = y) (y.-support g \subset D).
Proof.
by (apply: (iffP subsetP) => Dg x; [apply: contraNeq|apply: contraR]) => /Dg->.
Qed.
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, forall x, f x \in F x})
          (f \in pfamily_mem y (mem D) (fmem F)).
Proof.
apply: (iffP familyP) => [/= f_pfam | [/supportP f_supp f_fam] x].
  split=> [|x Ax]; last by have:= f_pfam x; rewrite Ax.
  by apply/subsetP=> x; case: ifP (f_pfam x) => //= _ fx0 /negP[].
by case: ifPn => Ax /=; rewrite inE /= (f_fam, f_supp).
Qed.
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)).
Proof.
apply: (iffP (pfamilyP y D (fun _ => R) f)) => [] [-> f_fam]; split=> //.
  by move=> _ /imageP[x Ax ->]; apply: f_fam.
by move=> x Ax; apply: f_fam; apply/imageP; exists x.
Qed.
End EqTheory.
Arguments supportP {aT rT y D g}.
Arguments pfamilyP {aT rT pT y D F f}.
Arguments pffun_onP {aT rT y D R f}.
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 forall x : aT, rT x}.

Lemma card_family (F : forall x, pred (rT x)) :
#|(family F : simpl_pred fT)| = foldr muln 1 [seq #|F x| | x : aT].

Proof.

rewrite /image_mem; set E := enum aT in (uniqE := enum_uniq aT) *.
have trivF x: x \notin E -> #|F x| = 1 by rewrite mem_enum.
elim: E uniqE => /= [_ | x0 E IH_E /andP[E'x0 uniqE]] in F trivF *.
  have /fin_all_exists[f0 Ff0] x: exists y0, F x =i pred1 y0.
    have /pred0Pn[y Fy]: #|F x| != 0 by rewrite trivF.
    by exists y; apply/fsym/subset_cardP; rewrite ?subset_pred1 // card1 trivF.
  apply: eq_card1 (finfun f0 : fT) _ _ => f; apply/familyP/eqP=> [Ff | {f}-> x].
    by apply/ffunP=> x; have /[!(Ff0, ffunE)]/eqP := Ff x.
  by rewrite ffunE Ff0 inE /=.
have [y0 Fxy0 | Fx00] := pickP (F x0); last first.
  by rewrite !eq_card0 // => f; apply: contraFF (Fx00 (f x0))=> /familyP; apply.
pose F1 x := if eqP is ReflectT Dx then xpred1 (ecast x (rT x) Dx y0) else F x.
transitivity (#|[predX F x0 & family F1 : pred fT]|); last first.
  rewrite cardX {}IH_E {uniqE}// => [x E'x|].
    rewrite /F1; case: eqP => [Dx | /nesym/eqP-x0'x]; first exact: card1.
    by rewrite trivF // negb_or x0'x.
  congr (_ * foldr _ _ _); apply/eq_in_map=> x Ex.
  by rewrite /F1; case: eqP => // Dx0; rewrite Dx0 Ex in E'x0.
pose g yf : fT := let: (y, f) := yf : rT x0 * fT in
  [ffun x => if eqP is ReflectT Dx then ecast x (rT x) Dx y else f x].
have gK: cancel (fun f : fT => (f x0, g (y0, f))) g.
  by move=> f; apply/ffunP=> x; rewrite !ffunE; case: eqP => //; case: x /.
rewrite -(card_image (can_inj gK)); apply: eq_card => [] [y f] /=.
apply/imageP/andP=> [[f1 /familyP/=Ff1] [-> ->]| [/=Fx0y /familyP/=Ff]].
  split=> //; apply/familyP=> x; rewrite ffunE /F1 /=.
  by case: eqP => // Dx; apply: eqxx.
exists (g (y, f)).
  by apply/familyP=> x; have:= Ff x; rewrite ffunE /F1; case: eqP; [case: x /|].
congr (_, _); first by rewrite /= ffunE; case: eqP => // Dx; rewrite eq_axiomK.
by apply/ffunP=> x; have:= Ff x; rewrite !ffunE /F1; case: eqP => // Dx /eqP.
Qed.

Lemma card_dep_ffun : #|fT| = foldr muln 1 [seq #|rT x| | x : aT].

Proof.

by rewrite -card_family; apply/esym/eq_card=> f; apply/familyP. Qed.

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

Proof.

rewrite card_family !/(image _ _) /(enum D) -enumT /=.
by elim: (enum aT) => //= x E ->; have [// | D'x] := ifP; rewrite card1 mul1n.
Qed.

Lemma card_pffun_on y0 D R : #|pffun_on y0 D R| = #|R| ^ #|D|.

Proof.

rewrite (cardE D) card_pfamily /image_mem.
by elim: (enum D) => //= _ e ->; rewrite expnS.
Qed.

Lemma card_ffun_on R : #|@ffun_on aT R| = #|R| ^ #|aT|.

Proof.

rewrite card_family /image_mem cardT.
by elim: (enum aT) => //= _ e ->; rewrite expnS.
Qed.

Lemma card_ffun : #|fT| = #|rT| ^ #|aT|.

Proof.

by rewrite -card_ffun_on; apply/esym/eq_card=> f; apply/forallP. Qed.

End FinFunTheory.

Section DependentFiniteProduct.

Variables (I : finType) (T_ : I -> finType).
Notation fprod_type := (forall i : I, T_ i) (only parsing).

Record fprod : predArgType := FProd
{ fprod_fun : {ffun I -> {i : I & T_ i}} ;
fprod_prop : [forall i : I, tag (fprod_fun i) == i] }.

Lemma tag_fprod_fun (f : fprod) i : tag (fprod_fun f i) = i.

Proof.

by have /'forall_eqP/(_ i) := fprod_prop f. Qed.

Definition fun_of_fprod (f : fprod) : fprod_type :=
fun i => etagged ('forall_eqP (fprod_prop f) i).
Coercion fun_of_fprod : fprod >-> Funclass.

#[hnf] HB.instance Definition _ := [isSub for fprod_fun].
#[hnf] HB.instance Definition _ := [Finite of fprod by <:].

Lemma fprod_of_prod_type_subproof (f : fprod_type) :
[forall i : I, tag ([ffun i => Tagged T_ (f i)] i) == i].

Proof.

by apply/'forall_eqP => i /=; rewrite ffunE. Qed.

Definition fprod_of_fun (f : fprod_type) : fprod :=
FProd (fprod_of_prod_type_subproof f).

Lemma fprodK : cancel fun_of_fprod fprod_of_fun.

Proof.

rewrite /fun_of_fprod /fprod_of_fun; case=> f fP.
by apply/val_inj/ffunP => i /=; rewrite !ffunE etaggedK.
Qed.

Lemma fprodE g i : fprod_of_fun g i = g i.

Proof.

rewrite /fprod_of_fun /fun_of_fprod/=.
by move: ('forall_eqP _ _); rewrite ffunE/= => e; rewrite eq_axiomK.
Qed.

Lemma fprodP (f1 f2 : fprod) : (forall x, f1 x = f2 x) <-> f1 = f2.

Proof.

split=> [eq_f12|->//]; rewrite -[f1]fprodK -[f2]fprodK.
by apply/val_inj/ffunP => i; rewrite !ffunE eq_f12.
Qed.

Definition dffun_of_fprod (f : fprod) : {dffun forall i : I, T_ i} :=
[ffun x => f x].

Definition fprod_of_dffun (f : {dffun forall i : I, T_ i}) : fprod :=
fprod_of_fun f.

Lemma dffun_of_fprodK : cancel dffun_of_fprod fprod_of_dffun.

Proof.

by move=> f; apply/fprodP=> i; rewrite fprodE ffunE. Qed.

#[local] Hint Resolve dffun_of_fprodK : core.

Lemma fprod_of_dffunK : cancel fprod_of_dffun dffun_of_fprod.

Proof.

by move=> f; apply/ffunP => i; rewrite !ffunE fprodE. Qed.

#[local] Hint Resolve fprod_of_dffunK : core.

Lemma dffun_of_fprod_bij : bijective dffun_of_fprod.

Proof.

by exists fprod_of_dffun. Qed.

Lemma fprod_of_dffun_bij : bijective fprod_of_dffun.

Proof.

by exists dffun_of_fprod. Qed.

Definition to_family_tagged_with (f : fprod) : {x in family (tagged_with T_)} :=
  exist _ (fprod_fun f) (fprod_prop f).

Definition of_family_tagged_with (f : {x in family (tagged_with T_)}) : fprod :=
  FProd (valP f).

Lemma to_family_tagged_withK :
  cancel to_family_tagged_with of_family_tagged_with.

Proof.

by case=> f fP; apply/val_inj. Qed.

#[local] Hint Resolve to_family_tagged_withK : core.

Lemma of_family_tagged_withK :
cancel of_family_tagged_with to_family_tagged_with.

Proof.

by case=> f fP; apply/val_inj. Qed.

#[local] Hint Resolve of_family_tagged_withK : core.

Lemma to_family_tagged_with_bij : bijective to_family_tagged_with.

Proof.

by exists of_family_tagged_with. Qed.

Lemma of_family_tagged_with_bij : bijective of_family_tagged_with.

Proof.

by exists to_family_tagged_with. Qed.

Lemma etaggedE (a : fprod) (i : I) (e : tag (fprod_fun a i) = i) :
etagged e = a i.

Proof.

by case: a e => //= f fP e; congr etagged; apply: eq_irrelevance. Qed.

End DependentFiniteProduct.

Arguments to_family_tagged_with {I T_}.
Arguments of_family_tagged_with {I T_}.

Notation "[ 'fprod' i : I => F ]" := (fprod_of_fun (fun i : I => F))
  (i name, only parsing) : function_scope.

Notation "[ 'fprod' : I => F ]" := (fprod_of_fun (fun _ : I => F))
  (only parsing) : function_scope.

Notation "[ 'fprod' i => F ]" := [fprod i : _ => F]
  (i name, format "[ 'fprod' i => F ]") : function_scope.

Notation "[ 'fprod' => F ]" := [fprod : _ => F]
  (format "[ 'fprod' => F ]") : function_scope.

Files

Module mathcomp.boot.finfun