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

4065 commits

Author SHA1 Message Date
Leonardo de Moura
9fe0d28107 fix: do not split on if-then-else terms when generating equation theorems 
Reason: avoid unnecessary case-analysis explosion
It is also unnecessary since we only refine the `below` and `F`
arguments over `match`-expressions.

This fixes the last case at issue #998
```
attribute [simp] BinaryHeap.heapifyDown
```

closes #998
 2022-02-09 17:43:35 -08:00
Leonardo de Moura
c685a2d9ed feat: add splitIte flag to splitTarget? tactic 2022-02-09 17:38:04 -08:00
Leonardo de Moura
7fc12014da fix: make sure splitTarget? skips match expressions that produce type errors at splitMatch 
We can now generate the equation theorem for
```
attribute [simp] Array.heapSort.loop
```

see #998
 2022-02-09 17:07:10 -08:00
Leonardo de Moura
e574c5373f feat: improve delta? method 
Use zeta reduction to create new opportunities of beta-reduction.

This issue fixes on the problems that were affecting the generation of
equation theorems for `Array.heapSort.loop` (see issue: #998).
After this fix, the equation theorem generation fails at `splitMatch`.
 2022-02-09 13:31:55 -08:00
Leonardo de Moura
8fbe7062fa fix: preserve unused let-decls at Meta.transform 2022-02-09 10:13:52 -08:00
Leonardo de Moura
3b67c7db81 fix: handling of letrec declarations in the well-founded recursion module 2022-02-09 10:13:52 -08:00
Leonardo de Moura
471ef75345 feat: improve test at packDomain 2022-02-09 10:13:52 -08:00
Leonardo de Moura
e66575d4fc refactor: move and generalize ensureNoRecFn 2022-02-09 10:13:52 -08:00
Leonardo de Moura
1cfe403edf chore: style 2022-02-09 10:13:52 -08:00
Leonardo de Moura
2ef0146140 fix: avoid unnecessary matcheApp.addArgs at BRecOn and Fix 
It fixes the following two cases from #998
```
attribute [simp] Lean.Export.exportName
attribute [simp] Lean.Export.exportLevel
```
 2022-02-08 15:06:14 -08:00
Leonardo de Moura
8692225432 fix: saveEqn at Lean/Elab/PreDefinition/Eqns.lean 
see #998
 2022-02-08 13:44:49 -08:00
Leonardo de Moura
33ed496661 feat: improve contradiction 2022-02-08 13:26:05 -08:00
Leonardo de Moura
3367f0b06a feat: use splitTarget? when proving equation theorems for recursive definitions 2022-02-08 12:53:09 -08:00
Leonardo de Moura
afb5cb16ee chore: simplify option names 
see #1011
 2022-02-08 12:23:24 -08:00
Leonardo de Moura
59acf01bc9 feat: relax auto-implicit restrictions 
The new options `relaxedAutoBoundImplicitLocal` can be used to
disable this feature.

closes #1011
 2022-02-08 12:17:42 -08:00
Leonardo de Moura
c486203481 fix: use simpTargetStar when proving equation theorems for recursive definitions 
Add `take` function reported at Zulip.
 2022-02-08 11:43:45 -08:00
Leonardo de Moura
c1777c17e3 feat: add simpTargetStar 2022-02-08 11:43:45 -08:00
Leonardo de Moura
824d0aa8a5 chore: remove leftover 2022-02-08 11:43:45 -08:00
Leonardo de Moura
a9bb646d4f chore: cleanup 2022-02-07 17:35:07 -08:00
Leonardo de Moura
8d7f0ea2f2 feat: add removeUnnecessaryCasts 
see #988
 2022-02-07 17:24:32 -08:00
Leonardo de Moura
9d34d9bc5a feat: cache and optimize mkCongrSimp? at simp 
see #988
 2022-02-07 17:01:21 -08:00
Leonardo de Moura
007f0e1d71 feat: use mkCongrSimp? at simp 
TODO: cache auto generated congr theorems, and `removeUnnecessaryCasts`

see #988
 2022-02-07 16:45:01 -08:00
Leonardo de Moura
93bd4a7f88 chore: lemma => thm 2022-02-07 13:55:23 -08:00
Leonardo de Moura
5baac1905f fix: use private names for theorems that are created on demand 
closes #1006
 2022-02-07 13:16:22 -08:00
Leonardo de Moura
eff63632b3 feat: improve error message when max heartbeats is reached during TC 
see #1007
 2022-02-07 11:23:48 -08:00
Gabriel Ebner
f8b43630a6 fix: refs to copied subobjects in diamond extension 2022-02-07 10:54:32 -08:00
Leonardo de Moura
9c2942c36d chore: "simp lemma" => "simp theorem" 2022-02-06 09:15:39 -08:00
Leonardo de Moura
d6dc077c86 refactor: CongrLemma => SimpCongrTheorem 2022-02-06 09:15:39 -08:00
Leonardo de Moura
96bae46045 refactor: SimpLemma => SimpTheorem 2022-02-06 09:15:39 -08:00
Sebastian Ullrich
2c7d67d498 fix: make info of fields synthesized by structure update synthetic 2022-02-06 08:50:07 -08:00
Joscha
196cf67eed fix: handle overlapping definitions 2022-02-06 16:52:18 +01:00
Leonardo de Moura
f78d355416 chore: style 2022-02-06 07:29:26 -08:00
Sebastian Ullrich
0ef5985b5f fix: binder info range for let rec/where 2022-02-06 07:21:51 -08:00
Leonardo de Moura
6de0b1fc67 feat: add mkCongrSimp.mkProof 
see #988
 2022-02-04 17:57:28 -08:00
Leonardo de Moura
3ae455bccf feat: add mkCongrSimp? 
TODO: proof is still missing

see #988
 2022-02-04 17:57:28 -08:00
Leonardo de Moura
a028a69159 feat: cache isProp and isDecInst at FunInfo 2022-02-04 17:57:28 -08:00
Sebastian Ullrich
a7ba103e0a chore: remove leanpkg 2022-02-04 19:03:40 +01:00
Sebastian Ullrich
ae062c6ead fix: match tactic should not trigger implicit lambdas 2022-02-04 07:55:56 -08:00
Mario Carneiro
6e7d76f4d8 fix: typo 2022-02-03 18:21:14 -08:00
Leonardo de Moura
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
Leonardo de Moura
e9d85f49e6 chore: remove tryPureCoe? 
Based on the discussion at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/for.2C.20unexpected.20need.20for.20type.20ascription/near/269083574
The consensus seemed to be that "auto pure" is more confusing than its worth.
 2022-02-03 16:25:24 -08:00
Leonardo de Moura
5f74cd4968 feat: add let pat := val | elseCase do-notation 2022-02-03 15:55:03 -08:00
Leonardo de Moura
420f5bb315 fix: hide internal namespaces from autocompletion 
closes #993
 2022-02-03 13:33:27 -08:00
Leonardo de Moura
17eab845ed fix: improve tryPostponeIfMVar 
see #992
 2022-02-03 13:24:19 -08:00
Sebastian Ullrich
22526051e0 fix: install sources to src/lean/, not lib/lean 
Not only is this more semantically appropriate (see e.g.
`/usr/src/{linux,rust,...}` on Debian), it also prevents .ilean files
from Lake tests (which are symlinked into the build directory as part of
`src/` during development) from ending up in the built-in LEAN_PATH and
being watched & loaded by the server.
 2022-02-03 18:20:21 +01:00
Gabriel Ebner
54cff10f3f fix: dependent fields in diamond extensions 2022-02-03 09:17:14 -08:00
Leonardo de Moura
c30380e2fa feat: lift the restriction in congr theorems that all function arguments on the lhs must be free variables 
see #988
 2022-02-02 18:23:18 -08:00
Leonardo de Moura
101fc12b54 feat: partially applied user congruence lemmas 
see #988
 2022-02-02 17:41:21 -08:00
Leonardo de Moura
dbb6dcd9a9 fix: remove irrelevant hypotheses in auto-generated equation theorems 2022-02-02 15:39:51 -08:00
Leonardo de Moura
188f0eb70f fix: splitMatch tactic 
Improve how we compute the motive for match-splitter eliminator.

closes #986
 2022-02-02 15:06:03 -08:00