Leonardo de Moura
044fe965da
fix(library/tactic/unfold_tactic): failed to unfold prefix
2017-01-05 18:01:19 -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
8144eaa9bf
feat(library/init/meta/smt/ematch): add hinst_lemmas API
2017-01-04 18:04:53 -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
30d90533bc
feat(library/tactic/destruct_tactic): support for non-dependent elimination
2017-01-03 18:33:57 -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
b636f03bb9
test(tests/lean/run/using_smt1): missing test
2017-01-03 15:13:15 -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
51efc6c178
fix(library/tactic/smt/congruence_closure): missing propagation
2017-01-03 13:48:14 -08:00
Leonardo de Moura
2262f70545
test(tests/lean/run/using_smt3): add zeta/nozeta test
2017-01-03 11:28:41 -08:00
Leonardo de Moura
61bf8d5902
test(tests/lean/run/blast_unit): add old blast unit propagation tests
2017-01-02 19:38:31 -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
ca6d3743c7
feat(library/tactic/smt): add mk_eq_true_intro mk_of_eq_true mk_eq_false_intro mk_not_of_eq_false
2017-01-02 13:39:16 -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
90096a3ee8
feat(library/init/meta/smt_tactic): add smt_tactic.close
2017-01-01 11:56:36 -08:00
Leonardo de Moura
35cc334b10
feat(library/init/meta): smt_tactic skeleton
2016-12-31 18:22:23 -08:00
Leonardo de Moura
7a06912427
test(tests/lean/run): add test for destruct tactic
2016-12-30 18:38:35 -08:00
Leonardo de Moura
5480036b7b
test(tests/lean/run): add ac_refl tests
2016-12-29 19:51:18 -08:00
Leonardo de Moura
79043177ee
fix(library/tactic/congruence/congruence_closure): bug in the interface between cc and ac modules
2016-12-29 19:25:29 -08:00
Leonardo de Moura
84cc00b1ea
fix(library/tactic/ac_tactics,library/tactic/congruence/theory_ac): crash when mixing different AC symbols
2016-12-29 18:38:40 -08:00
Leonardo de Moura
ec1c689073
test(tests/lean/run/cc_ac5): mix two AC symbols
2016-12-29 18:25:00 -08:00
Leonardo de Moura
c0f7d01cc4
fix(tests/lean/run/ematch2): remove example that produces a tsunami of redundant equalities to the AC module
2016-12-29 15:55:09 -08:00
Leonardo de Moura
97330f9f02
test(tests/lean/run): add new AC test with set union
2016-12-29 15:30:29 -08:00
Leonardo de Moura
312445fc57
test(tests/lean/run/cc_ac3): add test that requires superpose
2016-12-29 15:11:33 -08:00
Leonardo de Moura
7ccbf0eb02
feat(library/tactic/congruence/theory_ac): add collapse transition
2016-12-29 11:24:36 -08:00
Leonardo de Moura
4eafd201f6
test(tests/lean/run): add cc+ac sanity test
2016-12-28 21:35:26 -08:00
Leonardo de Moura
5b6e81ddb9
chore(tests/lean/run/cc1): remove trace option
2016-12-28 09:03:54 -08:00
Leonardo de Moura
fb54126d08
fix(library/tactic/congruence/congruence_closure): do not assume instances have been canonized.
2016-12-27 11:19:45 -08:00
Leonardo de Moura
f719991c71
feat(library/tactic/congruence/congruence_closure): propagate projection over constructor equality
2016-12-26 19:47:29 -08:00
Leonardo de Moura
941bbd3e96
fix(library/tactic/congruence/congruence_closure): crash when processing partially applied constructors
2016-12-26 18:51:03 -08:00
Leonardo de Moura
7a2ae8d40b
test(tests/lean/run/ematch1): add ematching example
2016-12-26 18:26:57 -08:00
Leonardo de Moura
6a5f6a84cd
feat(library/tactic/congruence/hinst_lemma): add heuristic instantiation lemmas
2016-12-25 20:11:58 -08:00
Leonardo de Moura
9b35adfc8c
feat(library/tactic/congruence/congruence_closure): add support for constructor equalities
2016-12-25 12:47:17 -08:00
Leonardo de Moura
a30081a715
feat(library/tactic/congruence/congruence_closure): interpreted values in the same equivalence class
2016-12-25 11:09:55 -08:00
Leonardo de Moura
b313328cb9
feat(library/equations_compiler): int constants
2016-12-25 10:00:18 -08:00
Leonardo de Moura
f9fb041e04
fix(library/comp_val): mk_int_val_ne_proof
...
There was a typo in the proof generation. The weird part is that the
proof was valid, but it was very inefficient to check.
The proof was valid because ((n:int) ≥ m) reduces to true/false if n and
m are integer numerals. Thus, if ((n:int) ≥ m) holds then `trivial` is a
valid proof.
However, the reduction is extremely inefficient since it relies on
computations in unary.
In the buggy version, we provided a proof for (a >= 0) where (b >= 0)
was expected. However, both types are definitionally equal to true.
This is why the proof worked.
2016-12-24 15:54:48 -08:00
Leonardo de Moura
3061d8b9a3
feat(library): add mk_int_val_ne_proof
2016-12-24 15:22:31 -08:00
Leonardo de Moura
0906d84c92
fix(library/tactic/congruence/congruence_closure): proof generation for congruence with different arity
2016-12-24 09:12:10 -08:00
Leonardo de Moura
a3600b6f98
test(tests/lean/run/cc6): add more cc tests
2016-12-24 08:50:51 -08:00
Leonardo de Moura
424a6acb68
fix(library/tactic/congruence/congruence_closure): missing proof construction step
2016-12-24 08:43:04 -08:00
Leonardo de Moura
a176bd324d
fix(library/tactic/congruence/congruence_closure): check_eq_true
2016-12-23 22:24:39 -08:00
Leonardo de Moura
a13d3c83c9
fix(library/tactic/congruence/congruence_closure): heq bug and add more tests
2016-12-23 21:57:49 -08:00
Leonardo de Moura
b1b694a532
fix(library/tactic/congruence/congruence_closure): bugs, and add basic cc tactic
2016-12-23 19:30:45 -08:00
Leonardo de Moura
ca261b7fa8
feat(library/init/meta/congruence_tactics): add option for retrieving only non-singleton equivalence classes, add auxiliary functions
2016-12-23 18:35:44 -08:00
Leonardo de Moura
a2850ac050
fix(library/tactic/congruence/congruence_closure): bugs in the fo-approx mode, and debug mode compilation errors
2016-12-23 17:31:20 -08:00
