pathologically slow linarith.lean

import tactic.slim_check
import data.int.parity
/- If you are an honest person: -/
notation `guarded_linarith` := begin linarith, try { assumption, }, end
notation `guarded_ring` := begin ring, try { assumption, }, end

/- If you are dishonest: -/
constant escape_hatch : false
-- notation `guarded_linarith` := begin exact false.elim escape_hatch, end
-- notation `guarded_ring` := begin exact false.elim escape_hatch, end

structure triple_t := (a b c cost : ℕ)
inductive reachable : triple_t → triple_t → Type
| refl (x : triple_t) : reachable x x
| increment_a (a b c cost : ℕ) : reachable ⟨a, b, c, cost⟩ ⟨a + 1, b, c, cost + 1⟩
| increment_b (a b c cost : ℕ) : reachable ⟨a, b, c, cost⟩ ⟨a, b + 1, c, cost + 1⟩
| increment_c (a b c cost : ℕ) : reachable ⟨a, b, c, cost⟩ ⟨a, b, c + 1, cost + 1⟩
| trans (x y z : triple_t) : reachable x y → reachable y z → reachable x z

inductive possible : triple_t → Prop
| intro
(a b c a1 b1 c1 cost : ℕ)
(h1 : (↑b1 : ℤ) - (↑a1 : ℤ) = (↑c1 : ℤ) - (↑b1 : ℤ))
(h2 : reachable ⟨a, b, c, 0⟩ ⟨a1, b1, c1, cost⟩) : possible ⟨a, b, c, cost⟩

inductive optimal : triple_t → Prop
| intro
(a b c cost : ℕ)
(h1 : possible ⟨a, b, c, cost⟩)
(h2 : ∀ cost' : ℕ, cost' < cost → ¬possible ⟨a, b, c, cost'⟩) : optimal ⟨a, b, c, cost⟩

def compute : ℕ → ℕ → ℕ → ℕ
| a b c :=
  let gap := (↑a : ℤ) + (↑c : ℤ) - 2 * (↑b : ℤ) in
  if gap < 0 then (-gap).to_nat
  else if gap % 2 = 0 then gap.to_nat / 2 else (gap.to_nat + 1) / 2 + 1

lemma optimal_ext_aux (predicate : ℕ → Prop) (c1 c2 : ℕ) (h1 : ∀ x, x < c1 → ¬predicate x) (h2 : ∀ x, x < c2 → ¬predicate x) (h3 : predicate c1) (h4 : predicate c2) : c1 = c2 := begin
  have h1' := h1 c2,
  have h2' := h2 c1,
  have h1_reversed : predicate c2 → ¬(c2 < c1) := begin
    intro h,
    intro condition,
    exact h1' condition h,
  end,
  have h2_reversed : predicate c1 → ¬(c1 < c2) := begin
    intro h,
    intro condition,
    exact h2' condition h,
  end,
  have inequality1 := h1_reversed h4,
  have inequality2 := h2_reversed h3,
  exact guarded_linarith,
end

lemma optimal_ext (a b c c1 c2 : ℕ) (h1 : optimal ⟨a, b, c, c1⟩) (h2 : optimal ⟨a, b, c, c2⟩) : c1 = c2 := begin
  have := optimal_ext_aux (λ cost, possible ⟨a, b, c, cost⟩),
  cases h1,
  cases h2,
  norm_num at this,
  exact this c1 c2 h1_h2 h2_h2 h1_h1 h2_h1,
end

lemma real_meaning_of_reachable {a b c a1 b1 c1 cost cost1 : ℕ}
  (H : reachable ⟨a, b, c, cost⟩ ⟨a1, b1, c1, cost1⟩) :
  a ≤ a1 ∧ b ≤ b1 ∧ c ≤ c1 ∧ cost ≤ cost1 ∧ (a1 - a) + (b1 - b) + (c1 - c) = cost1 - cost :=
begin
  generalize_hyp h1 : (⟨a, b, c, cost⟩ : triple_t) = e₁ at H,
  generalize_hyp h2 : (⟨a1, b1, c1, cost1⟩ : triple_t) = e₂ at H,
  induction H generalizing a b c a1 b1 c1 cost cost1,
  case reachable.trans : _ y _ _ _ ih1 ih2  {
    cases y with a2 b2 c2 cost2,
    obtain ⟨gg, ggg, gggg, ggggg, gggggg⟩ := ih1 h1 rfl,
    obtain ⟨gg', ggg', gggg', ggggg', gggggg'⟩ := ih2 rfl h2,
    repeat {
      split,
      exact guarded_linarith,
    },
    have statement := nat.sub_add_sub_cancel gg' gg,
    have statement := nat.sub_add_sub_cancel ggg' ggg,
    have statement := nat.sub_add_sub_cancel gggg' gggg,
    have statement := nat.sub_add_sub_cancel ggggg' ggggg,
    exact guarded_linarith,
  },
  {
    cases h1,
    cases h2,
    repeat {
      split,
      exact guarded_linarith,
    },
    norm_num,
  },
  all_goals {
    cases h1,
    cases h2,
    try { split, apply nat.le_succ, },
    repeat {
      split,
      exact guarded_linarith,
    },
    try { split, apply nat.le_succ, },
    repeat {
      split,
      exact guarded_linarith,
    },
    simp [nat.succ_sub],
    try { apply nat.le_succ, },
  },
end

lemma correct : ∀ a b c : ℕ, optimal ⟨a, b, c, compute a b c⟩ := begin
  intros a b c,
  apply optimal.intro,
  {
    rw compute,
    norm_num,
    split_ifs,
    {
      apply possible.intro a b c ((↑a : ℤ) + ((2 : ℤ) * (↑b : ℤ) - ((↑a : ℤ) + (↑c : ℤ)))).to_nat b c,
      {
        suffices : (↑b : ℤ) - ↑((2 * (↑b : ℤ) - ↑c).to_nat) = -↑b + (↑c : ℤ), from guarded_ring,
        have := @int.to_nat_of_nonneg (2 * ↑b - ↑c) begin
          exact guarded_linarith,
        end,
        rw this,
        exact guarded_ring,
      },
      {
        have : ((↑a : ℤ) + (2 * ↑b - (↑a + ↑c))).to_nat = a + ((2 * (↑b : ℤ)- (↑a + ↑c))).to_nat := begin
          have goal := @int.to_nat_add_nat (2 * (↑b : ℤ) - (↑a + ↑c)) (guarded_linarith) a,
          have : 2 * (↑b : ℤ) - (↑a + ↑c) + ↑a = (↑a : ℤ) + (2 * ↑b - (↑a + ↑c)) := guarded_ring,
          rw this at goal,
          rw goal,
          exact guarded_ring,
        end,
        rw this,
        have : ∀ d : ℕ, reachable {a := a, b := b, c := c, cost := 0} {a := a + d, b := b, c := c, cost := d} := begin
          intro d,
          induction d with d hd,
          {
            norm_num,
            exact reachable.refl _,
          },
          {
            have : a + d.succ = a + d + 1 := guarded_ring,
            rw this,
            have := reachable.increment_a (a + d) b c d,
            exact reachable.trans _ _ _ hd this,
          }
        end,
        exact this (2 * (↑b : ℤ) - (↑a + ↑c)).to_nat,
      }
    },
    {
      apply possible.intro a b c a (b + (((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2)) c (((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2),
      have := int.coe_nat_add b (((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2),
      rw this,
      have : (↑b : ℤ) + ↑(((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2) - ↑a - (↑c - (↑b + ↑(((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2))) = 0 := begin
        suffices : 2 * (↑b : ℤ) + (2 * ↑(((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2) + (-↑a - ↑c)) = 0, from guarded_ring,
        have g1 := @int.div_mul_cancel ((↑a : ℤ) + ↑c - 2 * ↑b).to_nat 2,
        have g2 := @int.dvd_nat_abs_of_of_nat_dvd 2 ((↑a : ℤ) + ↑c - 2 * ↑b) h_1,
        have g3 : ∀ (a : ℤ) (h : 0 ≤ a), a.nat_abs = a.to_nat := begin
          intros a h,
          have := int.to_nat_add_to_nat_neg_eq_nat_abs a,
          have changed : 0 < a ∨ 0 = a := lt_or_eq_of_le h, 
          cases changed,
          rw (norm_num.int_to_nat_neg a changed) at this,
          norm_num at this,
          tauto,
          rw changed.symm,
          norm_num,
        end,
        rw (g3 ((↑a : ℤ) + ↑c - 2 * ↑b) (guarded_linarith)) at g2,
        have := g1 begin
          apply int.coe_nat_dvd.mpr,
          norm_num,
          tauto,
        end,
        rw (int.mul_comm (((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2) 2) at this,
        have aux : (↑(((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2) : ℤ) = ↑(((↑a : ℤ) + ↑c - 2 * ↑b).to_nat) / 2 := by norm_cast,
        rw aux,
        rw this,
        rw @int.to_nat_of_nonneg ((↑a : ℤ) + ↑c - 2 * ↑b) (guarded_linarith),
        exact guarded_ring,
      end,
      exact sub_eq_zero.mp this,
      have : ∀ d : ℕ, reachable {a := a, b := b, c := c, cost := 0} {a := a, b := b + d, c := c, cost := d} := begin
        intro d,
        induction d with d hd,
        {
          norm_num,
          exact reachable.refl _,
        },
        {
          have : b + d.succ = b + d + 1 := guarded_ring,
          rw this,
          have := reachable.increment_b a (b + d) c d,
          exact reachable.trans _ _ _ hd this,
        }
      end,
      exact this (((↑a : ℤ) + ↑c - 2 * ↑b).to_nat / 2),
    },
    {
      apply possible.intro a b c (a + 1) (b + (((↑a : ℤ) + ↑c - 2 * ↑b).to_nat + 1) / 2) c,
      norm_num,
      rw @int.to_nat_of_nonneg ((↑a : ℤ) + ↑c - 2 * ↑b) (guarded_linarith),
      have : (↑b : ℤ) + (↑a + ↑c - 2 * ↑b + 1) / 2 - (↑a + 1) - (↑c - (↑b + (↑a + ↑c - 2 * ↑b + 1) / 2)) = 0 := begin
        suffices : 2 * (↑b : ℤ) + (2 * ((↑a + ↑c - 2 * ↑b + 1) / 2) + (-↑a + (-↑c - 1))) = 0, from guarded_ring,
        have : ∀ { a : ℤ } (h : ¬2 ∣ a), 2 ∣ (a + 1) := begin
          intros a h,
          have := int.odd_iff.mpr (int.two_dvd_ne_zero.mp h),
          have := (@int.even_add_one a).mpr begin
            exact int.odd_iff_not_even.mp this,
          end,
          exact even_iff_two_dvd.mp this,
        end,
        have := this h_1,
        have := @int.div_mul_cancel ((↑a : ℤ) + ↑c - 2 * ↑b + 1) 2 this,
        rw (int.mul_comm (((↑a : ℤ) + ↑c - 2 * ↑b + 1) / 2) 2) at this,
        rw this,
        exact guarded_ring,
      end,
      exact sub_eq_zero.mp this,
      have : ∀ d : ℕ, reachable {a := a, b := b, c := c, cost := 0} {a := a, b := b + d, c := c, cost := d} := begin
        intro d,
        induction d with d hd,
        {
          norm_num,
          exact reachable.refl _,
        },
        {
          have : b + d.succ = b + d + 1 := guarded_ring,
          rw this,
          have := reachable.increment_b a (b + d) c d,
          exact reachable.trans _ _ _ hd this,
        }
      end,
      have g1 := this ((((↑a : ℤ) + ↑c - 2 * ↑b).to_nat + 1) / 2),
      have g2 := reachable.increment_a a (b + (((↑a : ℤ) + ↑c - 2 * ↑b).to_nat + 1) / 2) c ((((↑a : ℤ) + ↑c - 2 * ↑b).to_nat + 1) / 2),
      exact reachable.trans _ _ _ g1 g2,
    }
  },
  {
    intro cost',
    intro h,
    intro h1,
    cases h1,
    rw compute at h,
    norm_num at h,
    split_ifs at h,
    {
      have := real_meaning_of_reachable h1_h2,
      have expression := int.coe_nat_inj'.mpr this.right.right.right.right,
      norm_num at expression,
      have := @int.of_nat_sub h1_a1 a (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have := @int.of_nat_sub h1_b1 b (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have := @int.of_nat_sub h1_c1 c (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have g1 : (↑h1_a1 : ℤ) - ↑a + (↑h1_b1 - ↑b) + (↑h1_c1 - ↑c) - 3 * (↑h1_b1 - ↑b) = (↑cost' : ℤ) - 3 * (↑h1_b1 - ↑b) := guarded_linarith,
      have : ∀ (a b c a' b' c' : ℤ), a' - a + (b' - b) + (c' - c) - 3 * (b' - b) = a' - 2 * b' + c' - (a - 2 * b + c) := begin
        intros a b c a' b' c',
        exact guarded_ring,
      end,
      rw (this (↑a : ℤ) b c h1_a1 h1_b1 h1_c1) at g1,
      clear this,
      have : (↑h1_a1 : ℤ) - 2 * ↑h1_b1 + ↑h1_c1 = 0 := guarded_linarith,
      rw this at g1,
      clear this,
      have : 0 - ((↑a : ℤ) - 2 * ↑b + ↑c) = (2 * (↑b : ℤ) - (↑a + ↑c)) := guarded_ring,
      rw this at g1,
      clear this,
      have aux := g1.symm,
      have := @int.sub_le_sub_left 0 (3 * (↑h1_b1 - ↑b)) (guarded_linarith) cost',
      rw aux at this,
      norm_num at this,
      have := int.coe_nat_le_coe_nat_of_le h,
      norm_num at this,
      rw (@int.to_nat_of_nonneg (2 * (↑b : ℤ) - (↑a + ↑c)) (guarded_linarith)) at this,
      exact guarded_linarith,
    },
    {
      have := real_meaning_of_reachable h1_h2,
      have expression := int.coe_nat_inj'.mpr this.right.right.right.right,
      norm_num at expression,
      have := @int.of_nat_sub h1_a1 a (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have := @int.of_nat_sub h1_b1 b (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have := @int.of_nat_sub h1_c1 c (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have double := int.mul_div_cancel_left ((↑h1_a1 : ℤ) - ↑a + (↑h1_b1 - ↑b) + (↑h1_c1 - ↑c)) (two_ne_zero' : 2 ≠ 0),
      have : ∀ a b c a' b' c' : ℤ, 2 * (a' - a + (b' - b) + (c' - c)) = (a + c - 2 * b) + 2 * (a' - a) + 2 * (c' - c) + (2 * b' - a - c) := begin
        intros a b c a' b' c',
        exact guarded_ring,
      end,
      have := this a b c h1_a1 h1_b1 h1_c1,
      rw this at double,
      clear this,
      clear this,
      have : (2 * (↑h1_b1 : ℤ) - ↑a - ↑c) ≥ (2 * (↑h1_b1 : ℤ) - ↑h1_a1 - ↑h1_c1) := guarded_linarith,
      rw (show (2 * (↑h1_b1 : ℤ) - ↑h1_a1 - ↑h1_c1) = 0, from guarded_linarith) at this,
      have : ((↑a : ℤ) + ↑c - 2 * ↑b + 2 * (↑h1_a1 - ↑a) + 2 * (↑h1_c1 - ↑c) + (2 * ↑h1_b1 - ↑a - ↑c)) ≥ ((↑a : ℤ) + ↑c - 2 * ↑b) := guarded_linarith,
      have := @int.div_le_div _ _ 2 (guarded_linarith) this,
      rw double at this,
      rw expression at this,
      have := int.coe_nat_le_coe_nat_of_le h,
      norm_num at this,
      rw (@int.to_nat_of_nonneg ((↑a : ℤ) + ↑c - 2 * ↑b) (guarded_linarith)) at this,
      exact guarded_linarith,
    },
    {
      have := real_meaning_of_reachable h1_h2,
      have expression := int.coe_nat_inj'.mpr this.right.right.right.right,
      norm_num at expression,
      have := @int.of_nat_sub h1_a1 a (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have := @int.of_nat_sub h1_b1 b (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      have := @int.of_nat_sub h1_c1 c (guarded_linarith),
      norm_num at this,
      rw this at expression,
      clear this,
      rename h1_a1 a',
      rename h1_b1 b',
      rename h1_c1 c',
      have ignore_b_prime : (↑b' : ℤ) - ↑b = (↑cost' : ℤ) - (↑a' - ↑a) - (↑c' - ↑c) := guarded_linarith,
      have inject_gap : (↑a' : ℤ) + ↑c' - 2 * ↑b' = 0 := guarded_linarith,
      have target : 2 * ↑cost' - ((↑a : ℤ) + ↑c - 2 * ↑b + 3) = 3 * ((↑a' : ℤ) - ↑a) + 3 * (↑c' - ↑c) - 3 := guarded_linarith,
      have coerced := int.coe_nat_le_coe_nat_of_le h,
      norm_num at coerced,
      rw (@int.to_nat_of_nonneg ((↑a : ℤ) + ↑c - 2 * ↑b) (guarded_linarith)) at coerced,
      have strict : ¬((↑a' : ℤ) = ↑a ∧ (↑c' : ℤ) = ↑c) := begin
        intro h,
        cases h,
        rw [h_left, h_right] at inject_gap,
        have target : even (0 : ℤ) := dec_trivial,
        rw inject_gap.symm at target,
        have sum_is_even := ((@int.even_sub (↑a + ↑c) (2 * ↑b')).mp (by tauto)).mpr begin
          use (↑b' : ℤ),
        end,
        have sum_is_odd := ((@int.odd_sub (↑a + ↑c) (2 * ↑b)).mp (int.odd_iff.mpr (int.two_dvd_ne_zero.mp h_2))).mpr begin
          use (↑b : ℤ),
        end,
        exact (int.even_iff_not_odd.mp sum_is_even) sum_is_odd,
      end,
      have strict' := (decidable.not_and_iff_or_not ((↑a' : ℤ) = (↑a : ℤ)) ((↑c' : ℤ) = (↑c : ℤ))).mp strict,
      cases strict',
      {
        have := @int.coe_nat_le_coe_nat_of_le a a' (by tauto),
        have := lt_or_eq_of_le this,
        cases this,
        {
          have : 3 * ((↑a' : ℤ) - ↑a) + 3 * (↑c' - ↑c) - 3 ≥ 0 := guarded_linarith,
          rw target.symm at this,
          have : ((↑a : ℤ) + ↑c - 2 * ↑b + 1) < 2 * (↑cost' : ℤ) := guarded_linarith,
          have div_lt_div : ∀ x y : ℤ, x < y → even y → x / 2 < y / 2 := begin
            intros a b c d,
            rw [int.div_lt_iff_lt_mul],
            have := int.div_add_mod b 2,
            rw (int.even_iff.mp d) at this,
            norm_num at this,
            exact guarded_linarith,
            norm_num,
          end,
          have := div_lt_div ((↑a : ℤ) + ↑c - 2 * ↑b + 1) (2 * (↑cost' : ℤ)) this begin
            use (↑cost' : ℤ),
          end,
          have cancel := int.mul_div_cancel_left (↑cost' : ℤ) (two_ne_zero' : 2 ≠ 0),
          rw cancel at this,
          exact guarded_linarith,
        },
        {
          exact strict' this_1.symm,
        }
      },
      {
        have := @int.coe_nat_le_coe_nat_of_le c c' (by tauto),
        have := lt_or_eq_of_le this,
        cases this,
        {
          have : 3 * ((↑a' : ℤ) - ↑a) + 3 * (↑c' - ↑c) - 3 ≥ 0 := guarded_linarith,
          rw target.symm at this,
          have : ((↑a : ℤ) + ↑c - 2 * ↑b + 1) < 2 * (↑cost' : ℤ) := guarded_linarith,
          have div_lt_div : ∀ x y : ℤ, x < y → even y → x / 2 < y / 2 := begin
            intros a b c d,
            rw [int.div_lt_iff_lt_mul],
            have := int.div_add_mod b 2,
            rw (int.even_iff.mp d) at this,
            norm_num at this,
            exact guarded_linarith,
            norm_num,
          end,
          have := div_lt_div ((↑a : ℤ) + ↑c - 2 * ↑b + 1) (2 * (↑cost' : ℤ)) this begin
            use (↑cost' : ℤ),
          end,
          have cancel := int.mul_div_cancel_left (↑cost' : ℤ) (two_ne_zero' : 2 ≠ 0),
          rw cancel at this,
          exact guarded_linarith,
        },
        {
          exact strict' this_1.symm,
        }
      }
    }
  }
end