Lemma row_echelon_partial_to_upper_triangular_partial { m n : nat } (mat : Matrix F m n) (p : n > 0) (iter : ⟦ S m ⟧%stn) : @is_row_echelon_partial F m n mat iter -> @is_upper_triangular_partial F m n iter mat. Proof. unfold is_row_echelon_partial, is_upper_triangular_partial. destruct iter as [iter p']. unfold is_row_echelon_partial_1, is_row_echelon_partial_2. induction iter as [| iter IH]. { intros ? ? ? ? contr; contradiction (negnatlthn0 n contr). } intros [re_1 re_2] i j lt lt'. simpl in p'. pose (iter_lt_sn := (istransnatlth _ _ _ p' (natgthsnn m))). destruct (natlehchoice i iter) as [? | eq]. {now apply natlthsntoleh. } - destruct (maybe_choice' (leading_entry_compute _ (mat i))) as [t | none]. + destruct t as [t eq]. rewrite (IH iter_lt_sn); try easy. use tpair; simpl. * intros i_1 i_2 j_1 j_2 i1_lt_iter H ? ?. rewrite (re_1 i_1 i_2 j_1 j_2); try easy. apply (istransnatlth _ _ _ i1_lt_iter (natgthsnn iter)). * intros i_1 i_2 i1_lt_iter ? ?; rewrite (re_2 i_1 i_2); try easy. apply (istransnatlth _ _ _ i1_lt_iter (natgthsnn iter)). + now rewrite (leading_entry_compute_inv1 _ _ none). - assert (eq' : i = (iter,, p')). { apply subtypePath_prop; apply eq. } destruct (maybe_choice' (leading_entry_compute F (mat i))) as [[t jst] | none]. 2: { now rewrite (leading_entry_compute_inv1 _ _ none). } destruct (natlthorgeh j t) as [j_lt_t | contr_gt]. { rewrite (pr2 (leading_entry_compute_inv2 _ _ _ jst)); try easy. } pose (H1 := leading_entry_compute_inv2 _ _ _ jst). destruct (natchoice0 i) as [contr0 | ?]. { apply fromempty; refine (negnatgth0n _ _); rewrite contr0; apply lt. } destruct (prev_stn i) as [u u_lt]; try assumption. destruct (maybe_choice' (leading_entry_compute _ (mat u))) as [[prev eq''] | none_prev]. + pose (H2 := (leading_entry_compute_inv2 _ _ _ eq'')). contradiction (pr1 H2); rewrite (IH iter_lt_sn); try easy. * use tpair; simpl. -- intros i_1 i_2 j_1 j_2 i1_lt_iter H' ? ?. rewrite (re_1 i_1 i_2 j_1 j_2); try easy. apply (istransnatlth _ _ _ i1_lt_iter (natgthsnn iter)). -- intros i_1 i_2 i1_lt_iter ? ?; rewrite (re_2 i_1 i_2); try easy. apply (istransnatlth _ _ _ i1_lt_iter (natgthsnn _)). * destruct (natgthorleh u prev) as [gt | leh]; try assumption. contradiction (pr1 H1); rewrite (re_1 u i t prev); try easy. -- apply natgehsntogth; rewrite u_lt, eq'; apply natgehsnn. -- apply natgehsntogth; rewrite u_lt, eq'; apply isreflnatleh. -- destruct (natgthorleh t prev) as [gt | leh']; try assumption. apply (istransnatleh contr_gt); refine (istransnatleh _ leh). apply natlehsntolth, natlthsntoleh; rewrite u_lt; apply lt. * apply natgehsntogth; rewrite u_lt, eq'; apply (isreflnatleh). + rewrite (re_2 u i ); try easy. * simpl; apply natlthtolths. rewrite <- eq. try apply (natlehlthtrans _ _ _ contr_gt lt ). apply natgehsntogth; rewrite u_lt, eq'; apply isreflnatleh. * apply funextfun; intros j'; rewrite ((leading_entry_compute_inv1 _ _ none_prev) j'); reflexivity. * try apply (natlehlthtrans _ _ _ contr_gt lt). apply natgehsntogth; rewrite u_lt, eq'; apply isreflnatleh. Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Nat. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.Matrix. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.IteratedBinaryOperations. Require Import UniMath.Algebra.GaussianElimination.Auxiliary. Require Import UniMath.Algebra.GaussianElimination.Vectors. Require Import UniMath.Algebra.GaussianElimination.Matrices. Require Import UniMath.Algebra.GaussianElimination.Elimination.