A quantifier's facts are read inside its body

[Rafael-SOWNet]

Part of #1409.

This implements Prob 8.9.24 for every prime, as agreed on #1409. forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k) is now True. It was left as written, because the claim needs p prime and 0 < k < p, and only the quantifiers around it say so.

How the facts reach the rule

A quantifier hands its facts down while it decides its body. It establishes that its name is in the set it ranges over, and, while a claim is simplified, the conjuncts of its hypothesis.

• For forall x in S : H implies C, the conjuncts of H are in scope while C is simplified, and never while H is.
• For exists and exists!, each conjunct is simplified with the ones before it in scope.
• Scopes nest, so the inner quantifier knows p is prime in either order of the two quantifiers. A curried hypothesis, 0 < k implies (k < p implies ...), works too.

The rule for p divides binomial(p, k) reads them through QuantifierFacts.PrimeDividesItsBinomial.

Why nothing leaks

The bound name is renamed first, to a name no other expression has, taken from a process-wide counter. Every fact is about a renamed name. A node that caches its simplification can only have read a fact if it mentions a renamed name, and every such node is built during this decision. So nothing reachable from outside the decision can hold a verdict that depended on the facts, including through a cache keyed on structure. For the same reason, a conjunct of the hypothesis that mentions only free names is not put in scope.

WhatTheQuantifiersEstablishDoesNotLeaveThem shares one claim node between a statement and the caller. The statement is True, and afterwards the claim on its own is still p divides binomial(p, k) under Evaled, InnerSimplified and Simplify().

A substitution stops at a binder, so an inner quantifier that binds p again isn't renamed through, and the outer facts don't reach it: forall p in PP : forall p in ZZ+ : ... is False. The renaming happens only where a rule in the body reads facts. Every other statement is decided as before, under its own names.

What the rule needs

It needs p prime, k whole, k > 0 and p - k > 0. Positivity is read off the comparisons and memberships in scope, up to a constant: k <= p - 1 bounds p - k below by 1, and a prime is at least 2. So over the primes p divides binomial(p, 1) is True, and p divides binomial(p, 2) is False (a counterexample at p = 2). Without primality, or without either bound on k, the statement is False. For a real k it stays unevaluated.

Proof recording

Steps recorded under a renamed name are written back under the given one. When the facts reduce a body to True, the statement is recorded as written, so the proof reads:

    p divides binomial(p, k) is True: p is prime and 0 < k < p, so p divides p! = binomial(p, k) k! (p - k)! and none of the factors of k! (p - k)! [Nat.Prime.dvd_choose_self]
  forall k in ZZ : 0 < k and k < p implies p divides binomial(p, k) is True: p divides binomial(p, k) holds for every k in ZZ with 0 < k and k < p [intro]
forall p in PP : forall k in ZZ : 0 < k and k < p implies p divides binomial(p, k) is True: the body holds for every p in PP [intro]

Nat.Prime.dvd_choose_self (hp : p.Prime) (hk : k ≠ 0) (hkp : k < p) : p ∣ choose p k is in Mathlib/Data/Nat/Choose/Dvd.lean.

Measured

The unit suite passes on net10.0: 12738 passed, 14 skipped, none failed, out of 12752, of which 14 are new.

The allocation gate passes on all 19 gated benchmarks.

Fermat's little theorem is next, derived from this rule through the binomial theorem as the book does.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura