QuantumLib.VecSet


In this file, we define more advanced linear algebra concepts such as bases, linear independence, etc...

Require Import Psatz.
Require Import Reals.

Require Export Matrix.

some preliminary defs and lemmas


Local Open Scope nat_scope.

Definition e_i {n : nat} (i : nat) : Vector n :=
  fun x y ⇒ (if (x =? i) && (x <? n) && (y =? 0) then C1 else C0).

Definition pad1 {n m : nat} (A : Matrix n m) (c : C) : Matrix (S n) (S m) :=
  col_wedge (row_wedge A Zero 0) (c .* e_i 0) 0.

Lemma WF_pad1 : ∀ {n m : nat} (A : Matrix n m) (c : C),
  WF_Matrix A ↔ WF_Matrix (pad1 A c).

Lemma WF_e_i : ∀ {n : nat} (i : nat),
  WF_Matrix (@e_i n i).

#[export] Hint Resolve WF_e_i WF_pad1 : wf_db.

Lemma I_is_eis : ∀ {n} (i : nat),
  get_vec i (I n) = e_i i.

Lemma reduce_mul_0 : ∀ {n} (A : Square (S n)) (v : Vector (S n)),
  get_vec 0 A = @e_i (S n) 0 → (reduce A 0 0) × (reduce_row v 0) = reduce_row (A × v) 0.

Lemma reduce_mul_n : ∀ {n} (A : Square (S n)) (v : Vector (S n)),
  get_vec n A = @e_i (S n) n → (reduce A n n) × (reduce_row v n) = reduce_row (A × v) n.


Lemma append_mul : ∀ {n m} (A : Matrix n m) (v : Vector n) (a : Vector m),
  (col_append A v) × (row_append a (@Zero 1 1)) = A × a.

Lemma matrix_by_basis : ∀ {n m} (T : Matrix n m) (i : nat),
  i < m → get_vec i T = T × e_i i.

Lemma pad1_conv : ∀ {n m : nat} (A : Matrix n m) (c : C) (i j : nat),
  (pad1 A c) (S i) (S j) = A i j.

Lemma pad1_mult : ∀ {n m o : nat} (A : Matrix n m) (B : Matrix m o) (c1 c2 : C),
  pad1 (A × B) (c1 × c2)%C = (pad1 A c1) × (pad1 B c2).

Lemma pad1_row_wedge_mult : ∀ {n m : nat} (A : Matrix n m) (v : Vector m) (c : C),
  pad1 A c × row_wedge v Zero 0 = row_wedge (A × v) Zero 0.

Lemma pad1_I : ∀ (n : nat), pad1 (I n) C1 = I (S n).

Lemma pad1ed_matrix : ∀ {n m : nat} (A : Matrix (S n) (S m)) (c : C),
  (∀ (i j : nat), (i = 0 ∨ j = 0) ∧ i ≠ j → A i j = C0) → A 0 0 = c →
  ∃ a, pad1 a c = A.

Lemma reduce_pad1 : ∀ {n : nat} (A : Square n) (c : C),
  A = reduce (pad1 A c) 0 0.

Lemma pad1_col_swap : ∀ {n m : nat} (A : Matrix n m) (x y : nat) (c : C),
  (pad1 (col_swap A x y) c) = col_swap (pad1 A c) (S x) (S y).

Lemma pad1_col_scale : ∀ {n m : nat} (A : Matrix n m) (x : nat) (c1 c2 : C),
  (pad1 (col_scale A x c1) c2) = col_scale (pad1 A c2) (S x) c1.

Lemma pad1_col_add : ∀ {n m : nat} (A : Matrix n m) (x y : nat) (c1 c2 : C),
  (pad1 (col_add A x y c1) c2) = col_add (pad1 A c2) (S x) (S y) c1.

Defining properties which are invarient under column operations, etc...


Inductive invr_col_swap : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| invr_swap : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
    (∀ (n m x y : nat) (T : Matrix n m), x < m → y < m → P n m T → P n m (col_swap T x y))
    → invr_col_swap P.

Inductive invr_col_scale : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| invr_scale : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
    (∀ (n m x : nat) (T : Matrix n m) (c : C), c ≠ C0 → P n m T → P n m (col_scale T x c))
    → invr_col_scale P.

Inductive invr_col_add : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| invr_add : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
    (∀ (n m x y : nat) (T : Matrix n m) (c : C),
        x ≠ y → x < m → y < m → P n m T → P n m (col_add T x y c))
    → invr_col_add P.

Inductive invr_col_add_many : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| invr_add_many : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
    (∀ (n m col : nat) (T : Matrix n m) (as' : Vector m),
        col < m → as' col 0 = C0 → P n m T → P n m (col_add_many col as' T))
    → invr_col_add_many P.

Inductive invr_col_add_each : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| invr_add_each : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
    (∀ (n m col : nat) (T : Matrix n m) (as' : Matrix 1 m),
        col < m → WF_Matrix as' → P n m T → P n m (col_add_each col (make_col_zero col as') T))
    → invr_col_add_each P.

Inductive invr_pad1 : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| invr_p : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
    (∀ (n m : nat) (T : Matrix n m) (c : C), c ≠ C0 → P (S n) (S m) (pad1 T c) → P n m T)
    → invr_pad1 P.

Inductive prop_zero_true : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| PZT : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
  (∀ (n m : nat) (T : Matrix n m), (∃ i, i < m ∧ get_vec i T = Zero) → P n m T) →
  prop_zero_true P.

Inductive prop_zero_false : (∀ n m : nat, Matrix n m → Prop) → Prop :=
| PZF : ∀ (P : (∀ n m : nat, Matrix n m → Prop)),
  (∀ (n m : nat) (T : Matrix n m), (∃ i, i < m ∧ get_vec i T = Zero) → ¬ (P n m T)) →
  prop_zero_false P.

Ltac apply_mat_prop tac :=
  let H := fresh "H" in
  assert (H := tac); inversion H; subst; try apply H.

Lemma mat_prop_col_add_many_some : ∀ (e n m col : nat) (P : ∀ n m : nat, Matrix n m → Prop)
                                     (T : Matrix n m) (as' : Vector m),
  (skip_count col e) < m → col < m →
  (∀ i : nat, (skip_count col e) < i → as' i 0 = C0) → as' col 0 = C0 →
  invr_col_add P →
  P n m T → P n m (col_add_many col as' T).

Lemma invr_col_add_col_add_many : ∀ (P : ∀ n m : nat, Matrix n m → Prop),
  invr_col_add P → invr_col_add_many P.

Lemma mat_prop_col_add_each_some : ∀ (e n m col : nat) (P : ∀ n m : nat, Matrix n m → Prop)
                                     (as' : Matrix 1 m) (T : Matrix n m),
  WF_Matrix as' → (skip_count col e) < m → col < m →
  (∀ i : nat, (skip_count col e) < i → as' 0 i = C0) → as' 0 col = C0 →
  invr_col_add P →
  P n m T → P n m (col_add_each col as' T).

Lemma invr_col_add_col_add_each : ∀ (P : ∀ n m : nat, Matrix n m → Prop),
  invr_col_add P → invr_col_add_each P.

Lemma mat_prop_col_swap_conv : ∀ {n m} (P : ∀ n m : nat, Matrix n m → Prop) (T : Matrix n m) (x y : nat),
  invr_col_swap P →
  x < m → y < m →
  P n m (col_swap T x y) → P n m T.

Lemma mat_prop_col_scale_conv : ∀ {n m} (P : ∀ n m : nat, Matrix n m → Prop)
                                  (T : Matrix n m) (x : nat) (c : C),
  invr_col_scale P →
  c ≠ C0 →
  P n m (col_scale T x c) → P n m T.

Lemma mat_prop_col_add_conv : ∀ {n m} (P : ∀ n m : nat, Matrix n m → Prop)
                                (T : Matrix n m) (x y : nat) (c : C),
  invr_col_add P →
  x ≠ y → x < m → y < m →
  P n m (col_add T x y c) → P n m T.

Lemma mat_prop_col_add_many_conv : ∀ {n m} (P : ∀ n m : nat, Matrix n m → Prop)
                                     (T : Matrix n m) (col : nat) (as' : Vector m),
  invr_col_add P →
  col < m → as' col 0 = C0 →
  P n m (col_add_many col as' T) → P n m T.

Lemma mat_prop_col_add_each_conv : ∀ {n m} (P : ∀ n m : nat, Matrix n m → Prop)
                                     (T : Matrix n m) (col : nat) (as' : Matrix 1 m),
  invr_col_add P →
  col < m → WF_Matrix as' →
  P n m (col_add_each col (make_col_zero col as') T) → P n m T.

Defining and proving lemmas relating to the determinant


Fixpoint parity (n : nat) : C :=
  match n with
  | 0 ⇒ C1
  | S 0 ⇒ -C1
  | S (S n) ⇒ parity n
  end.

Lemma parity_S : ∀ (n : nat),
  (parity (S n) = -C1 × parity n)%C.

Fixpoint Determinant (n : nat) (A : Square n) : C :=
  match n with
  | 0 ⇒ C1
  | S 0 ⇒ A 0 0
  | S n' ⇒ (big_sum (fun i ⇒ (parity i) × (A i 0) × (Determinant n' (reduce A i 0)))%C n)
  end.

Arguments Determinant {n}.

Lemma Det_simplify : ∀ {n} (A : Square (S (S n))),
  Determinant A =
  (big_sum (fun i ⇒ (parity i) × (A i 0) × (Determinant (reduce A i 0)))%C (S (S n))).

Lemma Det_simplify_fun : ∀ {n} (A : Square (S (S (S n)))),
  (fun i : nat ⇒ parity i × A i 0 × Determinant (reduce A i 0))%C =
  (fun i : nat ⇒ (big_sum (fun j ⇒
           (parity i) × (A i 0) × (parity j) × ((reduce A i 0) j 0) ×
           (Determinant (reduce (reduce A i 0) j 0)))%C (S (S n))))%C.

Lemma reduce_I : ∀ (n : nat), reduce (I (S n)) 0 0 = I n.

Lemma Det_I : ∀ (n : nat), Determinant (I n) = C1.

Lemma Det_make_WF : ∀ (n : nat) (A : Square n),
  Determinant A = Determinant (make_WF A).

Lemma Det_Mmult_make_WF_l : ∀ (n : nat) (A B : Square n),
  Determinant (A × B) = Determinant (make_WF A × B).

Lemma Det_Mmult_make_WF_r : ∀ (n : nat) (A B : Square n),
  Determinant (A × B) = Determinant (A × (make_WF B)).

Lemma Det_Mmult_make_WF : ∀ (n : nat) (A B : Square n),
  Determinant (A × B) = Determinant ((make_WF A) × (make_WF B)).

Definition M22 : Square 2 :=
  fun x y ⇒
  match (x, y) with
  | (0, 0) ⇒ 1%R
  | (0, 1) ⇒ 2%R
  | (1, 0) ⇒ 4%R
  | (1, 1) ⇒ 5%R
  | _ ⇒ C0
  end.

Lemma Det_M22 : (Determinant M22) = (Copp (3%R,0%R))%C.

Now, we show the effects of the column operations on determinant

Lemma Determinant_scale : ∀ {n} (A : Square n) (c : C) (col : nat),
  col < n → Determinant (col_scale A col c) = (c × Determinant A)%C.

Lemma Det_diff_1 : ∀ {n} (A : Square (S (S (S n)))),
  Determinant (col_swap A 0 1) =
  big_sum (fun i ⇒ (big_sum (fun j ⇒ ((A i 1) × (A (skip_count i j) 0) × (parity i) × (parity j) ×
                             Determinant (reduce (reduce A i 0) j 0))%C)
                             (S (S n)))) (S (S (S n))).

Lemma Det_diff_2 : ∀ {n} (A : Square (S (S (S n)))),
  Determinant A =
  big_sum (fun i ⇒ (big_sum (fun j ⇒ ((A i 0) × (A (skip_count i j) 1) × (parity i) × (parity j) ×
                             Determinant (reduce (reduce A i 0) j 0))%C)
                             (S (S n)))) (S (S (S n))).

Lemma Determinant_swap_01 : ∀ {n} (A : Square n),
  1 < n → Determinant (col_swap A 0 1) = (-C1 × (Determinant A))%C.

Lemma Determinant_swap_adj : ∀ {n} (A : Square n) (i : nat),
  S i < n → Determinant (col_swap A i (S i)) = (-C1 × (Determinant A))%C.

Lemma Determinant_swap_ik : ∀ {n} (k i : nat) (A : Square n),
  i + (S k) < n → Determinant (col_swap A i (i + (S k))) = (-C1 × (Determinant A))%C.

Lemma Determinant_swap : ∀ {n} (A : Square n) (i j : nat),
  i < n → j < n → i ≠ j →
  Determinant (col_swap A i j) = (-C1 × (Determinant A))%C.

Lemma col_0_Det_0 : ∀ {n} (A : Square n),
  (∃ i, i < n ∧ get_vec i A = Zero) → Determinant A = C0.

Lemma col_same_Det_0 : ∀ {n} (A : Square n) (i j : nat),
  i < n → j < n → i ≠ j →
  get_vec i A = get_vec j A →
  Determinant A = C0.

Lemma col_scale_same_Det_0 : ∀ {n} (A : Square n) (i j : nat) (c : C),
  i < n → j < n → i ≠ j →
  get_vec i A = c .* (get_vec j A) →
  Determinant A = C0.

Lemma Det_col_add_comm : ∀ {n} (T : Matrix (S n) n) (v1 v2 : Vector (S n)),
  (Determinant (col_wedge T v1 0) + Determinant (col_wedge T v2 0) =
   Determinant (col_wedge T (v1 .+ v2) 0))%C.

Lemma Determinant_col_add0i : ∀ {n} (A : Square n) (i : nat) (c : C),
  i < n → i ≠ 0 → Determinant (col_add A 0 i c) = Determinant A.

Lemma Determinant_col_add : ∀ {n} (A : Square n) (i j : nat) (c : C),
  i < n → j < n → i ≠ j → Determinant (col_add A i j c) = Determinant A.

We can now define some invariants for Determinant

Definition det_neq_0 {n m : nat} (A : Matrix n m) : Prop :=
  n = m ∧ @Determinant n A ≠ C0.

Definition det_eq_c (c : C) {n m : nat} (A : Matrix n m) : Prop :=
  n = m ∧ @Determinant n A = c.

Lemma det_neq_0_swap_invr : invr_col_swap (@det_neq_0).

Lemma det_neq_0_scale_invr : invr_col_scale (@det_neq_0).

Lemma det_neq_0_add_invr : invr_col_add (@det_neq_0).

Lemma det_neq_0_pad1_invr : invr_pad1 (@det_neq_0).

Lemma det_neq_0_pzf : prop_zero_false (@det_neq_0).

Lemma det_0_swap_invr : invr_col_swap (@det_eq_c C0).

Lemma det_0_scale_invr : invr_col_scale (@det_eq_c C0).

Lemma det_c_add_invr : ∀ (c : C), invr_col_add (@det_eq_c c).

Lemma det_0_pad1_invr : invr_pad1 (@det_eq_c C0).

#[export] Hint Resolve det_neq_0_swap_invr det_neq_0_scale_invr det_neq_0_add_invr det_neq_0_pad1_invr : invr_db.
#[export] Hint Resolve det_neq_0_pzf det_0_swap_invr det_0_scale_invr det_c_add_invr det_0_pad1_invr : invr_db.

Lemma Determinant_col_add_many : ∀ (n col : nat) (A : Square n) (as' : Vector n),
  col < n → as' col 0 = C0 →
  Determinant A = Determinant (col_add_many col as' A).

Lemma Determinant_col_add_each : ∀ (n col : nat) (as' : Matrix 1 n)
                                          (A : Square n),
  col < n → WF_Matrix as' → as' 0 col = C0 →
  Determinant A = Determinant (col_add_each col as' A).

Defining linear independence, and proving lemmas etc...


Definition linearly_independent {n m} (T : Matrix n m) : Prop :=
  ∀ (a : Vector m), WF_Matrix a → @Mmult n m 1 T a = Zero → a = Zero.

Definition linearly_dependent {n m} (T : Matrix n m) : Prop :=
  ∃ (a : Vector m), WF_Matrix a ∧ a ≠ Zero ∧ @Mmult n m 1 T a = Zero.

Lemma lindep_implies_not_linindep : ∀ {n m} (T : Matrix n m),
  linearly_dependent T → ¬ (linearly_independent T).

Lemma not_lindep_implies_linindep : ∀ {n m} (T : Matrix n m),
  not (linearly_dependent T) → linearly_independent T.

Lemma lin_indep_vec : ∀ {n} (v : Vector n),
  WF_Matrix v → v ≠ Zero → linearly_independent v.

Lemma invertible_l_implies_linind : ∀ {n} (A B : Square n),
  A × B = I n → linearly_independent B.

Lemma lin_indep_col_reduce_n : ∀ {n m} (A : Matrix n (S m)),
  linearly_independent A → linearly_independent (reduce_col A m).

Lemma lin_indep_smash : ∀ {n m2 m1} (A1 : Matrix n m1) (A2 : Matrix n m2),
  linearly_independent (smash A1 A2) → linearly_independent A1.

Lemma lin_dep_mult_r : ∀ {n m o} (A : Matrix n m) (B : Matrix m o),
  linearly_dependent B → linearly_dependent (A × B).

Lemma lin_dep_col_append_n : ∀ {n m} (A : Matrix n m) (v : Vector n),
  linearly_dependent A → linearly_dependent (col_append A v).

Lemma lin_indep_swap_invr : invr_col_swap (@linearly_independent).

Lemma lin_indep_scale_invr : invr_col_scale (@linearly_independent).

Lemma lin_indep_add_invr : invr_col_add (@linearly_independent).

Lemma lin_indep_pad1_invr : invr_pad1 (@linearly_independent).

Lemma lin_indep_pzf : prop_zero_false (@linearly_independent).

Lemma lin_dep_swap_invr : invr_col_swap (@linearly_dependent).

Lemma lin_dep_scale_invr : invr_col_scale (@linearly_dependent).

Lemma lin_dep_add_invr : invr_col_add (@linearly_dependent).

Lemma lin_dep_pzt : prop_zero_true (@linearly_dependent).

#[export] Hint Resolve lin_indep_swap_invr lin_indep_scale_invr lin_indep_add_invr lin_indep_pad1_invr : invr_db.
#[export] Hint Resolve lin_indep_pzf lin_dep_swap_invr lin_dep_scale_invr lin_dep_add_invr lin_dep_pzt : invr_db.

we begin to prove that if n < m, then any Matrix n m is linearly_dependent. This is quite useful, as we get a vector that can be used to cancel a column

Lemma lin_dep_gen_elem : ∀ {m n} (T : Matrix n (S m)),
  WF_Matrix T → linearly_dependent T →
  (∃ i, i < (S m) ∧
             (∃ v : Vector m, WF_Matrix v ∧
                 @Mmult n m 1 (reduce_col T i) v = (-C1) .* (get_vec i T))).

Lemma gt_dim_lindep_ind_step1 : ∀ {n m} (T : Matrix (S n) (S m)) (col : nat),
  WF_Matrix T → col ≤ m → get_vec col T = @e_i (S n) 0 →
  linearly_dependent (reduce_row (reduce_col T col) 0) → linearly_dependent T.

Lemma gt_dim_lindep_ind_step2 : ∀ {n m} (T : Matrix (S n) (S m))
                                       (v : Vector (S m)) (col : nat),
  WF_Matrix T → col < S m → v col 0 = C0 →
  reduce_col (reduce_row T 0) col × (reduce_row v col) =
                     - C1 .* get_vec col (reduce_row T 0) →
  linearly_dependent (reduce_row (reduce_col T col) 0) → linearly_dependent T.

Lemma gt_dim_lindep : ∀ {m n} (T : Matrix n m),
  n < m → WF_Matrix T → linearly_dependent T.

defining a new type of matrix which we will show is the lin_indep/invertible matrices


Inductive op_to_I {n : nat} : Square n → Prop :=
| otI_I: op_to_I (I n)
| otI_swap : ∀ (A : Square n) (x y : nat), x < n → y < n →
                                         op_to_I A → op_to_I (col_swap A x y)
| otI_scale : ∀ (A : Square n) (x : nat) (c : C), x < n → c ≠ C0 →
                                         op_to_I A → op_to_I (col_scale A x c)
| otI_add : ∀ (A : Square n) (x y : nat) (c : C), x < n → y < n → x ≠ y →
                                         op_to_I A → op_to_I (col_add A x y c).

Lemma op_to_I_WF : ∀ {n} (A : Square n),
  op_to_I A → WF_Matrix A.

#[export] Hint Resolve op_to_I_WF : wf_db.

Definition otI_multiplicative {n} (A : Square n) : Prop :=
  ∀ (B : Square n), (op_to_I B → op_to_I (B × A)).

Lemma otI_implies_otI_multiplicative : ∀ {n} (A : Square n),
  op_to_I A → otI_multiplicative A.

Lemma otI_Mmult : ∀ {n} (A B : Square n),
  op_to_I A → op_to_I B →
  op_to_I (A × B).

Definition otI_pad1ed {n} (A : Square n) : Prop :=
  ∀ (c : C), (c ≠ C0 → op_to_I (pad1 A c)).

Lemma otI_implies_otI_pad1ed : ∀ {n} (A : Square n),
  op_to_I A → otI_pad1ed A.

Lemma otI_pad1 : ∀ {n} (A : Square n) (c : C),
  c ≠ C0 → op_to_I A →
  op_to_I (pad1 A c).

Lemma otI_lin_indep : ∀ {n} (A : Square n),
  op_to_I A → linearly_independent A.

Definition op_to_I' {n m : nat} (A : Matrix n m) :=
  n = m ∧ @op_to_I n A.

Lemma otI_equiv_otI' : ∀ {n} (A : Square n),
  op_to_I' A ↔ op_to_I A.

Lemma otI'_add_invr : invr_col_add (@op_to_I').

Lemma otI_col_add_many : ∀ (n col : nat) (A : Square n) (as' : Vector n),
  col < n → as' col 0 = C0 →
  op_to_I A → op_to_I (col_add_many col as' A).

Lemma otI_col_add_each : ∀ (n col : nat) (A : Square n) (as' : Matrix 1 n),
  col < n → WF_Matrix as' → as' 0 col = C0 →
  op_to_I A → op_to_I (col_add_each col as' A).

Now we prove more properties of invariants

a case for when we consider (Mat -> Prop)s that are the same as lin_indep, invertible, etc... these props will satisfy 'prop_zero_false P'
Lemma mpr_step1_pzf_P : ∀ {n} (A : Square (S n)) (P : ∀ m o, Matrix m o → Prop),
  invr_col_add P → invr_col_scale P →
  prop_zero_false P →
  WF_Matrix A → P (S n) (S n) A →
  (∃ B : Square (S n), op_to_I B ∧ P (S n) (S n) (A × B) ∧
                       (∃ i, i < (S n) ∧ get_vec i (A × B) = e_i 0)).

a different case for when we consider (Mat -> Prop)s that are the same as lin_dep, not_invertible, etc...
Lemma mrp_step1_pzt_P0 : ∀ {n} (A : Square (S n)) (P P0: ∀ m o, Matrix m o → Prop),
  invr_col_add P → invr_col_scale P →
  invr_col_add P0 → prop_zero_true P0 →
  WF_Matrix A → P (S n) (S n) A →
  (∃ B : Square (S n), op_to_I B ∧ P (S n) (S n) (A × B) ∧
                       (∃ i, i < (S n) ∧ get_vec i (A × B) = e_i 0)) ∨ P0 (S n) (S n) A.

in both cases, we can use mrp_step2 when we get that (exists i, ... )
Lemma mpr_step2 : ∀ {n} (A : Square (S n)) (P : ∀ m o, Matrix m o → Prop),
  invr_col_add P → invr_col_swap P →
  WF_Matrix A → P (S n) (S n) A →
  (∃ i, i < (S n) ∧ get_vec i A = e_i 0) →
  (∃ B : Square (S n), op_to_I B ∧ P (S n) (S n) (A × B) ∧
                            (∃ a : Square n, pad1 a C1 = (A × B))).

these two lemmas allow us to reduce our study of Square (S n) to Square n, allowing us to induct on n. Then, 'invr_pad1 P' allows us to jump from the n case to (S n)
Lemma mat_prop_reduce_pzf_P : ∀ {n} (A : Square (S n)) (P : ∀ m o, Matrix m o → Prop),
  invr_col_swap P → invr_col_scale P →
  invr_col_add P → prop_zero_false P →
  invr_pad1 P →
  WF_Matrix A → P (S n) (S n) A →
  (∃ B : Square (S n), op_to_I B ∧ P (S n) (S n) (A × B) ∧
                            (∃ a : Square n, pad1 a C1 = (A × B))).

Lemma mat_prop_reduce_pzt_P0 : ∀ {n} (A : Square (S n)) (P P0 : ∀ m o, Matrix m o → Prop),
  invr_col_swap P → invr_col_scale P →
  invr_col_add P →
  invr_pad1 P →
  invr_col_add P0 → prop_zero_true P0 →
  WF_Matrix A → P (S n) (S n) A →
  (∃ B : Square (S n), op_to_I B ∧ P (S n) (S n) (A × B) ∧
                            (∃ a : Square n, pad1 a C1 = (A × B))) ∨ P0 (S n) (S n) A.

now, we prove some theorems with these powerful lemmas
Theorem invr_P_implies_invertible_r : ∀ {n} (A : Square n) (P : ∀ m o, Matrix m o → Prop),
  invr_col_swap P → invr_col_scale P →
  invr_col_add P → prop_zero_false P →
  invr_pad1 P →
  WF_Matrix A → P n n A →
  (∃ B, op_to_I B ∧ A × B = I n).

Corollary lin_ind_implies_invertible_r : ∀ {n} (A : Square n),
  WF_Matrix A →
  linearly_independent A →
  (∃ B, op_to_I B ∧ A × B = I n).

Inverses of square matrices


Definition Minv {n : nat} (A B : Square n) : Prop := A × B = I n ∧ B × A = I n.

Definition invertible {n : nat} (A : Square n) : Prop :=
  ∃ B, Minv A B.

Lemma Minv_unique : ∀ (n : nat) (A B C : Square n),
                      WF_Matrix A → WF_Matrix B → WF_Matrix C →
                      Minv A B → Minv A C → B = C.

Lemma Minv_symm : ∀ (n : nat) (A B : Square n), Minv A B → Minv B A.

Lemma Minv_flip : ∀ (n : nat) (A B : Square n),
  WF_Matrix A → WF_Matrix B →
  A × B = I n → B × A = I n.

Lemma Minv_left : ∀ (n : nat) (A B : Square n),
    WF_Matrix A → WF_Matrix B →
    A × B = I n → Minv A B.

Lemma Minv_right : ∀ (n : nat) (A B : Square n),
    WF_Matrix A → WF_Matrix B →
    B × A = I n → Minv A B.

Corollary lin_indep_invertible : ∀ (n : nat) (A : Square n),
  WF_Matrix A → (linearly_independent A ↔ invertible A).

Lemma Minv_otI_l : ∀ (n : nat) (A B : Square n),
  WF_Matrix A → WF_Matrix B →
  Minv A B →
  op_to_I A.

We finish proving lemmas about invarients

Finally, we show that if all 6 nice properties are true about two (Mat -> Prop)s, then they are equivalent on well formed matrices
Theorem invr_P_equiv_otI : ∀ {n} (A : Square n) (P : ∀ m o, Matrix m o → Prop),
  invr_col_swap P → invr_col_scale P →
  invr_col_add P → prop_zero_false P →
  invr_pad1 P → P n n (I n) →
  WF_Matrix A →
  (P n n A ↔ op_to_I A).

slightly weaker version, if 4 nice properties are true, then op_to_I -> P
Theorem invr_P_implies_otI_weak : ∀ {n} (A : Square n) (P : ∀ m o, Matrix m o → Prop),
  invr_col_swap P → invr_col_scale P →
  invr_col_add P →
  P n n (I n) →
  (op_to_I A → P n n A).

Corollary lin_indep_det_neq_0 : ∀ {n} (A : Square n),
  WF_Matrix A → (linearly_independent A ↔ det_neq_0 A).

Corollary lin_dep_det_eq_0 : ∀ {n} (A : Square n),
  WF_Matrix A → (linearly_dependent A ↔ det_eq_c C0 A).

Corollary lin_dep_indep_dec : ∀ {n} (A : Square n),
  WF_Matrix A → { linearly_independent A } + { linearly_dependent A }.

we define another set of invariants to help show that Det A × Det B = Det (A × B)


Definition Det_mult_comm_l (n m : nat) (A : Matrix n m) :=
  n = m ∧ (∀ (B : Square n), (Determinant B) × (@Determinant n A) = (@Determinant n (B × A)))%C.

Lemma Dmc_I : ∀ {n}, Det_mult_comm_l n n (I n).

Lemma Dmc_make_WF : ∀ {n} (A : Square n),
  Det_mult_comm_l n n (make_WF A) ↔ Det_mult_comm_l n n A.

Lemma Dmc_Mmult : ∀ {n} (A B : Square n),
  Det_mult_comm_l n n A → Det_mult_comm_l n n B →
  Det_mult_comm_l n n (A × B).

Lemma Dmc_swap_I : ∀ (n x y : nat),
  x < n → y < n →
  Det_mult_comm_l n n (row_swap (I n) x y).

Lemma Dmc_scale_I : ∀ (n x : nat) (c : C),
  Det_mult_comm_l n n (row_scale (I n) x c).

Lemma Dmc_add_I : ∀ (n x y : nat) (c : C),
  x ≠ y → x < n → y < n → Det_mult_comm_l n n (row_add (I n) x y c).

Lemma Dmc_swap_invr : invr_col_swap (Det_mult_comm_l).

Lemma Dmc_scale_invr : invr_col_scale (Det_mult_comm_l).

Lemma Dmc_add_invr : invr_col_add (Det_mult_comm_l).

Local Close Scope nat_scope.

Lemma otI_Dmc : ∀ {n} (A : Square n),
  op_to_I A → Det_mult_comm_l n n A.

Lemma Determinant_multiplicative_WF : ∀ {n} (A B : Square n),
  WF_Matrix A → WF_Matrix B →
  (Determinant A) × (Determinant B) = Determinant (A × B).

Theorem Determinant_multiplicative : ∀ {n} (A B : Square n),
  (Determinant A) × (Determinant B) = Determinant (A × B).