From 66cd4f11969022f058fac6f89208929d64a09c16 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Sun, 20 Mar 2016 17:15:49 -0400 Subject: [PATCH] feat(algebra/matrix): generalize theorems, define module/ring instances --- library/algebra/matrix.lean | 274 ++++++++++++++++++++++++++++++------ 1 file changed, 229 insertions(+), 45 deletions(-) diff --git a/library/algebra/matrix.lean b/library/algebra/matrix.lean index e8e90f41f..d9d4360d7 100644 --- a/library/algebra/matrix.lean +++ b/library/algebra/matrix.lean @@ -1,24 +1,26 @@ -import data.real data.tuple data.fin algebra.field data.list +import data.real data.tuple data.fin algebra.module data.list open nat tuple eq.ops rat -- list namespace matrix -definition matrix (A : Type) [field A] (m n : ℕ) := fin m → fin n → A +definition matrix (A : Type) (m n : ℕ) := fin m → fin n → A -definition rvector (A : Type) [field A] (n : ℕ) := matrix A 1 n +definition rvector (A : Type) (n : ℕ) := matrix A 1 n -definition cvector (A : Type) [field A] (m : ℕ) := matrix A m 1 +definition cvector (A : Type) (m : ℕ) := matrix A m 1 + +/-definition val_of_singleton_matrix [coercion] {A : Type} (M : matrix A 1 1) : A := + M !fin.zero !fin.zero-/ -- useful for testing -definition cvector_of_list {A : Type} [field A] (l : list A) : cvector A (list.length l) := +definition cvector_of_list {A : Type} (l : list A) : cvector A (list.length l) := λ i j, list.ith l (fin.val i) !fin.val_lt -definition rvector_of_list {A : Type} [field A] (l : list A) : rvector A (list.length l) := +definition rvector_of_list {A : Type} (l : list A) : rvector A (list.length l) := λ i j, list.ith l (fin.val j) !fin.val_lt section variable {A : Type} -variable [linear_ordered_field A] variables {m n k : ℕ} definition col_of (M : matrix A m n) (j : fin n) : cvector A m := λ a b, M a j @@ -29,16 +31,16 @@ definition r_ith (v : rvector A n) (i : fin n) := v !fin.zero i definition c_ith (v : cvector A m) (i : fin m) := v i !fin.zero -definition nonneg (M : matrix A m n) := ∀ i j, M i j ≥ 0 +definition nonneg [weak_order A] [has_zero A] (M : matrix A m n) := ∀ i j, M i j ≥ 0 -definition r_dot (u v : rvector A n) := Suml (fin.upto n) (λ i, r_ith u i * r_ith v i) +definition r_dot [semiring A] (u v : rvector A n) := Suml (fin.upto n) (λ i, r_ith u i * r_ith v i) -definition c_dot (u v : cvector A m) := Suml (fin.upto m) (λ i, c_ith u i * c_ith v i) +definition c_dot [semiring A] (u v : cvector A m) := Suml (fin.upto m) (λ i, c_ith u i * c_ith v i) -- generalize this to transpose and remove coercion definition cvector_of_rvector [coercion] (u : rvector A n) : cvector A n := λ i j, u !fin.zero i -definition mul (M : matrix A m n) (N : matrix A n k) : matrix A m k := +definition mul [semiring A] (M : matrix A m n) (N : matrix A n k) : matrix A m k := λ (a : fin m) (b : fin k), c_dot (cvector_of_rvector (row_of M a)) (col_of N b) -- why doesn't coercion work? infix `⬝` := mul @@ -70,7 +72,13 @@ theorem col_of_cvector (v : cvector A m) : col_of v !fin.zero = v := rewrite (fin_one_eq_zero y) end -theorem Suml_assoc {B C : Type} (la : list B) (lb : list C) (f : B → C → A) : +theorem row_of_ith (M : matrix A m n) (x : fin m) (y : fin n) : (row_of M x) !fin.zero y = M x y := + rfl + +theorem col_of_ith (M : matrix A m n) (x : fin m) (y : fin n) : (col_of M y) x !fin.zero = M x y := + rfl + +theorem Suml_assoc [semiring A] {B C : Type} (la : list B) (lb : list C) (f : B → C → A) : Suml la (λ a, Suml lb (λ b, f a b)) = Suml lb (λ b, Suml la (λ a, f a b)) := begin @@ -95,7 +103,7 @@ theorem length_cons_pos {A : Type} (h : A) (tt : list A) : 0 < list.length (list apply !list.cons_ne_nil H' end -theorem big_sum_dist_left (a : A) {T : Type} (f : T → A) (l : list T) : +theorem big_sum_dist_left [semiring A] (a : A) {T : Type} (f : T → A) (l : list T) : a * Suml l f = Suml l (λ k, a * f k) := begin induction l with h tt ih, @@ -103,7 +111,7 @@ theorem big_sum_dist_left (a : A) {T : Type} (f : T → A) (l : list T) : rewrite [*Suml_cons, left_distrib, ih] end -theorem big_sum_dist_right (a : A) {T : Type} (f : T → A) (l : list T) : +theorem big_sum_dist_right [semiring A] (a : A) {T : Type} (f : T → A) (l : list T) : Suml l f * a= Suml l (λ k, f k * a) := begin induction l with h tt ih, @@ -111,7 +119,7 @@ theorem big_sum_dist_right (a : A) {T : Type} (f : T → A) (l : list T) : rewrite [*Suml_cons, right_distrib, ih] end -theorem Suml_nonneg_of_nonneg {T : Type} (l : list T) (f : T → A) +theorem Suml_nonneg_of_nonneg [ordered_semiring A] {T : Type} (l : list T) (f : T → A) (H : Π (i : ℕ) (Hi : i < list.length l), f (list.ith l i Hi) ≥ 0) : Suml l f ≥ (0 : A) := begin induction l with h tt ih, @@ -135,7 +143,7 @@ theorem Suml_nonneg_of_nonneg {T : Type} (l : list T) (f : T → A) exact add_nonneg Hh Htt end -theorem Suml_le_of_le {T : Type} (l : list T) (f g : T → A) (H : ∀ t : T, f t ≤ g t) : +theorem Suml_le_of_le [ordered_semiring A] {T : Type} (l : list T) (f g : T → A) (H : ∀ t : T, f t ≤ g t) : Suml l f ≤ Suml l g := begin induction l, @@ -146,7 +154,7 @@ theorem Suml_le_of_le {T : Type} (l : list T) (f g : T → A) (H : ∀ t : T, f assumption} end -theorem inner_sum_assoc {S T : Type} (l1 : list S) (l2 : list T) (f : S → A) (g : S → T → A) : +theorem inner_sum_assoc [semiring A] {S T : Type} (l1 : list S) (l2 : list T) (f : S → A) (g : S → T → A) : Suml l1 (λ s, f s * Suml l2 (λ t, g s t)) = Suml l1 (λ s, Suml l2 (λ t, f s * g s t)) := begin congruence, @@ -155,34 +163,36 @@ theorem inner_sum_assoc {S T : Type} (l1 : list S) (l2 : list T) (f : S → A) ( rewrite big_sum_dist_left end --- clean this up... -theorem dot_mul_assoc (y : rvector A m) (M : matrix A m n) (x : cvector A n) : - y ⬝ (M ⬝ x) = (y ⬝ M) ⬝ x := +theorem Suml_distrib [semiring A] {S : Type} (l : list S) (f : S → A) (a : A) : + Suml l (λ x, f x * a) = (Suml l f) * a := + begin + induction l, + {rewrite [*Suml_nil, zero_mul]}, + {rewrite [*Suml_cons, right_distrib], congruence, assumption} + end + +theorem m_mul_assoc [semiring A] {o p : ℕ} (M : matrix A m n) (N : matrix A n o) (O : matrix A o p) : + M ⬝ (N ⬝ O) = (M ⬝ N) ⬝ O := begin rewrite ↑mul, repeat (apply funext; intro), - rewrite [fin_one_eq_zero x_1, fin_one_eq_zero x_2, ↑c_dot, ↑c_ith, *row_of_rvector, *col_of_cvector], - rewrite [inner_sum_assoc, Suml_assoc], - congruence, - apply funext, - intro b, - unfold cvector_of_rvector, - rewrite big_sum_dist_right, - congruence, - apply funext, - intro b, - unfold row_of, unfold col_of, - rewrite *mul.assoc + rewrite [↑c_dot, ↑c_ith, ↑row_of, ↑cvector_of_rvector, ↑col_of, inner_sum_assoc, Suml_assoc], + congruence, apply funext, intro, + rewrite -Suml_distrib, + congruence, apply funext, intro, + rewrite mul.assoc end -theorem cvector_of_rvector_nonneg_of_nonneg {u : rvector A n} (Hu : nonneg u) : nonneg (cvector_of_rvector u) := +theorem cvector_of_rvector_nonneg_of_nonneg [weak_order A] [has_zero A] {u : rvector A n} (Hu : nonneg u) : + nonneg (cvector_of_rvector u) := λ i j, !Hu theorem c_ith_cvector_of_rvector_eq_c_ith (u : rvector A n) (i : fin n) : c_ith (cvector_of_rvector u) i = r_ith u i := rfl -theorem c_dot_nonneg_of_nonneg (u v : cvector A m) (Hu : nonneg u) (Hv : nonneg v) : c_dot u v ≥ 0 := +theorem c_dot_nonneg_of_nonneg [ordered_semiring A] (u v : cvector A m) (Hu : nonneg u) (Hv : nonneg v) : + c_dot u v ≥ 0 := begin unfold c_dot, apply Suml_nonneg_of_nonneg, @@ -192,14 +202,16 @@ theorem c_dot_nonneg_of_nonneg (u v : cvector A m) (Hu : nonneg u) (Hv : nonneg apply Hv end -theorem row_of_nonneg_of_nonneg {M : matrix A m n} (HM : nonneg M) (i : fin m) : nonneg (row_of M i) := +theorem row_of_nonneg_of_nonneg [weak_order A] [has_zero A] {M : matrix A m n} (HM : nonneg M) (i : fin m) : + nonneg (row_of M i) := λ a b, !HM -theorem col_of_nonneg_of_nonneg {M : matrix A m n} (HM : nonneg M) (i : fin n) : nonneg (col_of M i) := +theorem col_of_nonneg_of_nonneg [weak_order A] [has_zero A] {M : matrix A m n} (HM : nonneg M) (i : fin n) : + nonneg (col_of M i) := λ a b, !HM -theorem mul_nonneg_of_nonneg (M : matrix A m n) (N : matrix A n k) (HM : nonneg M) (HN : nonneg N) : - nonneg (M ⬝ N) := +theorem mul_nonneg_of_nonneg [ordered_semiring A] (M : matrix A m n) (N : matrix A n k) + (HM : nonneg M) (HN : nonneg N) : nonneg (M ⬝ N) := begin intros, unfold mul, @@ -213,7 +225,7 @@ theorem mul_nonneg_of_nonneg (M : matrix A m n) (N : matrix A n k) (HM : nonneg One direction of Farkas' lemma -/ -theorem farkas_rl (M : matrix A m n) (b : cvector A m) +theorem farkas_rl [ordered_semiring A] (M : matrix A m n) (b : cvector A m) (H : ∃ y : rvector A m, nonneg (y ⬝ M) ∧ (y ⬝ b) !fin.zero !fin.zero < 0) : ¬ ∃ x : cvector A n, nonneg x ∧ M ⬝ x = b := begin @@ -222,10 +234,10 @@ theorem farkas_rl (M : matrix A m n) (b : cvector A m) cases Hx with Nx Mxb, cases H with y Hy, cases Hy with NA Nmyb, - rewrite [-Mxb at Nmyb, dot_mul_assoc at Nmyb], + rewrite [-Mxb at Nmyb, m_mul_assoc at Nmyb], apply not_le_of_gt Nmyb, apply mul_nonneg_of_nonneg, - repeat assumption + exact NA, exact Nx -- why doesn't assumption work here? end @@ -234,7 +246,7 @@ theorem farkas_rl (M : matrix A m n) (b : cvector A m) If you can find a nonnegative row vector c such that c ⬝ M = 0 and c ⬝ b < 0, then the system M ⬝ x ≤ b is unsat. -/ -theorem farkas_rl' (M : matrix A m n) (b : cvector A m) +theorem farkas_rl' [ordered_semiring A] (M : matrix A m n) (b : cvector A m) (H : ∃ c : rvector A m, nonneg c ∧ c ⬝ M = (λ x y, (0 : A)) ∧ (c ⬝ b) !fin.zero !fin.zero < 0) : ¬ ∃ x : cvector A n, ∀ i, (M ⬝ x) i !fin.zero ≤ c_ith b i := begin @@ -244,7 +256,7 @@ theorem farkas_rl' (M : matrix A m n) (b : cvector A m) cases Hc with Hcn Hc, cases Hc with HcM Hcb, have H : c ⬝ (M ⬝ x) = (λ a b, 0), begin - rewrite [dot_mul_assoc, HcM, ↑mul], + rewrite [m_mul_assoc, HcM, ↑mul], repeat (apply funext; intro), rewrite [fin_one_eq_zero, row_of_rvector, ↑c_dot], have Hz : (λ i, c_ith (cvector_of_rvector (λ (x : fin 1) (y : fin n), 0)) i * c_ith (col_of x x_2) i) @@ -271,6 +283,24 @@ theorem farkas_rl' (M : matrix A m n) (b : cvector A m) exact not_lt_self _ HZ end +/- + An alternate form of the above. +-/ +theorem farkas_rl'' [ordered_semiring A] (M : matrix A m n) (b : cvector A m) (c : rvector A m) + (Hcnn : nonneg c) (HcM : ∀ (x : fin n), (c ⬝ M) !fin.zero x = 0) (Hcb : (c ⬝ b) !fin.zero !fin.zero < 0) : + ¬ ∃ x : cvector A n, ∀ i, (M ⬝ x) i !fin.zero ≤ c_ith b i := + begin + apply farkas_rl', + existsi c, + split, + assumption, + split, + repeat (apply funext; intro), + rewrite fin_one_eq_zero, + apply HcM, + assumption + end + section open list definition decidable_quant [instance] (P : fin n → Prop) [∀ k, decidable (P k)] : decidable (∀ k, P k) := @@ -287,6 +317,162 @@ definition matrix_decidable_eq [instance] [decidable_eq A] : decidable_eq (matri decidable.inr (begin intro Heq, apply H, intros, congruence, exact Heq end) end +end + +section matrix_arith_m_n + +definition m_add {A : Type} [has_add A] {m n : ℕ} (B C : matrix A m n) : matrix A m n := + λ x y, B x y + C x y + +definition m_neg {A : Type} [has_neg A] {m n : ℕ} (B : matrix A m n) : matrix A m n := + λ x y, -B x y + +definition m_smul {A : Type} [has_mul A] {m n : ℕ} (c : A) (B : matrix A m n) : matrix A m n := + λ x y, c * B x y + +definition m_left_module [instance] [reducible] (A : Type) [ring A] (m n : ℕ) : left_module A (matrix A m n) := + begin + fapply left_module.mk, + {exact m_smul}, + {exact m_add}, + {intros, unfold m_add, repeat (apply funext; intro), rewrite add.assoc}, + {exact λ a b, 0}, + {intros, unfold m_add, repeat (apply funext; intro), rewrite zero_add}, + {intros, unfold m_add, repeat (apply funext; intro), rewrite add_zero}, + {exact m_neg}, + {intros, rewrite [↑m_neg, ↑m_add], repeat (apply funext; intro), rewrite add.left_inv}, + {intros, unfold m_add, repeat (apply funext; intro), rewrite add.comm}, + {intros, rewrite [↑m_smul, ↑m_add], repeat (apply funext; intro), rewrite left_distrib}, + {intros, rewrite [↑m_smul, ↑m_add], repeat (apply funext; intro), rewrite -right_distrib}, + {intros, unfold m_smul, repeat (apply funext; intro), rewrite mul.assoc}, + {intro, unfold m_smul, repeat (apply funext; intro), rewrite one_mul} + end + +end matrix_arith_m_n + +theorem false_of_fin_zero (x : fin 0) : false := + have t : empty, from equiv.fn (fin.fin_zero_equiv_empty) x, + empty.induction_on (λ c, false) t + +section matrix_arith_square +open fin +definition sq_matrix_id (A : Type) [has_zero A] [has_one A] (m : ℕ) : matrix A m m := + λ x y, if x = y then 1 else 0 + +theorem Suml_map {A B C : Type} [add_monoid C] (l : list A) (f : A → B) (g : B → C) : + Suml (list.map f l) g = Suml l (λ a, g (f a)) := + begin + induction l, + rewrite Suml_nil, + rewrite [list.map_cons, *Suml_cons, v_0] + end + +-- this is annoying! +theorem b_vec_dot {A : Type} [semiring A] {m : ℕ} (k : fin m) (f : fin m → A) : + Suml (upto m) (λ j, (f j) * if j = k then 1 else 0) = f k := + begin + induction m, + apply false.elim (false_of_fin_zero k), + rewrite [upto_succ, Suml_cons], + cases decidable.em (maxi = k) with Heq Hneq, + {rewrite [if_pos Heq, -Heq, mul_one, -add_zero (f maxi) at {2}], + congruence, + have H : (λ a_1 : fin a, f (lift_succ a_1) * ite (lift_succ a_1 = maxi) 1 0) = (λ a_1, 0), begin + apply funext, + intro b, + rewrite [if_neg lift_succ_ne_max, mul_zero] + end, + rewrite [Suml_map, H, Suml_zero]}, + {rewrite [if_neg Hneq, mul_zero, zero_add, Suml_map], + note Hlt := lt_max_of_ne_max (ne.symm Hneq), + have Hfk : f k = f (lift_succ (fin.mk (val k) Hlt)), begin + congruence, + induction k with kv Hkv, + exact rfl + end, + rewrite [Hfk, -(v_0 (fin.mk (val k) Hlt) (λ v, f (lift_succ v)))], + congruence, apply funext, intro j, + cases decidable.em (lift_succ j = k) with Hjk Hnjk, + have Hjk' : j = mk (val k) Hlt, begin + induction j with vj Hvj, + congruence, + rewrite -Hjk + end, + rewrite [if_pos Hjk, if_pos Hjk'], + have Hjk' : j ≠ mk (val k) Hlt, begin + intro Hjk, + apply Hnjk, + rewrite Hjk, + induction k, + unfold [lift_succ, lift] + end, + rewrite [if_neg Hnjk, if_neg Hjk']} + end + +theorem b_vec_dot' {A : Type} [semiring A] {m : ℕ} (k : fin m) (f : fin m → A) : + Suml (upto m) (λ j, (if k = j then 1 else 0) * f j) = f k := + begin + have H : (λ j, (if k = j then 1 else 0) * f j) = (λ j, (f j) * if j = k then 1 else 0), begin + apply funext, intro, + cases decidable.em (k = x) with Heq Hneq, + rewrite [if_pos Heq, if_pos (eq.symm Heq), mul_one, one_mul], + rewrite [if_neg Hneq, if_neg (ne.symm Hneq), mul_zero, zero_mul] + end, + rewrite [H, b_vec_dot] + end + +theorem sq_matrix_mul_one {A : Type} [semiring A] {m : ℕ} (M : matrix A m m) : mul M (sq_matrix_id A m) = M := + begin + rewrite [↑sq_matrix_id, ↑mul], + repeat (apply funext; intro), + rewrite [↑row_of, ↑cvector_of_rvector, ↑col_of, ↑c_dot, ↑c_ith, b_vec_dot] + end + +theorem sq_matrix_one_mul {A : Type} [semiring A] {m : ℕ} (M : matrix A m m) : mul (sq_matrix_id A m) M = M := + begin + rewrite [↑sq_matrix_id, ↑mul], + repeat (apply funext; intro), + rewrite [↑row_of, ↑cvector_of_rvector, ↑col_of, ↑c_dot, ↑c_ith, b_vec_dot'] + end + +theorem sq_matrix_left_distrib {A : Type} [ring A] {m : ℕ} (M N O : matrix A m m) : + mul M (m_add N O) = m_add (mul M N) (mul M O) := + begin + rewrite [↑mul, ↑m_add], + repeat (apply funext; intros), + rewrite [↑c_dot, ↑cvector_of_rvector, ↑row_of, ↑col_of, ↑c_ith, -Suml_add], + congruence, + apply funext, + intro, + rewrite left_distrib + end + +theorem sq_matrix_right_distrib {A : Type} [ring A] {m : ℕ} (M N O : matrix A m m) : + mul (m_add N O) M = m_add (mul N M) (mul O M) := + begin + rewrite [↑mul, ↑m_add], + repeat (apply funext; intros), + rewrite [↑c_dot, ↑cvector_of_rvector, ↑row_of, ↑col_of, ↑c_ith, -Suml_add], + congruence, + apply funext, + intro, + rewrite right_distrib + end + +definition m_square_ring [instance] [reducible] (A : Type) [ring A] (m : ℕ) : ring (matrix A m m) := + ⦃ring, m_left_module A m m, + mul := λ B C, mul B C, + mul_assoc := λ B C D, eq.symm !m_mul_assoc, + one := sq_matrix_id A m, + one_mul := sq_matrix_one_mul, + mul_one := sq_matrix_mul_one, + left_distrib := sq_matrix_left_distrib, + right_distrib := by intros; apply sq_matrix_right_distrib + ⦄ + +end matrix_arith_square + + section test open list rat -- why aren't rats pretty printing right? definition c1 : cvector ℚ _ := cvector_of_list [3, 4, 2] @@ -305,6 +491,4 @@ eval (c2 ⬝ c1) !fin.zero !fin.zero end test -end -check farkas_rl end matrix