stuck proving divisibility theorem

Stream: new members

[Adam Dingle]

Consider this simple theorem, where all variables are integers:

If c divides a_1, .., a_k, then c divides (a_1 · u_1 + ... + a_k · u_k) for all integers u_1, ..., u_k.

Question 1: Does this theorem exist somewhere in MathLib (perhaps over some more general algebraic structure)?

As an exercise, I'd like to state this theorem in Lean and prove it. Here's my attempt at stating it:

open BigOperators
open Finset (range)

variable (c : ℤ) (k : ℕ) (a : ℕ → ℤ)

theorem div : (∀i ∈ range k, c ∣ a i) →
              (∀u : ℕ → ℤ, c ∣ ∑i in range k, a i * u i) :=

Question 2: Does this formulation look reasonable? I've used functions from ℕ → ℤ to represent the sequences, and I've used Finset.range to iterate over integers up to k. Also, I'm using indices from 0 .. k - 1 even though the original statement uses indices 1 .. k. Are these typical idiomatic choices?

Now I'd like to prove it. Here, in English, is a simple proof:

By the definition of divisibility, there exist integers q_1 .. q_k such that a_i = q_i · c for i = 1, ..., k. Then

(a_1 · u_1 + ... + a_k · u_k) = (q_1 · c · u_1 + ... + q_k · c · u_k) = (q_1 · u_1 + ... + q_k · u_k) · c.

And so c divides (a_1 · u_1 + ... + a_k · u_k).

Here's my attempt to translate just the first part of the proof into Lean:

theorem div (h : ∀i ∈ range k, c ∣ a i) :
              (∀u : ℕ → ℤ, c ∣ ∑i in range k, a i * u i) :=

  let q i (r : i ∈ range k): ℤ :=
    let ⟨d, _⟩ := h i r
    d
  sorry

For now, I'm only trying to establish the sequence q. Unfortunately the code above fails to compile, and I'm a bit stuck. I believe that h i r has type (c | a i), which is defined to mean ∃ d, a i = c * d. So I thought I could use 'let' to get the value d. However Lean won't accept the statement 'let ⟨d, _⟩ := h i r':

tactic 'cases' failed, nested error:
tactic 'induction' failed, recursor 'Exists.casesOn' can only eliminate into Prop
c: ℤ
a: ℕ → ℤ
i: ℕ
motive: c ∣ a i → Sort ?u.16204
h_1: (d : ℤ) → (h : a i = c * d) → motive (_ : ∃ c_1, a i = c * c_1)
x✝: c ∣ a i
⊢ motive x✝

Question 3: What's wrong in my code above? How to fix it?

I'd appreciate any feedback on the questions above - thanks.

[Yaël Dillies]

Yes, it's (the direct composition of things) in mathlib: See docs#Finset.dvd_sum

[Yaël Dillies]

You will need one more lemma, which I am leaving for you to find

[Junyan Xu]

To get the integers q_1 ... q_k as a function q, you need to use the choose tactic which invokes the axiom of choice:

theorem div (h : ∀i ∈ range k, c ∣ a i) :
              (∀u : ℕ → ℤ, c ∣ ∑i in range k, a i * u i) := by
  choose q hq using h

Even though you can construct a function q satisfying hq by induction on k (since range k is (computably) finite you can avoid choice), invoking choice is more convenient.

[Kevin Buzzard]

There's no reason to have the source equal to Nat, here's a free generalization:

import Mathlib

open BigOperators
open Finset (range)

variable (c : ℤ) (α : Type) (a : α → ℤ) (s : Finset α)

theorem div : (∀ i ∈ s, c ∣ a i) →
    (∀ u : α → ℤ, c ∣ ∑ i in s, a i * u i) :=
  sorry

[Ruben Van de Velde]

Could be even more general if you put a * after that Type (or so I hear, I don't know what universes are)

[Kevin Buzzard]

And the target could be anything for which | makes sense I guess (e.g. any commutative ring? Probably something even more general?)

[Adam Dingle]

Thanks to everyone for the helpful replies.

It hadn't occurred to me that accessing the existential h i r could require choice. However if I wanted to build a function with an infinite domain that used an existential to compute its value at each point, then the axiom of choice would indeed be necessary. So it's not surprising that Lean restricts access to an existential in a function definition (even though in my case I'm only accessing it for a finite number of values in the domain).

Thanks especially to Junyan for the pointer to the choose tactic, which seems super helpful here. This is another tactic I didn't know about, and will add to my vocabulary. :)

[Eric Rodriguez]

Kevin Buzzard said:

And the target could be anything for which | makes sense I guess (e.g. any commutative ring? Probably something even more general?)

Semigroups (docs#semigroupDvd)

[Kevin Buzzard]

@Adam Dingle the "axiom of choice" in lean's dependent type theory refers to the concept of getting data out of a proof, ie moving from the Prop universe to the Type universe. So going from "there exists an x" to "here is the x" uses the axiom of choice (or even from "there exists a unique x" to "here is the x"! This would not use AC in set theory). The usual set-theoretic axiom of choice follows from this principle. The reason it's a bit different in type theory is that type theory isolates the noncomputable part of the process. Even if you can prove there's a unique x with a property, you still don't have a formula for it in the sense of constructive mathematics, so the process of getting it is noncomputable.

[Adam Dingle]

@Kevin Buzzard This is informative and helpful. Thanks!

[Kevin Buzzard]

Here's an explicit example of a situation where you can prove there's a unique x with some property, but there's no known algorithm to figure out what the x is. Another example would be the function $G$ related to Waring's problem: it's certainly true that there exists a unique natural number N such that every sufficiently large natural is the sum of N natural cubes, but there are infinitely many naturals which aren't the sum of N-1 natural cubes, but right now humanity knows of no algorithm to figure out this N, all we know is that it's between 4 and 7. So Lean would need what it calls the axiom of choice to define the function $G(n)$ described here, but really this is just another way of saying "there's no known computer program which computes this function" (indeed if there were then it probably wouldn't be an open problem to figure out $G(3)$.)

[Adam Dingle]

Kevin, thanks for the interesting examples.

I've tried to continue my proof, but I'm a bit stuck again.

Once again, I'm trying to prove that

If c divides a_1, .., a_k, then c divides (a_1 · u_1 + ... + a_k · u_k) for all integers u_1, ..., u_k.

(As Kevin and others have pointed out, I could generalize this in various ways, but I'm sticking to integers and indices 1..k in the interest of keeping things simple and concrete, since this is just an exercise.)

And once again, here's my proof in English:

===
By the definition of divisibility, there exist integers q_1 .. q_k such that a_i = q_i · c for i = 1, ..., k. Then

(a_1 · u_1 + ... + a_k · u_k) = (q_1 · c · u_1 + ... + q_k · c · u_k) = (q_1 · u_1 + ... + q_k · u_k) · c.

And so c divides (a_1 · u_1 + ... + a_k · u_k).
===

As Junyan pointed out, I can use choose to get the integers q_i. After that, as the first step of the proof I'd like to show that

(a_1 · u_1 + ... + a_k · u_k) = (q_1 · c · u_1 + ... + q_k · c · u_k)

At first I thought I could write this equality as

∑i in range k, a i * u i = ∑i in range k, (c * q i) * u i

However q has type (i : ℕ) → i ∈ range k → ℤ, so it needs evidence that i is a valid index. And as far as I can tell no such evidence is available inside an instance of ∑. So as a workaround, I've written

  let q' i := if r : i ∈ range k then q i r else 0

This feels awkward, but at least it allows me to write the sum using q'. So here is where I am now:

open BigOperators
open Finset (range)

variable (c : ℤ) (k : ℕ) (a : ℕ → ℤ)

theorem div (h : ∀i ∈ range k, c ∣ a i) :
            (∀u : ℕ → ℤ, c ∣ ∑i in range k, a i * u i) := by
  choose q hq using h
  let q' i := if r : i ∈ range k then q i r else 0
  intro u
  have : ∑i in range k, a i * u i = ∑i in range k, (c * q' i) * u i := by sorry
  sorry

I can't immediately see how to prove that the sums are equal. At the first sorry the proof state is

c: ℤ
k: ℕ
a: ℕ → ℤ
q: (i : ℕ) → i ∈ range k → ℤ
hq: ∀ (i : ℕ) (a_1 : i ∈ range k), a i = c * q i a_1
q': ℕ → ℤ := fun i => if r : i ∈ range k then q i r else 0
u: ℕ → ℤ
⊢ ∑ i in range k, a i * u i = ∑ i in range k, c * q' i * u i

For any i in range k, hq tells me that a_i = c * q_i. So really I'd like to make this substitution in the goal. But to do that I need evidence that i ∈ range k, and I don't see how I can get to that. Perhaps I have to fall back on proving that these sums are equal using induction up to k, but that feels heavy-handed. Is there an easier way?

[Adam Dingle]

I just figured out that instead of choose I can use choose!:

  choose! q hq using h

That gives me q: ℕ → ℤ, which is great - I no longer need the awkward q'.

However I'm still unsure about how to substitute into the goal, because even with this change hq will still need evidence that i ∈ range k.

[Adam Dingle]

Aha - I just discovered this theorem in the library:

theorem Finset.sum_congr {β : Type u}  {α : Type v}  {s₁ : Finset α}  {s₂ : Finset α}  {f : α → β} {g : α → β}  [AddCommMonoid β]  (h : s₁ = s₂) :
(∀ x ∈ s₂, f x = g x) → Finset.sum s₁ f = Finset.sum s₂ g

This looks like what I need. I'll try to use it to make the proof work.

[Kevin Buzzard]

Re where you are now: what are your imports? Your code doesn't work for me as it stands, and different imports making it work can have different behaviours.

[Adam Dingle]

Actually I just completed the proof:

import Mathlib

open BigOperators
open Finset (range)

variable (c : ℤ) (k : ℕ) (a : ℕ → ℤ)

theorem div (h : ∀i ∈ range k, c ∣ a i) :
            (∀u : ℕ → ℤ, c ∣ ∑i in range k, a i * u i) := by
  choose! q hq using h
  intro u
  let he :=
    calc ∑i in range k, a i * u i

     _ = ∑i in range k, c * (q i * u i) := by
        apply Finset.sum_congr ; rfl
        intros x hx
        rwa [hq, mul_assoc]

     _ = c * ∑i in range k, q i * u i := by
        rw [Finset.mul_sum]

  exact ⟨_, he⟩

[Kevin Buzzard]

Here's a calc-free proof:

import Mathlib

open BigOperators
open Finset -- not just Finset.range, we want more!

variable (c : ℤ) (k : ℕ) (a : ℕ → ℤ)

theorem dvd (h : ∀i ∈ range k, c ∣ a i) (u : ℕ → ℤ) : -- `div` is `/`, there is no `/` mentioned
    c ∣ ∑i in range k, a i * u i := by -- move `u` before the colon to save `intro u`
  choose! q hq using h
  use ∑ i in range k, q i * u i
  rw [mul_sum]
  apply sum_congr rfl
  intros
  rw [hq, mul_assoc]
  assumption

[Adam Dingle]

Kevin Buzzard said:

Here's a calc-free proof:

Thanks for the simplified proof! I'll see what I can learn from it. :)

[Kevin Buzzard]

Here's the proof in the correct generality: note that the same proof still works, using concrete types like Nat just (in my opinion) makes things more confusing (because there's more ways to go wrong).

import Mathlib

open BigOperators
open Finset

theorem Finset.dvd_sum'
    -- source
    {α : Type*} (S : Finset α)
    -- target
    {R : Type*} [CommSemiring R]
    (c : R) (a : α → R)
    (h : ∀ i ∈ S, c ∣ a i) (u : α → R) :
    c ∣ ∑i in S, a i * u i := by
  -- exactly the same proof (mutatis mutandis)
  choose! q hq using h
  use ∑ i in S, q i * u i
  rw [mul_sum]
  apply sum_congr rfl
  intros
  rw [hq, mul_assoc]
  assumption

variable (c : ℤ) (k : ℕ) (a : ℕ → ℤ)

-- your application
theorem dvd (h : ∀i ∈ range k, c ∣ a i) (u : ℕ → ℤ) : -- `div` is `/`, there is no `/` mentioned
    c ∣ ∑i in range k, a i * u i := by
  apply Finset.dvd_sum'
  assumption

[Kevin Buzzard]

And here's the proof using the lemmas mathlib already has:

theorem dvd (h : ∀i ∈ range k, c ∣ a i) (u : ℕ → ℤ) :
    c ∣ ∑i in range k, a i * u i := by
  apply Finset.dvd_sum
  peel h with n hn h
  exact Int.dvd_trans h ⟨u n, rfl⟩

[Eric Rodriguez]

Using Kevin's version with a general indexing set (which often works better in Lean than using range or something of the like) you can also use Finset induction, (iirc docs#Finset.induction_on) which is a much more natural proof. I'm not at a computer at the current moment but happy to write this up if you'd like an example

[Adam Dingle]

Eric Rodriguez said:

Using Kevin's version with a general indexing set (which often works better in Lean than using range or something of the like) you can also use Finset induction, (iirc docs#Finset.induction_on) which is a much more natural proof. I'm not at a computer at the current moment but happy to write this up if you'd like an example

Thanks. If you'd be willing to write this version up, I'd be happy to see it - I am relatively new to Lean and learn something from every proof I see. :)

[Eric Rodriguez]

import Mathlib

open BigOperators
open Finset

theorem Finset.dvd_sum'
    -- source
    {α : Type*} (S : Finset α)
    -- target
    {R : Type*} [CommSemiring R]
    (c : R) (a : α → R)
    (h : ∀ i ∈ S, c ∣ a i) (u : α → R) :
    c ∣ ∑i in S, a i * u i := by
  classical -- we need this for `Finset.induction_on`
  induction S using Finset.induction_on
  case empty => simp
  case insert h k S hkS ih =>
    specialize ih (fun i hi ↦ h _ <| mem_insert_of_mem hi)
    rw [Finset.sum_insert hkS]
    refine dvd_add ?_ ih
    exact (h k (mem_insert_self k S)).mul_right _

-- with a bit more detail:
example
    -- source
    {α : Type*} (S : Finset α)
    -- target
    {R : Type*} [CommSemiring R]
    (c : R) (a : α → R)
    (h : ∀ i ∈ S, c ∣ a i) (u : α → R) :
    c ∣ ∑i in S, a i * u i := by
  classical -- we need this for `Finset.induction_on`
  -- when you get complaints about `DecidableEq`
  -- being needed _whilst already in a proof_, you should try `classical` beforehand.
  -- The situation is a bit more difficult if you're still writing the statement.
  -- I tried to use the `induction` and the last goal was `DecidableEq α`, hence I added `classical`.
  induction S using Finset.induction_on
  case empty => simp
  -- `simp` is a "simplifier" - this does not always mean it makes your
  -- expressions simpler, but it does mean it's often worth trying on
  -- goals that are "structurally" likely to be true.
  case insert h k S hkS ih =>
    -- I'm not sure why `ih` has this weird hypothesis, but it's easy to fix; let's do that first.
    -- I did not remember the name of `mem_insert_of_mem` (although it's not hard),
    -- but instead I originally wrote:
    -- `specialize ih (fun i hi ↦ h i <| by exact?)`
    -- (<| basically inserts brackets around the next expression)
    -- and that found it. You can also use:
    -- `specialize ih (fun i hi ↦ h i <| exact?%)`
    specialize ih (fun i hi ↦ h i <| mem_insert_of_mem hi)
    rw [Finset.sum_insert hkS]
    -- Instead of `specialize`ing earlier, I could also have written:
    --  `refine dvd_add ?_ <| ih (fun i hi ↦ h i <| mem_insert_of_mem hi)`
    refine dvd_add ?_ ih
    -- I could've found this by first writing `specialize h k exact?%` and then putting in
    -- what `exact?%` found; this actually gives you a slightly different suggestion
    -- try figure out what that one means!
    -- I then just did `exact?` after, and it found the right thing. I then tidied it using
    -- "dot notation"; the divides symbol is called `Dvd.dvd`, so you're allowed to use a hypothesis
    -- `h : something ∣ something_else` with a method called `Dvd.dvd.foo` by writing `h.foo`.
    -- To clarify: my original proof was:
    /- specialize h k exact?%
      exact? -/
    -- which soon turned into:
    /-
    specialize h k <| mem_insert.mpr (Or.inl rfl)
    exact Dvd.dvd.mul_right h (u k)
    -/
    -- and then tidied it a bit more to: (I changed the theorem to use something a bit more designed for this)
    -- Note that I can skip `u k` and instead write `_` because Lean's elaborator sees what it must be.
    exact (h k (mem_insert_self k S)).mul_right _

[Patrick Massot]

Kevin, why are you providing a calc free proof? calc proofs are much easier to read.

[Kevin Buzzard]

Because it's a beginner who showed some interest so I thought I'd show them another way