Library LangAlg.finite_functions

We prove here that there is a finite number of functions between two finite decidable sets.

Set Implicit Arguments.
Require Export tools.

We will consider here maps modulo function extensionality.
Global Instance eqf { A B } : SemEquiv (A → B) :=
  fun f g ⇒ ∀ n, f n = g n.

eqf is an equivalence relation.
Global Instance eqf_Equivalence {A B}:
  Equivalence (@eqf A B).

Section s.

We assume the source and target of our functions are decidable.
  Variables src trg : Set.
  Variable D : decidable_set src.
  Variable R : decidable_set trg.

hom is the type of partial functions.
  Notation hom := (src → option trg).

The domain of f is the list l if the elements of l are exactly the values where f is defined.
  Definition domain (f : hom) l := ∀ x , f x ≠ None ↔ x ∈ l.

We use a somewhat relaxed notion of range here: we say that m is a range of f if every value produced by f appears in the list m. Note that m could contain more values.
  Definition range (f : hom) m := ∀ x y, f x = Some y → y ∈ m.

The map f is a finite function from l to m if l is its domain and m is its range.
  Definition finite_function f l m := domain f l ∧ range f m.

finite_functions l m generates a list of all finite functions from l to m, modulo eqf.
  Fixpoint finite_functions (l :list src) (m : list trg) :=
    match l with
    | [] ⇒ [fun _ ⇒ None]
    | a::l ⇒
      bimap (fun f b n ⇒ if eqX n a then Some b else f n)
            (finite_functions l m) m
    end.

If f is a finite function from l to m, there is an extensionally equivalent function g in the list finite_functions l m.
  Lemma finite_function_is_finite l m f :
    finite_function f l m →
    ∃ g, g ∈ (finite_functions l m) ∧ f ≃ g.

If we're given a default value, we can complete a partial function as a total function.
  Definition make_total y0 (f : hom) x :=
    match f x with None ⇒ y0 | Some v ⇒ v end.

Given a list l and a total function f, we can compute a partial function whose domain is l and whose values are those of f.
  Definition restriction l (f : src → trg) : hom :=
    fun x ⇒ if inb x l then Some (f x) else None.

We define finite support for total function using the default value y0 instead of the undefined value None we used for partial functions.
  Definition finite_support (f : src → trg) l m y0 :=
    ∀ x, (f x ≠ y0 → x ∈ l) ∧ f x ∈ m.

If f has finite support, then its restriction to its domain is a finite function, and f is extensionally equivalent to the completion of its restriction.
  Lemma finite_support_finite_function f l m y0 :
    finite_support f l m y0 →
    finite_function (restriction l f) l m
    ∧ f ≃ make_total y0 (restriction l f).

Translates the list of finite partial functions into a list of finitely supported total functions.
  Definition finite_support_functions l m y0 :=
    map (make_total y0) (finite_functions l m).

This list is exhaustive.
  Lemma get_finite_support_function f l m y0 :
    finite_support f l m y0 →
    ∃ g, g ∈ (finite_support_functions l m y0) ∧ f ≃ g.
End s.