max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
10996 commits 1 branch 0 tags 5.3 GiB
Commit graph

977 commits

Author SHA1 Message Date
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
b8e09bb86e refactor(library/tactic/smt): move ematch Lean bindings to ematch.cpp 2017-01-05 10:35:59 -08:00
Leonardo de Moura
aaffcc59a9 refactor(library/tactic/smt): move hinst_lemma(s) Lean bindings to hinst_lemmas.cpp 2017-01-05 10:30:34 -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
df9ee8be69 chore(library/tactic/smt/hinst_lemmas): style 2017-01-04 20:38:15 -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
7c6f449db0 chore(library/tactic/smt/hinst_lemmas): improve error message 2017-01-04 18:15:15 -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
2e15304f05 feat(frontends/lean): add support for smt_state in the info_manager 2017-01-04 14:23:48 -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
d6ab3739ff refactor(frontends/lean/elaborator): move tactic executation code to tactic_evaluator 2017-01-04 08:42:59 -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
554cef1d36 feat(library/tactic/smt/congruence_closure): propagate disequalities 2017-01-03 14:53:27 -08:00
Leonardo de Moura
34073c6f32 feat(library/tactic/smt/smt_state): improve smt_goal formatting 2017-01-03 13:50:25 -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
d546dc57cd feat(library/tactic/smt/smt_state): use simplifier in the preprocessing step 2017-01-03 11:58:00 -08:00
Leonardo de Moura
78f4ab605e feat(library/tactic/smt): preprocessing configuration options 2017-01-03 11:06:33 -08:00
Leonardo de Moura
7f4693a26d chore(library/vm/vm_nat): add default value at force_to_unsigned 2017-01-03 10:26:36 -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
a7cd840c74 fix(library/tactic/smt/congruence_closure): incorrect condition 2017-01-02 19:33:55 -08:00
Leonardo de Moura
2239791eab fix(library/tactic/smt/congruence_closure): typo 2017-01-02 18:55:45 -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
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
316507081c feat(library/tactic/smt): unit propagation interface 2017-01-02 10:28:26 -08:00
Leonardo de Moura
6e53d73e61 feat(library/tactic/smt): add cc_propagation_handler 2017-01-02 09:58:57 -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
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
Leonardo de Moura
19154e1ff3 chore(library/tactic/smt/smt_state): typo 2017-01-01 10:41:09 -08:00
Leonardo de Moura
d2e935522c feat(library/tactic/smt/smt_state): unique names at intro_all 2017-01-01 09:44:39 -08:00
Leonardo de Moura
35cc334b10 feat(library/init/meta): smt_tactic skeleton 2016-12-31 18:22:23 -08:00
Leonardo de Moura
5f87ec3356 feat(library/tactic): allow user to write their own pretty printer for tactic states 2016-12-30 18:58:50 -08:00
Leonardo de Moura
b86494f0d4 feat(library/tactic): add destruct tactic that is similar to cases, but does not use revert/intro/clear 
This tactic is useful for building more complex tactics using ematch and
cc because it does not invalidate cc_state nor ematch_state.
 2016-12-30 17:05:24 -08:00
Leonardo de Moura
9c069a3eda refactor(library/tactic/congruence): rename directory to smt 2016-12-30 13:15:19 -08:00
Leonardo de Moura
a0e9d38241 feat(library/init/meta/congruence_tactics): allow user to configure congruence_closure module 2016-12-30 12:42:10 -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
73bf232fea fix(library/module): deadlock? 
This commit also undoes the hackish workaround used at e33bd2e665

@gebner Could you please take a quick look at this fix, and check
whether it makes sense?
 2016-12-29 17:56:50 -08:00
Leonardo de Moura
e33bd2e665 chore(library/unfold_macros): checking whether commit 7f86ad64eb broke the remote build 2016-12-29 16:18:13 -08:00
Leonardo de Moura
3faa72de24 chore(library/tactic/ac_tactics): style 2016-12-29 15:36:38 -08:00
Leonardo de Moura
4f463d6b85 fix(library/tactic/congruence/theory_ac): typo 2016-12-29 15:04:04 -08:00
Leonardo de Moura
b3d15b196d feat(library/tactic/ac_tactics,library/tactic/congruence/theory_ac): add superpose transition 2016-12-29 14:54:25 -08:00
Leonardo de Moura
846caf53f7 refactor(library/tactic/ac_tactics,library/tactic/congruence/theory_ac): minimize number of AC macros 2016-12-29 13:15:42 -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
7d17840e3f feat(library/tactic/congruence/theory_ac): add compose transition 2016-12-29 11:11:44 -08:00