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

3659 commits

Author SHA1 Message Date
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
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
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
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
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
8cea32f42d chore: fix test 2022-02-06 09:15:39 -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
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
17eab845ed fix: improve tryPostponeIfMVar 
see #992
 2022-02-03 13:24:19 -08:00
Leonardo de Moura
42b3ed5903 test: add Pi.single test 
see #988
 2022-02-03 09:22:22 -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
b7c853692d test: add test for decide congruence issue 
TODO: congruence lemma must be automatically generated.

see #988
 2022-02-02 17:49:03 -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
188f0eb70f fix: splitMatch tactic 
Improve how we compute the motive for match-splitter eliminator.

closes #986
 2022-02-02 15:06:03 -08:00
Leonardo de Moura
65e1fc1211 feat: at splitMatch only generalize discriminants that are not FVar 2022-02-02 15:06:03 -08:00
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