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

2268 commits

Author SHA1 Message Date
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
Leonardo de Moura
5b7dc31ad1 chore(library/blast/backward): remove unnecessary include 2015-12-28 14:26:18 -08:00
Leonardo de Moura
079a25f770 refactor(library/blast/forward): make sure backward and forward modules use same naming convention 2015-12-28 12:37:16 -08:00
Leonardo de Moura
482ffe4242 fix(library/attribute_manager): memory leak 2015-12-28 12:31:38 -08:00
Leonardo de Moura
c8b9c98eb6 refactor(library/blast/backward): use priority_queue, make sure head is normalized when building index 2015-12-28 12:26:06 -08:00
Leonardo de Moura
26d0a62052 refactor(*): make sure we use LEAN_DEFAULT_PRIORITY 
We recently implemented the attribute manager.
 2015-12-28 10:47:56 -08:00
Leonardo de Moura
f177082c3b refactor(*): normalize metaclass names 
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).

Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write

   definition foo [coercion] ...
   definition bla [forward] ...

and

  open [coercion] nat
  open [forward] nat

It is easier to remember and is uniform.
 2015-12-28 10:39:15 -08:00
Leonardo de Moura
89a5d00714 chore(library/blast): style 2015-12-28 09:08:18 -08:00
Leonardo de Moura
2a5a904416 feat(library/blast/discr_tree): remove hack for setting m_fn flag 2015-12-28 09:08:18 -08:00
Leonardo de Moura
93b912ec89 feat(library/blast): use discrimination trees instead of head_map for indexing hypotheses 2015-12-28 09:08:18 -08:00
Leonardo de Moura
1f1fafd535 feat(library/blast/discr_tree): erase operation 2015-12-28 09:08:18 -08:00
Leonardo de Moura
45c29d422f feat(library/blast/discr_tree): set edge m_fn flag 2015-12-28 09:08:18 -08:00
Leonardo de Moura
43e1292f22 feat(library/blast): add discrimination trees 2015-12-28 09:08:17 -08:00
Leonardo de Moura
a7d1625765 fix(library/blast/forward/forward_lemma_set): check pattern inference when setting attribute 2015-12-17 22:50:14 -08:00
Leonardo de Moura
128b557d37 refactor(frontends/lean): use attribute_manager to simplify decl_attributes 2015-12-17 22:28:53 -08:00
Leonardo de Moura
d81b2d0f29 feat(library/attribute_manager, frontends/lean/builtin_cmds): use attribute manager information when pretty print definitions 2015-12-17 21:16:31 -08:00
Leonardo de Moura
45dbf76df9 refactor(library): add attribute manager 2015-12-17 20:58:15 -08:00
Leonardo de Moura
61ecf018e9 feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ... 2015-12-17 12:18:32 -08:00
Leonardo de Moura
c824a0e050 chore(library,hott): enforce naming conventions 2015-12-17 11:36:58 -08:00
Leonardo de Moura
70f71a18c8 doc(library/type_context): explain why we need tmp_local_generator 2015-12-15 18:58:07 -08:00
Leonardo de Moura
73b28c91a6 fix(library/type_context): local constant management bug 2015-12-15 18:49:26 -08:00
Leonardo de Moura
1387cdfa0f feat(library/type_context): add eta-expansion to type_context 2015-12-15 17:24:53 -08:00
Leonardo de Moura
10273bf176 feat(library/blast/forward/pattern): improve pattern inference heuristic 2015-12-15 12:55:43 -08:00
Rob Lewis
ec5990f4de fix(library/norm_num): fix incorrect assert 2015-12-14 14:09:54 -05:00
Sebastian Ullrich
2185ee7e95 feat(library/tactic): make let tactic transparent, introduce new opaque note tactic 
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
 2015-12-14 10:14:02 -08:00
Leonardo de Moura
95fba3dba6 chore(library/constants): sort constant decls 2015-12-13 21:39:45 -08:00
Leonardo de Moura
193a9d8cde refactor(library/norm_num): avoid manual constant name initialization 
@rlewis1988 We group all Lean constants used in the C++ code at
src/library/constants.txt

Jeremy and Floris check this file before renaming constants in the
library. So, they can quickly decide whether C++ code will be affected
or not.

We also have a python script for initializing the C++ name objects.
To use the script:
   - go to src/library
   - execute
       python ../../script/gen_constants_cpp.py constants.txt

It will create the boring initialization and finalization code, and
declare a procedure get_<id>_name() for each constant in the file constants.txt.

I also move the norm_num1.lean to the set of unit tests that are
executed whenever we push a commit to the main branch.

I found an assertion violation at line 606. Could you take a look?

Best,
Leo
 2015-12-13 21:38:59 -08:00
Leonardo de Moura
727a4f5a3a feat(library/tactic/intros_tactic): use '_' to say that some names are irrelevant in the intro tactic 
See #695
 2015-12-13 16:47:31 -08:00
Leonardo de Moura
d4e49a8434 feat(library/tactic/intros_tactic): intro without argument should introduce a single variable 
see #695
 2015-12-13 16:28:39 -08:00