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 "i≠j"
  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 "i≠j" "i≠j+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  "i≠j+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