Library mathcomp.ssreflect.finfun
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype tuple.
Distributed under the terms of CeCILL-B. *)
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.
{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).
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 FinFunTuple.
Context {T : Type} {n : nat}.
Definition tuple_of_finfun (f : T ^ n) : n.-tuple T := [tuple f i | i < n].
Definition finfun_of_tuple (t : n.-tuple T) : (T ^ n) := [ffun i ⇒ tnth t i].
Lemma finfun_of_tupleK : cancel finfun_of_tuple tuple_of_finfun.
Lemma tuple_of_finfunK : cancel tuple_of_finfun finfun_of_tuple.
End FinFunTuple.
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.