Leonardo de Moura
0ea267e4de
feat: add simp lemma preprocessor
2021-03-09 19:16:14 -08:00
Leonardo de Moura
66f1a88f2c
feat: simp [-decl]
2021-03-04 17:50:44 -08:00
Leonardo de Moura
db499a646f
chore: add profileitM for simp
2021-03-04 17:27:01 -08:00
Leonardo de Moura
fe94731779
perf: do not use decide for rewriting True/False
2021-03-04 13:50:17 -08:00
Leonardo de Moura
9baee4354c
chore: add trace.Debug.Meta.Tactic.simp
...
It is an attempt to distinguish trace messages that are relevant only
for developers.
@Kha I am considering using the prefix `trace.Debug` for (debugging) messages that
are just for us.
2021-03-04 12:27:10 -08:00
Leonardo de Moura
960e964b71
feat: allow user to "erase" [simp] lemmas
2021-03-04 11:36:12 -08:00
Leonardo de Moura
152a84c468
perf: reject rewrites that produce same expr
2021-03-03 20:20:22 -08:00
Leonardo de Moura
1a7535263e
fix: unfolding class projections at simp
2021-02-16 17:55:57 -08:00
Leonardo de Moura
399af03c7c
refactor: move defeq unfolding to reduce, use transform to implement dsimp
2021-02-16 17:41:18 -08:00
Leonardo de Moura
2ef6605cdf
feat: do not simplify proofs
2021-02-16 16:13:56 -08:00
Leonardo de Moura
5f80659b45
fix: unfold constants at simp
2021-02-16 15:42:31 -08:00
Leonardo de Moura
4ec85a39a5
fix: Not should not be reducible, special support for Ne
...
Unification hint for `Not`
2021-02-15 17:36:11 -08:00
Leonardo de Moura
e97df2f61b
feat: functions to unfold at simp
2021-02-15 15:32:25 -08:00
Leonardo de Moura
1c5de9842d
feat: use decide at simp
2021-02-15 13:08:45 -08:00
Leonardo de Moura
7bdd3ae5a2
feat: simplify ctor_1 ... = ctor_2 ...
2021-02-15 12:40:19 -08:00
Leonardo de Moura
0787886cea
feat: improve simp local lemma elaboration
2021-02-13 18:55:19 -08:00
Leonardo de Moura
2944da2a0b
feat: use simp itself as default method for discharging hypotheses of conditional rewriting rules
2021-02-13 18:55:19 -08:00
Leonardo de Moura
3a9cd7e85b
refactor: use Simp.Context instead of Config+SimpLemmas+CongrLemmas
2021-02-13 18:55:19 -08:00
Leonardo de Moura
4ac78266ad
fix: make sure temporary metavars don't leak
2021-02-12 16:52:56 -08:00
Leonardo de Moura
1945858d89
fix: assigned metavariables in SimpLemmas
2021-02-12 16:52:56 -08:00
Leonardo de Moura
b51e3cb1fe
feat: process congr lemmas at simp
2021-02-12 16:52:56 -08:00
Leonardo de Moura
da91fc4526
refactor: move synthesizeArgs
2021-02-12 16:52:56 -08:00
Leonardo de Moura
9ba8a30fb2
feat: add Repr instance for CongrLemmas
2021-02-11 18:13:33 -08:00
Leonardo de Moura
ffa4a577be
feat: add @[congr] attribute
2021-02-11 17:51:04 -08:00
Leonardo de Moura
5e0b6a404f
chore: naming convention
2021-02-11 15:05:26 -08:00
Leonardo de Moura
544a6cbb94
chore: cleanup
2021-01-05 12:29:29 -08:00
Leonardo de Moura
e517d72bee
feat: simpForall
2021-01-01 17:24:56 -08:00
Leonardo de Moura
244b72befd
feat: simpArrow
2021-01-01 17:15:15 -08:00
Leonardo de Moura
15c052d44a
feat: basic simpLet
2021-01-01 15:54:29 -08:00
Leonardo de Moura
493d089878
feat: add support for simp { contextual := true }
2021-01-01 15:39:41 -08:00
Leonardo de Moura
e742dd1348
feat: allow user to set Simp.Config at simp
2021-01-01 15:12:18 -08:00
Leonardo de Moura
ce09e795b9
feat: finalizeProof at rewrite step
2021-01-01 11:33:34 -08:00
Leonardo de Moura
3a369938c8
feat: simpLambda
2021-01-01 09:52:01 -08:00
Leonardo de Moura
59762b727e
refactor: move pre and fuel check to simpLoop
2021-01-01 09:01:39 -08:00
Leonardo de Moura
b756562d4a
feat: simp beta/proj/recursor/matcher
2021-01-01 08:29:21 -08:00
Leonardo de Moura
8d83e71c5e
refactor: use tail recursion at simp loop
2021-01-01 05:59:10 -08:00
Leonardo de Moura
4a06057410
feat: simp
2020-12-31 15:44:18 -08:00
Leonardo de Moura
a32c45a515
feat: simp infrastructure
2020-12-30 18:00:04 -08:00
Leonardo de Moura
34f6f8ef5d
feat: pre/post simp lemmas
2020-12-30 13:46:14 -08:00
Leonardo de Moura
03cc69f1db
feat: track permutation simp lemmas
2020-12-30 13:46:14 -08:00
Leonardo de Moura
64f7af9da5
feat: add SimpM
2020-12-29 14:21:02 -08:00
Leonardo de Moura
7165d50c93
feat: simp lemmas of the form not p
2020-12-28 17:03:32 -08:00
Leonardo de Moura
a58b799bd6
chore: add instances for debugging purposes
2020-12-28 16:34:02 -08:00
Leonardo de Moura
9611e2d84e
feat: add simp attribute
2020-12-28 08:20:28 -08:00
