Module triangular

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finfun bigop prime binomial ssralg finset fingroup finalg.
Require Import perm zmodp matrix mxalgebra.

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

Open Local Scope ring_scope.

Section Triangular.

Variable F : fieldType.

Lemma castmx_det :
forall n p (m : 'M[F]_n) (h : n = p), \det m = \det (castmx (h, h) m).

Proof.

by move => n p m h; move: (h) m; rewrite h => h' m; rewrite castmx_id.
Qed.

Definition lower_triangular n (A:'M[F]_(n + 1)) :=
forall (i j : 'I_(n+1)), i <= j -> A i j = (i == j)%:R.

Lemma lower_triangular_drsubmx : forall n (A:'M[F]_(n + 1)), (lower_triangular A) -> (drsubmx A) = 1.

Proof.

move => n A H.
apply/matrixP => i j. rewrite !mxE [i]ord1 [j]ord1.
rewrite (H (rshift n 0) (rshift n 0)); last by done.
rewrite /=.
by have -> : (rshift n 0 == rshift n 0); first by done.
Qed.

Lemma not_eq_nat_of_ord_not_eq_ord n (i j:'I_n) : (nat_of_ord i)!=(nat_of_ord j) -> i!=j.

Proof.

by move=>H; apply/eqP => H1; rewrite H1 in H; move : H; move/eqP.
Qed.

Lemma lower_triangular_ursubmx : forall n (A:'M[F]_(n + 1)), (lower_triangular A) -> (ursubmx A) = 0.

Proof.

move => n A H.
apply/matrixP => i j. rewrite !mxE.
rewrite (H (lshift 1 i) (rshift n j)); last first.
by rewrite [j]ord1 /= addn0 leq_eqVlt (ltn_ord i); apply/orP; right.
move : i; case H2 : n =>[|n1] i; first by move : (ltn_ord i).
rewrite /=.
case H3 : (lshift 1 i == rshift n1.+1 j); last by done.
move : H3; move/eqP => //=.
have H4 : (nat_of_ord (lshift 1 i)) != (nat_of_ord (rshift n1.+1 j)); last first.
by move => H5; move : (not_eq_nat_of_ord_not_eq_ord H4); rewrite H5; move/eqP.
by rewrite /= [j]ord1 addn0 neq_ltn; move : (ltn_ord i) => ->.
Qed.

Lemma lower_triangular_det_1 : forall n (A:'M[F]_(n+1)), (lower_triangular A) -> \det A = 1.

Proof.

elim => [|n IHn] A H.
  have H1 : (0 + 1)%N = 1%N; first by rewrite add0n.
  rewrite (castmx_det A H1) (mx11_scalar (castmx (H1, H1) A)) det_scalar1 castmxE /=.
  by apply : H.
rewrite -(submxK A).
have -> : (drsubmx A) = 1.
  by apply : lower_triangular_drsubmx.
have -> : (ursubmx A) = 0.
  by apply : lower_triangular_ursubmx.
rewrite det_lblock det1 /= GRing.mulr1.
have H1 : (n.+1)%N = (n + 1)%N; first by rewrite addn1.
set A' := (ulsubmx A); move/(_ (castmx (H1,H1) A')): IHn.
move => H2.
have H3 : lower_triangular (castmx (H1, H1) A'); last first.
  by rewrite (castmx_det A' H1); move : (H2 H3) => ->.
rewrite /lower_triangular.
move => i j ij.
rewrite /A' castmxE //= !mxE.
by apply : (H (lshift 1 (cast_ord (esym H1) i)) (lshift 1 (cast_ord (esym H1) j))).
Qed.

Lemma lower_triangular_invertible : forall n (A:'M[F]_(n+1)), (lower_triangular A) -> A \in unitmx.

Proof.

by move => n A H; move : (lower_triangular_det_1 H); rewrite unitmxE; move => ->; rewrite GRing.unitr1.
Qed.

Lemma lower_triangular_product : forall n (A:'M[F]_(n+1)), (lower_triangular A) -> A *m (invmx A) = 1%:M.

Proof.

move => n A H.
move : (lower_triangular_invertible H) => H1.
apply : (mulmxV H1).
Qed.

End Triangular.