Zulip Chat Archive

Stream: new members

Topic: linarith on coerced fins


Yakov Pechersky (Sep 16 2020 at 20:17):

Is there a way to get linarith to simplify this proof at all? It is just dealing with a lot of inequalities.

import data.matrix.notation
import tactic.wlog
import tactic.linarith

variables {n : }

lemma nat.sub_add_one (hpos : 0 < n) : n - 1 + 1 = n :=
begin
  cases n,
  { exact absurd hpos (lt_irrefl 0) },
  simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero],
end

lemma nat.not_lt_pred_ge {m n : } (h : m < n - 1) (H : n  m) : false :=
begin
  have hn : n < n - 1 := lt_of_le_of_lt H h,
  cases n,
  { rw [nat.nat_zero_eq_zero, nat.zero_sub] at hn,
    exact absurd hn (lt_irrefl 0) },
  { rw [nat.succ_sub_succ_eq_sub, nat.sub_zero] at hn,
    exact nat.not_succ_lt_self hn },
end

example (x y : fin (n + 2)) (j : fin n) (h : y  x) :
  x.succ_above ((x.pred_above y h).succ_above j) = y.succ_above ((y.pred_above x (ne.symm h)).succ_above j) :=
begin
  wlog H : y < x using [x y],
  { rcases lt_trichotomy x y with H|rfl|H,
    { exact or.inr H },
    { contradiction },
    { exact or.inl H } },
  unfold fin.pred_above,
  rw [dif_pos H, dif_neg (not_lt_of_lt H)],
  have H' := fin.lt_iff_coe_lt_coe.mp H,
  have posx : 0 < x.val := lt_of_le_of_lt (fin.zero_le y) y < x,
  unfold fin.succ_above,
  all_goals { simp_rw [fin.lt_iff_coe_lt_coe] at * },
  split_ifs,
  any_goals { refl <|> rw fin.cast_succ_fin_succ },
  all_goals {
    simp only [fin.val_eq_coe, fin.coe_cast_lt,
               fin.coe_succ, fin.coe_cast_succ, fin.coe_pred,
               not_lt, ne.def, fin.cast_succ_inj] at * },
  { have hj : (x : ) - 1 = j :=
      le_antisymm (x : ) - 1  j (nat.le_pred_of_lt (j : ) < x),
    rw hj at *,
    rw nat.sub_add_one posx at *,
    exact absurd (y : ) < x (not_lt_of_lt (x : ) < y) },
  { have hj : (x : ) - 1 = j :=
      le_antisymm (x : ) - 1  j (nat.le_pred_of_lt (j : ) < x),
    rw hj at *,
    rw nat.sub_add_one posx at *,
    have hy : y = x :=
      le_antisymm (y : )  x (nat.le_of_pred_lt (x : ) - 1 < y),
    exact absurd hy h },
  { exact absurd (x : )  j (nat.not_lt_pred_ge (j : ) < x - 1) },
  { have hy : (y : ) = j + 1 :=
      le_antisymm (y : )  j + 1 (j : ) < y,
    have : (j : ) < x,
      { refine lt_trans (nat.lt_succ_self j) _,
        convert fin.lt_iff_coe_lt_coe.mp H,
        rw hy },
    exact absurd (j : ) < x (not_lt_of_ge (x : )  j) },
  { have : (x : )  j + 1 :=
      nat.le_add_of_sub_le_right (x : ) - 1  j,
    exact absurd (j : ) + 1 < x (not_lt_of_ge (x : )  j + 1) },
  { have : (j : ) + 1 < x :=
      nat.add_lt_of_lt_sub_right (j : ) < x - 1,
    exact absurd (j : ) + 1 < x (not_lt_of_ge (x : )  j + 1) },
  { have : (j : ) < y :=
      lt_trans (nat.lt_succ_self j) (j : ) + 1 < y,
    exact absurd (j : ) < y (not_lt_of_ge (y : )  j) },
end

Yakov Pechersky (Sep 16 2020 at 20:17):

For reference, here is a (not fully-golfed) proof that does not use split_ifs:

import data.matrix.notation
import tactic.wlog
import tactic.linarith

variables {n : }

lemma nat.sub_add_one (hpos : 0 < n) : n - 1 + 1 = n :=
begin
  cases n,
  { exact absurd hpos (lt_irrefl 0) },
  simp only [nat.succ_sub_succ_eq_sub, nat.sub_zero],
end

lemma nat.not_lt_pred_ge {m n : } (h : m < n - 1) (H : n  m) : false :=
begin
  have hn : n < n - 1 := lt_of_le_of_lt H h,
  cases n,
  { rw [nat.nat_zero_eq_zero, nat.zero_sub] at hn,
    exact absurd hn (lt_irrefl 0) },
  { rw [nat.succ_sub_succ_eq_sub, nat.sub_zero] at hn,
    exact nat.not_succ_lt_self hn },
end

example (x y : fin (n + 2)) (j : fin n) (h : y  x) :
  x.succ_above ((x.pred_above y h).succ_above j) = y.succ_above ((y.pred_above x (ne.symm h)).succ_above j) :=
begin
  wlog H : y < x using [x y],
  { rcases lt_trichotomy x y with H|rfl|H,
    { exact or.inr H },
    { contradiction },
    { exact or.inl H } },
  unfold fin.pred_above,
  rw [dif_pos H, dif_neg (not_lt_of_lt H)],
  have lessy : y.val < n + 1 := lt_of_lt_of_le y < x (fin.le_last x),
  have posx : 0 < x.val := lt_of_le_of_lt (fin.zero_le y) y < x,
  have hx : x  0 := ne_of_gt posx,
  cases fin.succ_above_lt_ge y j.succ with Hyj Hyj,
  { have hyj : j.cast_succ < y.cast_lt lessy,
      { rw fin.lt_iff_coe_lt_coe at Hyj ,
        refine lt_trans _ Hyj,
        simp only [nat.succ_pos', lt_add_iff_pos_right,
                    fin.coe_succ, fin.coe_cast_succ] },
    rw fin.succ_above_below _ _ hyj,
    cases fin.succ_above_lt_ge (x.pred hx) j with hxj hxj,
    { rw fin.succ_above_below _ _ hxj,
      rw fin.succ_above_below,
      rw fin.succ_above_below,
      { exact hyj },
      { rw fin.lt_iff_coe_lt_coe,
        refine lt_trans hxj _,
        rw [fin.val_eq_coe, fin.coe_pred],
        exact nat.pred_lt (ne_of_gt posx) } },
    { cases eq_or_lt_of_le hxj with Hxj Hxj,
      { rw [fin.cast_succ_fin_succ, Hxj, fin.succ_pred] at Hyj,
        exact absurd H (not_lt_of_lt Hyj) },
      { rw fin.succ_above_above _ _ hxj,
        rw fin.succ_above_above x,
        rw fin.succ_above_below y _ Hyj,
        { rw fin.cast_succ_fin_succ },
        { rw fin.le_iff_coe_le_coe,
          rw [fin.coe_cast_succ],
          refine nat.le_of_pred_lt _,
          convert Hxj,
          simpa only [fin.val_eq_coe, fin.coe_pred] } } } },
  { rcases eq_or_lt_of_le Hyj with hyj|hyj,
    { simp_rw [hyj, fin.cast_lt_cast_succ],
      rw fin.succ_above_below _ _ (fin.cast_succ_lt_succ j),
      rw fin.succ_above_below x,
      rw fin.succ_above_below (x.pred hx),
      rw fin.cast_succ_fin_succ,
      rw fin.succ_above_below _ _ (fin.cast_succ_lt_succ j.cast_succ),
      { rw fin.lt_iff_coe_lt_coe,
        rw [fin.coe_cast_succ, fin.coe_pred],
        refine nat.le_pred_of_lt _,
        convert y < x,
        simp only [hyj, fin.val_eq_coe, fin.coe_succ, fin.coe_cast_succ] },
      { refine lt_trans _ y < x,
        rw [hyj, fin.cast_succ_fin_succ],
        exact fin.cast_succ_lt_succ _ } },
    { replace Hyj : y  j.cast_succ.cast_succ,
        { rw fin.lt_iff_coe_lt_coe at hyj,
          rw [fin.coe_cast_succ, fin.coe_succ] at hyj,
          exact nat.lt_succ_iff.mp hyj },
      have hyj' : y.cast_lt lessy  j.cast_succ,
        { rw fin.le_iff_coe_le_coe at Hyj ,
          refine le_trans Hyj _,
          rw fin.coe_cast_succ },
        rw fin.succ_above_above _ _ hyj',
      cases fin.succ_above_lt_ge (x.pred hx) j with hxj hxj,
      { rw fin.succ_above_below _ _ hxj,
        rw fin.succ_above_above y _,
        rw fin.succ_above_below,
        { rw fin.cast_succ_fin_succ },
        { rw fin.lt_iff_coe_lt_coe,
          rw [fin.coe_cast_succ, fin.coe_succ],
          refine nat.add_lt_of_lt_sub_right _,
          convert hxj,
          rw [fin.val_eq_coe, fin.coe_pred] },
        { rw fin.le_iff_coe_le_coe,
          exact hyj' } },
      { rw fin.succ_above_above _ _ hxj,
        rw fin.succ_above_above x,
        rw fin.succ_above_above y _ (le_of_lt hyj),
        rw [fin.le_iff_coe_le_coe, fin.coe_cast_succ, fin.coe_succ],
        refine nat.le_add_of_sub_le_right _,
        convert hxj,
        rw [fin.val_eq_coe, fin.coe_pred] } } }
end

Reid Barton (Sep 16 2020 at 20:23):

I guess this is what omega is supposed to be for

Yakov Pechersky (Sep 16 2020 at 20:28):

omega didn't work, even for the seemingly simple

  { have hj : (x : ) - 1 = j :=
      le_antisymm (x : ) - 1  j (nat.le_pred_of_lt (j : ) < x),
    rw hj at *,
    rw nat.sub_add_one posx at *,
    have hy : y = x :=
      le_antisymm (y : )  x (nat.le_of_pred_lt (x : ) - 1 < y),
    omega, -- fails here
    exact absurd hy h },

Last updated: Dec 20 2023 at 11:08 UTC