Sorted nonnegative tuple must have zero elements at start

Stream: Is there code for X?

[MohanadAhmed]

Given a sorted (monotone) tuple (with m elements) of non-negative elements, and we know exactly r (r \leq m) are zero, all the r elements at the beginning must be zero.

import Mathlib.Data.Fin.Basic
import Mathlib.Data.Fin.Tuple.Sort
import Mathlib.Data.Real.Basic

/-- A sorted nonnegative list with m elements and exactly r ≤ m zero elemnts has the first
(r) elemnts as zero -/
lemma wierd (m r : ℕ) (hrm : r ≤ m) (f : Fin m → ℝ)
    (h_nonneg : ∀ (i : Fin m), 0 ≤  f i)
    (h_nz_cnt : Fintype.card { i // f i =  0} = r)
    (h_sorted : Monotone f)
    (j : Fin m):
    ( j < r ) → f j = 0 := by sorry

[MohanadAhmed]

Ok this got out of hand!!
I am finally able to prove it but this should not be that hard. Where did I go in the wrong direction??

import Mathlib.Data.Fin.Basic
import Mathlib.Data.Fin.Tuple.Sort
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.Sum
import Mathlib.Data.Fintype.Card

lemma wierd0 (m : Type)[Fintype m](p: m → Prop)[DecidablePred p] :
    Fintype.card m = Fintype.card {i // p i} + Fintype.card {i // ¬ p i} := by
  rw [Fintype.card_subtype_compl, ← Nat.add_sub_assoc, Nat.add_sub_cancel_left]
  exact Fintype.card_subtype_le _

lemma wierd01 (m : Type)[Fintype m] (p q : m → Prop) [DecidablePred p] [DecidablePred q] :
  Fintype.card {i // p i} = Fintype.card {j : {i // p i} // q j} +
    Fintype.card {j : {i // p i} // ¬ q j} := by
  exact wierd0 { i // p i } fun i ↦ q ↑i

-- set_option pp.explicit true
/-- A sorted nonnegative list with m elements and exactly r ≤ m non-zero elemnts has the first
(m - r) elemnts as zero -/
lemma wierd2 (m r : ℕ) [NeZero m] (hrm : r ≤ m) (f : Fin m → ℝ)
    (h_nonneg : ∀ (i : Fin m), 0 ≤  f i)
    (h_nz_cnt : Fintype.card { i // f i =  0} = r)
    (h_sorted : Monotone f)
    (j : Fin m):
    ( (j:ℕ) < r) → f j = 0 := by
  intro hjm
  have hj := eq_or_lt_of_le ( h_nonneg j)
  cases' hj with hj hj
  · exact hj.symm
  · exfalso
    unfold Monotone at h_sorted
    have : ∃ q : Fin m, (r) ≤ q ∧ f q = 0 := by
      by_contra h
      push_neg at h
      have h1 : m - r < Fintype.card {i // f i ≠ 0} := by
        have h2 : Fintype.card {i // f i ≠ 0} = Fintype.card {j : {i // f i ≠ 0} // j < r} +
          Fintype.card {j : {i // f i ≠ 0} // ¬ (j < r)} := wierd0 _ _
        rw [h2]
        have h3 : 1 ≤ Fintype.card {j : {i // f i ≠ 0} // j < r} := by
          apply Fintype.card_pos_iff.2
          refine' Nonempty.intro ?_
          refine' ⟨ ⟨ j, ne_of_gt hj⟩, hjm ⟩
        have h4 : (m - r) = Fintype.card {j : {i // f i ≠ 0} // ¬ (j < r)} := by
          simp only [ne_eq, not_lt]
          rw [← Fintype.card_fin (m - r)]
          rw [Fintype.card_eq]
          apply Nonempty.intro
          refine' ⟨fun z => ?_, fun y => ?_ , ?_, ?_ ⟩
          · let q : Fin m := ⟨r + z, ?_ ⟩
            have hrq : r ≤ q := by simp only [le_add_iff_nonneg_right, zero_le]
            refine ⟨ ⟨q, ?_⟩, ?_ ⟩
            apply h q hrq
            simp only [le_add_iff_nonneg_right, zero_le]
            have : z < m - r := by apply Fin.is_lt
            rw [add_comm]
            apply Nat.add_lt_of_lt_sub this
          · refine' ⟨y - r, ?_⟩
            apply Nat.lt_sub_of_add_lt
            rw [Nat.sub_add_cancel]
            apply Fin.is_lt
            apply y.prop
          · intro x
            dsimp
            simp only [ge_iff_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero,
              add_tsub_cancel_left, Fin.eta]
          · intro x
            dsimp
            conv_lhs =>
              congr
              congr
              congr
              rw [Nat.add_sub_cancel']
              rfl
              exact x.prop
            done
        have h5 : m - r < m - r + 1 := by exact Nat.lt.base (m - r)
        apply lt_of_lt_of_le h5 _
        rw [Nat.add_comm]
        exact (Nat.add_le_add h3 (le_of_eq h4))
      simp only [Fintype.card_subtype_compl, Fintype.card_fin] at h1
      rw [h_nz_cnt] at h1
      apply (lt_irrefl _) h1
    obtain ⟨q , hq⟩ := this
    have hjq : j < q := by exact_mod_cast lt_of_lt_of_le hjm hq.left
    have h1 : (f q < f j) := by
      rw [hq.2]
      exact hj
    have h2 := h_sorted (le_of_lt hjq)
    apply (not_lt.2 h2) h1

[Ruben Van de Velde]

You nerd-sniped me badly - this is an alternative proof (which can probably be tidied up quite a bit still):

import Mathlib.Data.Fin.Basic
import Mathlib.Data.Fin.Tuple.Sort
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.Sum
import Mathlib.Data.Fintype.Card
import Mathlib.Order.LocallyFinite
import Mathlib.Data.Fin.Interval
import Mathlib.Data.List.Intervals
import Mathlib.Data.Fintype.Perm
import Mathlib.Logic.Equiv.Fin

lemma aux {α : Type*} [DecidableEq α] {n} (f : Fin n → α) (p : α → Bool) :
    List.countp p (List.ofFn f) = Fintype.card { i : Fin n // p (f i) } := by
  rw [List.ofFn_eq_map, List.countp_map, Fintype.card_subtype, Finset.card, Finset.filter_val,
    ← Multiset.countp_eq_card_filter, Fin.univ_def, Multiset.coe_countp]
  congr with x
  simp

/-- A sorted nonnegative list with m elements and exactly r ≤ m non-zero elemnts has the first
(m - r) elemnts as zero -/
lemma wierd2 (m r : ℕ) [NeZero m] (hrm : r ≤ m) (f : Fin m → ℝ)
    (h_nonneg : ∀ (i : Fin m), 0 ≤  f i)
    (h_nz_cnt : Fintype.card { i // f i =  0} = r)
    (h_sorted : Monotone f)
    (j : Fin m):
    ( (j:ℕ) < r) → f j = 0 := by
  intro hjm
  let l := List.ofFn f
  let j' : Fin (l.length) := ⟨j, by simp only [List.length_ofFn, Fin.is_lt]⟩
  suffices l.get j' = 0 by
    simpa
  have : List.Sorted (· ≤ ·) l := by
    simpa using h_sorted
  replace h_nz_cnt : l.countp (· = 0) = r := by
    rw [aux]
    simpa
  by_contra H
  have : 0 < l.get j' := by
    apply lt_of_le_of_ne ?_ (Ne.symm H)
    simpa using h_nonneg j
  have : ∀ k ≥ j', 0 < l.get k := by
    intros k hk
    apply lt_of_lt_of_le this
    simp only [List.get_ofFn, Fin.castIso_mk, Fin.eta]
    apply h_sorted
    rw [← Fin.val_fin_le]
    simpa using hk.le
  have h_nz_cnt' : List.countp (0 < ·) l = m - r := by
    symm
    rw [Nat.sub_eq_iff_eq_add hrm]
    trans l.length
    · simp
    rw [← h_nz_cnt]
    convert List.length_eq_countp_add_countp _ l using 2
    apply List.countp_congr fun x hx => ?_
    simp only [List.mem_ofFn, Set.mem_range] at hx
    obtain ⟨y, rfl⟩ := hx
    simp only [decide_eq_true_eq, not_lt, (h_nonneg y).le_iff_eq]
  apply lt_irrefl (m - r)
  calc m - r
    _ < m - j := ?_
    _ = (Finset.Ici j).card := ?_
    _ ≤ _ := ?_
    _ = m - r := h_nz_cnt'
  · apply Nat.sub_lt_sub_left ?_ hjm
    simp
  · simp
  · have : ∀ k ∈ Finset.Ici j, 0 < f k := by
      intro k hk
      have := this ⟨k, by simp⟩
      simp only [ge_iff_le, Fin.mk_le_mk, Fin.val_fin_le, List.get_ofFn, Fin.castIso_mk, Fin.eta] at this
      apply this
      simpa using hk
    rw [aux]
    simp only [decide_eq_true_eq]
    rw [Fintype.card_subtype]
    refine Finset.card_le_of_subset (?_)
    intro k hk
    simp [this k hk]

[MohanadAhmed]

Thanks! I will see if I can push it down further.

It is the kind of thing that you look at and say surely it cannot be that difficult and it just keeps going on and on ...... and on ...

[Kevin Buzzard]

Yeah this is the nature of formalisation of mathematics. You have to completely revisit your concept of what is straightforward, and an important question is "how can I make this kind of argument more straightforward to formalise". Sometimes the answer is more lemmas, sometimes a new tactic, sometimes the refactoring of a definition...

[Eric Rodriguez]

import Mathlib.Data.Fin.Basic
import Mathlib.Data.Fin.Tuple.Sort
import Mathlib.Data.Real.Basic
import Mathlib.Data.Fintype.Sum
import Mathlib.Data.Fintype.Card
import Mathlib.Order.LocallyFinite
import Mathlib.Data.Fin.Interval
import Mathlib.Data.List.Intervals
import Mathlib.Data.Fintype.Perm
import Mathlib.Logic.Equiv.Fin

-- set_option pp.explicit true
/-- A sorted nonnegative list with m elements and exactly r ≤ m non-zero elemnts has the first
(m - r) elemnts as zero -/
lemma wierd2 (m r : ℕ) [NeZero m] (f : Fin m → ℝ)
    (h_nonneg : ∀ (i : Fin m), 0 ≤  f i)
    (h_nz_cnt : Fintype.card { i // f i =  0} = r)
    (h_sorted : Monotone f)
    (j : Fin m) : ((j:ℕ) < r) → f j = 0 := by
    intro h
    contrapose! h_nz_cnt
    apply ne_of_lt
    replace h_nz_cnt := h_nz_cnt.lt_of_le' (h_nonneg _)
    have key : ∀ {i}, j ≤ i → f i ≠ 0
    · intro i hi
      exact (h_nz_cnt.trans_le (h_sorted hi)).ne'
    refine lt_of_le_of_lt ?_ h
    have := Fintype.card_subtype_compl (¬f · = 0)
    simp_rw [not_not] at this
    rw [this, Fintype.card_fin, tsub_le_iff_left, ←tsub_le_iff_right, Fintype.card_subtype]
    refine le_trans (by simp) (Finset.card_mono $ show Finset.Ici j ≤ _ from fun k hk ↦ ?_)
    simp only [Finset.mem_Ici] at hk
    simp only [Finset.mem_univ, forall_true_left, Finset.mem_filter, true_and]
    exact key hk

[Eric Rodriguez]

I think I found the "good" proof

[MohanadAhmed]

Thanks a lot @Eric Rodriguez
That is a lot smaller than what I was able to do.

So small question: whilst writing your proof. At any point did you think, surely this must be in mathlib?

[Eric Rodriguez]

No, but I will say that this was my second attempt and I had a think in between.

[Eric Rodriguez]

(deleted)

[MohanadAhmed]

Mabye my question was phrased in correctly. I mean in your attempts: did you need any subfacts/sublemmas that you thought must be in mathlib somewhere?

[Eric Wieser]

This seems like a slightly nicer lemma:

/-- All the elements `· ≤ a` appear the start of a sorted tuple -/
lemma wierd2' {α} [LinearOrder α] (m : ℕ) (f : Fin m → α) (a : α)
    (h_sorted : Monotone f)
    (j : Fin m) (h : j < Fintype.card {i // f i ≤ a}) :
    f j ≤ a := by
  contrapose! h
  have := Fintype.card_subtype_compl (¬f · ≤ a)
  simp_rw [not_not, not_le] at this
  rw [this, Fintype.card_fin, tsub_le_iff_tsub_le, Fintype.card_subtype]
  refine le_trans (by simp) (Finset.card_mono $ show Finset.Ici j ≤ _ from fun k hk ↦ ?_)
  simp only [Finset.mem_Ici] at hk
  exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, h.trans_le (h_sorted hk)⟩

[Eric Wieser]

It should be true as an iff too, right?

[MohanadAhmed]

Logically yes it should be true both ways.

lemma wierd6 {α} [LinearOrder α] (m : ℕ) (f : Fin m → α) (a : α)
    (h_sorted : Monotone f)
    (j : Fin m) :
    (j < Fintype.card {i // f i ≤ a}) ↔ f j ≤ a := by sorry

Small questions?

1. How does the show tactic work (Finset.card_mono $ show Finset.Ici j ≤ _ from fun k hk ↦ ?_)
2. Is the from clause here related to the from I see sometimes with suffices?

[Eric Rodriguez]

show (type) from X takes the term X and tries to force it to be the type (type). They're not separate tactics

[Eric Wieser]

The proof would probably be clearer with a calc block or transitivity where that show is

[MohanadAhmed]

Hello @Ruben Van de Velde , @Eric Wieser , @Eric Rodriguez , Lemma is in PR #6728.

[Eric Wieser]

I think we should strive to prove your iff version if we're going to have it in mathlib!