From c8b37912aa924cbf2ecabe28a848492b9b97070d Mon Sep 17 00:00:00 2001 From: Rafael Vuijk Date: Sun, 27 Sep 2026 09:01:09 +0000 Subject: [PATCH] A quantifier's facts are read inside its body forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k) was left as written: the claim needs p prime and 0 < k < p, and only the quantifiers around it say so. A quantifier whose body has a rule that reads facts now decides it with them in scope: that its name is in its set and, while a claim is simplified, the conjuncts of its hypothesis. The rule for p divides binomial(p, k) reads them (Nat.Prime.dvd_choose_self). The bound name is renamed first, to a name no other expression has, and every fact is about a renamed name, so nothing that read a fact is reachable from outside the decision, through a node's own cache or a structural one. Steps recorded under a renamed name are written back under the given one. Part of #1409. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura --- BREAKING-CHANGES.md | 17 + Sources/.editorconfig | 3 + .../Functions/Boolean/ProofRecording.cs | 43 +++ .../Functions/Boolean/QuantifierFacts.cs | 321 ++++++++++++++++++ .../Evaluation.Discrete.Classes.cs | 10 + .../UnitTests/Core/ProofRecordingTest.cs | 15 + .../Tests/UnitTests/Core/QuantifierTest.cs | 38 +++ 7 files changed, 447 insertions(+) create mode 100644 Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs diff --git a/BREAKING-CHANGES.md b/BREAKING-CHANGES.md index 9613a2ae6..f47ee9504 100644 --- a/BREAKING-CHANGES.md +++ b/BREAKING-CHANGES.md @@ -1523,6 +1523,23 @@ in 2.5.0. | `forall a in ZZ : a^7 mod 7 = a mod 7` | `UnhandledParseException` | `True` | | `forall a, b in ZZ : (a + b)^5 mod 5 = (a^5 + b^5) mod 5` | `UnhandledParseException` | `True` | +### A quantifier's facts are read inside its body + +`forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)` was left as +written. The claim holds because `p` is prime and `0 < k < p`, and only the quantifiers around it +say so. A quantifier now hands those facts down while it decides its body: the set its name ranges +over, and, while the claim is simplified, the conjuncts of the hypothesis. The rule for +`p divides binomial(p, k)` reads them. Nothing decided with them leaves the quantifier: +`p divides binomial(p, k)` on its own is still left as written. This is Sullivan and Mackey's +Prob 8.9.24 for every prime ([#1409](https://github.com/asc-community/AngouriMath/issues/1409)). +Quantifiers were a parse error in 2.5.0. + +| Input | Was (2.5.0) | Now | +|---|---|---| +| `forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)` | `UnhandledParseException` | `True` | +| `forall k in ZZ : forall p in PP : (0 < k and k < p) implies p divides binomial(p, k)` | `UnhandledParseException` | `True` | +| `forall p in PP : forall k in ZZ+ : k < p implies p divides binomial(p, k)` | `UnhandledParseException` | `True` | + ### `binomial(n, k)` is a function **Addition, not silent.** The binomial coefficient is a node, `Entity.Binomialf`, spelled diff --git a/Sources/.editorconfig b/Sources/.editorconfig index 98e221048..c157640f6 100644 --- a/Sources/.editorconfig +++ b/Sources/.editorconfig @@ -318,6 +318,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed [AngouriMath/Functions/Boolean/ProofRecording.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n +[AngouriMath/Functions/Boolean/QuantifierFacts.cs] +file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n + [Tests/UnitTests/Core/ProofRecordingTest.cs] file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n diff --git a/Sources/AngouriMath/Functions/Boolean/ProofRecording.cs b/Sources/AngouriMath/Functions/Boolean/ProofRecording.cs index 9ce22c43f..7f75f138b 100644 --- a/Sources/AngouriMath/Functions/Boolean/ProofRecording.cs +++ b/Sources/AngouriMath/Functions/Boolean/ProofRecording.cs @@ -142,6 +142,49 @@ internal static int Mark() return recording.steps.Count; } + /// + /// Writes the steps recorded since with + /// read as : a quantifier decides under a name of its own while + /// facts are in scope (), and its steps + /// are written under the name it was given. + /// + internal static void Rename(int mark, Entity.Variable from, Entity.Variable to) + { + var recording = current.Value; + if (recording is null || recording.closed) + return; + lock (recording.gate) + for (var i = mark; i < recording.steps.Count; i++) + { + var step = recording.steps[i]; + recording.steps[i] = step with + { + Statement = Functions.Boolean.QuantifierFacts.Renamed(step.Statement, from, to), + Rule = step.Rule.Replace(from.Name, to.Name), + Verdict = Functions.Boolean.QuantifierFacts.Renamed(step.Verdict, from, to), + }; + } + } + + /// + /// Writes the step the decision in progress recorded last, since , + /// as a step about by , keeping its + /// verdict and depth. A quantifier that decided its body with facts in scope records the + /// statement as it was written, rather than the body those facts made of it. + /// + internal static void Restate(int mark, Entity statement, string rule, string lemma) + { + var recording = current.Value; + if (recording is null || recording.closed) + return; + lock (recording.gate) + { + var last = recording.steps.Count - 1; + if (last >= mark && recording.steps[last].Depth == depth) + recording.steps[last] = recording.steps[last] with { Statement = statement, Rule = rule, Lemma = lemma }; + } + } + internal static void Rollback(int mark) { var recording = current.Value; diff --git a/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs b/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs new file mode 100644 index 000000000..80bcd65ae --- /dev/null +++ b/Sources/AngouriMath/Functions/Boolean/QuantifierFacts.cs @@ -0,0 +1,321 @@ +// +// Copyright (c) 2019-2026 Angouri. +// AngouriMath is licensed under MIT. +// Details: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md. +// Website: https://am.angouri.org. +// + +using System.Collections.Generic; +using System.Linq; +using System.Threading; +using AngouriMath.Core; +using PeterO.Numbers; +using static AngouriMath.Entity; +using static AngouriMath.Entity.Number; +using static AngouriMath.Entity.Set; + +namespace AngouriMath.Functions.Boolean +{ + /// + /// What the quantifiers around a statement establish while they decide it: each bound name + /// is a member of the set it ranges over, and a claim made under a hypothesis is made where + /// the hypothesis holds. A rule that needs one of those facts, such as that p is prime + /// or that 0 < k < p, asks here. + /// + /// + /// + /// A node has no parent, so a rule inside a body cannot walk up to the quantifier that binds + /// its names. The quantifier hands the facts down instead, for as long as it takes to decide: + /// the set its name ranges over, and for forall x in S : H implies C the conjuncts of + /// H while C is simplified. They are never in scope while H itself is + /// simplified, or H implies C would lose its hypothesis. For exists and + /// exists! each conjunct of the body is simplified with the ones before it in scope. + /// Scopes nest, so the inner quantifier of forall p in PP : forall k in ZZ : ... knows + /// that p is prime. Nothing leaves a scope: a verdict reached with the facts is the + /// verdict on the quantified statement, which states them, and it carries no condition. + /// + /// + /// The bound name is renamed first, to a name no other expression has, and every fact is + /// about a renamed name. That is what keeps a verdict from escaping through a cache. 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 and is reachable from nothing else. A + /// cache keyed on the structure of an expression cannot serve it elsewhere either, since no + /// other expression has the name. For the same reason a conjunct of the hypothesis about the + /// free names alone is not recorded: a rule reading it could simplify a node that is shared. + /// A substitution stops at a binder, so an inner quantifier that binds the same name again + /// is not renamed through, and the outer facts about the name do not reach it. + /// + /// + /// Only a body in which a rule reads the facts is renamed and decided this way. Every other + /// statement is decided as it was, under its own names. + /// + /// https://github.com/asc-community/AngouriMath/issues/1409 + /// + internal static class QuantifierFacts + { + /// One scope: the name it renamed, where it bound one, and what it establishes. + private sealed class Frame + { + internal readonly Variable? Renamed; + internal readonly Entity[] Facts; + internal readonly Frame? Next; + internal Frame(Variable? renamed, Entity[] facts, Frame? next) => (Renamed, Facts, Next) = (renamed, facts, next); + } + + [System.ThreadStatic] private static Frame? top; + + /// Numbers the renamed names, which is what makes each one unlike any other. + [ConcurrentField] private static long lastRenamed; + + /// + /// Decides the quantified statement with the facts in scope, or + /// where no rule in the body reads them, for the statement to be decided as before. The + /// verdict is where it is not settled, beside the body simplified + /// as far as it went, under the name it was given. + /// + internal static (Entity? Verdict, Entity Body)? Decide(Quantifiers.Kind kind, Entity var, Entity over, Entity body, bool isExact) + { + if (var is not Variable x || over is not Set set || !body.Nodes.Any(Reads)) + return null; + var renamed = Variable.CreateVariableUnchecked($"{x.Name}'{Interlocked.Increment(ref lastRenamed)}"); + var mark = ProofRecording.Mark(); + var enclosing = top; + top = new Frame(renamed, new[] { renamed.In(set) }, enclosing); + try + { + // One level down, so that what a rule records while the body is simplified is + // written under the statement the quantifier records when it decides. + var written = body.Substitute(x, renamed); + Entity simplified; + ProofRecording.Enter(); + try + { + simplified = Simplified(kind, written, isExact); + } + finally + { + ProofRecording.Leave(); + } + var verdict = Quantifiers.Decide(kind, renamed, set, simplified, isExact); + if (verdict is null) + ProofRecording.Rollback(mark); + // A body the facts made True is recorded as it was written: the decision's own + // step would otherwise read `forall k in ZZ : True`. + else if (kind == Quantifiers.Kind.All && simplified == Entity.Boolean.True) + ProofRecording.Restate(mark, new Forallf(renamed, set, written), + written is Impliesf(var hypothesis, var claim) + ? $"{claim} holds for every {renamed} in {set} with {hypothesis}" + : $"the body holds for every {renamed} in {set}", + "intro"); + ProofRecording.Rename(mark, renamed, x); + return (verdict is null ? null : Renamed(verdict, renamed, x), Renamed(simplified, renamed, x)); + } + finally + { + top = enclosing; + } + } + + /// + /// The body simplified with the facts in scope: a claim made under a hypothesis with the + /// conjuncts of the hypothesis in scope as well, and the hypothesis itself with only the + /// facts from outside it. + /// + private static Entity Simplified(Quantifiers.Kind kind, Entity body, bool isExact) + { + switch (kind, body) + { + // forall x in S : H implies C, and H1 implies (H2 implies C) with both in scope for C. + case (Quantifiers.Kind.All, Impliesf(var hypothesis, var claim)): + { + var assumed = hypothesis.InnerSimplified(isExact); + var enclosing = Establish(assumed); + Entity concluded; + try + { + concluded = Simplified(kind, claim, isExact); + } + finally + { + top = enclosing; + } + return new Impliesf(assumed, concluded).InnerSimplified(isExact); + } + // exists x in S : A and B and C, each conjunct with the ones before it in scope. + case (not Quantifiers.Kind.All, Andf): + { + var conjuncts = new List(); + var enclosing = top; + try + { + foreach (var conjunct in Andf.LinearChildren(body)) + { + var simplified = conjunct.InnerSimplified(isExact); + conjuncts.Add(simplified); + Establish(simplified); + } + } + finally + { + top = enclosing; + } + return conjuncts.Aggregate((left, right) => new Andf(left, right)).InnerSimplified(isExact); + } + default: + return body.InnerSimplified(isExact); + } + } + + /// + /// Puts in scope the conjuncts of that mention a renamed + /// name, and returns what was in scope before. + /// + private static Frame? Establish(Entity statement) + { + var enclosing = top; + var facts = Andf.LinearChildren(statement).Where(MentionsARenamedName).ToArray(); + if (facts.Length > 0) + top = new Frame(null, facts, enclosing); + return enclosing; + } + + /// + /// The expression with read as everywhere, + /// the name a quantifier binds included, which a substitution leaves alone. + /// + internal static Entity Renamed(Entity expression, Variable from, Variable to) + => expression.Replace(node => node switch + { + Variable name when name == from => to, + Quantifier quantifier when quantifier.Var == from => quantifier.New(to, quantifier.Over, quantifier.Body), + _ => node + }); + + /// + /// Whether a rule reads the facts at , which is what a body is + /// renamed and decided with the facts in scope for. + /// + private static bool Reads(Entity node) + => node is Dividesf(var divisor, Binomialf(var upper, _)) && divisor == upper; + + private static bool MentionsARenamedName(Entity expression) + { + if (top is null) + return false; + foreach (var name in expression.Vars) + for (var frame = top; frame is not null; frame = frame.Next) + if (frame.Renamed is { } renamed && renamed == name) + return true; + return false; + } + + private static IEnumerable InScope() + { + for (var frame = top; frame is not null; frame = frame.Next) + foreach (var fact in frame.Facts) + yield return fact; + } + + /// + /// Whether p divides binomial(p, k) follows from the facts in scope: p is + /// prime and k is a whole number with 0 < k < p. Then p divides + /// p! = binomial(p, k) k! (p - k)! and none of the factors of k! (p - k)!, + /// each of which is below the prime p. Sullivan and Mackey's Prob 8.9.24. + /// + internal static bool PrimeDividesItsBinomial(Entity p, Entity k) + { + if (top is null || !IsPrime(p) || !IsWhole(k) || !IsPositive(k) || !IsPositive(p - k)) + return false; + if (ProofRecording.Recording) + ProofRecording.AddBelow(new Dividesf(p, new Binomialf(p, k)), + $"{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", Entity.Boolean.True); + return true; + } + + private static bool IsPrime(Entity expression) + => expression is Integer number ? Functions.Primes.IsPrime(number.EInteger) == true : IsIn(expression, 0); + + private static bool IsWhole(Entity expression) + => expression is Integer || IsIn(expression, 3); + + /// + /// Whether the facts in scope put in the set of numbers ranked + /// by , or in one inside it. + /// + private static bool IsIn(Entity element, int rank) + { + if (!MentionsARenamedName(element)) + return false; + foreach (var fact in InScope()) + if (fact is Inf(var member, SpecialSet within) && member == element && Rank(within) is var inner and >= 0 && inner <= rank) + return true; + return false; + } + + /// The sets of numbers, each inside the next: PP, ZZ+, ZZ*, ZZ, QQ, RR, CC. + private static int Rank(SpecialSet set) => set switch + { + SpecialSet.Primes => 0, + SpecialSet.PositiveIntegers => 1, + SpecialSet.NonNegativeIntegers => 2, + SpecialSet.Integers => 3, + SpecialSet.Rationals => 4, + SpecialSet.Reals => 5, + SpecialSet.Complexes => 6, + _ => -1 + }; + + /// + /// Whether is positive by the facts in scope. Each fact bounds + /// a quantity below: a > b and b < a say a - b > 0, and a + /// member of the primes, the positive or the non-negative whole numbers is at least 2, 1 + /// or 0. The expression is positive where it is such a quantity plus a constant that is + /// not negative, or plus a positive one where the bound is not strict: p - 1 for a + /// prime p is p - 2 plus 1. + /// + private static bool IsPositive(Entity expression) + { + if (expression is Real number) + return number.IsPositive; + if (!MentionsARenamedName(expression)) + return false; + foreach (var fact in InScope()) + { + var bound = fact switch + { + Lessf(var smaller, var greater) => (Difference: greater - smaller, Strict: true), + Greaterf(var greater, var smaller) => (greater - smaller, true), + LessOrEqualf(var smaller, var greater) => (greater - smaller, false), + GreaterOrEqualf(var greater, var smaller) => (greater - smaller, false), + Inf(var member, SpecialSet.Primes) => (member - 2, false), + Inf(var member, SpecialSet.PositiveIntegers) => (member - 1, false), + Inf(var member, SpecialSet.NonNegativeIntegers) => (member, false), + _ => ((Entity Difference, bool Strict)?)null + }; + if (bound is var (difference, strict) && Gap(expression, difference) is { } gap + && (strict ? gap.Sign >= 0 : gap.Sign > 0)) + return true; + } + return false; + } + + /// + /// The constant a - b, where the two differ by one as polynomials, and + /// otherwise. + /// + private static ERational? Gap(Entity a, Entity b) + { + var difference = a - b; + var names = difference.Vars.Distinct().ToArray(); + if (names.Length > MultivariatePolynomial.MaxVariables) + return null; + var indices = new Dictionary(); + for (var i = 0; i < names.Length; i++) + indices[names[i]] = i; + if (MultivariatePolynomial.TryParse(difference, indices) is not { IsConstant: true } constant) + return null; + return constant.IsZero ? ERational.Zero : constant.Terms.Single().Value; + } + } +} diff --git a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs index 23c841e0e..4a1cd37d5 100644 --- a/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs +++ b/Sources/AngouriMath/Functions/Evaluation/Evaluation.Discrete/Evaluation.Discrete.Classes.cs @@ -406,6 +406,11 @@ protected override Entity InnerSimplify(bool isExact) => dividend.EInteger.IsZero ? True : False, (Integer divisor, Integer dividend) => dividend.EInteger.Remainder(divisor.EInteger).IsZero ? True : False, + // A prime p divides binomial(p, k) for a whole k with 0 < k < p, where the + // quantifiers around establish those facts. Sullivan and Mackey's Prob 8.9.24. + // https://github.com/asc-community/AngouriMath/issues/1409 + (_, Binomialf(var upper, var lower)) when a == upper + && Functions.Boolean.QuantifierFacts.PrimeDividesItsBinomial(a, lower) => True, (Number, Number) => MathS.NaN, _ => null }, @@ -487,6 +492,11 @@ partial record Quantifier protected override Entity InnerSimplify(bool isExact) { var over = Over.InnerSimplified(isExact); + // A body in which a rule reads what the quantifiers establish, that p is prime + // or that 0 < k < p, is decided with those facts in scope. + // https://github.com/asc-community/AngouriMath/issues/1409 + if (Functions.Boolean.QuantifierFacts.Decide(Kind, Var, over, Body, isExact) is var (verdict, decided)) + return verdict ?? New(Var, over, decided); var body = Body.InnerSimplified(isExact); return Functions.Boolean.Quantifiers.Decide(Kind, Var, over, body, isExact) ?? New(Var, over, body); } diff --git a/Sources/Tests/UnitTests/Core/ProofRecordingTest.cs b/Sources/Tests/UnitTests/Core/ProofRecordingTest.cs index 8382b388a..99cf9023a 100644 --- a/Sources/Tests/UnitTests/Core/ProofRecordingTest.cs +++ b/Sources/Tests/UnitTests/Core/ProofRecordingTest.cs @@ -83,6 +83,21 @@ public void ACutSetIsShiftedAndTheInductionBelowIt() Assert.Contains(steps, step => step.Depth == 2 && step.Rule.Contains("base case")); } + [Fact] + public void AFactTheQuantifiersEstablishIsReadUnderThem() + { + var (verdict, steps) = Prove("forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)"); + Assert.Equal(Entity.Boolean.True, verdict); + Assert.Equal(new[] { 2, 1, 0 }, steps.Select(step => step.Depth)); + Assert.Equal("Nat.Prime.dvd_choose_self", steps[0].Lemma); + Assert.Equal("p divides binomial(p, k)".ToEntity(), steps[0].Statement); + Assert.Equal("intro", steps[1].Lemma); + // Written as the statement was, under p and k, and not the names the decision + // renamed them to while the facts were in scope. + Assert.Equal("forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)".ToEntity(), steps[2].Statement); + Assert.All(steps, step => Assert.DoesNotContain("'", step.Rule)); + } + [Fact] public void WhatWasTriedAndAbandonedIsNotAStep() { diff --git a/Sources/Tests/UnitTests/Core/QuantifierTest.cs b/Sources/Tests/UnitTests/Core/QuantifierTest.cs index c33de302e..21a18dca7 100644 --- a/Sources/Tests/UnitTests/Core/QuantifierTest.cs +++ b/Sources/Tests/UnitTests/Core/QuantifierTest.cs @@ -91,6 +91,23 @@ public void DecidedOverAFiniteSet(string statement, string expected) [InlineData("exists! k in ZZ : (0 < k and k < 7) and 3 divides k and 2 divides k", "True")] [InlineData("forall k in ZZ : (0 < k and k < 7 and 2 divides k) implies 3 divides binomial(7, k) - 1", "False")] [InlineData("forall n in ZZ : n >= 5 implies 2^n > n^2", "True")] + // Prob 8.9.24 for every prime: that p is prime and 0 < k < p is established by the + // quantifiers around the claim, in either order and with the hypothesis curried, and the + // rule for p divides binomial(p, k) reads it. Without the primality, or without either + // bound, it fails. An inner quantifier that binds p again hides what the outer one + // established about it. + [InlineData("forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)", "True")] + [InlineData("forall k in ZZ : forall p in PP : (0 < k and k < p) implies p divides binomial(p, k)", "True")] + [InlineData("forall p in PP : forall k in ZZ : 0 < k implies (k < p implies p divides binomial(p, k))", "True")] + [InlineData("forall p in PP : forall k in ZZ+ : k < p implies p divides binomial(p, k)", "True")] + [InlineData("forall p in PP : forall k in ZZ : (1 <= k and k <= p - 1) implies p divides binomial(p, k)", "True")] + [InlineData("forall p in PP : p divides binomial(p, 1)", "True")] + // Not for k = p: binomial(2, 2) = 1, which 2 does not divide. + [InlineData("forall p in PP : p divides binomial(p, 2)", "False")] + [InlineData("forall p in ZZ+ : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)", "False")] + [InlineData("forall p in PP : forall k in ZZ : k < p implies p divides binomial(p, k)", "False")] + [InlineData("forall p in PP : forall k in ZZ : (0 < k and k <= p) implies p divides binomial(p, k)", "False")] + [InlineData("forall p in PP : forall p in ZZ+ : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)", "False")] // The set may be an interval, a set builder, or a special set with no member of its own. [InlineData("forall x in (0; 1) : x^2 < 1", "True")] [InlineData("forall x in [0; 1] : x^2 < 1", "False")] @@ -128,6 +145,27 @@ public void DecidedOverAnInfiniteSet(string statement, string expected) public void LeftAsWrittenWhereNothingDecidesIt(string statement) => Assert.Equal(statement.ToEntity(), statement.ToEntity().Simplify()); + [Fact] + public void AWholeNumberIsNotAssumedOfAReal() + // binomial(p, k) of a real k is not a whole number, so the rule for divisibility has + // nothing to read, and the statement is not decided. + => Assert.IsType("forall p in PP : forall k in RR : (0 < k and k < p) implies p divides binomial(p, k)".ToEntity().Simplify()); + + [Fact] + public void WhatTheQuantifiersEstablishDoesNotLeaveThem() + { + // One node, shared with the caller, that is True inside the statement only because the + // quantifiers around it establish that p is prime and 0 < k < p. Outside them it is + // not decided, after the statement has been decided as before. + var claim = MathS.FromString("p divides binomial(p, k)", useCache: false); + var statement = MathS.ForAll("p", "PP", MathS.ForAll("k", "ZZ", MathS.FromString("0 < k and k < p", useCache: false).Implies(claim))); + Assert.Equal(Entity.Boolean.True, statement.Evaled); + Assert.Equal(Entity.Boolean.True, statement.Simplify()); + Assert.IsType(claim.Evaled); + Assert.IsType(claim.InnerSimplified); + Assert.IsType(claim.Simplify()); + } + [Theory] [InlineData("forall x in RR : x^2 >= 0", "forall x in RR : x ^ 2 >= 0")] [InlineData("∀ x in RR : x^2 >= 0", "forall x in RR : x ^ 2 >= 0")]