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")]