Commit graph

1180 commits

Author SHA1 Message Date
Leonardo de Moura
e17ba27596 fix(library/tactic/rewrite_tactic): adjust the behavior of class resolution in rewriter
The solution is not very satisfactory. I should investigate it more.
2015-02-05 19:08:47 -08:00
Leonardo de Moura
e097977bac test(tests/lean/run): add more rewrite tactic tests 2015-02-05 14:09:07 -08:00
Leonardo de Moura
ffe0d1186e feat(library/tactic/rewrite_tactic): add "reduce_to" step at rewrite tactic 2015-02-05 13:59:55 -08:00
Leonardo de Moura
116c65bff5 feat(library/tactic/rewrite_tactic): add reduction step to rewrite tactic 2015-02-05 13:42:50 -08:00
Leonardo de Moura
808521223b feat(library/tactic/rewrite_tactic): support constant unfolding in rewrite tactic 2015-02-05 12:58:30 -08:00
Leonardo de Moura
1b73764ad3 fix(tests/lean/run/elim2): adjust test to reflect recent changes 2015-02-05 10:54:00 -08:00
Leonardo de Moura
d6958be7e7 fix(library/tactic/location): replace cache must not be used when only a subset of all occurrences should be replaced at replace_occurrences 2015-02-05 10:50:40 -08:00
Leonardo de Moura
dfad24e3f5 feat(frontends/lean): polish rewrite tactic notation 2015-02-05 10:15:58 -08:00
Leonardo de Moura
0abfa30ead fix(library/tactic/rewrite_tactic): elaboration bug in the rewrite tactic steps/elements 2015-02-05 10:01:18 -08:00
Leonardo de Moura
15efadfbdc feat(frontends/lean/parse_rewrite_tactic): cleanup rewrite tactic notation
Make a rewrite command sequence explicit.
2015-02-04 20:16:24 -08:00
Leonardo de Moura
14c72e82f6 feat(library/tactic/rewrite_tactic): add support for rewriting hypotheses 2015-02-04 20:04:19 -08:00
Leonardo de Moura
90eb5c8ca5 test(tests/lean/hott): add test for rewriter in the HoTT version 2015-02-04 19:33:08 -08:00
Leonardo de Moura
61a029d9df fix(tests/lean/rewrite_loop): notation 2015-02-04 19:21:26 -08:00
Leonardo de Moura
d0171ffe7a test(tests/lean/run): add more rewrite tactic examples 2015-02-04 19:19:46 -08:00
Leonardo de Moura
89fde9d829 feat(library/tactic/rewrite_tactic): add maximum number of iterations threshold to rewrite tactic
The idea is to avoid nontermination.
2015-02-04 16:13:15 -08:00
Leonardo de Moura
0c8eaa38c8 test(tests/lean/run): add basic rewriter test 2015-02-04 15:30:18 -08:00
Leonardo de Moura
2a6ccb252e test(tests/lean/extra): add regression tests for issue #422 2015-02-04 10:55:03 -08:00
Leonardo de Moura
f79f43c702 refactor(library/match): use "special" meta-variables instead of free variables to represent placholders in the higher-order matcher 2015-02-03 15:15:04 -08:00
Leonardo de Moura
10357f3f53 fix(tests/lean/nonexhaustive): remove line "warning: imported file uses 'sorry'" from test produced output 2015-02-01 21:25:52 -08:00
Leonardo de Moura
36cfb7fac0 test(tests/lean/bad_set_option): add tests for bad 'set_option' command 2015-02-01 20:20:35 -08:00
Leonardo de Moura
9d1e312c12 test(tests/lean/extra): add extra tests for 'print' command 2015-02-01 20:20:26 -08:00
Leonardo de Moura
ed85ac254a test(tests/lean): add more tests for error messages 2015-02-01 20:04:22 -08:00
Leonardo de Moura
3f37c0e739 test(tests/lean/run): add 'export' command test 2015-02-01 19:57:26 -08:00
Leonardo de Moura
7d9d89bae6 test(tests/lean/extra): add test for saving recursive equation pre-terms 2015-02-01 19:49:14 -08:00
Leonardo de Moura
2403d555ee test(tests/lean/bad_eqns): add tests for definition package error messages 2015-02-01 19:36:06 -08:00
Leonardo de Moura
6cd4972a84 fix(tests/lean): adjust tests to reflect changes in the standard library 2015-02-01 11:36:38 -08:00
Leonardo de Moura
15716c1471 feat(frontends/lean/calc_proof_elaborator): reject proofs with metavariables in the calc-assistant 2015-02-01 11:11:27 -08:00
Leonardo de Moura
143143e94c fix(library/tactic/inversion_tactic): missing normalization step in the inversion_tactic 2015-02-01 10:38:30 -08:00
Leonardo de Moura
d52af105d7 feat(frontends/lean/decl_cmds): allow many constants to be set in the same attribute command 2015-01-31 23:55:14 -08:00
Leonardo de Moura
ea9a9d63d1 test(tests/lean): add tests for structure command error messages 2015-01-30 09:52:42 -08:00
Leonardo de Moura
7c59c959db fix(tests/lean/interactive): do not compare output of trace using non-deterministic commands such as "WAIT ms" 2015-01-30 09:52:42 -08:00
Leonardo de Moura
e75828b756 test(tests/lean/interactive): add tests for options structure.eta_thm and structure.proj_mk_thm 2015-01-29 16:52:23 -08:00
Leonardo de Moura
e9d8a960d9 test(tests/lean/interactive): add test for proof_state info 2015-01-29 16:44:10 -08:00
Leonardo de Moura
c74da8bea2 test(tests/lean/interactive): add tests for coercion and overload info 2015-01-29 16:39:27 -08:00
Leonardo de Moura
f04e462bf3 test(tests/lean/interactive): add more tests for lean server 2015-01-29 16:30:07 -08:00
Leonardo de Moura
e9e1f86b7f fix(library/app_builder): many bugs, add use_cache option, add tests 2015-01-29 15:30:31 -08:00
Leonardo de Moura
5bb2a41c64 feat(library/reducible): expose Lua API for reducible hints 2015-01-29 10:37:15 -08:00
Leonardo de Moura
e4b5e07498 fix(frontends/lean/elaborator): apply substitution before compiling pre-tactics into tactics
closes #415
2015-01-28 13:32:56 -08:00
Leonardo de Moura
94519b48b1 fix(tests/lean): adjust tests to reflect changes in the standard library 2015-01-27 11:37:17 -08:00
Leonardo de Moura
ad4c7c20f9 fix(kernel/inductive/inductive): fix assertion violation when K is applied to type incorrect term 2015-01-27 11:22:14 -08:00
Leonardo de Moura
e2c41fca75 feat(frontends/lean): modify syntax for local notation
The idea is to make it uniform with the syntax for defining local
attributes.
2015-01-26 11:51:17 -08:00
Leonardo de Moura
b4d6f6e3ed feat(frontends/lean): 'attribute' command is persistent by default 2015-01-26 11:51:17 -08:00
Leonardo de Moura
a1eeb0a6a1 fix(library/print): typo in is_used_name
closes #408
2015-01-25 08:58:08 -08:00
Leonardo de Moura
4f2e0c6d7f refactor(frontends/lean): add 'attribute' command
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
2015-01-24 20:23:21 -08:00
Leonardo de Moura
b5c4e603db feat(frontends/lean): allow parameters to be used in sections
Restriction:
- coercions and notations cannot be defined in parametric sections

closes #401
2015-01-23 17:42:19 -08:00
Leonardo de Moura
42b5b1e679 test(tests/lean): add new test for scoping rules 2015-01-22 11:41:19 -08:00
Leonardo de Moura
880faf89e0 feat(frontends/lean/structure_cmd): add implicit_infer_kind annotation to structure command
closes #354
2015-01-21 18:12:29 -08:00
Leonardo de Moura
12674114a4 feat(shell): set default behavior to "trusted"
closes #402
2015-01-21 16:25:09 -08:00
Leonardo de Moura
260795f981 fix(frontends/lean/structure_cmd): collect universe levels that only occur in structure parameters
fixes #395
2015-01-19 22:18:09 -08:00
Leonardo de Moura
002050fa97 feat(frontends/lean): increase binding power of ! and @
Remark: I did not add the constant "app".
Reason: It would break the standard library in many places.
Moreover, the current "max" is not just the binding power of
application, but also the binding power of identifiers, (, [, ...
It would be weird to call it "app"

closes #388
2015-01-19 18:40:33 -08:00
Leonardo de Moura
6fd0d452d3 test(tests/lean/run): adjust tests to reflect recent changes 2015-01-19 18:00:14 -08:00
Leonardo de Moura
edcc92d9c7 feat(frontends/lean): remove 'using' from structure instance command 2015-01-17 09:38:10 -08:00
Leonardo de Moura
fed96c9e0b test(tests/lean/run): add structure instance example 2015-01-17 09:27:15 -08:00
Leonardo de Moura
f9d7480f5c feat(frontends/lean): notation for creating structure instances 2015-01-16 17:14:30 -08:00
Leonardo de Moura
bfd679d52d feat(frontends/lean/structure_cmd): allow user to reference parent structures when defining new fields
See new test for an example.

closes #371
2015-01-16 13:04:48 -08:00
Leonardo de Moura
6c07ca5d41 perf(library/print): improve is_used_name 2015-01-15 19:01:13 -08:00
Leonardo de Moura
91366c989d test(tests/lean/run/finbug): add problematic definition test 2015-01-13 18:49:37 -08:00
Leonardo de Moura
37e852ba61 feat(frontends/lean/elaborator): improve error message for metavariable in inaccessible position on equation lhs 2015-01-13 14:38:25 -08:00
Leonardo de Moura
e5a8c67d22 fix(library/definitional/equations): assertion violation 2015-01-13 11:57:14 -08:00
Leonardo de Moura
1fbfe59a9a feat(library/tactic/goal): when listing context/goal variables, collect vars of same type in one line
closes #391
2015-01-13 11:14:44 -08:00
Leonardo de Moura
75d7e4ab9e feat(frontends/lean): add 'end' token to match expressions 2015-01-10 12:35:29 -08:00
Leonardo de Moura
d6eccd7c18 test(tests/lean/run): add match test 2015-01-10 10:43:24 -08:00
Leonardo de Moura
b172229a72 feat(frontends/lean): add 'match' expressions
We reuse the equations infrastructure to compile them.
2015-01-10 10:11:13 -08:00
Leonardo de Moura
6df9ffe5f6 fix(frontends/lean/elaborator): solve placeholders before invoking equantions compiler 2015-01-10 09:18:27 -08:00
Leonardo de Moura
a3bc1b0cd5 fix(library/definitional/equations): add more equation validation to avoid obscure error message 2015-01-09 18:52:21 -08:00
Leonardo de Moura
2e4a2451e6 refactor(library/reducible): simplify reducible/irreducible semantics 2015-01-08 18:52:18 -08:00
Leonardo de Moura
0ffb7c080f fix(tests/lean/run/inv_bug2): adjust test to reflect changes at data.vector 2015-01-08 12:11:52 -08:00
Leonardo de Moura
698754b2bb feat(library/definitional/equations): display elaborated equation lhs's when there are missing cases 2015-01-08 12:00:47 -08:00
Leonardo de Moura
4e49e73585 refactor(library/init/logic): add inhabited related functions, rename inhabited.default to default 2015-01-07 18:45:58 -08:00
Leonardo de Moura
1fab144aa7 refactor(library/init/nat): rename constants
closes #387
2015-01-07 18:26:51 -08:00
Jeremy Avigad
50f03c5a09 refactor(library/data/nat/order): make nat order an instance of linear_ordered_semigroup, rename various theorems 2015-01-07 18:18:28 -08:00
Leonardo de Moura
a3a6697f44 feat(library/definitional/equations): mutually recursive functions for mutually recursive datatypes 2015-01-06 14:07:17 -08:00
Leonardo de Moura
fb1cb3c623 test(tests/lean/run): define tree_list length function using recursive equations
tree_list is part of a mutually inductive datatype.
2015-01-06 11:57:34 -08:00
Leonardo de Moura
559ee3e3e1 fix(util/buffer): bug in expand method
fixes #385
2015-01-06 11:42:40 -08:00
Leonardo de Moura
6451cad38d test(tests/lean/run): define list head using recursive equations 2015-01-05 19:50:34 -08:00
Leonardo de Moura
3325d791de fix(library/definitional/equations): bug in recursive application elimination 2015-01-05 17:17:14 -08:00
Leonardo de Moura
cbae6a2ca0 test(tests/lean/run): define list filter function using recursive equations 2015-01-05 17:05:01 -08:00
Leonardo de Moura
a24a7f7fa1 test(tests/lean/run) define vector last and unzip functions using recursive equations 2015-01-05 17:04:55 -08:00
Leonardo de Moura
eedc31f7e9 fix(library/definitional/equations): bug in "complete" transition 2015-01-05 16:27:29 -08:00
Leonardo de Moura
3889b60152 feat(library/definitional/equations): allow inductive datatype parameters in recursive equations 2015-01-05 15:56:28 -08:00
Leonardo de Moura
d8f3bcec67 feat(library/init/logic): add 'arbitrary'
It is identical to default, but it is opaque.
That is, when we use 'arbitrary A', we cannot rely on the particular
value selected.
2015-01-05 13:27:09 -08:00
Leonardo de Moura
0d84943d52 test(tests/lean/run): show that nat has decidable equality using recursive equations 2015-01-05 12:41:18 -08:00
Leonardo de Moura
fd332e411d test(tests/lean/run): add more overlapping patterns examples 2015-01-05 12:25:14 -08:00
Leonardo de Moura
b46c377aa2 feat(library/definitional/equations): add "complete" transition for overlapping patterns 2015-01-05 11:49:27 -08:00
Leonardo de Moura
fdef3e5407 feat(library/definitional/equations): add support for reflexive datatypes in the definitional package 2015-01-05 11:13:35 -08:00
Leonardo de Moura
5e228d92d2 fix(library/definitional/equations): missing case 2015-01-04 20:49:53 -08:00
Leonardo de Moura
f07475667b test(tests/lean/run): define vector map using recursive equations 2015-01-04 19:56:50 -08:00
Leonardo de Moura
7ff03e2846 test(tests/lean/run): define vector diagonal using recursive equations 2015-01-04 17:58:35 -08:00
Leonardo de Moura
7488378445 test(tests/lean/run): define list append using recursive equations 2015-01-04 17:58:24 -08:00
Leonardo de Moura
7fca862fc3 test(tests/lean/run): define fibonacci using recursive equations 2015-01-04 17:47:18 -08:00
Leonardo de Moura
faf78ce3e6 feat(library/definitional/equations): brec_on compilation 2015-01-04 17:45:13 -08:00
Leonardo de Moura
5bf8141af2 test(tests/lean/hott): add test to demonstrate limitations of the current compilation procedure 2015-01-02 23:18:35 -08:00
Leonardo de Moura
92b6c06a21 test(tests/lean/run): add basic pattern matching compilation test 2015-01-02 22:22:20 -08:00
Leonardo de Moura
c66826787a test(tests/lean/run): add basic pattern matching compilation test 2015-01-02 22:07:31 -08:00
Leonardo de Moura
7f7d318b22 feat(library/definitional/equations): add dependent pattern matching compilation 2015-01-02 22:06:40 -08:00
Jeremy Avigad
1eea75b6fc fix(library/data/nat/div,tests/lean/run/ppbeta): make decidable for dvd transparent, name change in ppbeta 2014-12-26 16:44:43 -05:00
Jeremy Avigad
25394dddb7 refactor(library): change mul.left_id to mul_one, and similarly for mul.right_id, add.left_id, add.right_id 2014-12-23 21:14:36 -05:00
Jeremy Avigad
486bc321ff refactor(library/data/nat): rename theorems 2014-12-23 21:14:35 -05:00
Leonardo de Moura
2be83fbff7 test(tests/lean): remove data.nat dependency 2014-12-23 17:42:56 -08:00
Leonardo de Moura
264c88d332 test(tests/lean/hott): add tele_eq example using HoTT library 2014-12-22 09:43:16 -08:00