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

240 commits

Author SHA1 Message Date
Leonardo de Moura
3cf425ba52 fix: pattern hover information 
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
 2022-04-08 15:03:42 -07:00
Leonardo de Moura
ea682830d1 refactor: change addTermInfo type 2022-04-08 15:01:57 -07:00
Leonardo de Moura
099fba43d3 chore: remove trace[Meta.debug] leftovers 2022-04-08 06:49:09 -07:00
Leonardo de Moura
de2e2447d2 chore: style 2022-04-07 17:35:05 -07:00
Leonardo de Moura
a926cd1698 fix: mkUnfoldProof 
The hypotheses in an equation theorem may depend on each other
 2022-04-01 15:47:24 -07:00
Leonardo de Moura
096e4eb6d0 fix: equation generation for nested recursive definitions 
The issue was raised on Zulip. The issue is triggered in
declarations containing overlapping patterns and nested recursive
definitions occurring as the discriminant of `match`-expressions.
Recall that Lean 4 generates conditional equations for declarations
containing overlapping patterns.
To address the issue we had to "fold" `WellFounded.fix` applications
back as recursive applications of the functions being defined.

The new test exposes the issue.
 2022-03-31 17:04:06 -07:00
Leonardo de Moura
d21e62ecb7 refactor: custom simpMatch for WF module 
It is just the skeleton right now.
 2022-03-31 14:51:07 -07:00
Leonardo de Moura
1ab57d4fd4 feat: store fixedPrefixSize at WF.EqnInfo 2022-03-31 14:47:52 -07:00
Leonardo de Moura
23f3de5061 chore: proper trace message class 2022-03-31 11:04:42 -07:00
Leonardo de Moura
d1e4712038 fix: smart unfolding 
See new comment to understand the issue.

closes #1081
 2022-03-29 15:49:14 -07:00
Leonardo de Moura
a8bb7fab93 fix: typo at findRecArg 
The code was not traversing the indices if the datatype has parameters
 2022-03-29 12:12:43 -07:00
Leonardo de Moura
a2e467eb32 fix: mkEqnTypes 
stop as soon as `lhs` and `rhs` are definitionally equal, and avoid
unnecessary case analysis.

This commit fixes the last issue exposed by #1074

fixes #1074
 2022-03-25 19:13:21 -07:00
Leonardo de Moura
c95d5f25a3 feat: convert ites into dites in the WF module 
Motivation: the condition is often used in termination proofs.
 2022-03-19 10:11:50 -07:00
Leonardo de Moura
36d955e8cc feat: use simpler encoding for nonmutually recursive definitions 2022-03-19 09:43:18 -07:00
Leonardo de Moura
c7cdbf8ff8 feat: improve auto generated termination_by a bit 2022-03-19 09:28:19 -07:00
Leonardo de Moura
184b0b8e8d feat: improve "result types must be in the same universe level" error message 
The new error message makes it clear why the definition is not accepted.

See issue #1050
 2022-03-17 07:41:37 -07:00
Leonardo de Moura
b8a4f3a7a3 perf: quick filter for simpMatch when proving equation theorems 2022-03-15 15:53:29 -07:00
Leonardo de Moura
d2dc38fdb6 perf: use HasConstCache to minimize the number of visited terms at Structural and WF 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2022-03-15 08:40:47 -07:00
Leonardo de Moura
eccd5c11c9 perf: removeUnusedEqnHypotheses 2022-03-15 06:53:43 -07:00
Leonardo de Moura
c3c0b8b8a2 chore: remove unnecessary code 2022-03-15 05:26:33 -07:00
Leonardo de Moura
eb7539ef77 fix: mkEqnTypes overapplied lhs in equational theorems 
This issue was exposed by the "Dependent de Bruijn indices" from CPDT.
 2022-03-14 17:42:21 -07:00
Leonardo de Moura
2ac9cfb7b1 fix: eta expand partial applications of recursive function being defined 2022-03-14 10:05:33 -07:00
Leonardo de Moura
fa0964c07e fix: preserve variable name at WF decreasing goals when function has only one non fixed argument 2022-03-13 13:20:07 -07:00
Leonardo de Moura
7af09ac009 refactor: move equation theorem cache to Meta/Eqns.lean 2022-03-12 15:34:32 -08:00
Leonardo de Moura
7d5da95434 fix: remove unused hypotheses from conditional equation theorems 2022-03-11 14:10:57 -08:00
Leonardo de Moura
54b74796f6 feat: use tryContradiction at mkUnfoldProof 2022-03-11 12:52:15 -08:00
Leonardo de Moura
272dd5533f chore: style use · instead of . for lambda dot notation 
We are considering removing `.` as an alternative for `·` in the
lambda dot notation (e.g., `(·+·)`).
Reasons:
- `.` is not a perfect replacement for `·` (e.g., `(·.insert ·)`)
- `.` is too overloaded: `(f.x)` and `(f .x)` and `(f . x)`. We want to keep the first two.
 2022-03-11 07:49:03 -08:00
Leonardo de Moura
b745c4f51a fix: recursive overapplication at WF/Fix.lean 2022-03-03 18:13:34 -08:00
Leonardo de Moura
043d338271 feat: add getForbiddenByTrivialSizeOf 2022-03-03 11:12:32 -08:00
Leonardo de Moura
1155d52702 chore: update TODO comment 2022-03-02 12:51:46 -08:00
Leonardo de Moura
093ab49b7f feat: improve generateElements a bit 2022-03-02 11:58:47 -08:00
Leonardo de Moura
52403fca83 feat: add support for guessing (very) simple WF relations 
There are a lot of TODOs, but it is already useful for simple cases.

closes #847
 2022-03-02 11:52:00 -08:00
Leonardo de Moura
99204d2226 refactor: modify elabWFRel to CPS 2022-03-02 11:52:00 -08:00
Leonardo de Moura
1e205d635e fix: bug at wfRecursion 
"After compilation" attributes were being applied to soon when we did
not need to generate auxiliary functions.
 2022-03-01 17:48:06 -08:00
Leonardo de Moura
c5baf759e2 fix: we must use addAsAxiom before getFixedPrefix 
`getFixedPrefix` uses `isDefEq`, and it will fail if it needs to
retrieve the type of one of the recursive function being defined.
 2022-02-27 09:01:52 -08:00
Leonardo de Moura
2961e9cbf0 fix: heuristic for deciding which additional propositions must be included in equality theorems 2022-02-24 17:17:07 -08:00
Leonardo de Moura
bd3ad35a1c fix: we may get False in unreachable branches 2022-02-24 15:24:07 -08:00
Leonardo de Moura
52b53ab7a2 fix: heuristic for generating equation theorem types 
closes #1026
 2022-02-23 13:10:30 -08:00
Leonardo de Moura
dbe9bf61c5 fix: unfold auxiliary theorems created by decreasing_tactic 2022-02-23 09:02:23 -08:00
Leonardo de Moura
c9f8ec71df fix: invalid rewrite when proving equation theorems for declaration using well-founded recursion 2022-02-22 16:38:51 -08:00
Leonardo de Moura
e61d0be561 feat: isolate fixed prefix at well-founded recursion 
closes #1017
 2022-02-18 10:40:32 -08:00
Leonardo de Moura
75e771b6e8 feat: add support for fixed argument prefix at mkFix and elabWFRel 
This is needed for #1017

TODO: `addNonRecPreDefs` and equation theorems
 2022-02-18 07:59:32 -08:00
Leonardo de Moura
70312191f7 feat: make sure packDomain and packMutual ignore the fixed arguments 
TODO: adapt `elabWFRel`, `mkFix`, and etc.

This is needed for #1017
 2022-02-17 17:43:06 -08:00
Leonardo de Moura
9ee529e5ce fix: use PSum instead of Sum when using well-founded recursion 
See new test for example that did not work with `Sum` because type
alpha was `Sort u`.
 2022-02-17 16:14:34 -08:00
Leonardo de Moura
4a0ae8326c feat: compute the fixed prefix size for mutually recursive definitions 2022-02-17 14:12:05 -08:00
Leonardo de Moura
e1d9dc4b38 feat: store noncomputable declarations 2022-02-16 13:33:02 -08:00
Leonardo de Moura
d1e5e4166a feat: use sorry instead of trying to synthesize Inhabited at error recovery 2022-02-15 09:15:18 -08:00
Leonardo de Moura
f75fdcb19b feat: when Lean cannot prove termination, then report error and add definition as partial, and if it fails add as axiom 2022-02-15 07:44:27 -08:00
Leonardo de Moura
e8c23cdf7e feat: add cache at Lean/Elab/PreDefinition/WF/PackDomain.lean 2022-02-11 09:52:14 -08:00
Leonardo de Moura
123e0f42e9 feat: support partial and over applications at WF/PackDomain.lean 
closes #1013
 2022-02-11 09:28:17 -08:00