strange notation: P → Q → R

Stream: new members

[rzeta0]

I've reached Chapter 4 of Heather Macbeth's Mechanics of Proof and am finding new syntax being introduced without explanation.

Here is one I can't understand:

example {n : ℤ} (hn : ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n) : 15 ∣ n := by

The accompanying text says:

Let  n be an integer and suppose that every integer m  between 1 and 5 is a factor of n. Show that 15 is a factor of n.

I would have expected the hypothesis to be a conjunction, not a chained implication.

example {n : ℤ} (hn : ∀ m, 1 ≤ m ∧ m ≤ 5 ∧ m ∣ n) : 15 ∣ n := by

So what does P → Q → R mean?

[Eric Wieser]

∀ m, 1 ≤ m ∧ m ≤ 5 ∧ m ∣ n says "every number is between 1 and 5 and divides n" not, "every number that is between 1 and 5 divides n"

[Eric Wieser]

You could write ∀ m, 1 ≤ m ∧ m ≤ 5 → m ∣ n instead, which would have the correct meaning (see docs#and_imp for the equivalence)

[Kyle Miller]

"P → Q → R" means "if P and if Q then R". You can read each successive arrow as "and if"

[Kyle Miller]

It is logically equivalent to "P /\ Q -> R", but it is more convenient for lemmas. The first lets you pass in hypotheses for P and Q one at a time. The conjunctive version wants the hypotheses at once (and assembled with And.intro)

[rzeta0]

Eric Wieser said:

∀ m, 1 ≤ m ∧ m ≤ 5 ∧ m ∣ n says "every number is between 1 and 5 and divides n" not, "every number that is between 1 and 5 divides n"

This was the conceptual root of my misunderstanding. Thanks.

My reading of ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n based on my possibly mistaken understanding of implication is:

• for all m the following is true
• if 1 ≤ m true then m ≤ 5 true
• if m ≤ 5 true then m ∣ n true

but this doesn't match "every number that is between 1 and 5 divides n"

[Eric Wieser]

I think what you're missing is that ∀ m, 1 ≤ m → m ≤ 5 → m ∣ n means ∀ m, (1 ≤ m → (m ≤ 5 → m ∣ n))

[Eric Wieser]

Lean does not have python-style operation chaining

[rzeta0]

thanks Eric again for clarifying

so is that chain always equivalent to

∀ m, (1 ≤ m → (m ≤ 5 → m ∣ n))

and not

∀ m, ((1 ≤ m → m ≤ 5) → m ∣ n)

Is that just the way it is, or is there a deeper logic or rationale I'm missing? It just seems arbitrary.

[Kyle Miller]

The first one is the common case, and also if h : P -> Q -> R, then given x : P and y : Q, you can write h x y to get a proof of R. It lines up nicely with application notation.

[Kyle Miller]

Similarly, h x y is (h x) y and not h (x y). This is interestingly backwards from -> associativity, but that's how it needs to work so that no parentheses are needed in the common case.

[Eric Wieser]

It just seems arbitrary.

While not the case here for the reasons Kyle explains, for things like a + b + c meaning (a + b) + c and not a + (b + c), this choice basically is arbitrary; but the choice still has to be made, because forcing people to always write the ()s explicitly would be very annoying.