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

1358 commits

Author SHA1 Message Date
Leonardo de Moura
923fed8612 fix(frontends/lean/structure_cmd): bug in alias generation in the structure command 
This commit (and 75acb3bc66) closes #443
 2015-02-23 15:17:05 -08:00
Leonardo de Moura
75acb3bc66 fix(frontends/lean/structure_cmd): internal name of parameter/variable was being erased 2015-02-23 15:01:27 -08:00
Leonardo de Moura
7d35d18cad fix(library/tactic/rewrite_tactic): bug when matching terms that expanded into projections 2015-02-22 18:23:10 -08:00
Leonardo de Moura
753b9dcd75 fix(tests/lean/hott): adjust tests to reflect changes in standard library 2015-02-22 09:39:27 -08:00
Leonardo de Moura
33e562a7ce fix(frontends/lean/structure_cmd): effect of "include" command in the structure command 
closes #438
 2015-02-19 22:44:51 -08:00
Leonardo de Moura
421a30d75c feat(library): export [reducible] annotations from function namespace to top-level 
see issue #433
 2015-02-16 18:52:41 -08:00
Leonardo de Moura
7fc216183e feat(library/tactic): produce better error message when a tactic fails 
closes #348
 2015-02-16 18:42:15 -08:00
Leonardo de Moura
461c02d790 fix(tests/lean/hott/433): remove bogus comment, and use rewrite tactic 
Fix an issue raised by Floris.
See discussion at
https://github.com/leanprover/lean/issues/433
 2015-02-16 15:45:31 -08:00
Leonardo de Moura
4248ad644d fix(frontends/lean): priority expressions parser 2015-02-14 12:26:06 -08:00
Leonardo de Moura
5cbdd77ad0 feat(library/tactic/rewrite_tactic): improve matcher in rewrite_tactic 
closes #433
 2015-02-13 12:40:55 -08:00
Leonardo de Moura
8ffadce4ab feat(frontends/lean): add "premise" and "premises" command 
It is just an alternative notation for "variable" and "variables"

closes #429
 2015-02-11 18:46:03 -08:00
Leonardo de Moura
04e92e1e96 feat(frontends/lean/parser): reject explicit universe levels in variables and parameters 
This modification was motivated by issue #427
 2015-02-11 16:25:06 -08:00
Leonardo de Moura
a35cce38b3 feat(frontends/lean): new semantics for "protected" declarations 
closes #426
 2015-02-11 14:09:25 -08:00
Leonardo de Moura
eceed03044 feat(frontends/lean): add "except" notation for "open" command, allow multiple metaclasses to be opened in a single "open" command 2015-02-11 11:02:59 -08:00
Leonardo de Moura
1832fb6f54 feat(*): uniform metaclass names, metaclass validation at 'open' command 2015-02-11 10:35:04 -08:00
Leonardo de Moura
9d1cd073c5 feat(frontends/lean): add 'print metaclasses' command 2015-02-11 10:13:20 -08:00
Leonardo de Moura
60fca7575c fix(frontends/lean/pp): bugs when pretty printing abbreviations 2015-02-10 19:06:09 -08:00
Leonardo de Moura
f9832fb89f test(tests/lean/abbrev1): add test for abbreviation command 2015-02-10 18:28:48 -08:00
Leonardo de Moura
014271da8b feat(frontends/lean): better error messages for ill-terminated declarations 2015-02-10 14:38:00 -08:00
Leonardo de Moura
c04c0e8381 refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation 2015-02-07 15:19:41 -08:00
Leonardo de Moura
2126b8ec9a feat(library/tactic/apply_tactic): perform class-instance resolution in the apply tactic 
closes #360
 2015-02-06 16:14:03 -08:00
Leonardo de Moura
1e8a975daa feat(frontends/lean): extend parser: rewrite "fold" step 2015-02-06 15:22:34 -08:00
Leonardo de Moura
04f8278c90 test(tests/lean/run): add rewrite tactic test 2015-02-06 14:14:42 -08:00
Leonardo de Moura
5b25da8c43 feat(frontends/lean): add esimp tactic based on rewrite tactic 
closes #358
 2015-02-06 14:13:32 -08:00
Leonardo de Moura
b4139627e5 feat(library/tactic/rewrite_tactic): add option to prevent any kind of constant unfolding when perfoming pattern matching in the rewrite tactic 2015-02-06 13:27:33 -08:00
Leonardo de Moura
78bde6c9e6 test(tests/lean/run): add more rewrite tactic tests 2015-02-06 12:57:42 -08:00
Leonardo de Moura
2e626b29fb feat(library/tactic/rewrite_tactic): allow many constants to be provided in a single rewrite unfold step 2015-02-06 11:03:36 -08:00
Leonardo de Moura
56a46ae61e feat(frontends/lean/parse_tactic_location): make rewrite notation more uniform 2015-02-06 10:31:50 -08:00
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
Leonardo de Moura
1d79cb9c07 fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library 2014-12-22 09:40:15 -08:00
Leonardo de Moura
d2958044fd feat(frontends/lean): add multiple_instances command 
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command

          multiple_instances <class-name>

closes #370
 2014-12-21 17:28:44 -08:00
Leonardo de Moura
5efadb09cc feat(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT library 
This commit adds support for hypotheses (h : C As idxs) where the indices idxs
are just local constants. Before this commit the indices idxs had to be hsets.
Now, they can be hsets or local constants.

The new tests demonstrate new examples that can be handled by the
improved tactic in the HoTT library
 2014-12-21 15:19:25 -08:00
Leonardo de Moura
70f7ec3cf2 test(tests/lean/hott): add test for 'cases' tactic 2014-12-20 11:36:32 -08:00
Leonardo de Moura
677ec2a2fe feat(library/tactic/inversion_tactic): adjust inversion tactic to HoTT lib 2014-12-20 11:32:27 -08:00
Leonardo de Moura
2521dbb39e refactor(hott): use same name convention for sigma in the HoTT and standard libraries 2014-12-19 18:46:06 -08:00
Leonardo de Moura
1e2fc54f2f refactor(library/init/sigma): rename sigma.dpair->sigma.mk, sigma.dpr1->sigma.pr1, sigma.dpr2->sigma.pr2 2014-12-19 18:23:08 -08:00
Leonardo de Moura
9eea32b076 refactor(library/init/datatypes): change implicit arguments of sum.inl and sum.inr 2014-12-19 18:07:13 -08:00
Leonardo de Moura
07d7ea2f4e refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean 2014-12-19 15:08:21 -08:00
Leonardo de Moura
1797e2846f fix(tests/lean/run): replace "open [notation]" with "open [notations]" 2014-12-17 18:28:38 -08:00
Leonardo de Moura
43633085b9 fix(tests/lean): adjust tests to recent changes in the lean libraries 2014-12-16 13:28:43 -08:00
Leonardo de Moura
86f3d029c7 test(tests/lean/extra): more tests for equations compiler 2014-12-15 19:22:17 -08:00
Leonardo de Moura
abe129aa4f refactor(library): rename theorems "iff.flip_sign -> not_iff_not_of_iff" and "decidable_iff_equiv -> decidable_of_decidable_of_iff" 2014-12-15 19:17:51 -08:00
Leonardo de Moura
5cf8064269 refactor(library): rename exists_elim and exists_intro to exists.elim 
and exists.intro
 2014-12-15 19:07:38 -08:00
Jeremy Avigad
3e9a484851 refactor(library/logic/connectives): rename theorems 2014-12-15 15:05:44 -05:00
Leonardo de Moura
c6ebe9456e feat(library/data/nat): add "bounded" quantifiers 
Later, we will add support for arbitrary well-founded relations
 2014-12-13 15:42:38 -08:00
Leonardo de Moura
f0b002d5a7 fix(library/aliases): aliases in sections and contexts 2014-12-13 14:57:15 -08:00
Leonardo de Moura
c291063f3a fix(frontends/lean/structure_cmd): simplify structure names 2014-12-13 14:18:02 -08:00
Leonardo de Moura
c9365db41b test(tests/lean/extra): more tests for equation elaborator 2014-12-12 15:43:41 -08:00
Leonardo de Moura
477d79ae47 refactor(library/init): move more theorems to logic 2014-12-12 13:50:53 -08:00
Leonardo de Moura
d6c8e23b03 refactor(library/init/logic): move theorems to library/logic 2014-12-12 13:24:17 -08:00
Leonardo de Moura
29aaa21f2a fix(tests/lean/interactive): adjust test to reflect changes in the standard library 2014-12-11 19:53:41 -08:00
Leonardo de Moura
ab873cfff9 feat(frontends/lean/elaborator): replace metavariables in the equation lhs with fresh local constants before invoking compiler 2014-12-11 19:51:49 -08:00
Leonardo de Moura
b01cf73a91 feat(library/init/logic): add is_true and is_false 2014-12-11 18:14:03 -08:00
Leonardo de Moura
91ce99d921 feat(frontends/lean): type check 'decreasing' proofs in definition using well-founded recursion 2014-12-11 18:13:35 -08:00
Leonardo de Moura
b8f665e561 feat(frontends/lean): elaborate recursive equations 
Remark: we are not compiling them yet.
 2014-12-10 22:25:40 -08:00
Leonardo de Moura
4342454339 test(tests/lean/hott): add test for no_confusion construction for HoTT 2014-12-09 15:41:54 -08:00
Leonardo de Moura
05f27b8f0e feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures 
It seems most of the time these theorems are not used at all.
They are just polluting the namespace.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-12-09 12:40:09 -08:00
Leonardo de Moura
58432d0968 feat(library/definitional): add no_confusion construction that is compatible with the HoTT library 2014-12-08 22:11:48 -08:00
Leonardo de Moura
2bb51554d5 feat(library/definitional/util): add telescope equality for HoTT library 
This is needed for implementing no_confusion for HoTT.
We can't use heterogeneous equality in HoTT.
 2014-12-07 18:35:55 -08:00
Leonardo de Moura
466b671752 fix(tests/lean/interactive/coe): adjust test to reflect changes in the standard library 2014-12-05 22:27:03 -08:00
Leonardo de Moura
e72c4977f0 feat(frontends/lean): nicer notation for dependent if-then-else 2014-12-04 11:13:09 -08:00
Leonardo de Moura
ebda057499 fix(library/tactic/intros_tactic): seg fault at intros tactic, fixes #366 2014-12-04 09:26:10 -08:00
Leonardo de Moura
1a813fc720 test(tests/lean/run/nested_rec.lean): add nested recursion example based on well-founded recursion package 2014-12-03 22:11:01 -08:00
Leonardo de Moura
b6a1c118f4 fix(tests/lean/whnf): make sure the test does not produce 'sorry' 2014-12-03 21:12:33 -08:00
Leonardo de Moura
173e84c299 fix(tests/lean/struct_class): adjust test result to reflect recent changes 2014-12-03 20:32:33 -08:00
Leonardo de Moura
811bc6a31f feat(library/init/measurable): add 'measurable' type class 2014-12-03 18:54:24 -08:00
Leonardo de Moura
e5fc0f90b2 test(tests/lean/run): try different ways to pack mutually recursive datatypes 2014-12-03 15:28:44 -08:00
Leonardo de Moura
9ae96514e0 test(tests/lean/run): use 'cases' tactic 2014-12-03 15:28:22 -08:00
Leonardo de Moura
d10bb92a7d feat(library/aliases): protected definitions in nested namespaces, closes #331 2014-12-03 14:25:02 -08:00
Leonardo de Moura
0443c1e70c fix(frontends/lean): intro tactic + universe variables, fixes #362 2014-12-03 12:56:30 -08:00
Leonardo de Moura
fca97d5bb2 feat(library/definitional): add brec_on construction, closes #272 2014-12-03 10:39:32 -08:00
Leonardo de Moura
06f436840f fix(library/unifier): postpone class-instance constraints whose type could not be inferred 2014-12-01 22:27:23 -08:00
Leonardo de Moura
19d14678ef refactor(library/unifier): remove dead code 2014-12-01 21:57:34 -08:00
Leonardo de Moura
e6672b958f fix(library/tactic/inversion_tactic): add missing case 2014-12-01 19:11:44 -08:00
Leonardo de Moura
bc7ee2958f fix(library/tactic/inversion_tactic): bug in mutually recursive case 2014-12-01 18:32:38 -08:00
Leonardo de Moura
8137f94b3c fix(tests/lean): to reflect recent changes 2014-12-01 17:14:11 -08:00
Leonardo de Moura
6640fbf11b feat(library/definitional/brec_on): simplify universe level constraints for non-reflexive recursive datatypes 2014-12-01 17:11:06 -08:00
Leonardo de Moura
320971832d feat(frontends/lean/pp): add hard-coded pretty printer for nat numerals 2014-12-01 16:07:55 -08:00
Leonardo de Moura
263424b0fd test(tests/lean/slow): add "manual" 'path induction' tactic 2014-12-01 13:50:01 -08:00
Leonardo de Moura
193fed7061 fix(library/tactic/inversion_tactic): uninitialized variable 2014-11-30 22:41:22 -08:00
Leonardo de Moura
eefe03cf56 fix(tests/lean): adjust tests to modifications to standard library 2014-11-30 21:16:01 -08:00
Leonardo de Moura
dad94eafbe refactor(data/nat/decl): use new naming convention at data/nat/decl.lean 2014-11-30 15:07:09 -08:00
Leonardo de Moura
079bf7f633 test(tests/lean/run/vector): use nat.add 2014-11-30 13:53:02 -08:00
Leonardo de Moura
c08f4672e4 feat(library/tactic): add 'assert' tactic, closes #349 2014-11-29 21:34:49 -08:00
Leonardo de Moura
1a7dd56f0f fix(library/tools/tactic): 'cases' argument precedence 2014-11-29 21:03:45 -08:00
Leonardo de Moura
f51fa93292 feat(library/tactic): add 'fapply' tactic, closes #356 2014-11-29 19:20:41 -08:00
Leonardo de Moura
2c0472252e feat(frontends/lean): allow expressions to be used to define precedence, closes #335 2014-11-29 18:29:48 -08:00
Leonardo de Moura
2487e3b83d fix(frontends/lean/parser): user provided numeral notation should have precedence over the default based on 'num' 2014-11-29 17:29:03 -08:00
Leonardo de Moura
bc65aeb5e1 fix(frontends/lean/calc): add expected type for single-step calc expressions, fixes #357 
This is not an issue for calc expressions containing multiple steps,
since the transitivity step will "force" the expected type for the proofs.
 2014-11-29 15:35:09 -08:00
Leonardo de Moura
6fbbf66565 test(tests/lean/run/vector): define 'map' on vector using brec_on and new inversion tactic 2014-11-29 13:28:01 -08:00
Leonardo de Moura
a0d650d9cc fix(library/tactic/inversion_tactic): complete 'deletion' transition 2014-11-29 09:36:41 -08:00
Leonardo de Moura
7000365a04 fix(tests/lean): to reflect changes in the standard library 2014-11-28 23:03:37 -08:00
Leonardo de Moura
e0debca771 feat(library/tactic/inversion_tactic): add 'case ... with ...' variant that allows user to specify names for new hypotheses 2014-11-28 22:25:37 -08:00
Leonardo de Moura
22b2f3c78c fix(library/tactic/inversion_tactic): bug in injectivity transition 2014-11-28 22:07:35 -08:00
Leonardo de Moura
a6be460166 feat(library/tactic/inversion_tactic): basic 'inversion' tactic 2014-11-28 21:56:13 -08:00
Leonardo de Moura
f7deabfd19 feat(library/rename): add notation for rename 2014-11-26 19:02:11 -08:00
Leonardo de Moura
e55397d422 feat(library/tactic): add 'clears' and 'reverts' variants 2014-11-26 14:49:48 -08:00
Leonardo de Moura
2bd8f969d5 feat(library/tactic): add 'revert' tactic, closes #346 2014-11-26 14:23:42 -08:00
Leonardo de Moura
c28e9b9234 feat(library/tactic): add 'clear' tactic, closes #341 2014-11-26 13:11:36 -08:00
Leonardo de Moura
ffdeb0edc4 fix(frontends/lean/elaborator): unsolved metavariables, fix #329 2014-11-26 11:56:39 -08:00
Leonardo de Moura
df51ba8b7c feat(library/definitional/projection): use strict implicit inference, closes #344 2014-11-25 18:04:06 -08:00
Leonardo de Moura
edc9e4908c test(tests/lean/run): add another subterm example 2014-11-25 16:53:09 -08:00
Leonardo de Moura
f737a140c1 test(tests/lean/run): direct subterm for non-reflexive datatype 2014-11-25 16:22:11 -08:00
Leonardo de Moura
ef75cac1c0 feat(kernel/expr): change the rules for inferring implicit arguments, closes #344 2014-11-25 12:54:07 -08:00
Leonardo de Moura
24a15b6c46 fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343 2014-11-24 21:33:52 -08:00
Leonardo de Moura
f729762c23 test(tests/lean/run): add test for well_founded relation for mutually recursive datatypes 2014-11-24 14:58:30 -08:00
Leonardo de Moura
d81a6259e8 feat(frontends/lean/find_cmd): add options for controlling find_decl 2014-11-24 00:16:10 -08:00
Leonardo de Moura
f1e915a188 feat(frontends/lean): add 'find_decl' command 2014-11-23 23:00:59 -08:00
Leonardo de Moura
44a2ef8f6f fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file 2014-11-23 17:49:14 -08:00
Leonardo de Moura
64686c1278 feat(frontends/lean): allow user to associate precedence to binders, closes #323 2014-11-23 17:30:46 -08:00
Leonardo de Moura
cf3b0e1087 feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333 2014-11-23 17:30:46 -08:00
Leonardo de Moura
13fba433b0 feat(library/tactic/generalize): add 'generalizes' syntax sugar, closes #327 2014-11-23 17:30:22 -08:00
Leonardo de Moura
919007612a fix(tests/lean): adjust tests since module 'logic' depends on nat 
We need that because of the definitional package
 2014-11-22 17:34:05 -08:00
Leonardo de Moura
5db13da95f test(tests/lean/run/div_wf): cleanup div based on well founded recursion 2014-11-22 09:56:47 -08:00
Leonardo de Moura
064ecd3e3d refactor(library/data/nat): declare lt and le asap using inductive definitions, and make key theorems transparent for definitional package 
We also define key theorems that will be used to generate the
automatically generated a well-founded subterm relation for inductive
datatypes.
We also prove decidability and wf theorems asap.
 2014-11-22 00:19:39 -08:00
Leonardo de Moura
5d5fd2da50 fix(frontends/lean): tactic + section variables, fixes #332 2014-11-21 10:07:16 -08:00
Leonardo de Moura
7e7e7c241c test(tests/lean/run/gcd): gcd compiled by hand into wf recursion 2014-11-18 19:34:01 -08:00
Leonardo de Moura
4fbb5cfcca test(tests/lean/run/div_wf): cleanup 2014-11-18 17:59:14 -08:00
Leonardo de Moura
a065c7bf96 test(tests/lean/run/tree_height): experiment with wf relation based on the height 
This is easier to generate than the subterm relation
 2014-11-18 17:57:17 -08:00
Leonardo de Moura
5fbe990c7a test(tests/lean/run): define div using wf package 2014-11-18 13:55:58 -08:00
Leonardo de Moura
5daff18017 test(tests/lean/run): pre-quotient experiment 2014-11-17 18:30:11 -08:00
Leonardo de Moura
28c63e685b feat(frontends/lean): add '[local]' notation, closes #322 2014-11-16 21:15:04 -08:00
Leonardo de Moura
bf5f48730c refactor(library/data/subtype): define subtype using 'structure' command 2014-11-16 15:01:14 -08:00
Leonardo de Moura
a171f8fbc3 test(tests/lean/run): simple diag for square matrices 2014-11-15 18:49:17 -08:00
Leonardo de Moura
1b95b69251 test(tests/lean/run): define subterm relation for vectors 2014-11-15 16:17:51 -08:00
Leonardo de Moura
ea640257bf feat(frontends/lean/structure_cmd): generate no_confusion for structures too 2014-11-15 16:00:09 -08:00
Leonardo de Moura
b87559dac5 test(tests/lean/run): define subterm relation for trees by hand 2014-11-15 13:29:23 -08:00
Leonardo de Moura
7685516d1e feat(frontends/lean): better default for atomic notation 2014-11-14 16:25:13 -08:00
Leonardo de Moura
67de3b06f3 feat(kernel/level): improve universe level pretty printer 
Example: produce `l+2` instead of `succ (succ l)`.
 2014-11-14 14:51:03 -08:00
Leonardo de Moura
00df34a1c4 feat(library/unifier): generalize method process_succ_eq_max_core 2014-11-14 14:25:41 -08:00
Leonardo de Moura
488f989c46 fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop 2014-11-14 13:57:42 -08:00
Leonardo de Moura
58525905d0 fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command 2014-11-13 22:05:55 -08:00
Leonardo de Moura
51719145f9 feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2) 2014-11-12 17:28:33 -08:00
Leonardo de Moura
edd04881ee fix(library/logic): import prod and unit declarations in logic 
Reason: we need them for automatically generating constructions needed
by the definitional package
 2014-11-12 16:54:50 -08:00
Leonardo de Moura
6bc89f0916 feat(library/definitional): define ibelow and below 
These are helper definitions for brec_on and binduction_on
 2014-11-12 16:38:46 -08:00
Leonardo de Moura
97609d1625 test(tests/lean/run/nateq): add example that triggered previous modification 2014-11-12 15:11:08 -08:00
Leonardo de Moura
b07b82cf43 fix(library/definitional): marking cases_on and rec_on as reducible 
The idea is to avoid counter-intuitive behavior
 2014-11-12 15:03:30 -08:00
Leonardo de Moura
a3066e3eaa fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator 2014-11-12 13:10:19 -08:00
Leonardo de Moura
463e70332d test(tests/lean/run): define brec_on and binduction_on for a reflexive type 
We say an inductive type T is reflexive if it contains at least one constructor that
takes as an argument a function returning T.

For reflexive types it doesn't seen to be possible to define a single
brec_on that can eliminate to Type.{>=1} and Prop.
The universe level expressions get too complicated.
Even if we extend the universe constraint solver in the kernel, the
additional complexity might be a problem.

We workaround this issue by defining two versions of brec_on:
  - One (brec_on) that eliminates to Type.{>=1}, and
  - binduction_on that eliminates to Prop.

For non-reflexive types, we can combine both of them.
 2014-11-12 10:52:32 -08:00
Leonardo de Moura
5312afa7ec feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes 
The new test contains examples that required explicit levels.
 2014-11-12 10:52:32 -08:00
Leonardo de Moura
faf90c4b87 test(tests/lean/run): test brec_on on vectors 2014-11-11 17:23:59 -08:00
Leonardo de Moura
f6889951c6 fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion 2014-11-11 15:14:08 -08:00
Leonardo de Moura
e65b5884e5 test(tests/lean/run/forest): define brec_on for forests 
Almost everything explicit to get an idea of what needs to be generated automatically.
 2014-11-11 13:16:23 -08:00
Leonardo de Moura
b3e4a689cf test(tests/lean/run): define ackermann function using recursors 2014-11-11 11:06:10 -08:00
Leonardo de Moura
e2ce942513 fix(tests/lean): adjust test to new eval semantics 2014-11-10 21:10:33 -08:00
Leonardo de Moura
1f92751c4d test(tests/lean/run): fibonacci using well_founded recursion 2014-11-10 12:46:55 -08:00
Leonardo de Moura
363d4a7577 fix(library/definitional/no_confusion): assertion violation 2014-11-10 10:32:03 -08:00
Leonardo de Moura
fa26c2301c fix(frontends/lean): fix pretty-printing spacing problem 2014-11-09 14:49:43 -08:00
Leonardo de Moura
3aac26d658 fix(frontends/lean): tactic + variables bug, fixes #315 2014-11-09 14:43:22 -08:00
Leonardo de Moura
eff3c6b774 feat(frontends/lean): add variation of the foldl/foldr notation where initial element is suppressed, closes #314 
See tests/lean/fold.lean for examples
 2014-11-09 14:08:33 -08:00
Leonardo de Moura
ce889ddf60 feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1' 2014-11-09 12:55:13 -08:00