Theory Tensor_Rank

(* Author: Alexander Bentkamp, Universität des Saarlandes
*)
section ‹Tensor CP-Rank›

theory Tensor_Rank
imports Tensor_Unit_Vec
begin

inductive cprank_max1::"'a::ring_1 tensor  bool" where
order1: "order A  1  cprank_max1 A" |
higher_order: "order A = 1  cprank_max1 B  cprank_max1 (A  B)"

lemma cprank_max1_order0: "cprank_max1 B  order A = 0  cprank_max1 (A  B)"
proof (induction B rule:cprank_max1.induct)
  case order1
  then show ?case by (simp add: cprank_max1.order1)
next
  case (higher_order A' B)
  then have "order (A  A') = 1" by simp
  then show ?case using higher_order cprank_max1.higher_order by (metis mult.assoc)
qed

lemma cprank_max1_order_le1: "order A  0  cprank_max1 B  cprank_max1 (A  B)"
by (simp add: cprank_max1_order0)

lemma cprank_max1_prod: "cprank_max1 A  cprank_max1 B  cprank_max1 (A  B)"
  apply(induction A rule: cprank_max1.induct)
 apply (meson higher_order le_neq_trans less_one cprank_max1_order0)
by (simp add: higher_order mult.assoc)

lemma cprank_max1_prod_list:
assumes "B. Bset Bs  cprank_max1 B"
shows "cprank_max1 (prod_list Bs)"
  using assms by (induction Bs, metis dims_smult dims_tensor0 list.size(3) prod_list.Nil order1 order_0_multiple_of_one zero_le_one, simp add: cprank_max1_prod)

lemma cprank_max1_prod_listE:
  fixes A::"'a::comm_ring_1 tensor"
  assumes "cprank_max1 A"
  obtains Bs a where "B. Bset Bs  order B = 1" "a  prod_list Bs = A"
using assms proof (induction A arbitrary:thesis rule:cprank_max1.induct)
  case (order1 A)
  then show ?case
  proof (cases "order A = 0")
    case True
    then obtain a where "A = a  prod_list []" using order_0_multiple_of_one using prod_list.Nil by auto
    then show ?thesis using length_pos_if_in_set order1.prems by fastforce
  next
    case False
    then have "order A = 1" using order1 by linarith
    then have "A = 1  prod_list [A]" by (simp add: smult_1)
    then show ?thesis by (metis order A = 1 length_greater_0_conv length_pos_if_in_set order1.prems set_ConsD)
  qed
next
  case (higher_order A B)
  then obtain Bs b where "(B'. B'  set Bs  order B' = 1)" "b  prod_list Bs = B" by metis
  then have "(B. B  set (A # Bs)  order B = 1)" using higher_order by auto
  have "A  B = b  (A  prod_list Bs)" using smult_prod_extract2  b  prod_list Bs = B by metis
  then show ?case by (metis Ba. Ba  set (A # Bs)  order Ba = 1 higher_order.prems prod_list.Cons)
qed

inductive cprank_max :: "nat  'a::ring_1 tensor  bool" where
cprank_max0: "cprank_max 0 (tensor0 ds)" |
cprank_max_Suc: "dims A = dims B  cprank_max1 A  cprank_max j B  cprank_max (Suc j) (A+B)"

lemma cprank_max1: "cprank_max1 A  cprank_max 1 A"
  by (metis One_nat_def dims_tensor0 cprank_max.simps cprank_max0 tensor_add_0_right)

lemma cprank_max_plus: "cprank_max i A  cprank_max j B  dims A = dims B  cprank_max (i+j) (A+B)"
apply (induction A rule:cprank_max.induct)
 apply auto[1]
by (metis add_Suc plus_assoc plus_dim1 cprank_max.intros(2))

lemma cprank_max_listsum:
assumes "A. Aset As  dims A = ds"
and "A. Aset As  cprank_max n A"
shows "cprank_max (n*length As) (listsum ds As)"
using assms proof (induction As)
  case Nil
  then show ?case using listsum_Nil cprank_max.simps by fastforce
next
  case (Cons A As)
  then show ?case using cprank_max_plus[of n A "n * length As" "listsum ds As"]
    by (simp add: length_Cons list.set_intros(1) listsum_Cons listsum_dims set_subset_Cons subsetCE)
qed

lemma cprank_maxE:
assumes "cprank_max n A"
obtains BS where "(B. Bset BS  cprank_max1 B)" and "(B. Bset BS  dims A = dims B)" and "listsum (dims A) BS = A" and "length BS = n"
using assms proof (induction arbitrary:thesis rule:cprank_max.induct)
  case (cprank_max0 ds)
  have "Tensor_Plus.listsum (dims (tensor0 ds)) [] = tensor0 ds" by (simp add: listsum_Nil)
  then show ?case using cprank_max0.prems by fastforce
next
  case (cprank_max_Suc A B j)
  then obtain BS where BS_def:"(B. B  set BS  cprank_max1 B)" "(B'. B'  set BS  dims B' = dims B)"
                       "listsum (dims B) BS = B" "length BS = j" by metis
  then have "listsum (dims (A + B)) (A # BS) = A + B"
    by (simp add: listsum_Cons cprank_max_Suc.hyps(1))
  then show ?case using BS_def length_Cons cprank_max_Suc.hyps(2) cprank_max_Suc.prems set_ConsD
    by (metis plus_dim1 cprank_max_Suc.hyps(1))
qed

lemma cprank_maxI:
assumes "B. Bset BS  cprank_max1 B"
and "B. Bset BS  dims B = ds"
shows "cprank_max (length BS) (listsum ds BS)"
using assms proof (induction BS)
  case Nil
  then show ?case by (simp add: listsum_Nil cprank_max0)
next
  case (Cons B BS)
  then show ?case
    by (simp add: length_Cons list.set_intros(1) list.set_intros(2) listsum_Cons listsum_dims cprank_max_Suc)
qed

lemma cprank_max_0E: "cprank_max 0 A  A = tensor0 (dims A)" by (metis dims_tensor0 length_0_conv cprank_max0 cprank_maxE)

lemma listsum_prod_distr_right:
assumes "(C. Cset CS  dims C = ds)"
shows "A  listsum ds CS = listsum (dims A @ ds) (map (λC. A  C) CS)"
using assms proof (induction CS)
  case Nil
  then show ?case by (simp add:listsum_Nil)
next
  case (Cons C CS)
  then have "dims C = dims (listsum ds CS)" by (simp add: list.set_intros(1) list.set_intros(2) listsum_dims)
  then show ?case unfolding listsum_Cons list.map(2)
    using tensor_prod_distr_right Cons.IH Cons.prems list.set_intros(2) by fastforce
qed

lemma cprank_max_prod_order1:
assumes "order A = 1"
and "cprank_max n B"
shows "cprank_max n (AB)"
proof -
  obtain CS where "(C. Cset CS  cprank_max1 C)"
              and "(C. Cset CS  dims C = dims B)"
              and "listsum (dims B) CS = B"
              and "length CS = n"
    using assms(2) cprank_maxE by metis
  define CS' where "CS' = map (λC. AC) CS"
  then have "C'. C'set CS'  cprank_max1 C'"
    using assms(1) higher_order C. C  set CS  cprank_max1 C imageE set_map by auto
  have "listsum (dims A @ dims B) CS' = AB" using CS'_def Tensor_Plus.listsum (dims B) CS = B
    using Ca. Ca  set CS  dims Ca = dims B listsum_prod_distr_right by fastforce
  then show ?thesis by (metis (mono_tags, lifting) CS'_def C'. C'  set CS'  cprank_max1 C' Ca. Ca  set CS  dims Ca = dims B length CS = n dims_tensor_prod imageE length_map cprank_maxI set_map)
qed

lemma cprank_max_upper_bound: (* Stronger bound is possible, one of the factors in prod_list can be dropped. *)
shows "cprank_max (prod_list (dims A)) A"
proof (induction A rule:subtensor_induct)
  case (order_0 A)
  then have "cprank_max 1 A" using order1 cprank_max1 by force
  then show ?case using order_0 by auto
next
  case (order_step A)
  define Bs where "Bs = map (λi. unit_vec (hd (dims A)) i  subtensor A i) [0..<hd (dims A)]"
  have "B. B  set Bs  dims A = dims B"
  proof -
    fix B assume "B  set Bs"
    obtain i where "i<hd (dims A)" "Bs!i=B" using Bs_def B  set Bs by auto
    then have "dims (unit_vec (hd (dims A)) i  subtensor A i) = dims A"
      using dims_unit_vec order_step.hyps
      by (metis append_Cons dims_subtensor dims_tensor_prod list.exhaust_sel self_append_conv2)
    then show "dims A = dims B" using Bs_def Bs ! i = B i < hd (dims A) by auto
  qed
  have "B. B  set Bs  cprank_max (prod_list (tl (dims A))) B"
  proof -
    fix B assume "B  set Bs"
    obtain i where "i<hd (dims A)" "Bs!i=B" using Bs_def B  set Bs by auto
    then have "cprank_max (prod_list (tl (dims A))) (unit_vec (hd (dims A)) i  subtensor A i)"
      by (metis One_nat_def dims_subtensor dims_unit_vec length_Cons list.size(3) order_step.IH order_step.hyps cprank_max_prod_order1)
    then show "cprank_max (prod_list (tl (dims A))) B" using Bs_def Bs ! i = B i < hd (dims A) by auto
  qed
  then show ?case using subtensor_decomposition[OF order_step.hyps] cprank_max_listsum
    by (metis (no_types, lifting) Bs_def Ba. Ba  set Bs  dims A = dims Ba diff_zero length_map length_upt list.exhaust_sel prod_list.Cons mult.commute order_step.hyps)
qed

definition cprank :: "'a::ring_1 tensor  nat" where
"cprank A = (LEAST n. cprank_max n A)"

lemma cprank_upper_bound: "cprank A  prod_list (dims A)"
unfolding cprank_def using cprank_max_upper_bound Least_le by fastforce

lemma cprank_max_cprank: "cprank_max (cprank A) A"
  unfolding cprank_def using cprank_max_upper_bound by (metis LeastI)

end