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

1118 commits

Author SHA1 Message Date
Leonardo de Moura
e997cd94c6 chore: style 2022-05-31 06:04:48 -07:00
Leonardo de Moura
9818de078b fix: fixes #1168 2022-05-30 07:24:23 -07:00
Leonardo de Moura
fb45eb4964 fix: universe polymorphic enumeration types 
Fixes issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Incorrect.20number.20of.20universe.20levels.20parameters/near/284283021
 2022-05-30 06:43:46 -07:00
Leonardo de Moura
2c5bafcbd8 fix: dead variables at match equation hypotheses 
This commit addresses an issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Structural.20Recursion.20Problem/near/284238723
 2022-05-28 16:09:35 -07:00
Leonardo de Moura
e26f86dd45 fix: improve simpH?, remove unnecessary hypotheses 2022-05-28 15:30:01 -07:00
Leonardo de Moura
3be437cad3 fix: make sure register_simp_attr declares an simp-like attribute parser for user simp attributes 
closes #1164
 2022-05-26 19:49:33 -07:00
Leonardo de Moura
988697b431 fix: fixes #1169 2022-05-26 07:05:32 -07:00
Leonardo de Moura
1d14637680 fix: missing withMVarContext 2022-05-26 06:18:14 -07:00
Leonardo de Moura
fad21a4cda chore: remove leftovers 2022-05-25 20:38:20 -07:00
Leonardo de Moura
2fc23a2a2b feat: make sure we can use split to synthesize code 2022-05-23 11:55:57 -07:00
Leonardo de Moura
56cd6c1ff5 fix: we should not use implicit targets when creating the key for the CustomEliminator map 2022-05-20 06:55:23 -07:00
Leonardo de Moura
063c77037f chore: fix typo 2022-05-20 06:44:25 -07:00
Sebastian Ullrich
61c7b8b94c chore: format string 2022-05-16 15:14:01 +02:00
Sebastian Ullrich
ff6537be1b fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
Leonardo de Moura
e729b32b2b feat: unfold should fail if it didn't unfold anything 2022-05-09 06:41:17 -07:00
Leonardo de Moura
4875224bd4 feat: unfold tactic tries to reduce match after unfolding 2022-05-09 06:35:40 -07:00
Leonardo de Moura
3cd46888bf fix: check types using default reducibility at synthInstance? 
closes #1131
 2022-05-08 06:49:14 -07:00
Leonardo de Moura
2c8c20d424 feat: add [eliminator] attribute specifying default recursors/eliminators for the cases and induction tactics 2022-05-07 15:09:42 -07:00
Leonardo de Moura
8c23bef399 feat: add support for casesOn applications to structural and well-founded recursion modules 2022-05-06 17:12:10 -07:00
Leonardo de Moura
090503cfd5 chore: cleanup 2022-05-06 17:12:10 -07:00
Leonardo de Moura
94b5a9b460 feat: improve split tactic 2022-05-03 17:46:50 -07:00
Leonardo de Moura
cddf9ddd95 fix: forallAltTelescope heterogeneous equality support 2022-04-29 15:37:20 -07:00
Leonardo de Moura
c19672e99e fix: basic support for the new discriminant equality encoding at split 
TODO: This is a temporary fix. We can do better.
 2022-04-29 15:29:39 -07:00
Leonardo de Moura
c241ef61b1 fix: use HEq (if needed) for encoding h : discr equalities 2022-04-29 15:05:48 -07:00
Leonardo de Moura
351f0deae9 feat: add mkEqHEq 2022-04-29 14:31:36 -07:00
Leonardo de Moura
941ad84ece fix: getMkMatcherInputInContext 2022-04-29 12:44:36 -07:00
Leonardo de Moura
d4d538cad8 fix: counterexample generation for new match encoding 2022-04-29 12:36:53 -07:00
Leonardo de Moura
6e1c51dd1a feat: splitter proof for new match encoding 2022-04-29 12:19:24 -07:00
Leonardo de Moura
89441aac2a feat: match equation theorem generation for new h : discr notation encoding 
TODO: splitter theorem generation still needs to be fixed.
 2022-04-29 11:48:25 -07:00
Leonardo de Moura
eac83586c6 chore: remove leftover 2022-04-29 09:10:27 -07:00
Leonardo de Moura
c959c80310 chore: reset local context at correct place 2022-04-29 09:08:44 -07:00
Leonardo de Moura
8d9626dab7 feat: delaborate match h : d with ... 2022-04-29 07:17:46 -07:00
Leonardo de Moura
0f7754847d chore: style 2022-04-29 07:17:46 -07:00
Leonardo de Moura
7a369848a0 feat: new mkMatcher 
TODO: adjust match elaborator
 2022-04-29 07:17:46 -07:00
Leonardo de Moura
f4b4b14797 refactor: prepare to handle match h: notation at Meta\Match\Match.lean 2022-04-29 07:17:46 -07:00
Leonardo de Moura
6af1da450e feat: disable only eta for classes during TC resolution 
closes #1123
 2022-04-26 08:20:39 -07:00
Leonardo de Moura
6bc5433b17 fix: add support for heterogeneous equality at processGenDiseq 2022-04-25 16:56:03 -07:00
Leonardo de Moura
3ad8dcb7ff fix: nasty interaction between TC resolution and Eta for structures 
See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60constructor.60.20and.20.60Applicative.60/near/279984801
 2022-04-24 08:19:29 -07:00
Leonardo de Moura
47b379e1bc feat: dsimp! tactic 2022-04-23 18:41:04 -07:00
Leonardo de Moura
342a26a023 feat: dsimp tactic 2022-04-23 18:05:18 -07:00
Leonardo de Moura
13bcbe91cd fix: regression reported at issue #1113 
see issue #1113
 2022-04-23 15:39:04 -07:00
Leonardo de Moura
36fad4bba0 fix: do not assign metavariables in the major premise type when trying K 2022-04-23 07:31:51 -07:00
Leonardo de Moura
875bf9bf34 fix: apply dsimp at lambda binders 
This fixes another regression reported at #1113
 2022-04-22 13:10:21 -07:00
Leonardo de Moura
c13ed7c0de fix: regression reported at #1113 
See #1113
 2022-04-22 11:43:58 -07:00
Leonardo de Moura
d1f10a2e71 feat: apply rfl theorems at dsimp 
closes #1113
 2022-04-21 16:26:57 -07:00
Leonardo de Moura
2a0dc1804b feat: improve isRflProof and isRflTheorem 
The `Eq.symm` of a `rfl` theorem is a `rfl` theorem, the application
of `rfl` theorem too.
 2022-04-21 15:40:38 -07:00
Leonardo de Moura
57c3114875 fix: simpAll and tests 
We need another `update stage0` to remove workaround at `AC.lean`
 2022-04-21 15:00:07 -07:00
Leonardo de Moura
da33347e9d fix: use defauld reducibility setting at mkImpDepCongrCtx and mkImpCongrCtx 2022-04-21 14:55:29 -07:00
Leonardo de Moura
f891c5724d feat: track rfl simp theorems 
See issue #1113

We need update stage0 before closing the issue.
 2022-04-21 13:42:04 -07:00
Leonardo de Moura
73076b855c fix: bug at processGenDiseq 2022-04-20 10:46:05 -07:00