Leonardo de Moura
7d17840e3f
feat(library/tactic/congruence/theory_ac): add compose transition
2016-12-29 11:11:44 -08:00
Leonardo de Moura
deaf252acf
chore(library/tactic/congruence/theory_ac): improve trace messages
2016-12-29 09:59:11 -08:00
Leonardo de Moura
9065cf0350
feat(library/tactic/congruence/theory_ac): add internalization, interface with congruence closure module, and trivial/simp/orient transitions
...
Still missing: superpose, collapse and compose transitions.
2016-12-28 21:35:16 -08:00
Leonardo de Moura
bb37b33237
fix(library/tactic/ac_tactics): binary.left_comm ==> left_comm
2016-12-28 21:23:07 -08:00
Leonardo de Moura
80670abb8f
fix(library/tactic/congruence/congruence_closure): assertion violation
2016-12-28 08:55:24 -08:00
Leonardo de Moura
1d519e4c7b
feat(library/tactic/congruence): add theory AC skeleton
2016-12-27 21:38:03 -08:00
Leonardo de Moura
4d0404bd6d
chore(library): define rb_expr_tree and rb_expr_map
2016-12-27 20:29:31 -08:00
Leonardo de Moura
b5c1b429e7
feat(library/tactic/ac_tactics): add ac_manager helper class
2016-12-27 17:57:56 -08:00
Leonardo de Moura
d3795b20dd
feat(library/defeq_canonizer): remove thread local cache
...
The goal is to avoid hard to debug behavior because any tactic (e.g., simp/dsimp/cc) using
defeq_canonize was breaking referential transparency.
2016-12-27 12:56:39 -08:00
Daniel Selsam
1af202f816
feat(library/tactic/simp_lemmas.cpp): tracing for invalid simp_lemmas
2016-12-27 11:45:07 -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
773389f9df
feat(library/init/meta/congruence_tactics): add cc_state.gmt and cc_state.inc_gmt
2016-12-27 10:49:20 -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
15f1c6bab2
chore(library/tactic/congruence/ematch): style
2016-12-26 18:23:57 -08:00
Leonardo de Moura
6661faf3da
fix(library/tactic/congruence/congruence_closure): but at add_occurrence
2016-12-26 18:13:06 -08:00
Leonardo de Moura
8419219ca6
feat(library/tactic/congruence/congruence_closure): add trace.debug.cc option
2016-12-26 18:13:02 -08:00
Leonardo de Moura
148d34b3bf
feat(library/tactic/congruence/congruence_closure): merge annotated term with term being annotated
2016-12-26 16:30:18 -08:00
Leonardo de Moura
9e46818563
feat(library/tactic/congruence): ematching
2016-12-26 15:52:18 -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
8f401c8752
chore(library/tactic/congruence/congruence_closure): remove unnecessary field
2016-12-24 09:14:25 -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
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
Leonardo de Moura
1aa92c7d7d
fix(library/tactic/congruence/congruence_closure): add entries for 'true' and 'false'
2016-12-23 15:54:09 -08:00
Leonardo de Moura
d431d7274a
feat(library/tactic/congruence/congruence_closure): hard code support for ne
2016-12-23 15:37:05 -08:00
Leonardo de Moura
6eb81d2472
feat(library/tactic/congruence/congruence_closure): add new configuration options for minimizing the number of entries and occurrences
2016-12-23 15:18:10 -08:00
Leonardo de Moura
17cc40b35e
feat(library/tactic/congruence/congruence_closure): do not recurse on values and instances when internalizing terms
2016-12-23 13:24:43 -08:00
Leonardo de Moura
104ee1b120
fix(library/tactic/congruence/congruence_tactics): stupid mistake
2016-12-22 20:54:20 -08:00
Leonardo de Moura
6329afc121
chore(library/tactic/congruence/congruence_closure): fix typo
2016-12-22 20:05:02 -08:00
Leonardo de Moura
77737a621d
fix(library/tactic/congruence/congruence_closure): name collision, we had congr_lemma_cache in two different modules
2016-12-22 19:35:38 -08:00
Leonardo de Moura
eefd4cd6ab
feat(library/tactic/congruence/congruence_tactics): add missing functions
2016-12-22 18:11:01 -08:00
Leonardo de Moura
f777aafa4e
feat(library/init/meta,library/tactic/congruence): add congruence closure lean API
2016-12-22 16:26:17 -08:00
Leonardo de Moura
d16a3df7a3
feat(library/tactic/congruence): initialization and pretty printing
2016-12-22 15:18:52 -08:00
Leonardo de Moura
6bc0952dbc
feat(library/tactic/congruence/congruence_closure): generate lazy eq_true proofs
2016-12-22 14:44:38 -08:00
Leonardo de Moura
f7dce940b6
feat(library/tactic/congruence/congruence_closure): proof generation
2016-12-22 14:23:33 -08:00
Daniel Selsam
49de5313fa
chore(library/tactic/change_tactic.cpp): better formatting for error message
2016-12-22 11:13:54 -08:00
Leonardo de Moura
60d3255577
fix(library/type_context): issue #1258 again
...
This is yet another fix.
2016-12-22 10:51:16 -08:00
Leonardo de Moura
49e296dee2
fix(library/type_context, library/tactic/induction_tactic): fix for issue #1258 was incorrect
...
The fix was incorrect because it could produce an invalid local context.
Actually, the regression tests/lean/run/1258.lean was producing an
assertion violation.
2016-12-21 21:13:29 -08:00
Leonardo de Moura
48cd421852
feat(library/tactic/congruence): add congruence closure basics
2016-12-21 20:46:25 -08:00
Leonardo de Moura
cc077554b5
fix(library/tactic/change_tactic): use id_locked in the change tactic to create checkpoint
...
closes #1260
2016-12-21 11:29:03 -08:00
Gabriel Ebner
a26e2c9108
feat(library/module): intermediary data structure for environment modifications
2016-12-20 10:15:19 -08:00
Leonardo de Moura
516f45428d
fix(library/tactic/simplify): missing clear cache operation
2016-12-19 21:32:46 -08:00
Leonardo de Moura
45efccd53e
fix(library/tactic/tactic_state): goal pp problem reported by Jared
2016-12-19 20:32:44 -08:00
