max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
32565 commits 1 branch 0 tags 5.3 GiB
Commit graph

32565 commits

This branch
This branch
All branches
Author SHA1 Message Date
Scott Morrison
f48079eb90
chore: begin development cycle for v4.8.0 (#3596) 2024-03-05 02:15:37 +00:00
Joe Hendrix
01104cc81e
chore: bool and prop lemmas for Mathlib compatibility and improved confluence (#3508) 
This adds a number of lemmas for simplification of `Bool` and `Prop`
terms. It pulls lemmas from Mathlib and adds additional lemmas where
confluence or consistency suggested they are needed.

It has been tested against Mathlib using some automated test
infrastructure.

That testing module is not yet included in this PR, but will be included
as part of this.

Note. There are currently some comments saying the origin of the simp
rule. These will be removed prior to merging, but are added to clarify
where the rule came from during review.

---------

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
 2024-03-04 23:56:30 +00:00
Leonardo de Moura
37450d47e2
fix: bug at elimOptParam (#3595) 
`let_expr` uses `cleanupAnnotations` which consumes `optParam` type
annotations.

cc @nomeata
 2024-03-04 23:56:00 +00:00
Scott Morrison
e814fc859e
chore: cherry-picking v4.6.1 release notes (#3592) 2024-03-04 12:59:00 +00:00
Marc Huisinga
093e1cf22a
test: add language server startup benchmark (#3558) 
Benchmark to catch future regressions as the one fixed in #3552.
 2024-03-04 09:01:51 +00:00
Leonardo de Moura
e6d6855a85
chore: missing double backticks (#3587) 2024-03-04 03:02:35 +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
Scott Morrison
3ad078fec9
chore: updates to RELEASES.md (#3585) 2024-03-04 02:32:30 +00:00
Leonardo de Moura
8689a56a5d
feat: #print equations <decl-name> command (#3584) 2024-03-04 02:32:20 +00:00
Scott Morrison
870c6d0dc4
chore: replacing proofs in Init/Data/Nat/Bitwise/Lemmas with omega (#3576) 
Replaces some tedious proofs with `omega`, and take advantage of `omega`
powerups to remove some preparatory steps.
 2024-03-04 02:19:31 +00:00
Scott Morrison
ad901498fa
chore: add release notes for #3507 and #3509 (#3583) 2024-03-04 00:55:53 +00:00
Kyle Miller
acb1b09fbf
fix: expression tree elaborator for relations now localizes error messages to the LHS or RHS (#3442) 
Added `withRef` when processing the LHS or RHS. Without this, in an
expression such as `true = ()` the entire expression would be
highlighted with "type mismatch, `()` has type `Unit` but is expected to
have type `Bool`". Now the error is localized to `()`.

This behavior was pointed out [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/error.20location.20bug/near/422665805).
 2024-03-04 00:53:32 +00:00
Scott Morrison
791142a7ff
feat: Nat.mul_mod (#3582) 
Proves
`Nat.mod_mul : x % (a * b) = x % a + a * (x / a % b)` and
`Nat.mod_pow_succ : x % b ^ (k + 1) = x % b ^ k + b ^ k * ((x / b ^ k) %
b)`, helpful for bitblasting.
 2024-03-03 23:31:07 +00:00
Scott Morrison
015af6d108
chore: use match_expr in omega (#3577) 2024-03-03 22:22:28 +00:00
Kyle Miller
04385b7fb9
doc: small improvements to docstrings for let and have tactics (#3560) 2024-03-03 22:00:32 +00:00
Joachim Breitner
2510808ebf
chore: add unicode directory name to gitignore (#3565) 
fixes #3358

---------

Co-authored-by: Mac Malone <tydeu@hatpress.net>
 2024-03-03 20:19:17 +00:00
Leonardo de Moura
9f305fb31f
fix: rename_i in macro (#3581) 
closes #3553

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2024-03-03 19:05:37 +00:00
Sebastian Ullrich
380dd9e6e7 fix: free threadpool threads before process exit 2024-03-03 20:12:46 +01:00
Sebastian Ullrich
908b98dad8 fix: task_manager termination under Emscripten 2024-03-03 20:12:46 +01:00
Leonardo de Moura
a4d41beab1
perf: match_expr join points (#3580) 
We use `let_delayed` to elaborate `match_expr` join points, which
elaborate the body of the `let` before its value. Thus, there is a
difference between:
- `let_delayed f (x : Expr) := <val>; <body>`
- `let_delayed f := fun (x : Expr) => <val>; <body>`

In the latter, when `<body>` is elaborated, the elaborator does not know
that `f` takes an argument of type `Expr`, and that `f` is a function.
Before this commit ensures the former representation is used.
 2024-03-03 18:15:49 +00:00
Leonardo de Moura
95f28be088
fix: generalize excessive resource usage (#3575) 
closes #3524
 2024-03-03 17:58:11 +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
870de4322c
fix: missing atomic at match_expr parser (#3572) 2024-03-02 21:55:07 +00:00
Joachim Breitner
4fdc243179
refactor: simplify some nomatch with nofun (#3564) 
and also don’t wrap `nomatch` with `False.elim`; it is not necessary, as
`nomatch` already inhabits any type.
 2024-03-02 20:43:31 +00:00
Leonardo de Moura
8a3c9cafb9 chore: update stage0 2024-03-02 10:07:15 -08:00
Leonardo de Moura
826f0580a6 fix: propagate expected type at do-match_expr 2024-03-02 10:07:15 -08:00
Leonardo de Moura
0359ff753b chore: use __do_jp workaround, and "implementation detail" variables at match_expr macro 2024-03-02 10:07:15 -08:00
Leonardo de Moura
8b2710c8b3 chore: use let_expr to cleanup code 2024-03-02 10:07:15 -08:00
Leonardo de Moura
0199228784 chore: update stage0 2024-03-02 08:16:18 -08:00
Leonardo de Moura
17e498c11f feat: expand let_expr macros 2024-03-02 08:16:18 -08:00
Leonardo de Moura
54ff38aa5f chore: update stage0 2024-03-02 08:16:18 -08:00
Leonardo de Moura
ecfaf8f3e7 feat: add let_expr notation 2024-03-02 08:16:18 -08:00
Leonardo de Moura
3c0e575fe0 feat: add matchExprPat parser 2024-03-02 08:16:18 -08:00
Leonardo de Moura
49f41a6224 chore: update stage0 2024-03-01 22:33:14 -08:00
Leonardo de Moura
7a27b04d50 feat: monadic match_expr 2024-03-01 22:33:14 -08:00
Leonardo de Moura
f777e0cc85 feat: macro expander for match_expr terms 2024-03-01 22:33:14 -08:00
Leonardo de Moura
64adb0627a feat: add auxiliary functions for compiling match_expr 2024-03-01 22:33:14 -08:00
Leonardo de Moura
ea9a417371 chore: update stage0 2024-03-01 22:33:14 -08:00
Leonardo de Moura
70d9106644 feat: match_expr parsers 2024-03-01 22:33:14 -08:00
Marc Huisinga
9cf3fc50c7
doc: update RELEASES.md for #3552 (#3561) 2024-03-02 00:27:21 +00:00
Joe Hendrix
78726c936f
chore: add library_search and #check_tactic to 4.7 RELEASES.md (#3549) 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
 2024-03-02 00:13:08 +00:00
Marc Huisinga
7e944c1a30
fix: load references asynchronously (#3552) 
In v4.6.0, there was a significant regression in initial server startup
performance because the .ilean files got bigger in #3082 and we load the
information stored in all .ilean files synchronously when the server
starts up.

This PR makes this loading asynchronous. The trade-off is that requests
that are issued right after the initial server start when the references
are not fully loaded yet may yield incomplete results.

Benchmark for this in a separate PR soon after this one.

---------

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2024-03-01 13:57:52 +00:00
Scott Morrison
18306db396
chore: protect Int.add_right_inj et al (#3551) 
Reducing some name conflicts in Mathlib.
 2024-03-01 13:01:39 +00:00
Scott Morrison
570b50dddd
chore: correct statement of Int.pow_zero, and protected theorems (#3550) 2024-03-01 12:38:02 +00:00
David Thrane Christiansen
43d6eb144e
chore: add error recovery to RELEASES.md (#3540) 
Adds the missing RELEASES.md from #3413. Apologies for the oversight!
 2024-03-01 05:38:18 +00:00
Siddharth
ed02262941
feat: generalize msb_eq_decide to also handle the zero width case (#3480) 
Note that this is a strict generalization of the previous statemens of
`getLsb_last` and `msb_eq_decide` that worked for bitwidths `>= 1`.
 2024-02-29 22:46:32 +00:00
Joe Hendrix
c0dfe2e439
feat: BitVec int lemmas (#3474) 
This introduces lemma support for BitVec.ofInt/BitVec.toInt as well as
lemmas upstreamed from Std and Mathlib for reasoning about emod and
bmod.
 2024-02-29 20:48:57 +00:00
Sebastian Ullrich
61fba365f2
fix: revert shared library split on non-Windows platforms (#3529) 
Avoids the performance hit and fixes #3528.
 2024-02-29 19:15:01 +00:00
Marcus Rossel
0362fcea69
chore: remove redundant 'generalizing' (#3544) 2024-02-29 13:24:14 +00:00
Marcus Rossel
60d056ffdf
doc: fix typos (#3543) 
The doc comment on
[Lean.Meta.viewSubexpr](https://leanprover-community.github.io/mathlib4_docs/Lean/Meta/ExprLens.html#Lean.Meta.viewSubexpr)
also seems broken, but I don't know how to fix it.
 2024-02-29 13:23:19 +00:00