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

7374 commits

Author SHA1 Message Date
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
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
dedb6ee01b fix: skip value if type is computationally irrelevant 2022-02-17 10:41:16 -08:00
Xubai Wang
ca521e1188 feat: add position to mod doc 2022-02-16 13:50:19 -08:00
Leonardo de Moura
373a64ee09 test: for isNoncomputable 2022-02-16 13:37:49 -08:00
Leonardo de Moura
ad5099ec3c fix: mkLetRecClosureFor for nested let-recs 
closes #1020
 2022-02-16 12:44:02 -08:00
Leonardo de Moura
3f4d8f370a fix: backtrack InfoTree when backtracking at the discriminant refinement method 
This commit addresses issue described at https://github.com/leanprover/lean4/issues/1018#issuecomment-1040597212

closes #1018
 2022-02-15 16:01:09 -08:00
Leonardo de Moura
fd9165415e feat: try to preserve variable names during discriminant refinement 
This fixes second issue at #1018
 2022-02-15 15:54:03 -08:00
Leonardo de Moura
56cdacfc28 feat: allow synthetic holes to be used as patterns 
They are useful for getting meaningful pattern variable names when the hole
is not an inaccessible pattern. See new test.

We are going to use this feature to address issue 2 at #1018.
 2022-02-15 15:34:14 -08:00
Leonardo de Moura
df584567f5 feat: (generalizing := true) is the default behavior for match-expressions 
closes #1018
 2022-02-15 11:12:04 -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
66e0b72c6f test: notation for providing names to equality proofs in match expressions is not whitespace sensitivity anymore 2022-02-14 15:51:23 -08:00
Leonardo de Moura
764a1d9f51 chore: fix tests 2022-02-14 15:47:12 -08:00
Leonardo de Moura
93b5b74b36 feat: modify notation for providing motive in "match" expressions 2022-02-14 15:36:14 -08:00
Leonardo de Moura
07043e73b0 chore: fix tests 2022-02-14 12:06:03 -08:00
Leonardo de Moura
aa63fda835 fix: mark auxiliary noConfusion declarations for enumeration types as [reducible] 
closes #1016
 2022-02-14 12:03:49 -08:00
Leonardo de Moura
82bce7ebec fix: declare local instaces occurring in patterns 2022-02-12 12:01:08 -08:00
Leonardo de Moura
999e80745e test: add test for already fixed issue reported on Zulip 2022-02-12 07:53:31 -08:00
Leonardo de Moura
ab41dd0d83 test: add test for issue #1013 2022-02-11 09:28:46 -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
Sebastian Ullrich
80e2e1daa8 test: mutual block not needed 2022-02-11 16:22:13 +01:00
Leonardo de Moura
712d6726e4 feat: rename tactic byCases => by_cases 2022-02-10 17:11:07 -08:00
Sebastian Ullrich
894dc0e1b8 fix: pretty-printing match dependent on let 2022-02-10 10:19:04 +01:00
Leonardo de Moura
54473ad523 test: add missing test for issue #998 2022-02-09 18:02:01 -08:00
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
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
Sebastian Ullrich
8cbd7ccf09 test: reimplement package tests using Lake 2022-02-09 12:21:11 -08:00
Leonardo de Moura
15e6dd262d chore: fix tests 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
Sebastian Ullrich
9e11ea3b34 chore: move test to correct folder 2022-02-09 14:32:18 +01:00
Sebastian Ullrich
a8e34b9310 test: mutual recursion over mutual inductive 2022-02-09 14:24:45 +01: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
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
398b9c136a chore: fix test 2022-02-08 11:43:45 -08:00
Leonardo de Moura
96336bb44d test: add tests for #998 
The previous changes fixed two of them.
 2022-02-08 11:43:45 -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
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
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
8cea32f42d chore: fix test 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
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