michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
8176 commits 3 branches 0 tags 28 MiB
Commit graph

2296 commits

Author SHA1 Message Date
Leonardo de Moura
9a1a9f3b5a refactor(library/fun_info_manager): use expr_unsigned_map 2016-01-06 17:29:22 -08:00
Leonardo de Moura
7312dd77b8 refactor(library/congr_lemma_manager): move expr_unsigned_map to separate module 2016-01-06 17:29:16 -08:00
Leonardo de Moura
43c5cbd1bf feat(library/fun_info_manager): more general fun_info_manager 2016-01-06 17:29:10 -08:00
Leonardo de Moura
3ca785b0e7 refactor(library/fun_info_manager): remove dead code 2016-01-06 17:29:02 -08:00
Leonardo de Moura
a992bb46a6 feat(library/fun_info_manager): update interface 2016-01-06 17:28:52 -08:00
Rob Lewis
a57b7fadfb style(replace_tactic): remove extra whitespace 2016-01-04 15:10:51 -05:00
Rob Lewis
031831f101 feat(library/tactic): add replace tactic 2016-01-04 14:43:31 -05:00
Leonardo de Moura
ba392f504f feat(kernel/expr,library/blast/blast,frontends/lean/decl_cmds): add workaround for allowing users to use blast inside of recursive equations 2016-01-03 21:53:31 -08:00
Leonardo de Moura
4478d570bd chore(library/congr_lemma_manager): fix style 2016-01-03 18:02:50 -08:00
Leonardo de Moura
19ebedd480 feat(library/type_context): improve type_context get_level_core, add virtual method for checking types whenever a metavariable is assigned 
We add an example where app_builder fails without these new features.
That is, app_builder fails to solve the unification problem.
 2016-01-03 17:58:27 -08:00
Leonardo de Moura
fcf532ea67 chore(library/app_builder): fix typo in trace message 2016-01-03 15:16:50 -08:00
Leonardo de Moura
d0fe59ef8a feat(library/congr_lemma_manager): add new kind of congr_arg 2016-01-03 15:10:07 -08:00
Leonardo de Moura
67d49aabd9 chore(library/congr_lemma_manager): document main methods 2016-01-03 14:39:34 -08:00
Leonardo de Moura
66a722ff5a feat(library/unifier): remove "eager delta hack", use is_def_eq when delta-constraint does not have metavariables anymore 
The "eager-delta hack" was added to minimize problems in the interaction
between coercions and delta-constraints.
 2016-01-03 12:39:32 -08:00
Leonardo de Moura
d02ead320a feat(library/unifier): remove unifier.computation option 2016-01-03 11:00:16 -08:00
Leonardo de Moura
9935cbc3d7 feat(library/blast/blast): communicate assigned metavariables back to tactic framework 
We need this feature to be able to solve (input) goals containing
metavariables using blast.
See new test for example.
 2016-01-02 20:05:44 -08:00
Leonardo de Moura
56d9b6b0d3 fix(library/blast/blast): convert uref and mref back into tactic metavariables 2016-01-02 19:23:04 -08:00
Leonardo de Moura
d85b4300b1 fix(library/blast/blast): bug at visit_meta_app 2016-01-02 19:08:56 -08:00
Leonardo de Moura
4eb2690c32 feat(library/scoped_ext): store set of opened namespaces 2016-01-02 13:35:08 -08:00
Leonardo de Moura
155df48665 feat(library): remove decl_stats 
We are not using (and will not use) this module in the blast proof procedures
 2016-01-02 13:00:43 -08:00
Leonardo de Moura
3c564fcc55 fix(library/user_recursors): 'print recursor-lemma' command 2016-01-01 18:12:12 -08:00
Leonardo de Moura
0963ce336f feat(library/blast): add 'grind' and 'grind_simp' blast strategies 
The use [intro] [intro!] [elim] [simp] lemmas.
The [simp] lemmas are only used by grind_simp.
 2016-01-01 17:32:13 -08:00
Leonardo de Moura
57c9ced111 feat(library/blast): add fail_action and fail_strategy helper functions 2016-01-01 17:18:05 -08:00
Leonardo de Moura
cd7708d556 feat(library/blast/backward/backward_strategy): add extensible backward chaining strategy 2016-01-01 17:07:15 -08:00
Leonardo de Moura
43f0183ce9 feat(library/blast/backward/backward_strategy): allow user to control the number of nested backward chaining steps 2016-01-01 16:46:49 -08:00
Leonardo de Moura
ac9d6c2021 refactor(library/data/bool): cleanup bool proofs and fix bxor definition 2016-01-01 13:52:42 -08:00
Leonardo de Moura
52ec7e6d57 feat(library/blast/recursor): add 'blast.recursor.max_rounds' options and iterative deepening for recursor_strategy 2016-01-01 13:09:37 -08:00
Leonardo de Moura
1bb21d202b refactor(library/blast): move recursor action and strategy to its own directory 2016-01-01 12:49:49 -08:00
Leonardo de Moura
317c32a7e2 fix(library/blast/state): avoid duplicated names at state::to_goal 2016-01-01 00:10:54 -08:00
Leonardo de Moura
712e19e22a fix(library/blast/forward/ematch): bug in the ematching procedure 2015-12-31 21:26:44 -08:00
Leonardo de Moura
54f2c0f254 feat(library/blast/forward): inst_simp should use the left-hand-side as a pattern (if none is provided by the user) 
The motivation is to reduce the number of instances generated by ematching.

For example, given

   inv_inv:  forall a, (a⁻¹)⁻¹ = a

the new heuristic uses ((a⁻¹)⁻¹) as the pattern.
This matches the intuition that inv_inv should be used a simplification
rule.

The default pattern inference procedure would use (a⁻¹). This is bad
because it generates an infinite chain of instances whenever there is a
term (a⁻¹) in the proof state.
By using (a⁻¹), we get
   (a⁻¹)⁻¹ = a
Now that we have (a⁻¹)⁻¹, we can match again and generate
   ((a⁻¹)⁻¹)⁻¹ = a⁻¹
and so on
 2015-12-31 20:20:39 -08:00
Leonardo de Moura
03f9e9acb0 feat(library/blast/forward): display lemma name when printing instance 2015-12-31 18:13:59 -08:00
Leonardo de Moura
c3dfabf741 feat(library/blast/strategies/portfolio): add 'rec_simp' 
recursors followed by simplification
 2015-12-31 15:00:38 -08:00
Leonardo de Moura
4134fdd925 feat(library/blast/strategies/rec_strategy): give priority to user defined recursors 2015-12-31 14:55:00 -08:00
Leonardo de Moura
76677c4535 feat(library/blast/actions/assert_cc_action): add target_cc_action 2015-12-31 14:53:55 -08:00
Leonardo de Moura
fdcdfbf385 feat(library/blast/simplifier/simplifier_actions): only add symplified hypothesis if it is not "true" 2015-12-31 14:25:38 -08:00
Leonardo de Moura
b35abcc6a8 refactor(library): rename strategy "msimp" ==> "inst_simp" 
"inst_simp" means "instantiate simplification lemmas"
The idea is to make it clear that this strategy is *not* a simplifier.
 2015-12-31 12:45:48 -08:00
Leonardo de Moura
4cf5c77575 feat(library/blast/strategies): add strategy for applying recursors 2015-12-31 12:35:16 -08:00
Leonardo de Moura
20b585c432 feat(library/blast/forward/ematch): use blast.event.ematch for ematch module abnormal behavior 2015-12-31 12:28:22 -08:00
Leonardo de Moura
935a2536ec fix(library/blast/actions/recursor_action): must normalize target for each subgoal 2015-12-31 12:25:17 -08:00
Leonardo de Moura
ba2cdc848a feat(library/util, library/pp_options): add pp.goal.max_hypotheses 
This commit also renames pp.compact_goals ==> pp.goal.compact
 2015-12-30 12:43:03 -08:00
Leonardo de Moura
23836f53bb feat(library/blast): do not display inactive hypotheses when displaying failure states 2015-12-30 12:08:33 -08:00
Leonardo de Moura
f2d4e81889 fix(library/blast/state): inactive hypotheses should be printed "after" active ones 2015-12-30 11:46:41 -08:00
Leonardo de Moura
2a454ce791 chore(library/blast/state): do not display set of active hypotheses 
This is just "noise" in error messages
 2015-12-30 11:31:59 -08:00
Leonardo de Moura
251b53c669 refactor(library/blast/strategies): rename 'debug_action_strategy' to 'action_strategy' 
Now, we can also provide a "name" for tracing purposes when
instantiating action_strategy.
 2015-12-29 20:45:24 -08:00
Leonardo de Moura
41a01bb606 feat(library/blast/forward/ematch): add option 'blast.ematch.max_instances' 2015-12-29 20:36:11 -08:00
Leonardo de Moura
0148bb08fd feat(library/blast): add 'ematch_simp' strategy for blast and msimp shortcut for it. 
This strategy is based on ematching and congruence closure, but it uses
the [simp] lemmas instead of [forward] lemmas.
 2015-12-29 20:04:31 -08:00
Leonardo de Moura
86a5379a96 feat(library/blast): include strategies failure states in the tactic_exception 
Reason: better flycheck error messages
 2015-12-29 17:14:55 -08:00
Leonardo de Moura
b92416d66c refactor(library/error_handling): move error_handling to library main dir 2015-12-29 15:31:40 -08:00
Leonardo de Moura
b117a10f82 refactor(library/blast/simplifier): use priority_queue to store simp/congr lemmas, use name convention used at forward/backward lemmas, normalize lemmas when blast starts, cache get_simp_lemmas 2015-12-28 17:52:57 -08:00