Leonardo de Moura
b28ed2453e
feat(frontends/lean/definition_cmds): allow meta recursive definitions without recursive equations
2017-02-04 13:44:05 -08:00
Leonardo de Moura
3b38f71f11
fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type
...
We had to change subtype to use Sort since the axiom
strong_indefinite_description uses it.
see #1341
2017-01-30 11:54:00 -08:00
Leonardo de Moura
6d12de6339
refactor(library/init/meta/smt): use default value for config structures
2017-01-23 14:18:06 -08:00
Leonardo de Moura
778d5382f6
refactor(library/init/meta/simp_tactic): use default field values at simplify_config
2017-01-23 10:22:48 -08:00
Jeremy Avigad
7496522830
fix(library/tools/super/clausifier): add rule for new iff
2017-01-22 14:19:11 -08:00
Leonardo de Moura
4de71cadfa
feat(library/init/meta): expose additional app_builder tactics
2017-01-20 20:27:07 -08:00
Gabriel Ebner
51924eb726
refactor(tools/super/lpo): add mk_lpo function
2017-01-12 21:47:46 +01:00
Gabriel Ebner
f8caacfcb3
fix(tools/super/superposition): use none transparency to remove beta-redex
2017-01-12 21:47:46 +01:00
Gabriel Ebner
b6a25f8074
feat(tools/super/defs): unfold definitions using dunfold_expr_core
2017-01-12 21:47:46 +01:00
Gabriel Ebner
17bc32e41b
chore(tools/super/prover_state): clean up prover monad definition
2017-01-12 21:47:46 +01:00
Gabriel Ebner
020cb5b271
fix(tools/super/clause): fix universal closure of clauses with dependent types
2017-01-12 21:47:46 +01:00
Gabriel Ebner
8319a4c927
perf(tools/super/trim): make trim much cheaper
2017-01-12 21:47:46 +01:00
Gabriel Ebner
f2b3c7ae30
fix(tools/super/misc_preprocessing): normalize clauses during preprocessing
2017-01-12 21:47:46 +01:00
Gabriel Ebner
42eb3ef497
feat(tools/super/inhabited): look in the local context as well
2017-01-12 21:47:46 +01:00
Leonardo de Moura
3967cd28fa
fix(library/vm/vm): curr_fn() may not be available
2017-01-12 11:47:45 -08:00
Leonardo de Moura
dc7e39887b
refactor(library/tools/super/simp): reorganize simplify lemmas API
2017-01-11 13:47:49 -08:00
Gabriel Ebner
d6a70b4aa3
chore(library/tools/super/clause_ops): remove unnecessary type annotations
2017-01-10 09:07:37 -08:00
Gabriel Ebner
890ba702e6
feat(tools/super/demod): demodulation
2017-01-10 09:07:37 -08:00
Gabriel Ebner
e0dd8326c8
feat(tools/super/clause): more compact formatting
2017-01-10 09:07:37 -08:00
Gabriel Ebner
beb355f798
feat(tools/super): clausify during preprocessing
...
Some inference produce terms with large useless redexes such as
(prod.fst (prod.mk _ _)). Since we do normalization during
preprocessing, we can avoid ever even looking at these terms.
2017-01-10 09:07:37 -08:00
Gabriel Ebner
38c311c47a
feat(tools/super/clausifier): fully normalize terms
2017-01-10 09:07:37 -08:00
Gabriel Ebner
244e061f76
refactor(tools/super/simp): do not enable simp by default
...
simp interacts badly with super's term ordering. I believe a better
approach is to pick the term ordering according to the available simp
rules, as in "More SPASS with Isabelle".
2017-01-10 09:07:37 -08:00
Gabriel Ebner
4e1106ffb5
feat(tools/super): use congruence closure
2017-01-10 09:07:37 -08:00
Leonardo de Moura
68629b2e5f
feat(library/init/category/transformers): disable instance has_monad_lift_t ==> has_coe
...
It produces non-termination because it triggers sub-problems of the
form (has_monad_lift_t t ?M), and this kind of sub-problem is bad
for the transitive closure rule:
instance has_monad_lift_t_trans (m n o) [has_monad_lift n o] [has_monad_lift_t m n] : has_monad_lift_t m o
The trick above only behaves well for synthesis subproblems that do not
contain sub-variables.
Note that the sub-problem (has_monad_lift_t t ?M) is created by a
similar rule used at has_coe_t.
instance {a : Type u₁} {b : Type u₂} {c : Type u₃} [has_coe a b] [has_coe_t b c] : has_coe_t a c
AND
instance {m n} [has_monad_lift_t m n] {α} : has_coe (m α) (n α) :=
We workaround the issue by disabling
instance {m n} [has_monad_lift_t m n] {α} : has_coe (m α) (n α)
and adding instances of it. Example:
meta instance (α : Type) : has_coe (tactic α) (solver α) := ...
meta instance (α : Type) : has_coe (tactic α) (prover α) := ...
meta instance (α : Type) : has_coe (tactic α) (smt_tactic α) := ...
2017-01-01 09:15:25 -08:00
Leonardo de Moura
35cc334b10
feat(library/init/meta): smt_tactic skeleton
2016-12-31 18:22:23 -08:00
Leonardo de Moura
66bc3c796a
feat(frontends/lean/elaborator): add extra coercion resolution rule for monads
...
We also removed the notation (♯tac) since it is not needed anymore.
@gebner, the comment at elaborator.cpp explains why you had to use the ♯
notation. The workaround is a little bit hackish, but I think it is
worth it. We will use monad lifts in many different places.
2016-12-31 13:50:15 -08:00
Leonardo de Moura
85f88c4174
refactor(library/data/monad/transformers): move transformers to init
2016-12-31 11:37:13 -08:00
Leonardo de Moura
5d825483c4
refactor(library/init/meta/interactive): tactic.interactive.types ==> interactive.types
...
Motivation: we will use auto-quotation for other tactic monads
2016-12-30 18:06:41 -08:00
Gabriel Ebner
f8331a0dfe
fix(library/tools/super/prover_state): correctly detect sos lemmas
2016-12-27 11:21:52 -08:00
Leonardo de Moura
305838bece
refactor(library/debugger): move debugger to tools
2016-12-17 10:50:13 -08:00
Leonardo de Moura
63ec7cd6cf
chore(library/tools/super): replace ↣ with ^.
...
The plan is to delete the funny arrow ↣ notation and keep only ^.
2016-12-16 19:14:05 -08:00
Leonardo de Moura
85ae8ce307
chore(tools/super): add copyright
2016-12-16 19:06:50 -08:00
Leonardo de Moura
4b97b00536
refactor(library/tools/super): move examples to test folder
2016-12-16 19:05:32 -08:00
Gabriel Ebner
6b15f6cef9
feat(library/tools/super): add super prover
2016-12-16 18:18:13 -08:00
Leonardo de Moura
d97e5b5061
chore(library): remove old files
2016-09-21 11:46:40 -07:00
Leonardo de Moura
0280281b1c
chore(library): remove old tactic definition
2016-06-06 14:11:40 -07:00
Leonardo de Moura
d88098f38d
chore(frontends/lean): remove some of the tactic support
2016-04-25 15:26:56 -07:00
Leonardo de Moura
3ab0e07ba9
feat(frontends/lean): add simp tactic frontend stub
...
This commit also removes the fake_simplifier. It doesn't work anymore
because simp is now a reserved word.
2015-07-14 09:54:53 -04:00
Floris van Doorn
37995edbd7
fix(tools.md): remove missing link
2015-06-04 20:14:13 -04:00
Leonardo de Moura
4f0f739ea6
feat(library): remove occurrences of 'opaque' keyword
2015-05-08 16:40:03 -07:00
Leonardo de Moura
697d4359e3
refactor(library): add 'init' folder
2014-11-30 20:34:12 -08:00
Leonardo de Moura
c08f4672e4
feat(library/tactic): add 'assert' tactic, closes #349
2014-11-29 21:34:49 -08:00
Leonardo de Moura
1a7dd56f0f
fix(library/tools/tactic): 'cases' argument precedence
2014-11-29 21:03:45 -08:00
Leonardo de Moura
f51fa93292
feat(library/tactic): add 'fapply' tactic, closes #356
2014-11-29 19:20:41 -08:00
Leonardo de Moura
2c0472252e
feat(frontends/lean): allow expressions to be used to define precedence, closes #335
2014-11-29 18:29:48 -08:00
Leonardo de Moura
e0debca771
feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses
2014-11-28 22:25:37 -08:00
Leonardo de Moura
c2602baf2b
feat(library/tools/tactic): add 'cases' alias for 'inversion' tactic
2014-11-28 19:33:11 -08:00
Leonardo de Moura
ebd320a6b3
feat(library/tactic): add first step of 'inversion' tactic
2014-11-26 21:28:00 -08:00
Leonardo de Moura
f7deabfd19
feat(library/rename): add notation for rename
2014-11-26 19:02:11 -08:00
Leonardo de Moura
e55397d422
feat(library/tactic): add 'clears' and 'reverts' variants
2014-11-26 14:49:48 -08:00
