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

1406 commits

Author SHA1 Message Date
Leonardo de Moura
425f42cd83 feat: better support for Nat literals at DiscrTree.lean 2023-06-21 22:30:09 -07:00
Leonardo de Moura
184f2ed597 chore: improve isNonTrivialProof 2023-06-21 20:28:17 -07:00
Leonardo de Moura
7367f2edc6 fix: unfold constant theorems when transparency is set to .all 2023-06-21 20:28:17 -07:00
Leonardo de Moura
9df2f6b0c9 fix: bump transparency to .all when reducing the major premise of Acc.rec and WellFounded.rec 2023-06-21 20:28:17 -07:00
Leonardo de Moura
2b8e55c2f1 fix: Nat literal bug at DiscrTree.lean 2023-06-21 20:28:17 -07:00
Leonardo de Moura
d6695a7a2e fix: use mkAuxTheoremFor when creating helper proof_n theorems 2023-06-21 20:28:17 -07:00
Scott Morrison
a44dd71ad6 feat: add flag for apply to defer failed typeclass syntheses as goals 2023-06-19 20:07:07 -07:00
Gabriel Ebner
bff612e59e fix: simp: synthesize non-inst-implicit tc args 
Fixes #2265.
 2023-06-09 16:32:02 -07:00
Leonardo de Moura
25384fe951 fix: fixes #2232 2023-05-31 05:48:25 -07:00
Leonardo de Moura
e04d67f55f chore: expand docstring for TransformStep.visit 2023-05-31 05:48:25 -07:00
Mario Carneiro
9ec9ea61a4 fix: infinite loop in isClassApp? 2023-05-30 18:47:17 -07:00
Leonardo de Moura
83cc0bcc96 fix: fixes #2199 2023-05-28 18:29:09 -07:00
Mario Carneiro
5d3ac5f80c fix: panic in Match.SimpH.substRHS 2023-05-28 17:04:28 -07:00
Parth Shastri
954190e457 fix: remove repeat calls to inferType in ignoreField 2023-05-15 09:35:44 -07:00
Gabriel Ebner
5781752985 fix: offset unification with a+a+1 
Fixes #2136
 2023-05-15 09:06:37 -07:00
Gabriel Ebner
1f21ababfa chore: remove etaExperiment option 2023-05-15 09:05:41 -07:00
Gabriel Ebner
8de8c80119 perf: do not unify proof arguments 2023-05-15 09:05:41 -07:00
Gabriel Ebner
89cb94fcab perf: try structure eta after delta 2023-05-15 09:05:41 -07:00
Gabriel Ebner
9211dd6541 chore: tc: re-enable eta 2023-05-15 09:05:41 -07:00
Jakob von Raumer
45b49e7f02 fix: typos 2023-05-05 12:07:54 -07:00
Sebastian Ullrich
8a302e6135 fix: match discriminant reduction should not unfold irreducible defs 2023-04-10 21:09:04 -07:00
Gabriel Ebner
7f51628986 fix: simp: strip mdata when testing for True/False 
Fixes #2173
 2023-04-10 21:06:42 -07:00
Gabriel Ebner
8075d1f45d fix: reset local context in mkInjectiveTheorems 2023-04-10 21:05:16 -07:00
Gabriel Ebner
4af329588e doc: clarify semi-out params 2023-04-10 13:00:04 -07:00
Gabriel Ebner
4544443d98 feat: reorder tc subgoals according to out-params 2023-04-10 13:00:04 -07:00
Sebastian Ullrich
b076d488e3 feat: show typeclass and tactic names in profile output 2023-03-27 17:47:52 +02:00
Gabriel Ebner
8650804b02 perf: cache tc results with mvars 2023-03-16 15:26:38 -07:00
Gabriel Ebner
d3c55ef249 perf: do not reset tc cache when adding local instances 2023-03-16 15:26:38 -07:00
Gabriel Ebner
0cc9d7a43d fix: do not reverse subgoals of local instances 2023-03-08 15:54:07 -08:00
Gabriel Ebner
2262579f9b fix: tc: filter out assigned subgoals at the correct place 2023-03-08 15:54:07 -08:00
Gabriel Ebner
3ab859553e fix: allow function coercion to assign universe mvars 2023-03-08 15:54:07 -08:00
Gabriel Ebner
1c641b569a chore: synthInstance trace message on cache hit 2023-03-08 15:54:07 -08:00
Gabriel Ebner
1f61633da7 fix: typo in trace class name 2023-03-08 15:54:07 -08:00
Gabriel Ebner
adcca17991 chore: add option to enable structure eta in tc search 2023-02-21 16:41:30 -08:00
Gabriel Ebner
75252d2b85 perf: whnf projections during defeq 2023-02-09 19:54:23 -08:00
Gabriel Ebner
ecc74c5a9d fix: defeq condition for projections 2023-02-09 19:54:23 -08:00
Gabriel Ebner
448f49ee91 Revert "fix: reenable structure eta during tc search" 
The fix is blocked by slow defeq checks for TC instances; see issues
1986 and 2055.  Enabling it right now causes lots of timeouts in
mathlib4.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bump.20to.202023-02-06/near/326223768

This reverts commit 15a045ee66.
 2023-02-09 11:37:30 -08:00
Gabriel Ebner
15a045ee66 fix: reenable structure eta during tc search 
Fixes #2074.
 2023-02-05 11:41:00 -08:00
Gabriel Ebner
c21d2f29a2 perf: do not backtrack after eta-defeq 2023-01-09 16:12:02 -08:00
Leonardo de Moura
fedf235cba fix: fixes #2011 
In Lean 4, we have support for typing constraints of the form
```
(?m ...).1 =?= v
```
where the type of `?m ...` is a structure with a single field.
This kind of constraint is reduced to `?m ... =?= ⟨v⟩`

This feature is implemented by the function `isDefEqSingleton`.
As far as I remember, Lean 3 does not implement this feature.

This commit disables this feature if the structure is a class.
The goal is to avoid the generation of counterintuitive instances by
typing inference.

For example, in the example at issue #2011, the following weird
instance was being generated for `Zero (f x)`
```
(@Zero.mk (f x✝) ((@instZero I (fun i => f i) fun i => inst✝¹ i).1 x✝)
```
where `inst✝¹` is the local instance `[∀ i, Zero (f i)]`
Note that this instance is definitinally equal to the expected nicer
instance `inst✝¹ x✝`.
However, the nasty instance trigger nasty unification higher order
constraints later.

Note that a few tests broke because different error messages were
produced. The new error messages seem better. I do not expect this
change to affect Mathlib4 since Lean 3 does not have this feature.
 2023-01-05 17:33:45 -08:00
Leonardo de Moura
dd682bf1d5 feat: add support for HO projections at DiscrTree 
closes #1937

Requires update stage0
 2023-01-05 13:33:43 -08:00
Leonardo de Moura
30c9f58e6a chore: remove leftover 2023-01-03 15:05:31 -08:00
Gabriel Ebner
70a6c06eef fix: erase *dependent* local instances 2023-01-03 11:39:46 -08:00
Gabriel Ebner
a2f5959118 chore: use deriving Nonempty 2022-12-22 03:48:15 +01:00
Gabriel Ebner
7736c051ff fix: assigned tc mvar check 2022-12-22 02:02:55 +01:00
Gabriel Ebner
6083b01c86 fix: remove maxCoeSize option 2022-12-22 02:02:55 +01:00
Gabriel Ebner
f798507bbf chore: tc: only normalize level mvars at current depth 2022-12-22 02:02:55 +01:00
Gabriel Ebner
572ffe77e3 fix: implement assertAfter using revert 2022-12-21 21:42:07 +01:00
Gabriel Ebner
eeab2af7ae fix: remove Inhabited Environment instance 2022-12-21 20:08:08 +01:00
Gabriel Ebner
e59ddb0c16 refactor: replace hardcoded list of coercions by attribute 2022-12-21 04:24:39 +01:00