Library binetcauchy

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq path.
Require Import ssralg fintype perm choice finfun.
Require Import matrix bigop zmodp mxalgebra fingroup.
Require Import minor.

Import GRing.Theory.

Set Implicit Arguments.

Open Scope ring_scope.

Section BinetCauchy.
Variable R : comRingType.
Variable k l : nat.

Let Z := ({ffun 'I_k -> 'I_l} * ('S_k))%type.

Variable A : 'M[R]_(k,l).
Variable B : 'M[R]_(l,k).

Definition weight (f: {ffun 'I_k -> 'I_l}) (s : 'S_k) :=
  ((-1) ^+ s) * \prod_(i : 'I_k) ((A i (f i)) * (B (f i) (s i))).

Lemma split_sumZ_sf (P : Z -> R) (C : pred {ffun 'I_k -> 'I_l}):
  \sum_(fz : Z | C fz.1) (P fz) =
  \sum_(s: 'S_k) (\sum_(f: {ffun 'I_k -> 'I_l} | C f) (P (f,s))).

Lemma split_sumZ_fs (P : Z -> R) (C : pred {ffun 'I_k -> 'I_l}):
  \sum_(fz : Z | C fz.1) (P fz) =
  \sum_(f: {ffun 'I_k -> 'I_l} | C f) (\sum_(s: 'S_k) (P (f,s))).

Lemma detAB_weight : \det (A *m B) = \sum_(fz : Z) (weight fz.1 fz.2).

Definition tilt (i j: 'I_k) (z: 'S_k) := (tperm i j * z)%g.

Lemma tiltK (i j: 'I_k) : involutive (tilt i j).

Lemma tilt_bij (i j: 'I_k) : bijective (tilt i j).

Lemma tilt_inj (i j : 'I_k) : injective (tilt i j).

Lemma sign_tilt2 (z: 'S_k) (i j: 'I_k) : i != j ->
  (-1)^+(tilt i j z) = -1* ((-1) ^+ z) :>R.

Lemma sig_tilt (z: 'S_k) (i j: 'I_k) : i != j ->
  ~~ odd_perm (tilt i j z) = odd_perm z.

Lemma reindex_with_tilt (P: 'S_k -> R) (i j: 'I_k) : i != j ->
 \sum_(z : 'S_k) (P z) =
 \sum_(z: 'S_k | odd_perm z) (P z + P (tilt i j z)).

Lemma fz_tilt_0 (i j: 'I_k) (f: {ffun 'I_k -> 'I_l}) z:
  i != j -> f i = f j -> weight f z + weight f (tilt i j z) = 0.

Lemma sum_bad : \sum_(fz : Z | ~~ injectiveb fz.1) (weight fz.1 fz.2) = 0.

Definition strictf (p q: nat) (f: 'I_p -> 'I_q) :=
  [forall x : 'I_p, [forall y : 'I_p, (x < y) == (f x < f y)]].

Lemma inj_strictf (p q : nat) (f: 'I_p -> 'I_q) : strictf f -> injective f.

Lemma inj_strictf_ffun (p q : nat) (f: {ffun 'I_p -> 'I_q}) :
 strictf f -> injective f.

Remark trans_ltn : ssrbool.transitive ltn.

Lemma sorted_enum : forall n (P: pred 'I_n),
  sorted ltn (map val (enum P)).

Lemma path_drop : forall (s: seq nat) (i j d x : nat), path ltn x s ->
  i < j -> path ltn (nth d (x :: s) i) (drop i.+1 (x :: s)).

Lemma path_ordered_nth (i j d d' x : nat) (s: seq nat): path ltn x s ->
  i < j -> i < size (x::s) -> j < size (x::s) ->
  nth d (x::s) i < nth d' (x::s) j.

Lemma sorted_ordered_nth i j d d' (s: seq nat): sorted ltn s ->
  i < j -> i < size s -> j < size s -> nth d s i < nth d' s j.

Lemma nth_change_default: forall (s: seq nat) d d' n, n < size s ->
  nth d s n = nth d' s n.

Lemma sorted_ordered_nth_gen (i j d d' x : nat) (s: seq nat):
  sorted ltn s ->
  i < size s -> j < size s -> nth d s i < nth d' s j -> i < j.

Lemma tool_nth : forall (s: seq 'I_l) (n:nat) (x: 'I_n) (d: 'I_l),
 nth (val d) (map val s) x = val (nth d s x).

Lemma cast0 (f: {ffun 'I_k -> 'I_l}) : size (enum (codom f)) = #|codom f|.

Lemma cast1 (f: {ffun 'I_k -> 'I_l}) : injective f -> k = #|codom f|.

Lemma step_weight (g f: {ffun 'I_k -> 'I_l}) (pi: 'S_k) (hf : injective f)
  (phi : 'S_k) : (forall x, f x = g (phi x)) ->
  let: sigma := (phi^-1 * pi)%g in
    weight f pi = ((-1)^+ phi * \prod_i (A i (g (phi i)))) *
                  ((-1)^+ sigma * \prod_i (B (g i) (sigma i))).

Definition same_codomb m n (f g: {ffun 'I_m -> 'I_n}) : bool :=
  [forall x, (x \in codom f) == (x \in codom g)].
Definition same_codom m n (f g: {ffun 'I_m -> 'I_n}) :=
  forall x, (x \in codom f) = (x \in codom g).

Lemma same_codomP m n (f g : {ffun 'I_m -> 'I_n}) :
  reflect (same_codom f g) (same_codomb f g).

Definition good (g: {ffun 'I_k -> 'I_l}) : pred {ffun 'I_k -> 'I_l} :=
 fun f => injectiveb f && (same_codomb f g).

Lemma goodP (g f: {ffun 'I_k -> 'I_l}) :
  reflect (injective f /\ same_codom f g) (good g f).

Lemma mem_same_codom (f g: {ffun 'I_k -> 'I_l}) :
  same_codom f g -> forall x, (f x) \in codom g.

Definition inv_g_of_fx (g f: {ffun 'I_k -> 'I_l}) :=
  match (same_codomP f g) with
    | ReflectT b => finfun (fun x => iinv (mem_same_codom b x))
    | ReflectF _ => finfun id
  end.

Lemma inv_g_of_fxE (g f: {ffun 'I_k -> 'I_l}) :
  same_codom f g ->
  forall x, g (inv_g_of_fx g f x) = f x.

Lemma inv_g_of_fx_inj (g f: {ffun 'I_k -> 'I_l}): injective f ->
  same_codom f g -> injectiveb (inv_g_of_fx g f).

Definition perm_f (g f: {ffun 'I_k -> 'I_l}) :=
  match goodP g f with
    | ReflectT b => Perm (inv_g_of_fx_inj (proj1 b) (proj2 b))
    | ReflectF _ => 1%g
  end.

Lemma perm_fE (g f: {ffun 'I_k -> 'I_l}) : injective f ->
  same_codom f g -> forall x, f x = g ((perm_f g f) x).

Lemma codom_perm (g: {ffun 'I_k -> 'I_l}) (p: 'S_k) :
  forall x, (x \in codom (finfun (g \o p))) = (x \in codom g).

Lemma from_good_to_perm (g: {ffun 'I_k -> 'I_l})
  (P : {ffun 'I_k -> 'I_l} -> R) : injective g ->
  \sum_(f | good g f) P f = \sum_(phi : 'S_k) (P (finfun (g \o phi))).

Lemma one_step (g : {ffun 'I_k -> 'I_l}) : injective g ->
  minor k id g A * minor k g id B =
  \sum_(fz : Z | good g fz.1) weight fz.1 fz.2.

Lemma gather_by_strictness :
  \sum_(g : {ffun 'I_k -> 'I_l} | strictf g)
     \sum_(fz : Z | good g fz.1) weight fz.1 fz.2 =
  \sum_(g : {ffun 'I_k -> 'I_l} | strictf g)
     (minor k id g A) * (minor k g id B).

Definition strict_from (f: {ffun 'I_k -> 'I_l}) (hf: injective f) :=
  finfun (fun x => @enum_val _ (mem (codom f)) (cast_ord (cast1 hf) x)).

Lemma strict_fromP (f: {ffun 'I_k -> 'I_l}) (hf: injective f):
  strictf (strict_from hf) /\ same_codom f (strict_from hf).

Lemma strictf_lift m n (f: {ffun 'I_m.+1 -> 'I_n}) :
  strictf f -> strictf (finfun (fun x => f (lift 0 x))).

Lemma strictf_uniq : forall m n (f g: {ffun 'I_m -> 'I_n}),
  strictf f -> strictf g -> same_codom f g -> f = g.

Definition strict_from_f (fz :Z) :=
  match injectiveP fz.1 with
    | ReflectT h => strict_from h
    | ReflectF _ => fz.1
  end.

Lemma strict_from_fP (fz : Z) : injective fz.1 ->
  strictf (strict_from_f fz) /\ same_codom fz.1 (strict_from_f fz).

Lemma BinetCauchy:
  \det (A *m B) = \sum_(f: {ffun 'I_k -> 'I_l} | strictf f)
                       ((minor k id f A) * (minor k f id B)).

End BinetCauchy.