Diff of naturals vs. diff of real (upper bound)

Stream: new members

[Reuven Peleg]

Hi all
During writing a proof I found myself get tangled in real vs natural casting, and had to write this lemma:

lemma nat_diff_le_cast (a b c : ℕ) : a - b ≤ c -> (a: ℝ) - (b: ℝ) ≤ c := by
  intro h
  rw [tsub_le_iff_right]
  rw [tsub_le_iff_right] at h
  norm_cast

It states that if (natural) diff is bound, then (real) diff is bound as well. This lemma works, but I was surprised it had to be written so explicilty given how common natural and real numbers are.
Is this reasonably good code? Can it be written more ellegantly using some existing lemmas or tactics?

[Ruben Van de Velde]

It's not so surprising that this is somewhat hard, because subtraction on natural numbers is poorly behaved

[Kevin Buzzard]

Yes, I wonder whether the reason this is not there is that people instinctively don't use natural subtraction when doing arithmetic, so this kind of lemma doesn't come up. i.e. the point at which you switch to reals is before you actually do the natural subtraction, rather than after you did it and realise you're now in a mess.

[Riccardo Brasca]

@Reuven Peleg What Ruben and Kevin are saying is that if a = 1, b = 2 and c = 3 then a - b = 0 (because subtraction on natural numbers truncates to 0) and your theorem says 0 ≤ 3 → -1 ≤ 3, that is true, but this probably not what you think.

[Reuven Peleg]

@Riccardo Brasca this is what I needed, since I have a goal of ↑S2.card - ↑S1.card ≤ 1 given S2.card - S1.card ≤ 1. Cardinality is Nat so I need this conversion.
The ultimate goal is to prove |(S1.card : ℝ) - (S2.card: ℝ)| <= 1, on which I had to use by_cases and demonstrate each substraction is <= 1. Even given S2.card - S1.card <= 1 and S1.card - S2.card <= 1 it was not easy, due to the mentioned Real/Nat relationship.
So my overall proof seems like this:

  let S1 := ...
  let S2 := ...

  have h_card_diff1 : S1.card - S2.card <= 1 := by sorry  -- Actual proof here
  have h_card_diff1_R : (S1.card : ℝ) - (S2.card : ℝ) <= 1 := by
    exact_mod_cast nat_diff_le_cast S1.card S2.card 1 h_card_diff1

  have h_card_diff2 : S2.card - S1.card <= 1 := by sorry  -- Actual proof here
  have h_card_diff2_R : (S2.card : ℝ) - (S1.card : ℝ) <= (1 : ℝ) := by
    exact_mod_cast nat_diff_le_cast S2.card S1.card 1 h_card_diff2

  have h_card_abs_diff : |(S1.card : ℝ) - (S2.card: ℝ)| <= 1 := by
    by_cases h_pos : 0 ≤ (S1.card : ℝ) - (S2.card : ℝ)
    · rw [abs_eq_self.mpr h_pos]
      linarith
    · push_neg at h_pos
      apply le_of_lt at h_pos
      rw [abs_eq_neg_self.mpr h_pos]
      linarith
  grind

And the journey from h_card_diff1 and h_card_diff2 to the goal felt a bit long, which I get (formalization is robust) but felt like I missed something since I am still getting used to LEAN.

[Riccardo Brasca]

Well, we should understand why you have that goal

[Reuven Peleg]

Thanks for the help and interest.
The broader context is Differential Privacy and the notion of sensibility: When I run a count qurey (cardinality of a filter over the dataset) on 2 neighboring datasets (only 1 item is different) the difference is limited to 1. So the goal is derived from the definition of sensibility (absolute difference of the query on the databases).
The full current code can be found on GitHub.
So the theorem is

theorem count_sensitivity_one (criteria : α → Bool) :
    has_sensitivity (countMatching criteria : Query ι α ℕ) 1
-- with
variable [PseudoMetricSpace β]
def has_sensitivity (q : Query ι α β) (Δ : ℝ) : Prop :=
  ∀ db1 db2, are_neighbors db1 db2 -> dist (q db1) (q db2) <= Δ
-- and
def countMatching (criteria : α -> Bool) : Query ι α ℕ :=
  fun db => (Finset.univ.filter (fun i => criteria (db i))).card

and after some basic rw and intro I have

k : ι
hk : {i | db1 i ≠ db2 i} = {k}
⊢ |↑{i | criteria (db1 i) = true}.card - ↑{i | criteria (db2 i) = true}.card| ≤ 1

Then I establish the cardinality of difference

  let S1 := (Finset.univ.filter (fun i => criteria (db1 i)))
  let S2 := (Finset.univ.filter (fun i => criteria (db2 i)))
  have h_diff_card : S1 \ S2 ⊆ {k} ∧ S2 \ S1 ⊆ {k} := by grind

And follows that

h_card_diff1 : S1.card - S2.card ≤ 1
h_card_diff2 : S2.card - S1.card ≤ 1

Which I turn into absolute difference

[Kevin Buzzard]

Are you sure you don't want a<=1+b rather than a-b<=1? The former looks easier to work with.

[Ruben Van de Velde]

Maybe better proof of the original question:

import Mathlib

lemma aux (a b : ℕ) : (a - b : ℝ) ≤ ↑(a - b) := by
  by_cases! hab : a < b
  · simp [-tsub_le_iff_right, hab.le, sub_nonpos]
  · simp [-tsub_le_iff_right, hab]

lemma nat_diff_le_cast (a b c : ℕ) : a - b ≤ c -> (a: ℝ) - (b: ℝ) ≤ c := by
  intro h
  apply le_trans (aux a b) (mod_cast h)