The current `ToExpr Int` instance produces `@Int.ofNat (@OfNat.ofNat Nat
i ...)` for nonnegative `i` and `@Int.negSucc (@OfNat.ofNat Nat (-i+1)
...)` for negative `i`.
However it should be producing `@OfNat.ofNat Int i ...` for nonnegative
`i`, and `@Neg.neg ... (@OfNat.ofNat Int (-i) ...)` for negative `i`.
This is very helpful when dealing with bitvectors, where a case analysis
on the bitwidth leaves one with hypotheses of the form `x<2^(Nat.succ
w)`.
Design decisions I am unsure about:
- Is creating a helper `succ?` the correct way to match on the exponent
`e+1`?
- I'm not certain why the prior call to `Int.ofNat_pow` also checked
that the exponent was a ground natural. I removed this, since we now
explicitly handle cases where the exponent is a term of the form `e+1`.
---------
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Joe Hendrix <joe@lean-fro.org>
Co-authored-by: Alex Keizer <alex@keizer.dev>
This PR is an effort to improve reasoning at the Nat level about
bitvectors and reduce of Fin and Nat.
It slightly tightens some proofs, but is generally aimed at reducing
inconsistencies between definitions at the Nat and Fin types in favor of
more consistently using Nat operations.
This ports leanprover/std4#664 to Lean core.
Here was the rational I provided in the discussion for
leanprover/std4#664:
It's mostly about consistency. If we use the same types and style in
definitions and proofs, there is less surprise when unfolding or
otherwise using definitions. We use some Nat based operations that
haven't been extended to Fin such as the bitwise operations, and I don't
want to pay the overhead of introducing a Fin version of every Bitvector
operation.
So this basically means Nat is preferred.
One argument potentially in favor of Fin is that we could reuse results
proven there, but that doesn't really seem to be the case so far.
A second argument is that we want to simplify expression to use more
canonical forms and we currently can pretty-print those operations
better using ofNat than ofFin. We could define the notations using ofFin
of course though, but that's additional operators that will show up in
expressions.
Adds a simple error-recovery mechanism to Lean's parser, similar to
those used in other combinator parsing libraries.
Lean itself isn't very amenable to error recovery with this mechanism,
as it requires global knowledge of the grammar in question to write
recovery rules that don't break backtracking or `<|>`. I only found a
few opportunities.
But for DSLs, this is really important. In particular, Verso parse
errors interacted very badly with Lean parse errors in a way that
required frequent "restart file" commands, but this mechanism allows me
to both recover from Verso parse errors and to have Lean skip the rest
of the file rather than repeatedly trying to parse it as Lean commands.
This is a quite substantial tactic.
It also includes the infamour `NatCast` typeclass (which I've equipped
with a module-doc). I wasn't at all sure where that should live, so it
is currently randomly in `Lean/Elan/Tactic/NatCast.lean`: presumably if
we're doing this it will go somewhere in `Init`.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
When updating Std, be careful that not every lemma has been upstreamed,
so we need to be careful to only delete things that have already been
declared.
Before the `zeta` / `zetaDelta` split, `dsimp` was performing `zeta`
by going inside of a `let`-expression, performing `zetaDelta`, and
then removing the unused `let`-expression.
Loose fvars are never supposed to be pretty printed, but having them
print with "fvar" in the name can help with debugging broken tactics and
elaborators.
Metaprogramming users often do not realize at first that `_uniq.???` in
pretty printing output refers to fvars not in the current local context.
