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

933 commits

Author SHA1 Message Date
Leonardo de Moura
cb02d1deae feat(library/blast/congruence_closure): add support for specialized congr lemmas in the congruence closure module 2016-01-06 17:30:20 -08:00
Leonardo de Moura
c9930d0a29 feat(library/blast/simplifier/simplifier): subsingleton normalization for application arguments and lambdas 2016-01-06 17:30:08 -08:00
Leonardo de Moura
f3b8aef24c feat(library/fun_info_manager,library/congr_lemma_manager,blast/simplifier): specialized congruence lemmas 
We still need a lot of polishing.
 2016-01-06 17:29:35 -08: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
Jeremy Avigad
a22346e411 fix(lean/tests/lean/run/new_obtain{3,4}): adapt tests to new notation for image 2016-01-03 18:52:25 -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
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
17a2f1fe47 chore(tests/lean/run/blast_grind1): use 'core_grind' 
Reason: we will change the semantics of 'grind'
 2016-01-01 16:46:15 -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
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
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
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
96bec8b4f9 fix(frontends/lean/builtin_cmds): allow token and metaclass to have the same name 2015-12-28 09:57:45 -08:00
Leonardo de Moura
fe66e2aa4a fix(tests/lean): subtype notation is not in the top-level anymore 2015-12-28 09:04:11 -08:00
Leonardo de Moura
2502039a5c fix(frontends/lean/parser): tactic notation that may take numerical parameters 2015-12-17 11:27:31 -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
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
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
e3a35ba4fd feat(frontends/lean): add 'with_attributes' tactical 
closes #494
 2015-12-13 18:27:44 -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
Leonardo de Moura
ce622e9179 feat(frontends/lean): add auto-include for structures and inductive decls 2015-12-13 13:39:34 -08:00
Leonardo de Moura
20de22a8ad feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included) 2015-12-13 13:20:54 -08:00
Leonardo de Moura
b6bac2e542 chore(tests/lean/run): adjust tests 2015-12-13 12:23:44 -08:00
Leonardo de Moura
ef546c5c5b refactor(library): use anonymous instance implicit arguments 2015-12-13 11:46:48 -08:00
Leonardo de Moura
b7de10a6d2 feat(library/trace): allow user to disable subclasses of a trace class 
Example:

set_option trace.blast true         -- enables trace.blast class and all subclasses
set_option trace.blast.action false -- disables the given subclass

Result: all blast classes are traced but blast.action
 2015-12-11 11:03:16 -08:00
Leonardo de Moura
a35fd06a33 test(tests/lean/run/blast_simp4): add simp test 2015-12-11 10:23:58 -08:00
Leonardo de Moura
ac0bd539b0 feat(frontends/lean/notation_cmd): allow 'abstract ... end' to be used in notation declarations 
helps #825
 2015-12-11 09:55:27 -08:00
Leonardo de Moura
13f9d8dd6c fix(tests/lean): move hott tests 2015-12-10 10:55:27 -08:00
Leonardo de Moura
8b3cbb8fdd fix(library/tactic/induction_tactic): apply substitution to hypothesis type (it may contain metavars) 
closes #876
 2015-12-10 10:11:55 -08:00
Leonardo de Moura
50323e5b14 fix(tests/lean/run/simplifier1): option name 2015-12-09 12:30:20 -08:00
Leonardo de Moura
bed03272f5 fix(tests/lean/run/blast_cc1): option name 2015-12-09 12:23:00 -08:00
Leonardo de Moura
3f9549485f feat(frontends/lean/parser): restore config options in the end of sections/namespaces 2015-12-09 11:24:37 -08:00
Leonardo de Moura
273f6fc04c fix(tests/lean/run): new option names 2015-12-08 20:06:43 -08:00
Leonardo de Moura
b145a7332a feat(library/blast/congruence_closure): use new tracing infrastructure 2015-12-08 15:18:21 -08:00
Leonardo de Moura
7da64a768f refactor(library/type_context): with the new tracing infrastructure, type_context doesn't need an io_state 2015-12-08 14:58:08 -08:00
Leonardo de Moura
50df6b5698 feat(frontends/lean): rename '[intro]' ==> '[intro!]' and '[backward]' ==> '[intro]' 2015-12-07 21:33:35 -08:00
Leonardo de Moura
041c1cbb17 feat(library/blast): add strategies "grind" and "core_grind" 2015-12-07 20:30:59 -08:00
Leonardo de Moura
af7ffcf575 chore(tests/lean/run/blast_meta_bug): use "ematch" strategy in the test 2015-12-07 12:23:01 -08:00
Leonardo de Moura
121648dda6 fix(library/congr_lemma_manager): issue with reducible annotation when generating congruence lemmas 2015-12-07 12:09:30 -08:00
Leonardo de Moura
f31553d916 feat(library/blast/strategies/portfolio): add more strategies for debugging purposes 2015-12-07 11:59:21 -08:00
Leonardo de Moura
54c0921bbb feat(library/blast/forward/pattern): consider patterns with nested lambdas in the pattern inference procedure 2015-12-07 10:39:42 -08:00
Leonardo de Moura
85379b7706 feat(library/blast/actions/simple_actions): make sure contradiction action works even if classical logic support is not enabled 
not (not (not a)) -> not a
 2015-12-07 09:30:14 -08:00
Leonardo de Moura
c7390684ba feat(library/blast/strategies/portfolio): add 'unit' strategy for testing unit propagation 2015-12-07 08:45:54 -08:00
Leonardo de Moura
bccf716fd5 chore(tests/lean/run/blast_unit): remove reducible-not tests 2015-12-07 08:44:09 -08:00
Leonardo de Moura
2d007c7c23 feat(library/blast/simplifier/simp_rule_set): rename metaclass to '[simps]' 
The previous name [rrs] was too cryptic.
 2015-12-06 20:49:27 -08:00
Leonardo de Moura
1eb28b842e feat(library/blast/simplifier): add eta-reduction to simplifier 2015-12-06 20:41:25 -08:00
Leonardo de Moura
b044f9e8c1 feat(library/blast/strategies): add "ematch" strategy for testing ematching 2015-12-06 15:01:49 -08:00
Leonardo de Moura
5626431c7f test(tests/lean/run): use 'simp' when testing the simplifier 2015-12-06 14:35:14 -08:00
Leonardo de Moura
67e291ac84 feat(library/blast/strategies): add strategy for testing congruence closure module 2015-12-06 14:33:21 -08:00
Leonardo de Moura
732a92de05 feat(frontends/lean): add 'simp' as shortcut for 'with_options [blast.strategy "simp"] blast' 2015-12-06 13:14:04 -08:00
Leonardo de Moura
b36ce49f2b fix(tests,doc): adjust tests to changes in the standard library 2015-12-05 23:52:16 -08:00
Leonardo de Moura
648f6c5f82 fix(library/blast/strategies): constructor action was being applied too soon 2015-12-05 19:44:07 -08:00
Leonardo de Moura
ae8efb684e fix(tests/lean/run/blast9): missing option 2015-12-05 19:26:37 -08:00
Leonardo de Moura
aa998bfad3 fix(library/fun_info_manager): reducibility issue 2015-12-05 19:26:06 -08:00
Leonardo de Moura
6193816f6a fix(library/tmp_type_context): bug at pop() 2015-12-05 19:14:33 -08:00
Leonardo de Moura
df567717f8 feat(library/blast/strategies): add 'blast.strategy "preprocess"' 2015-12-05 18:17:15 -08:00
Daniel Selsam
08e0fc796b feat(library/blast/actions): by_contradiction action 2015-12-04 20:19:05 -08:00
Leonardo de Moura
2682fe9525 feat(library/blast/blast): force 'ne' to be always transparent 2015-12-04 18:24:36 -08:00
Leonardo de Moura
5da1b52e47 feat(library/blast/unit/unit_propagate): make sure unif_propagate works even if 'not' is marked as '[reducible]' 2015-12-04 16:49:21 -08:00
Leonardo de Moura
5d38a5a5cd test(tests/lean/run/blast_ematch10): make sure the test is for the cc module 2015-12-04 14:03:51 -08:00
Leonardo de Moura
a8b6a286dd fix(library/app_builder): make sure app_builder works even if iff is marked as reducible 2015-12-04 13:51:56 -08:00
Leonardo de Moura
07cb35fd3c fix(library/abstract_expr_manager): incorrect handling of de-Bruijn variables 2015-12-04 09:27:21 -08:00
Daniel Selsam
6e478696d2 feat(library/blast/unit): preprocessor placeholder 2015-12-04 08:30:04 -08:00
Daniel Selsam
0df4556eb5 feat(library/blast/unit): quantified and non-Prop facts 2015-12-04 08:30:03 -08:00
Daniel Selsam
2bf9989bd9 refactor(library/blast/unit): simplify module 2015-12-04 08:30:03 -08:00
Leonardo de Moura
6bbe72190d fix(library/congr_lemma_manager): bug in congruence lemma generator 2015-12-03 14:21:30 -08:00
Leonardo de Moura
038369533e fix(library/blast/recursor_action): indexed families 2015-12-02 23:43:15 -08:00
Leonardo de Moura
1c1cfdd010 test(tests/lean/run): add Dan's reducible+ematch test 2015-12-02 23:32:43 -08:00
Leonardo de Moura
87995b96e3 fix(library/blast/congruence_closure): is_relation_app ==> is_equivalence_relation_app 2015-12-02 23:28:57 -08:00
Leonardo de Moura
950f356d9a refactor(library/blast,frontends/lean): forward pattern index 2015-12-02 22:52:55 -08:00
Leonardo de Moura
a83a7f8356 feat(library/blast/forward/pattern): remove redundant multi-patterns 2015-12-02 22:52:55 -08:00
Leonardo de Moura
2090e9124c test(tests/lean/run): add more tests from algebra 2015-12-02 22:52:55 -08:00
Leonardo de Moura
48de943678 test(tests/lean/run): add Daniel's example 2015-12-02 22:52:55 -08:00
Leonardo de Moura
4f06e91ce5 test(tests/lean/run): add new test 2015-12-02 22:52:55 -08:00
Leonardo de Moura
1ab39a518f chore(tests/lean/run/blast_ematch5): disable unnecessary options 2015-12-02 22:52:54 -08:00
Leonardo de Moura
32ad59adc1 feat(library/blast/forward/ematch): add support for multi-patterns 2015-12-02 22:52:54 -08:00
Leonardo de Moura
a8bb4ba109 fix(library/blast/congruence_closure): bug in congruence closure proof extraction 2015-12-02 22:52:54 -08:00
Leonardo de Moura
5844e96734 test(tests/lean/run): add basic ematching tests 2015-12-02 22:52:54 -08:00
Leonardo de Moura
08bb966581 feat(library/blast/forward/ematch): generate new instances 2015-12-02 22:52:54 -08:00
Leonardo de Moura
e4e9c30e66 fix(frontends/lean/builtin_cmds): print patterns 2015-12-02 22:52:54 -08:00
Leonardo de Moura
fdd442bd38 feat(frontends/lean/decl_attributes): turn on [forward] if pattern hints have been provided 2015-12-02 22:52:54 -08:00
Leonardo de Moura
41ff4bc193 feat(library/blast/forward/pattern): pattern inference and heuristic instantiation index 2015-11-25 23:45:08 -08:00
Leonardo de Moura
84b54ad027 test(tests/lean/run): disable recursor tactic and add tests for unit+cc 2015-11-25 06:43:48 -08:00
Daniel Selsam
ca71a2eb12 feat(library/blast/unit): conjunctive conclusions 2015-11-24 22:45:39 -08:00
Daniel Selsam
eac1ebbf72 feat(library/blast/unit): propagate clauses 2015-11-24 21:16:01 -08:00
Leonardo de Moura
67a4cd3972 feat(frontends/lean): add print [no_pattern] command 2015-11-24 18:48:22 -08:00
Leonardo de Moura
f4a7268bd7 fix(library/blast/congruence_closure): bug in add_eqv_step 2015-11-23 14:26:33 -08:00
Leonardo de Moura
0bd417bc2a test(tests/lean/run/blast23): missing test 2015-11-22 18:23:01 -08:00
Leonardo de Moura
1bd827dffc feat(library/blast/simplifier/simplifier_actions): add simplify_hypothesis_action 2015-11-22 17:49:00 -08:00
Leonardo de Moura
fc461ce832 feat(library/app_builder): avoid redundant proof terms at mk_of_iff_true and mk_not_of_iff_false 2015-11-22 15:49:17 -08:00
Leonardo de Moura
94f7b7f95d feat(library/blast/congruence_closure): add support for propagating units in the congruence closure module 
See blast_cc12.lean for example.
 2015-11-22 15:39:44 -08:00
Leonardo de Moura
6fc0e41439 fix(library/blast/congruence_closure): proof generation for congruences such as (a = b) <-> (b = a) 
The congruence closure module treats these two terms as the same thing.
So, we should take this into account when building proofs
 2015-11-21 19:50:59 -08:00
Leonardo de Moura
5e9914ef45 feat(library/blast/congruence_closure): avoid eq.rec if major premise is eq.refl 2015-11-21 19:00:16 -08:00
Leonardo de Moura
091b0f0cc7 feat(library/blast): add option for disabling congruence closure 2015-11-21 17:45:25 -08:00