From HB Require Import structures.
From mathcomp
Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum.
From mathcomp
Require Import matrix mxalgebra vector falgebra ssrnum algC algnum.
From mathcomp
Require Import fieldext.
From mathcomp Require Import vector.


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

Local Open Scope ring_scope.
Import GRing.Theory Num.Theory.

Reserved Notation "'[ u , v ]"
  (at level 2, format "'[hv' ''[' u , '/ ' v ] ']'").
Reserved Notation "'[ u , v ]_ M"
         (at level 2, format "'[hv' ''[' u , '/ ' v ]_ M ']'").
Reserved Notation "'[ u ]_ M" (at level 2, format "''[' u ]_ M").
Reserved Notation "'[ u ]" (at level 2, format "''[' u ]").
Reserved Notation "u '``_' i"
    (at level 3, i at level 2, left associativity, format "u '``_' i").
Reserved Notation "A ^_|_" (at level 8, format "A ^_|_").
Reserved Notation "A _|_ B" (at level 69, format "A _|_ B").
Reserved Notation "eps_theta .-sesqui" (at level 2, format "eps_theta .-sesqui").

Notation "u '``_' i" := (u (GRing.zero [the zmodType of 'I_1]) i) : ring_scope.
Notation "''e_' i" := (delta_mx 0 i)
 (format "''e_' i", at level 3) : ring_scope.

Local Notation "M ^ phi" := (map_mx phi M).
Local Notation "M ^t phi" := (map_mx phi (M ^T)) (phi at level 30, at level 30).

Structure revop X Y Z (f : Y -> X -> Z) := RevOp {
  fun_of_revop :> X -> Y -> Z;
  _ : forall x, f x =1 fun_of_revop^~ x
}.

Lemma eq_map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) (f : R -> R) :
  f =1 id -> M ^ f = M.

HB.mixin Record isBilinear (R : ringType) (U U' : lmodType R) (V : zmodType)
    (s : R -> V -> V) (s' : R -> V -> V) (f : U -> U' -> V) := {
  additivel_subproof : forall u', additive (f^~ u');
  additiver_subproof : forall u, additive (f u);
  linearl_subproof : forall u', scalable_for s (f^~ u');
  linearr_subproof : forall u, scalable_for s' (f u);
}.

HB.structure Definition Bilinear (R : ringType) (U U' : lmodType R) (V : zmodType)
    (s : R -> V -> V) (s' : R -> V -> V) :=
  {f of isBilinear R U U' V s s' f}.

Definition bilinear_for (R : ringType) (U U' : lmodType R) (V : zmodType)
    (s : GRing.Scale.law R V) (s' : GRing.Scale.law R V) (f : U -> U' -> V) :=
  ((forall u', GRing.linear_for (s : R -> V -> V) (f^~ u'))
  * (forall u, GRing.linear_for s' (f u)))%type.

HB.factory Record bilinear_isBilinear (R : ringType) (U U' : lmodType R) (V : zmodType)
    (s : GRing.Scale.law R V) (s' : GRing.Scale.law R V) (f : U -> U' -> V) := {
  bilinear_subproof : bilinear_for s s' f;
}.

HB.builders Context R U U' V s s' f of bilinear_isBilinear R U U' V s s' f.
HB.instance Definition _ := isBilinear.Build R U U' V s s' f
    (fun u' => additive_linear (bilinear_subproof.1 u'))
    (fun u => additive_linear (bilinear_subproof.2 u))
    (fun u' => scalable_linear (bilinear_subproof.1 u'))
    (fun u => scalable_linear (bilinear_subproof.2 u)).
HB.end.

Module BilinearExports.
Notation bilinear f := (bilinear_for *:%R *:%R f).
Notation biscalar f := (bilinear_for *%R *%R f).
Module Bilinear.
Definition map (R : ringType) (U U' : lmodType R) (V : zmodType)
    (s : R -> V -> V) (s' : R -> V -> V)
    (phUU'V : phant (U -> U' -> V)) := Bilinear.type U U' s s'.
End Bilinear.
Notation "{ 'bilinear' fUV | s & s' }" := (Bilinear.map s s' (Phant fUV))
  (at level 0, format "{ 'bilinear' fUV | s & s' }") : ring_scope.
Notation "{ 'bilinear' fUV | s }" := (Bilinear.map s.1 s.2 (Phant fUV))
  (at level 0, format "{ 'bilinear' fUV | s }") : ring_scope.
Notation "{ 'bilinear' fUV }" := {bilinear fUV | *:%R & *:%R}
  (at level 0, format "{ 'bilinear' fUV }") : ring_scope.
Notation "{ 'biscalar' U }" := {bilinear U -> U -> _ | *%R & *%R}
  (at level 0, format "{ 'biscalar' U }") : ring_scope.
Notation "[ 'bilinear' 'of' f 'as' g ]" := (Bilinear.clone _ _ _ _ _ _ f g)
  (at level 0, format "[ 'bilinear' 'of' f 'as' g ]") : form_scope.
Notation "[ 'bilinear' 'of' f ]" := (Bilinear.clone _ _ _ _ _ _ f _)
  (at level 0, format "[ 'bilinear' 'of' f ]") : form_scope.
End BilinearExports.
Export BilinearExports.

Section applyr.

Variables (R : ringType) (U U' : lmodType R) (V : zmodType) (s s' : R -> V -> V).

Definition applyr_head t (f : U -> U' -> V) u v := let: tt := t in f v u.

End applyr.

Notation applyr := (applyr_head tt).

Section BilinearTheory.

Variable R : ringType.

Section GenericProperties.

Variables (U U' : lmodType R) (V : zmodType) (s : R -> V -> V) (s' : R -> V -> V).
Variable f : {bilinear U -> U' -> V | s & s'}.

Section GenericPropertiesr.

Variable z : U.

#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
  GRing.isAdditive.Build _ _ (f z) (@additiver_subproof _ _ _ _ _ _ f z).
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
  GRing.isScalable.Build _ _ _ _ (f z) (@linearr_subproof _ _ _ _ _ _ f z).

Lemma linear0r : f z 0 = 0
Lemma linearNr : {morph f z : x / - x}
Lemma linearDr : {morph f z : x y / x + y}
Lemma linearBr : {morph f z : x y / x - y}
Lemma linearMnr n : {morph f z : x / x *+ n}
Lemma linearMNnr n : {morph f z : x / x *- n}
Lemma linear_sumr I r (P : pred I) E :
  f z (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f z (E i).

Lemma linearZr_LR : scalable_for s' (f z)
Lemma linearPr a : {morph f z : u v / a *: u + v >-> s' a u + v}.

End GenericPropertiesr.

Lemma applyrE x : applyr f x =1 f^~ x

Section GenericPropertiesl.

Variable z : U'.

#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
  GRing.isAdditive.Build _ _ (applyr f z) (@additivel_subproof _ _ _ _ _ _ f z).
#[local, non_forgetful_inheritance]
HB.instance Definition _ :=
  GRing.isScalable.Build _ _ _ _ (applyr f z) (@linearl_subproof _ _ _ _ _ _ f z).

Lemma linear0l : f 0 z = 0
Lemma linearNl : {morph f^~ z : x / - x}.
Lemma linearDl : {morph f^~ z : x y / x + y}.
Lemma linearBl : {morph f^~ z : x y / x - y}.
Lemma linearMnl n : {morph f^~ z : x / x *+ n}.
Lemma linearMNnl n : {morph f^~ z : x / x *- n}.
Lemma linear_suml I r (P : pred I) E :
  f (\sum_(i <- r | P i) E i) z = \sum_(i <- r | P i) f (E i) z.

Lemma linearZl_LR : scalable_for s (f^~ z).
Lemma linearPl a : {morph f^~ z : u v / a *: u + v >-> s a u + v}.

End GenericPropertiesl.

End GenericProperties.

Section BidirectionalLinearZ.

Variables (U : lmodType R) (V : zmodType) (s : R -> V -> V).
Variables (S : ringType) (h : GRing.Scale.law S V).


End BidirectionalLinearZ.

End BilinearTheory.

Canonical rev_mulmx (R : ringType) m n p := @RevOp _ _ _ (@mulmxr R m n p)
  (@mulmx R m n p) (fun _ _ => erefl).

Lemma mulmx_is_bilinear (R : comRingType) m n p :
  bilinear_for
    (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _)
    (@mulmx R m n p).

HB.instance Definition _ (R : comRingType) m n p :=
  bilinear_isBilinear.Build R
    [the lmodType R of 'M[R]_(m, n)] [the lmodType R of 'M[R]_(n, p)]
    [the zmodType of 'M[R]_(m, p)] _ _ (@mulmx R m n p)
    (mulmx_is_bilinear R m n p).





Section BilinearForms.

Variables (R : fieldType) (theta : {rmorphism R -> R}).
Variables (n : nat) (M : 'M[R]_n).
Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n).

Definition form u v := (u *m M *m (v ^t theta)) 0 0.

Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u] : ring_scope.

Lemma form0l u : '[0, u] = 0.

Lemma form0r u : '[u, 0] = 0.

Lemma formDl u v w : '[u + v, w] = '[u, w] + '[v, w].

Lemma formDr u v w : '[u, v + w] = '[u, v] + '[u, w].

Lemma formZr a u v : '[u, a *: v] = theta a * '[u, v].

Lemma formZl a u v : '[a *: u, v] = a * '[u, v].

Lemma formNl u v : '[- u, v] = - '[u, v].

Lemma formNr u v : '[u, - v] = - '[u, v].

Lemma formee i j : '['e_i, 'e_j] = M i j.

Lemma form0_eq0 : M = 0 -> forall u v, '[u, v] = 0.

End BilinearForms.

Section Sesquilinear.

Variable R : fieldType.
Variable n : nat.
Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n).

Section Def.
Variable eps_theta : (bool * {rmorphism R -> R}).

Definition sesqui :=
  [qualify M : 'M_n | M == ((-1) ^+ eps_theta.1) *: M ^t eps_theta.2].
Fact sesqui_key : pred_key sesqui
Canonical sesqui_keyed := KeyedQualifier sesqui_key.
End Def.

Local Notation "eps_theta .-sesqui" := (sesqui eps_theta).

Variables (eps : bool) (theta : {rmorphism R -> R}).
Variables (M : 'M[R]_n).
Local Notation "''[' u , v ]" := (form theta M u%R v%R) : ring_scope.
Local Notation "''[' u ]" := '[u, u] : ring_scope.

Lemma sesquiE : (M \is (eps,theta).-sesqui) = (M == (-1) ^+ eps *: M ^t theta).

Lemma sesquiP : reflect (M = (-1) ^+ eps *: M ^t theta)
                        (M \is (eps,theta).-sesqui).

Hypothesis (thetaK : involutive theta).
Hypothesis (M_sesqui : M \is (eps, theta).-sesqui).

Lemma trmx_sesqui : M^T = (-1) ^+ eps *: M ^ theta.

Lemma maptrmx_sesqui : M^t theta = (-1) ^+ eps *: M.

Lemma formC u v : '[u, v] = (-1) ^+ eps * theta '[v, u].

Lemma form_eq0C u v : ('[u, v] == 0) = ('[v, u] == 0).

Definition ortho m (B : 'M_(m,n)) := (kermx (M *m (B ^t theta))).
Local Notation "B ^_|_" := (ortho B) : ring_scope.
Local Notation "A _|_ B" := (A%MS <= B^_|_)%MS : ring_scope.

Lemma normalE u v : (u _|_ v) = ('[u, v] == 0).

Lemma form_eq0P {u v} : reflect ('[u, v] = 0) (u _|_ v).

Lemma normalP p q (A : 'M_(p, n)) (B :'M_(q, n)) :
  reflect (forall (u v : 'rV_n), (u <= A)%MS -> (v <= B)%MS -> u _|_ v)
          (A _|_ B).

Lemma normalC p q (A : 'M_(p, n)) (B :'M_(q, n)) : (A _|_ B) = (B _|_ A).

Lemma normal_ortho_mx p (A : 'M_(p, n)) : ((A^_|_) _|_ A).

Lemma normal_mx_ortho p (A : 'M_(p, n)) : (A _|_ (A^_|_)).

Lemma rank_normal u : (\rank (u ^_|_) >= n.-1)%N.

Definition rad := 1%:M^_|_.

Lemma rad_ker : rad = kermx M.

Theorem formDd u v : u _|_ v -> '[u + v] = '[u] + '[v].

Lemma formZ a u : '[a *: u]= (a * theta a) * '[u].

Lemma formN u : '[- u] = '[u].

Lemma form_sign m u : '[(-1) ^+ m *: u] = '[u].

Lemma formD u v : let d := '[u, v] in
  '[u + v] = '[u] + '[v] + (d + (-1) ^+ eps * theta d).

Lemma formB u v : let d := '[u, v] in
  '[u - v] = '[u] + '[v] - (d + (-1) ^+ eps * theta d).

Lemma formBd u v : u _|_ v -> '[u - v] = '[u] + '[v].







End Sesquilinear.

Notation "eps_theta .-sesqui" := (sesqui _ eps_theta) : ring_scope.

Notation symmetric_form := (false, idfun).-sesqui.
Notation skew := (true, idfun).-sesqui.
Notation hermitian := (false, @Num.conj_op _).-sesqui.