Leonardo de Moura
436d7befa5
fix: dsimp should reduce kernel projections ( #3607 )
...
closes #3395
2024-03-05 14:56:27 +00:00
Leonardo de Moura
414f0eb19b
fix: bug at Result.mkEqSymm ( #3606 )
...
`cache` and `dischargeDepth` fields were being reset.
2024-03-05 14:37:09 +00:00
Leonardo de Moura
bba4ef3728
feat: simprocs for folding numeric literals ( #3586 )
...
This PR folds exposed `BitVec` (`Fin`, `UInt??`, and `Int`) ground
literals.
cc @shigoel
2024-03-04 02:51:04 +00:00
Leonardo de Moura
c66c5bb45b
fix: simp? suggests generated equations lemma names ( #3573 )
...
closes #3547
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
2024-03-02 23:59:35 +00:00
Leonardo de Moura
8b2710c8b3
chore: use let_expr to cleanup code
2024-03-02 10:07:15 -08:00
Leonardo de Moura
a23292f049
feat: add option tactic.skipAssignedInstances := true for backward compatibilty ( #3526 )
...
When using `set_option tactic.skipAssignedInstances false`, `simp` and
`rw` will synthesize instance implicit arguments even if they have
assigned by unification. If the synthesized argument does not match the
assigned one the rewrite is not performed. This option has been added
for backward compatibility.
2024-02-28 05:52:29 +00:00
Leonardo de Moura
86ca8e32c6
feat: improve simp discharge trace messages ( #3523 )
2024-02-28 04:39:57 +00:00
Leonardo de Moura
855fbed024
fix: regression on match expressions with builtin literals ( #3521 )
2024-02-27 18:49:44 +00:00
Leonardo de Moura
5e101cf983
feat: use attribute command to add and erase simprocs ( #3511 )
2024-02-26 23:41:49 +00:00
Leonardo de Moura
bb0695b017
fix: simp? should track unfolded let-decls ( #3510 )
...
closes #3501
2024-02-26 20:49:24 +00:00
Leonardo de Moura
f0b4902f7a
fix: simp should not try to synthesize instance implicit arguments that have been inferred by unification ( #3507 )
2024-02-26 20:17:55 +00:00
Leonardo de Moura
6d569aa7b5
refactor: use LitValue.lean to implement simprocs
2024-02-24 16:08:07 -08:00
Leonardo de Moura
5b15e1a9f3
fix: disable USize simprocs ( #3488 )
2024-02-24 02:37:39 +00:00
Leonardo de Moura
2defc58159
chore: rename isNatLit => isRawNatLit
...
Motivation: consistency with `mkRawNatLit`
2024-02-23 15:16:12 -08:00
Leonardo de Moura
4d4b79757d
chore: move BitVec to top level namespace
...
Motivation: `Nat`, `Int`, `Fin`, `UInt??` are already in the top level
namespace. We will eventually define `UInt??` and `Int??` using `BitVec`.
2024-02-23 15:15:57 -08:00
Sebastian Ullrich
8bf9d398af
chore: CI: flag Lean modules not using prelude ( #3463 )
...
Co-authored-by: Henrik Böving <hargonix@gmail.com>
2024-02-23 08:06:55 +00:00
Leonardo de Moura
53146db620
fix: zetaDelta := false regression ( #3459 )
...
See new test. It is a mwe for an issue blocking Mathlib.
2024-02-22 19:10:02 +00:00
Leonardo de Moura
ddd6342737
fix: support for Fin and BitVec literal normalization ( #3443 )
2024-02-21 19:05:47 +00:00
Leonardo de Moura
d55bab41bb
feat: Int.toNat simproc ( #3440 )
2024-02-21 17:12:14 +00:00
Scott Morrison
35e374350c
chore: upstream norm_cast tactic ( #3322 )
...
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>
2024-02-19 17:49:17 -08:00
Leonardo de Moura
489f2da711
feat: add simproc for BitVec.signExtend ( #3409 )
2024-02-19 15:15:37 -08:00
Leonardo de Moura
5d9552d66c
feat: simprocs for BitVec ( #3407 )
2024-02-19 14:01:00 -08:00
Leonardo de Moura
90b5a0011d
feat: assume function application arguments occurring in local simp theorems have been annotated with no_index ( #3406 )
...
closes #2670
2024-02-19 12:43:34 -08:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08:00
Leonardo de Moura
cd9648a61e
fix: dsimp zeta bug
...
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.
2024-02-18 14:14:55 -08:00
Leonardo de Moura
9fe72c5f95
chore: set zetaDelta := false by default in the simplifier
2024-02-18 14:14:55 -08:00
Leonardo de Moura
457d33d660
feat: configuration options zeta and zetaDelta
...
TODO: bootstrapping issues, set `zetaDelta := false` in the simplifier.
2024-02-18 14:14:55 -08:00
Leonardo de Moura
c8236ccd47
chore: basic simprocs for String
2024-02-17 17:51:24 -08:00
Leonardo de Moura
559a18874c
chore: simprocs for Eq
2024-02-17 17:51:24 -08:00
Leonardo de Moura
3dcc8cab3e
feat: simprocs for Char.val, default char, and Char.ofNatAux
2024-02-17 17:51:24 -08:00
Leonardo de Moura
fb18ef3688
feat: simprocs for UInt??.ofNatCore and UInt??.toNat
2024-02-17 17:51:24 -08:00
Leonardo de Moura
3e5695e07e
feat: simprocs for Char ( #3382 )
2024-02-17 20:36:51 +00:00
Sebastian Ullrich
dda88c9926
feat: infoview.maxTraceChildren ( #3370 )
...
Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.
2024-02-17 14:04:46 +00:00
Leonardo de Moura
baa9fe5932
fix: simp gets stuck on autoParam ( #3315 )
...
closes #2862
2024-02-17 13:42:19 +00:00
Leonardo de Moura
678797b67b
fix: simp fails to discharge autoParam premises even when it can reduce them to True ( #3314 )
...
closes #3257
2024-02-17 13:41:48 +00:00
Eric Wieser
0554ab39aa
doc: Add a docstring to Simp.Result and its fields ( #3319 )
2024-02-13 13:57:24 +00:00
Leonardo de Moura
760e824b9f
fix: we should not crash when simp loops ( #3269 )
...
see #3267
2024-02-07 02:30:28 +00:00
Leonardo de Moura
cf092e7941
refactor: add helper function evalPropStep ( #3252 )
2024-02-04 21:50:34 +00:00
Leonardo de Moura
a4226a4f6d
fix: tolerate missing simp and simproc sets
...
When we declare a `simp` set using `register_simp_attr`, we
automatically create `simproc` set. However, users may create `simp`
sets programmatically, and the associated `simproc` set may be missing
and vice-versa.
2024-02-01 16:58:54 +11:00
Leonardo de Moura
76224e409b
fix: Mathlib regressions reported by Scott
2024-02-01 16:58:54 +11:00
Leonardo de Moura
c3383de6ff
feat: add helper method withDischarger
2024-02-01 16:58:54 +11:00
Leonardo de Moura
da072c2ec8
fix: simp cache issue
2024-02-01 16:58:54 +11:00
Leonardo de Moura
d3c71ce2ff
refactor: remove unfoldGround and cacheGround workarounds from simp
2024-02-01 16:58:54 +11:00
Leonardo de Moura
168217b2bd
chore: remove TODOs
2024-02-01 16:58:54 +11:00
Leonardo de Moura
8deb1838aa
feat: add seval
2024-02-01 16:58:54 +11:00
Leonardo de Moura
3d1b3c6b44
chore: getSimpCongrTheorems to CoreM
2024-02-01 16:58:54 +11:00
Leonardo de Moura
676121c71d
chore: style
2024-02-01 16:58:54 +11:00
Leonardo de Moura
6439d93389
chore: remove dead code
2024-02-01 16:58:54 +11:00
Leonardo de Moura
01469bdbd6
refactor: remove workaround
...
We don't need to keep passing `discharge?` method around anymore.
2024-02-01 16:58:54 +11:00
Leonardo de Moura
01750e2139
chore: mark simprocs that are relevant for the symbolic evaluator
2024-02-01 16:58:54 +11:00
