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

3634 commits

Author SHA1 Message Date
Leonardo de Moura
f02013fd76 fix: induction MetaM tactic 
The major premise may be a let-declaration.

closes #983
 2022-01-31 13:41:38 -08:00
Leonardo de Moura
e5ef61225b fix: missing condition at lpo case 3 2022-01-28 09:47:35 -08:00
Leonardo de Moura
cb4a86ac68 fix: do not validate local eq theorems 
see #973
 2022-01-27 11:50:20 -08:00
Leonardo de Moura
2fff4c42b7 fix: make sure irreducible constants are not unfolded when using the default reducibility setting 2022-01-26 11:55:21 -08:00
Leonardo de Moura
02677cf326 fix: igore instance implicit arguments in term ordering used at simp 
closes #972
 2022-01-24 18:57:31 -08:00
Leonardo de Moura
7ada79bf2e fix: use an AC-compatible ordering on Expr at simp 
closes #968
 2022-01-22 09:42:59 -08:00
Leonardo de Moura
0615020cf7 feat: make sure Expr.approxDepth does not overflow 2022-01-22 07:45:19 -08:00
Leonardo de Moura
0c959b6942 chore: fix tests 2022-01-20 15:25:59 -08:00
Leonardo de Moura
f9fa24435d chore: remove problematic instance hasOfNatOfCoe 
See #403
See https://github.com/leanprover-community/mathport/issues/94
 2022-01-20 14:47:25 -08:00
Leonardo de Moura
d190d6dda4 fix: use default reducibility when proving equation theorems for definition 
Addresses issue reported by @fpfu at #945
 2022-01-20 08:23:51 -08:00
Leonardo de Moura
1e21815e41 fix: equality theorem generation when named patterns are used 
closed #945
 2022-01-18 14:37:51 -08:00
Leonardo de Moura
1c1e6d79a7 feat: add equality proof for named patterns 
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.

closes #501
 2022-01-18 12:43:01 -08:00
Leonardo de Moura
cd903bde77 refactor: [s : Setoid α] => {s : Setoid α} or (s : Setoid α) 
See comment at https://github.com/leanprover/lean4/issues/952#issuecomment-1015265136

cc @gebner
 2022-01-18 09:24:06 -08:00
Leonardo de Moura
da06bb6605 fix: matching inside new termination_by 2022-01-17 08:47:05 -08:00
Leonardo de Moura
189f4bd372 chore: fix tests 2022-01-15 12:18:09 -08:00
Leonardo de Moura
b0d9c16c7a chore: rename PointedType => NonemptyType 2022-01-15 11:43:53 -08:00
Leonardo de Moura
e3241e82bc feat: define PointedType as { α : Type u // Nonempty α } 2022-01-14 20:36:51 -08:00
Leonardo de Moura
1620987b6c fix: recursive applications in discriminants 2022-01-13 09:56:33 -08:00
Leonardo de Moura
3fbf5acbee fix: add missing [reducible] annotations Init/WF.lean 2022-01-12 17:12:55 -08:00
Leonardo de Moura
98864f707e test: add test for #879 
The new `termination_by` syntax should address issue #879

closes #879
 2022-01-12 16:25:09 -08:00
Leonardo de Moura
9162901c86 fix: expandTerminationByNonCore 2022-01-12 16:22:54 -08:00
Leonardo de Moura
91a0ac8a12 feat: elaborate new termination_by syntax 2022-01-12 16:15:30 -08:00
Leonardo de Moura
111d09fda3 fix: must apply afterCompilation attributes *after* smart unfolding definition was declared 
The `[simp]` attribute checks whether the smart unfolding defintion
has been declared.

closes #946
 2022-01-12 08:28:03 -08:00
Leonardo de Moura
45bd328d5e fix: tests and add WellFoundedRelation.rel to list of definitions to unfold at decreasing_tactic 2022-01-12 08:28:03 -08:00
Leonardo de Moura
068cc700d8 test: ackermann 2022-01-11 15:03:07 -08:00
Leonardo de Moura
381f66428a chore: use termination_by' 
We are going to define a higher level syntax for `termination_by`.
 2022-01-11 15:00:53 -08:00
Leonardo de Moura
4c918a2363 feat: use default_decreasing_tactic at WF/Fix.lean 2022-01-10 14:55:38 -08:00
Leonardo de Moura
0dd3ce0598 chore: fix test 2022-01-10 14:31:23 -08:00
Leonardo de Moura
b797c982fc feat: add mkUnfoldProof 2022-01-07 13:51:45 -08:00
Mario Carneiro
dcaf3c615f fix: induction generalizing precedence 2022-01-07 10:45:45 +01:00
Leonardo de Moura
bef161caf7 feat: add better support for discharging equation theorem hypotheses 2022-01-06 14:42:23 -08:00
Leonardo de Moura
90b179bea9 fix: add equation theorems even if definition supports smart unfolding 
See new test.
 2022-01-06 13:53:03 -08:00
Leonardo de Moura
d8d7d63830 fix: registers eqns info before adding definition 
Otherwise `[simp]` at definition will fail to generate equational theorems.
 2022-01-06 12:24:40 -08:00
Leonardo de Moura
7acbbb4fbb fix: auxiliary whnfAux used at mkEqns 2022-01-06 09:57:41 -08:00
Leonardo de Moura
60934bf1d5 feat: add support for removing [simp] attribute from definitions with equational theorems 2022-01-05 16:57:59 -08:00
Leonardo de Moura
c2e52bd577 feat: use getEqnsFor? when applying [simp] at definitions 2022-01-05 15:59:39 -08:00
Leonardo de Moura
030e932db8 feat: use getEqnsFor? at simp 2022-01-05 11:28:24 -08:00
Leonardo de Moura
4d1343d670 chore: use _eq instead of eq to name auto generated equational theorems 2022-01-04 17:23:34 -08:00
Leonardo de Moura
b2918e0c76 test: add tests for WF.mkEqns 2022-01-04 17:18:51 -08:00
Leonardo de Moura
d782a97f5c feat: add WF.mkProof for WF.mkEqns 2022-01-04 17:00:54 -08:00
Leonardo de Moura
b9f7d1defb fix: constant folding after erasure 
closes #909
 2022-01-03 10:33:07 -08:00
Gabriel Ebner
e605c541d0 fix: do not infer type in erase_irrelevant 
At the time erase_irrelevant is called, we have already eliminated the
`cast`-applications.  Therefore non-atomic expressions may no longer
be well-typed (and `infer_type` can fail).
 2022-01-03 07:13:55 -08:00
Sebastian Ullrich
555584375a fix: compare fields top-down in deriving Ord 2022-01-03 07:02:13 -08:00
Leonardo de Moura
be6bc67eb0 fix: ensure match-expressions compiled using if-then-else can be reduced with TransparencyMode.reducible 
closes #891
 2021-12-18 10:55:42 -08:00
Leonardo de Moura
c954fc9ec7 fix: bug at simpLoop 2021-12-18 06:48:08 -08:00
Leonardo de Moura
0a81093db5 fix: bug at simpProj 
This bug was reported at https://github.com/dwrensha/lean4-maze/issues/1
 2021-12-15 17:07:00 -08:00
Gabriel Ebner
7e483d3a0a feat: support syntax abbreviations in dynamic quotations 2021-12-15 11:17:58 +00:00
Leonardo de Moura
b6ef65d8fd fix: where structure instance parser 
closes #753
 2021-12-12 07:52:52 -08:00
Leonardo de Moura
a3361e7d86 fix: missing universe assignments made during TC resolution 
closes #796
 2021-12-12 07:07:13 -08:00
Leonardo de Moura
483f32edd8 feat: in pure code, do use assume Id monad at do notation 
This feature produced counterintuitive behavior and confused users.
See discussion at #770.

As pointed out by @tydeu, it is not too much work to write `Id.run <|`
before the `do` when we want to use the `do` notation in pure code.

closes #770
 2021-12-10 12:55:14 -08:00