Simplifiying expression involving substraction and modulo

Stream: new members

[Antoine Labelle]

Hi,
After simplifying some expression, Lean leaves me with the expression m - (m + (m + 1 - ↑k)) % (m + 1) (where m : ℕ and k : fin (m+1), so ↑k ≤ m. The simplifier fails to simplify further - I guess it's because everything is in ℕ, so we might have problems if we subtracted something larger from something smaller. In this case in know that ↑k ≤ m prevents such problems, but how can I tell this to Lean so that it can performs the simplification by itself in ℤ ?

[Yakov Pechersky]

Can you just case on k as 0 and above 0?

[Yakov Pechersky]

How did you get this simplified expression? There is a lot of fin api to help avoid modulus arithmetic hell

[Antoine Labelle]

I'm not sure how cases on k can help, can you elaborate?

[Kyle Miller]

One thing that helps with precise suggestions is a #mwe. (tactic#extract_goal can help with that.) Edit: spoke too soon, thanks for the code :down:

[Antoine Labelle]

Here is my entire code. I get this expression after simplifying an inequality between the cardinalities of two finsets at line 42.

import algebra.big_operators.basic
import algebra.big_operators.order
import data.finset.sort
import data.fintype.card
import data.fin.interval

open_locale big_operators
open finset

lemma rev_rev {m : ℕ} (k : fin (m+1)) : m - ↑(fin.last m - k) = ↑k :=
begin
  rw fin.coe_sub,
end

theorem imo1994 (n : ℕ) (m : ℕ) (A : finset ℕ) (hm : A.card = m + 1)
  (hrange : ∀ a ∈ A, 1 ≤ a ∧ a ≤ n) (hadd : ∀ a b ∈ A, a + b ≤ n → a + b ∈ A) :
  (m+1)*(n+1) ≤ 2*(∑ x in A, x) :=
begin
  set a := order_emb_of_fin A hm,  -- We sort the elements of A
  set rev := equiv.sub_left (fin.last m), -- i ↦ m-i

  -- The key inequality
  have hpair : ∀ k ∈ univ, (a k) + a (rev k) ≥ n+1,
  { rintros k -,
    by_contradiction,

    -- We exhibit k+1 elements of A greater than a (rev k)
    set f : fin (k+1) ↪ ℕ := ⟨λ i, a i + a (rev k),
    begin
      apply injective_of_le_imp_le,
      intros i j hij,
      rw [add_le_add_iff_right, a.map_rel_iff] at hij,
      sorry,
    end⟩,

    -- Proof that the f i are greater than a (rev k)
    have hf : map f univ ⊆ map a.to_embedding (Ioc (rev k) (fin.last m)),
    { sorry },

    have ineq := card_le_of_subset hf,

    simp [fin.coe_sub] at ineq,
    sorry,
  },

  -- We reindex the sum by fin (m+1)
  have : ∑ x in A, x = ∑ i : fin (m+1), a i,
  { convert sum_image (λ x hx y hy, (order_embedding.eq_iff_eq a).1),
    rw ←coe_inj, simp },
  rw this, clear this,

  -- The rest is a simple calculation by rearranging one of the two sums
  calc 2 * ∑ i : fin (m+1), a i = ∑ i : fin (m+1), a i + ∑ i : fin (m+1), a i       : two_mul _
                            ... = ∑ i : fin (m+1), a i + ∑ i : fin (m+1), a (rev i) : by {rw equiv.sum_comp rev}
                            ... = ∑ i : fin (m+1), (a i + a (rev i))                : sum_add_distrib.symm
                            ... ≥ ∑ i : fin (m+1), (n+1)                            : sum_le_sum hpair
                            ... = (m+1) * (n+1)                                     : by {simp}

end

[Yakov Pechersky]

If k is 0, then the deepest nested subtraction is m-1, which cancels to 0 in the mod op, then the addition cancels, then the subtraction cancels, and you get 0. If 0 < k, that is, for some k', k = k'+1, the subtraction cancels to m - k', which allows us to remove the modulus because that is obviously strictly less the m+1. Then you're left with m - (m - k'), and since we know that k' < m, we can reassociate the subtraction, and you're left over with k'. I hope I don't have an off by one error there.

[Kyle Miller]

tactic#zify can help sometimes, and you can give it inequalities to help it zify subtraction, if what you're wanting is to actually make everything be in terms of operations in Z. I don't know how it interacts with modulo, though.

[Antoine Labelle]

Yakov Pechersky said:

If k is 0, then the deepest nested subtraction is m-1, which cancels to 0 in the mod op, then the addition cancels, then the subtraction cancels, and you get 0. If 0 < k, that is, for some k', k = k'+1, the subtraction cancels to m - k', which allows us to remove the modulus because that is obviously strictly less the m+1. Then you're left with m - (m - k'), and since we know that k' < m, we can reassociate the subtraction, and you're left over with k'. I hope I don't have an off by one error there.

The expression we take the modulus of is m+(m-k'), not m-k' unfortunately, so I don't think it works.

[Kevin Buzzard]

Add import tactic at the top of your file, and then starting at line 42

    simp [fin.coe_sub] at ineq,
    -- you have natural subtraction which is horrible.
    -- let's get rid of it.
    cases k with k hk, -- turn k into a natural
    simp only [fin.coe_mk] at ineq, -- get k's in ineq
    rw [nat.lt_succ_iff,le_iff_exists_add] at hk, -- turn k < m + 1
    -- into ∃ (c : ℕ), m = k + c
    rcases hk with ⟨c, rfl⟩, -- nuke m completely and replace with k+c
    have foo : k + c + 1 - k = c + 1,
      rw [add_assoc, add_tsub_cancel_left],
    rw foo at ineq, -- one nat subtraction gone!
    -- now compute the mod
    rw (show k + c + (c + 1) = c + (k + c + 1), by ring) at ineq,
    simp only [nat.add_mod_right] at ineq,
    rw nat.mod_eq_of_lt (show c < k + c + 1, by linarith) at ineq,
    -- the simplifier can get rid of the remaining nat.sub
    simpa using ineq,

[Kevin Buzzard]

nat subtraction is horrible and it's taken me years to work out the tricks to kill it. I would recommend avoiding it completely.