Theory Quadrilateral_Inequality

section ‹Quadrangle Inequality›

theory Quadrilateral_Inequality
imports Main
begin

(* did not use @{const is_arg_min} because no benefit *)
definition is_arg_min_on :: "('a  ('b::linorder))  'a set  'a  bool" where
"is_arg_min_on f S x = (x  S  (y  S. f x  f y))"

definition Args_min_on :: "(int  ('b::linorder))  int set  int set" where
"Args_min_on f I = {k. is_arg_min_on f I k}"

lemmas Args_min_simps = Args_min_on_def is_arg_min_on_def

lemma is_arg_min_on_antimono: fixes f :: "_  _::order"
shows " is_arg_min_on f S x; f y  f x; y  S   is_arg_min_on f S y"
by (metis antisym is_arg_min_on_def)

lemma ex_is_arg_min_on_if_finite: fixes f :: "'a  'b :: linorder"
shows " finite S; S  {}   x. is_arg_min_on f S x"
unfolding is_arg_min_on_def using ex_min_if_finite[of "f ` S"] by fastforce


locale QI =
  fixes c_k :: "int  int  int  nat"
  fixes c :: "int  int  nat"
  and w :: "int  int  nat"
  assumes QI_w: "i  i'; i' < j; j  j' 
    w i j + w i' j' w i' j + w i j'"
  assumes monotone_w: "i  i'; i' < j; j  j'  w i' j  w i j'"
  assumes c_def: "i < j  c i j = Min ((c_k i j) ` {i+1..j})"
  assumes c_k_def: " i < j;  k  {i+1..j}  
    c_k i j k = w i j + c i (k-1) + c k j"
begin

abbreviation "mins i j  Args_min_on (c_k i j) {i+1..j}"

definition "K i j  (if i = j then i else Max (mins i j))"

lemma c_def_rec:
  "i < j  c i j = Min ((λk. c i (k-1) + c k j + w i j) ` {i+1..j})"
using c_def c_k_def by (auto simp: algebra_simps image_def)

lemma mins_subset: "mins i j  {i+1..j}"
by (auto simp: Args_min_simps)

lemma mins_nonempty: "i < j  mins i j  {}"
using ex_is_arg_min_on_if_finite[OF finite_atLeastAtMost_int, of "i+1" j "c_k i j"]
by(auto simp: Args_min_simps)

lemma finite_mins: "finite(mins i j)"
by(simp add: finite_subset[OF mins_subset])

lemma is_arg_min_on_Min:
assumes "finite A" "is_arg_min_on f A a" shows "Min (f ` A) = f a" 
proof -
  from assms(2) have "f ` A  {}"
    by (fastforce simp: is_arg_min_on_def)
  thus ?thesis using assms by (simp add: antisym is_arg_min_on_def)
qed

lemma c_k_with_K: "i < j  c i j = c_k i j (K i j)"
using Max_in[of "mins i j"] finite_mins[of i j] mins_nonempty[of i j]
  is_arg_min_on_Min[of "{i+1..j}" "c_k i j"]
by (auto simp: Args_min_simps c_def K_def)

lemma K_subset: assumes "i  j" shows "K i j  {i..j}" using mins_subset K_def
proof cases
  assume "i = j"
  thus ?thesis 
    using K_def by auto
next
  assume "¬i = j"
  hence "K i j  {i+1..j}" using mins_subset K_def i  j
    by (metis Max_in finite_mins less_le mins_nonempty subsetCE)

  thus ?thesis  by auto
qed

lemma lemma_2:
  " l = nat (j'- i);  i  i';  i'  j;  j  j' 
    c i j + c i' j'  c i j' + c i' j"
proof(induction l arbitrary: i i' j j' rule:less_induct)
  case (less l)
  show ?case 
  proof cases
    assume "l  1"
    hence "i = i'  j = j'" using less.prems by linarith
    thus ?case by auto
  next
    assume "¬ l  1"
    show ?case
    proof cases
      assume "i  i'" thus ?thesis using less.prems by auto
    next
      assume "¬i  i'"
      hence "i < i'" by simp
      show ?thesis 
      proof cases
        assume "j  j'" thus ?thesis using less.prems by auto
      next
        assume "¬ j  j'"
        show ?thesis 
        (*-----------------------case 1: i' = j --------------------------------------------------*)
        proof cases 
          assume "i' = j"
          let ?k = "K i j'"
          have "?k  {i+1..j'}" 
            unfolding K_def
            using mins_subset Max_in[OF finite_mins mins_nonempty] less.prems ¬ i'  i
            by (smt subsetCE)
          show ?thesis
          (*---------------------case 1.1: i' = j ∧ k ≤ j ----------------------------------------*)
          proof cases
            assume "?k  j"

            have a: "c i j  w i j + c i (?k-1) + c ?k j"
            proof -
              have "c i j = Min ((λk. c i (k-1) + c k j + w i j) ` {i+1..j})"
                using c_def_rec ¬ i'  i i' = j by auto
              also have "...  c i (?k-1) + c ?k j + w i j"
                using ?k{i+1..j'} ?k  j by simp
              finally show ?thesis by simp
            qed

            have "nat (j' - ?k) < l" using ?k{i+1..j'} less.prems by simp
            hence b: "c ?k j + c j j'  c ?k j' + c j j"
              using ?k  j less.prems
                less.IH [where i = ?k and i' = j and j = j and j' = j', OF _ refl]
              by auto

            have "c i j + c i' j' = c i j + c j j'" by (simp add: i' = j)
            also have "... w i j + c i (?k-1) + c ?k j + c j j'"
              using a by auto
            also have "...  w i j'+ c i (?k-1) + c ?k j + c j j'"
              using less.prems monotone_w i < i' by simp
            also have "...  w i j'+ c i (?k-1) + c ?k j' + c j j"
              using b by auto
            also have "... = c i j' + c j j" using ?k{i+1..j'}
              by(simp add: c_k_def c_k_with_K)
            finally show ?thesis by(simp add: i' = j)
          next
          (*---------------------case 1.2: i' = j ∧ k ≥ j ----------------------------------------*)
            assume "¬ ?k  j"
            hence "?k  {j+1..j'}" using ?k  {i+1..j'} by auto
            have a: "c j j'  w j j' + c j (?k-1) + c ?k j'"
            proof -
             have "c j j' = Min ((λk. c j (k-1) + c k j' + w j j') ` {j+1..j'})"
               using c_def_rec ¬ j'  j by auto
             also have "...  c j (?k-1) + c ?k j' + w j j'"
              using ?k  {j+1..j'} by simp
             finally show "c j j'  w j j' + c j (?k-1) + c ?k j'" by simp
            qed

            have "nat ((?k-1) -i) < l" using ?k  {i+1..j'} less.prems by simp
            hence b: "c i j + c j (?k-1)  c i (?k-1) + c j j"
              using less.prems ¬ ?k  j
                less.IH[where i=i and i'=j and j=j and j'="(?k-1)", OF _ refl]
              by auto

            have "c i j + c i' j' = c i j + c j j'" by(simp add: i' = j)
            also have "...  w j j' + c j (?k-1) + c ?k j' + c i j"
              using a by simp
            also have "...  w i j'+ c j (?k-1) + c ?k j' + c i j"
              using less.prems monotone_w ?k  {j+1..j'} by simp
            also have "...  w i j'+ c i (?k-1) + c ?k j' + c j j"
              using b by simp
            also have "...  c i j' + c j j"
              using ?k{i+1..j'} by (simp add: c_k_def c_k_with_K)
            finally show ?thesis by(simp add: i' = j)
          qed
        next
          (*---------------------case 2 i' ≠ j ---------------------------------------------------*)
          assume "i'  j"
          let ?y = "K i' j"
          let ?z = "K i j'"
          have "?y  {i'+1..j}"
            using mins_subset less.prems i'  j Max_in[OF finite_mins mins_nonempty]
            unfolding K_def by (metis le_less subsetCE)
          have "?z  {i+1..j'}"
            using mins_subset less.prems i'  j Max_in[OF finite_mins mins_nonempty]
            unfolding K_def by (smt subsetCE)
          have w_mon: "w i' j' + w i j  w i' j + w i j'"
            using less.prems QI_w i'  j by force

          have "i' < j'" "i < j" using i'  j less.prems by auto
          show ?thesis
          (*---------------------case 2.1 i' ≠ j ∧ z ≤ y ----------------------------------------*)
          proof cases
            assume "?z  ?y"
            have "?y  {i'+1..j'}" using less.prems ?y  {i'+1..j} by simp
            have "?z  {i+1..j}" using ?z  {i+1..j'} ?z  ?y ?y  {i'+1..j} by simp

            have a: "c i' j'  w i' j' + c i' (?y-1) + c ?y j'"
            proof -
              have "c i' j' = Min((λk. c i' (k-1) + c k j' + w i' j') ` {i'+1..j'})"
                by (simp add: c_def_rec[OF  i' < j'])
              also have "...  w i' j' + c i' (?y-1) + c ?y j'"
                using ?y  {i'+1..j'} by simp
              finally show ?thesis .
            qed

            have b: "c i j  w i j + c i (?z-1) + c ?z j"
            proof -
              have "c i j = Min ((λk. c i (k-1) + c k j + w i j)  ` {i+1..j})"
                using i < j by (simp add: c_def_rec)
              also have "...  w i j + c i (?z-1) + c ?z j"
                using ?z  {i+1..j} by simp
              finally show ?thesis .
            qed

            have "nat (j' - ?z) < l" using ?z  {i+1..j} less.prems by simp
            hence IH_step: "c ?z j + c ?y j'  c ?z j' + c ?y j"
              using ?z  ?y j  j' ?y  {i'+1..j}
               less.IH[where i = ?z and i' = ?y and j = j and j' = j', OF _ refl]
              by simp

            have "c i' j' + c i j
               w i' j + w i j' + c i' (?y-1) + c i (?z-1) + c ?y j' + c ?z j"
              using a b w_mon by simp
            also have "  w i j' + w i' j +  c i' (?y-1) + c i (?z-1) + c ?y j + c ?z j'"
              using IH_step by auto
            also have "... = c i j' + c i' j" using ?z  {i+1..j'} ?y  {i'+1..j}
              by(simp add: c_k_def c_k_with_K)
            finally show ?thesis by linarith
          next
            (*---------------------case 2.1 i' ≠ j ∧ z > y ---------------------------------------*)
            assume "¬?z  ?y"

            have "?y  {i+1..j}" using less.prems ?y  {i'+1..j} by simp
            have "?z  {i'+1..j'}" using ?z  {i+1..j'} ¬?z  ?y ?y  {i'+1..j}
              by simp

            have a: "c i' j'  w i' j' + c i' (?z-1) + c ?z j'"
            proof -
              have  "c i' j' =  Min ((λk. c i' (k-1) + c k j' + w i' j') ` {i'+1..j'})"
                using i' < j' by(simp add: c_def_rec)
              also have "...  w i' j' + c i' (?z-1) + c ?z j'"
                using ?z  {i'+1..j'} by simp
              finally show ?thesis .
            qed

            have b: "c i j  w i j + c i (?y-1) + c ?y j"
            proof -
              have "c i j = Min ((λk. c i (k-1) + c k j + w i j)  ` {i+1..j})"
                using i < j by(simp add: c_def_rec)
              also have "...  w i j + c i (?y-1) + c ?y j"
                using ?y  {i+1..j} by simp
              finally show ?thesis .
            qed
            
            have "nat (?z - 1 - i) < l" using ?z  {i'+1..j'} less.prems by simp
            hence IH_Step: " c i (?y-1) + c i' (?z-1)  c i' (?y-1) + c i (?z-1)"
              using ?y  {i'+1..j} ¬?z  ?y i  i'
                less.IH[where i=i and i'=i' and j="?y-1" and j'="?z-1", OF _ refl]
              by simp

            have "c i' j' + c i j
               w i' j +  w i j' + c i' (?z-1) + c i (?y-1) + c ?z j' + c ?y j"
              using a b w_mon by simp
            also have "  w i' j +  w i j' + c i (?z-1) + c i' (?y-1) + c ?z j' + c ?y j"
              using IH_Step by auto
            also have "... = c i j' + c i' j" using ?z  {i + 1..j'} ?y  {i' + 1..j}
              by(simp add: c_k_def c_k_with_K)
            finally show ?thesis by linarith
          qed
        qed
      qed
    qed
  qed
qed

corollary QI': assumes "i < k" " k  k'"  "k'  j "  "c_k i j k'  c_k i j k"
shows "c_k i (j+1) k'  c_k i (j+1) k"
proof -
  have "c k j + c k' (j+1)  c k' j + c k (j+1)"
    using lemma_2[of _ "j+1" k k' j] assms(1-3) by fastforce

  hence "c_k i j k + c_k i (j+1) k'  c_k i j k' + c_k i (j+1) k"
    using assms(1-3) c_k_def by simp

  thus "c_k i (j+1) k'  c_k i (j+1) k"
    using assms(4) by simp
qed

corollary QI'': assumes "i+1 < k" "k  k'" "k'  j+1" "c_k i (j+1) k'  c_k i (j+1) k"
shows "c_k (i+1) (j+1) k'  c_k (i+1) (j+1) k" 
proof -
  have "c i k + c (i + 1) k'  c i k' + c (i + 1) k"
    using lemma_2[of _ k' i "i+1" k] assms(1,2) by fastforce

  hence "c_k i (j+1) k + c_k (i+1) (j+1) k'  c_k i (j+1) k' + c_k (i+1) (j+1) k"
    using c_k_def assms(1-3) lemma_2 by simp

  thus "c_k (i+1) (j+1) k'  c_k (i+1) (j+1) k"
    using assms(4) by simp
qed


lemma lemma_3_1: assumes "i  j" shows "K i j  K i (j+1)"
proof cases
  assume "i = j"
  thus ?thesis
    by (metis K_def K_subset atLeastAtMost_iff less_add_one less_le)
next
  assume "ij"
  hence "i < j" using i  j by simp

  let ?k = "K i (j+1)"
  have "K i j  {i+1..j}" using K_def
    by (metis Max_in i < j mins_nonempty[OF i < j] finite_mins less_le mins_subset subsetCE)

  have "i < j+1" using i < j by linarith
  hence "K i (j+1)  {i+1..j+1}"
    by (metis Max_in K_def mins_nonempty[OF i < j+1] finite_mins less_le mins_subset subsetCE)

  have *: "is_arg_min_on (c_k i (j+1)) {i+1..j+1} ?k"
  proof -
    have "K i (j+1)  mins i (j+1)" using finite_mins mins_nonempty i < j K_def by fastforce
    thus "is_arg_min_on (c_k i (j+1)) {i+1..j+1} (K i (j+1))"
      unfolding Args_min_simps by blast
  qed 
  show ?thesis
  proof cases
    assume "?k = j+1" thus ?thesis using K i j  {i+1..j} by simp
  next
    assume "?k  j+1"
    hence "?k  {i+1..j}" using K i (j+1)  {i+1..j+1} by auto
    have "ij" "ij+1" using i < j by auto
    hence K_simps: "K i j = Max (mins i j)" "K i (j+1) = Max (mins i (j+1))"
      unfolding K_def by auto
    show ?thesis unfolding K_simps
    proof (rule Max.boundedI[OF finite_mins mins_nonempty[OF i < j]])
      fix k' assume k': "k'  mins i j"
      show "k'  Max (mins i (j+1))"
      proof (rule ccontr) 
        assume "~ k'  Max (mins i (j+1))"
        have "c_k i (j+1) k'  c_k i (j+1) ?k" unfolding K_simps
        proof (rule QI')
          show "i < Max (mins i (j+1))" 
            using K i (j + 1)  {i+1..j + 1} K_simps by auto
          show "Max (mins i (j+1))  k'" using ~ k'  Max (mins i (j+1))
            by linarith
          show "k'  j" using mins_subset atLeastAtMost_iff k' by blast
          show "c_k i j k'  c_k i j (Max (mins i (j + 1))) " 
            using k' ?k  {i+1..j} by(simp add: K_simps Args_min_simps)
        qed

        hence "is_arg_min_on (c_k i (j+1)) {i+1..j+1} k'"
          apply(rule is_arg_min_on_antimono[OF *])
          using mins_subset k' by fastforce
        hence "k'  mins i (j+1)" using k' by (auto simp: Args_min_on_def)
        thus False using finite_mins ¬ k'  Max (mins i (j + 1)) by auto
      qed
    qed
  qed
qed

lemma lemma_3_2: assumes "i  j" shows "K i (j+1)  K (i+1) (j+1)"
proof cases
  assume "i = j"
  thus ?thesis
    by (metis K_def K_subset atLeastAtMost_iff less_add_one less_le)
next
  assume "i  j"
  hence "i < j" using i  j by simp
  let ?k = "K (i+1) (j+1)"
  have "K i (j+1)  {i+1..j+1}" unfolding K_def
    by (metis Max_in i < j finite_mins less_irrefl mins_nonempty mins_subset subsetCE zless_add1_eq)

  have "i+1 < j+1" using i < j by linarith
  hence "K (i+1) (j+1)  {i+1+1..j+1}"
    using mins_nonempty[OF i+1 < j+1] mins_subset Max_in K_def finite_mins
    by (metis atLeastatMost_empty atLeastatMost_empty_iff2 contra_subsetD empty_subsetI less_add_one psubsetI)

  have *: "is_arg_min_on (c_k (i+1)(j+1)) {i+1+1..j+1} ?k"
  proof -
    have "K (i+1) (j+1)  mins (i+1) (j+1)"
      using finite_mins mins_nonempty i + 1 < j + 1 unfolding K_def
      by (metis Max_in not_less_iff_gr_or_eq)
    thus "is_arg_min_on (c_k (i+1) (j+1)) {i+1+1..j+1} (K (i+1) (j+1))"
      unfolding Args_min_on_def by blast
  qed 
  show ?thesis
  proof cases
    assume "?k = j+1" thus ?thesis using K i (j+1)  {i+1..j+1} by simp
  next
    assume "?k  j+1"
    hence "?k  {i+1+1..j}" using K (i+1) (j+1)  {i+1+1..j+1} by auto

    have  "ij+1" "i+1  j+1" using i < j by auto
    hence K_simps: "K i (j+1) = Max (mins i (j+1))" 
                      "K (i+1) (j+1) = Max (mins (i+1) (j+1))"
      unfolding K_def by auto
    have "i < j+1" using i+1 < j+1 by simp

    show ?thesis unfolding K_simps
    proof (rule Max.boundedI[OF finite_mins mins_nonempty[OF i < j+1]])
      fix k' assume k': "k'  mins i (j+1)"
      show "k'  Max (mins (i + 1) (j + 1))"
      proof (rule ccontr)
        assume "~ k'  Max (mins (i+1)(j+1))"
        have "c_k (i+1) (j+1) k'  c_k (i+1) (j+1) ?k" unfolding K_simps
          thm QI'[of "i+1" "Max(mins (i+1)(j+1))" k' "j"]
        proof (rule QI'')
          show "i+1  < Max (mins (i+1)(j+1))"
            using K (i+1) (j+1)  {i+1+1..j+1} K_simps 
            by auto
          show "Max (mins (i + 1) (j + 1))  k'" 
            using ~ k'  Max (mins (i+1)(j+1)) K_simps by linarith
          show "k'  j+1"
            using mins_subset k' by fastforce
          show "c_k i (j+1) k'  c_k i (j+1) (Max (mins (i + 1) (j + 1)))" 
            using k' ?k  {(i+1)+1..j + 1} K_simps
            by(simp add: Args_min_simps)
        qed

        hence "is_arg_min_on (c_k (i+1) (j+1)) {i+1+1..j+1} k'"
          apply(rule is_arg_min_on_antimono[OF *])
          using mins_subset k' K_simps ?k  {i+1+1..j}
            ¬ k'  Max (mins (i + 1) (j + 1)) atLeastAtMost_iff
          by force
        hence "k'  mins (i+1) (j+1)" by (simp add: k' Args_min_on_def)
        thus False using finite_mins ¬ k'  Max (mins (i+1)(j+1)) Max_ge
          by blast
      qed
    qed
  qed
qed

lemma lemma_3: assumes "i  j" 
  shows "K i j  K i (j+1)" "K i (j+1)  K (i+1) (j+1)"
using assms lemma_3_1 lemma_3_2 by blast+

end (* locale QI *)

end