Jeremy Avigad
20edc93b17
fix(library/init/data/list/lemmas): fix theorem names, now nil_append and cons_append
2017-01-10 09:10:33 -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
b8f1b16cfe
chore(init/meta/smt/congruence_closure): remove unnecessary line
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
a43b856086
feat(library/init/meta/smt): add simp tactics to smt_tactic
...
We can simplify the target without affecting the smt state
2017-01-09 19:19:48 -08:00
Leonardo de Moura
5050e40aec
feat(library/init/meta/smt): add slift smt tactic
2017-01-09 19:07:54 -08:00
Leonardo de Moura
b1c1d2dfa4
feat(library/init/meta): improve dsimp tactic notation
2017-01-09 17:31:35 -08:00
Leonardo de Moura
fa4d47edd8
chore(library/init/algebra/ring): document messy problem in the algebraic hierarchy
2017-01-08 23:35:39 -08:00
Leonardo de Moura
f56250d41e
chore(library/init/data/nat/lemmas): mark nat.add_zero as protected
2017-01-07 14:17:56 -08:00
Leonardo de Moura
0c4c41ae54
feat(library/init/meta): produce nicer error message for overloaded simp/ematch lemma
2017-01-07 14:13:46 -08:00
Leonardo de Moura
c29a2bdac9
feat(library/init/meta/tactic): add eta reduction tactic
2017-01-06 19:56:10 -08:00
Leonardo de Moura
d333c444cd
test(tests/lean/run): add tactic examples
2017-01-06 18:48:03 -08:00
Leonardo de Moura
5e3f26ec95
feat(library/tactic/smt/congruence_closure): propagate not_exists
2017-01-06 14:00:36 -08:00
Leonardo de Moura
13a11b4374
feat(library/init/meta/interactive): add get_eqn_lemmas_for tactic, allow user to provide definition name as an argument to simp
2017-01-06 11:45:09 -08:00
Leonardo de Moura
db70c78704
feat(library/equations_compiler): make sure automatically generated equational lemmas use internal names
2017-01-06 11:40:34 -08:00
Leonardo de Moura
15eaf30192
feat(library/tactic/smt/smt_state): allow user to provide a function ("to be unfolded") in the ematch_using tactic
2017-01-06 00:33:58 -08:00
Leonardo de Moura
7e4b79b221
feat(library/tactic/smt/smt_state): add ematch_using tactic
2017-01-06 00:24:25 -08:00
Leonardo de Moura
4a76579cd0
feat(library/tactic/smt): add tactics for getting/setting ematching lemmas
2017-01-05 20:35:57 -08:00
Leonardo de Moura
7ba889b5cf
feat(frontends/lean/tactic_notation): try/repeat for smt_tactic in interactive mode
2017-01-05 18:31:57 -08:00
Gabriel Ebner
4d4e47921a
fix(library/init/core): mark all rfl-lemmas as lemmas
2017-01-05 18:09:28 -08:00
Leonardo de Moura
82f8eeb280
feat(frontends/lean/definition_cmds): generate equational lemmas for regular definitions that were elaborated without using the equation compiler
2017-01-05 18:02:14 -08:00
Leonardo de Moura
b18b49dd6b
feat(library/tactic/smt/smt_state): add tactic for adding equational lemmas for a definition
2017-01-05 15:47:58 -08:00
Leonardo de Moura
3742d6573d
feat(library/tactic/smt/smt_state): add preprocess tactic
2017-01-05 13:43:50 -08:00
Leonardo de Moura
8eadaf51d8
feat(library/init/meta/smt): add helper tactics: get_facts, proof_for, refutation_for, add_lemmas_from_facts, ...
2017-01-05 12:59:11 -08:00
Leonardo de Moura
52c1a15313
feat(library/tactic/smt): add tactics for adding new lemmas to ematch state
2017-01-05 11:44:25 -08:00
Leonardo de Moura
0969997c64
feat(library/tactic/smt): add ematch smt_tactic
2017-01-04 22:41:36 -08:00
Leonardo de Moura
858ce76e73
feat(library/init/meta/smt/ematch): add commands for creating attributes for hinst_lemmas
2017-01-04 20:31:38 -08:00
Leonardo de Moura
d784aba249
feat(library/tactic/smt/hinst_lemmas): change how transparency is used to process hinst_lemmas
2017-01-04 19:12:37 -08:00
Leonardo de Moura
8144eaa9bf
feat(library/init/meta/smt/ematch): add hinst_lemmas API
2017-01-04 18:04:53 -08:00
Leonardo de Moura
384e8bc795
refactor(library/init/meta/smt): move ematch stuff to new file, and remove priority from hinst_lemma
2017-01-04 17:23:06 -08:00
Leonardo de Moura
5f2b247af9
feat(frontends/lean/tactic_evaluator): step-by-step evaluation for 'begin [smt] ... end' blocks
2017-01-04 14:06:44 -08:00
Leonardo de Moura
d53215a2fb
feat(frontends/lean/tactic_notation, library/init/meta/smt): add by_cases and by_contradiction smt_tactics, support for classical reasoning, add support for 'begin [smt] with config, ... end'
2017-01-04 12:03:45 -08:00
Leonardo de Moura
59f3c9775a
feat(frontends/lean/tactic_notation): add support for begin [smt] ... end blocks
...
TODO: add support for inspecting intermediate states.
2017-01-04 11:13:00 -08:00
Leonardo de Moura
3a62ca0581
refactor(library/init/meta): move smt tactics to library/init/meta/smt, and add interactive definitions
2017-01-04 09:36:50 -08:00
Leonardo de Moura
3adcf30d2f
feat(library/init/meta/smt_tactic): add assert/assertv/define/definev/pose/note for smt_tactic
2017-01-03 17:12:00 -08:00
Leonardo de Moura
554cef1d36
feat(library/tactic/smt/congruence_closure): propagate disequalities
2017-01-03 14:53:27 -08:00
Leonardo de Moura
78f4ab605e
feat(library/tactic/smt): preprocessing configuration options
2017-01-03 11:06:33 -08:00
Leonardo de Moura
de8491474c
feat(library/tactic/smt/congruence_closure): more propagation rules for implication, and cleanup
2017-01-02 19:35:12 -08:00
Leonardo de Moura
cefccd0e47
feat(library/tactic/smt): perform "unit propagation" in the congruence closure module
2017-01-02 18:49:26 -08:00
Leonardo de Moura
b200a86240
feat(library/tactic/smt): simplify congruence_closure internalization, visit lemmas at unit_propagation
2017-01-02 12:23:32 -08:00
Leonardo de Moura
32cc36214a
feat(library/init/meta/smt_tactic): allow user to select simp attribute to be used during SMT preprocessing, use preprocessing at intros too
2017-01-01 22:26:26 -08:00
Leonardo de Moura
50b25ad45f
feat(library/init/meta/smt_tactic): add smt_tactic.destruct, and a few combinators
2017-01-01 14:50:34 -08:00
Leonardo de Moura
effe19d334
feat(library/tactic/smt/smt_state): add smt_tactic.intros, define smt_state in Lean as (list smt_goal)
2017-01-01 14:17:03 -08:00
Leonardo de Moura
90096a3ee8
feat(library/init/meta/smt_tactic): add smt_tactic.close
2017-01-01 11:56:36 -08:00
Scott Morrison
548ca37c47
fix(library/init/meta/interactive): correcting a typo in a comment
2017-01-01 09:34:32 -08:00
