You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
We today have the scalar_eq_nf tactic to reason about some non-linear arithmetic goals, typically of the shape:
c_0 * a_0 ^ n_0 ... + c_n * a_n ^ n_n = ...
(see the proofs about the big num functions in the tutorial)
Issue 1: properly normalize equalities
Under the hood, scalar_eq_nf calls ring_nf, the tactic to normalize semiring expressions, but it does slightly more because of the following problem. If we have an equality whose both sides are simplified to the same expression thanks to ring_nf, then ring_nf simplifies the equality to true. However, if they are not equal, ring_nf simply normalizes the two sides. For instance, if the goal is:
a + a + 3 * b + c + d = a + 2 * b + 2 * c + d
then ring_nf simplifies it to:
2 * a + 3 * b + c + d = a + 2 * b + 2 * c + d
What we would rather have (especially for big expressions) is (we count the coefficients on each side and eliminate terms whenever possible):
a + b = c
For this reason, scalar_eq_nf first applies the rewriting: a = b <-> a - b = 0 so that we actually get:
a + b - c = 0
This is far better than the default behavior of ring_nf but still not exactly what we want, and can be confusing at times.
Issue 2: boost the simplification
Because scalar_eq_nf (and also scalar_nf) simply call ring_nf they inherit its limitations, meaning it can not simplify expressions which often appear and that the user expects to get simplified.
For instance, if we write (where n is a natural number): 2 ^ n = 2 * 2 ^ (n - 1) then it will not simplify.
As a result, we have to do this kind of manipulations:
have : 2 ^ (i * 32) = (2 ^ ((i - 1) * 32) * 4294967296 : Int) := by
Doing this is not completely trivial, because we have to prove that n = (n - 1) + 1 typically by using scalar_tac (note that this equality is not true if n = 0, because then n - 1 = 0 - we are working with natural numbers), then do exactly the rewriting we want (on the 2 ^ n expression, but not the other ones). Also, identifying for which n we need to do that is not trivial (let's say the goal is: 2 ^ n + 4 ^ m = 2 * 2 ^ (n - 1) + 8 ^ (k - 1), we should do something with n but not with k - we'll have to prove that 4 ^ m = 8 ^(k - 1) by other means). But I believe this kind of issues will be recurrent enough to be worth investigating.
The text was updated successfully, but these errors were encountered:
We today have the
scalar_eq_nf
tactic to reason about some non-linear arithmetic goals, typically of the shape:(see the proofs about the big num functions in the tutorial)
Issue 1: properly normalize equalities
Under the hood,
scalar_eq_nf
callsring_nf
, the tactic to normalize semiring expressions, but it does slightly more because of the following problem. If we have an equality whose both sides are simplified to the same expression thanks toring_nf
, thenring_nf
simplifies the equality totrue
. However, if they are not equal,ring_nf
simply normalizes the two sides. For instance, if the goal is:then
ring_nf
simplifies it to:What we would rather have (especially for big expressions) is (we count the coefficients on each side and eliminate terms whenever possible):
For this reason,
scalar_eq_nf
first applies the rewriting:a = b <-> a - b = 0
so that we actually get:This is far better than the default behavior of
ring_nf
but still not exactly what we want, and can be confusing at times.Issue 2: boost the simplification
Because
scalar_eq_nf
(and alsoscalar_nf
) simply callring_nf
they inherit its limitations, meaning it can not simplify expressions which often appear and that the user expects to get simplified.For instance, if we write (where
n
is a natural number):2 ^ n = 2 * 2 ^ (n - 1)
then it will not simplify.As a result, we have to do this kind of manipulations:
aeneas/tests/lean/Tutorial/Solutions.lean
Line 490 in b1ca1ff
Doing this is not completely trivial, because we have to prove that
n = (n - 1) + 1
typically by usingscalar_tac
(note that this equality is not true ifn = 0
, because thenn - 1 = 0
- we are working with natural numbers), then do exactly the rewriting we want (on the2 ^ n
expression, but not the other ones). Also, identifying for whichn
we need to do that is not trivial (let's say the goal is:2 ^ n + 4 ^ m = 2 * 2 ^ (n - 1) + 8 ^ (k - 1)
, we should do something withn
but not withk
- we'll have to prove that4 ^ m = 8 ^(k - 1)
by other means). But I believe this kind of issues will be recurrent enough to be worth investigating.The text was updated successfully, but these errors were encountered: