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

1595 commits

Author SHA1 Message Date
Leonardo de Moura
582dbecfd0 feat(library,hott): add notation T1 : T2 as syntax sugar for (focus (T1; all_goals T2)) 
closes #775
 2015-08-08 10:16:25 -07:00
Leonardo de Moura
1f34c72192 fix(frontends/lean/parser): fixes #770 2015-08-08 09:48:31 -07:00
Leonardo de Moura
dc2e702373 feat(library/unifier): generate approximate solution for universe constraints of the form (max u ?m =?= max u v) 
closes #777
 2015-08-08 09:29:59 -07:00
Leonardo de Moura
6c5832a564 feat(frontends/lean/decl_cmds): allow recursive examples 
closes #774
 2015-08-08 08:26:25 -07:00
Leonardo de Moura
06f20694c8 fix(frontends/lean/builtin_exprs): fixes #768 2015-08-08 04:20:17 -07:00
Leonardo de Moura
d46dbce86e feat(library/tactic/tactic): apply substitution in 'then' combinator 
closes #778
 2015-08-08 03:42:21 -07:00
Floris van Doorn
7f76d7e648 fix(tests): update test 2015-08-07 13:34:41 -07:00
Leonardo de Moura
5568085ab9 fix(frontends/lean/elaborator): closes #771 
Produce nicer error message when type/goal is a metavariable and
universe metavariables have already been instantiated with universe
parameters.
 2015-08-07 13:29:22 -07:00
Leonardo de Moura
6a079fdd2d fix(library/tactic/exact_tactic): fixes #779 2015-08-07 13:29:22 -07:00
Leonardo de Moura
f21647899f feat(frontends/lean/builtin_exprs): rename 'show' hidden name to 'this' 
This is useful if 'show' is recursive
 2015-08-07 13:29:21 -07:00
Floris van Doorn
11b1f416f6 feat(nat): add unfold attributes to add, mul, sub and of_num in namespace nat_esimp in both libraries 2015-08-04 13:23:20 +02:00
Floris van Doorn
7a780b1b60 feat(hott): various minor changes in the HoTT library 2015-08-04 13:01:11 +02:00
Leonardo de Moura
0309a1e131 fix(tests/lean/extra/show_goal_bag): adjust test to recent changes in the standard library 2015-08-04 06:52:20 +02:00
Leonardo de Moura
1f304ad4b9 fix(frontends/lean/pp): pretty printing 'binder' 
This commit also replaces many occurrences of 'binders' with 'binder'.
 2015-07-31 11:27:38 -07:00
Leonardo de Moura
656b642c4a fix(frontends/lean): identifier size when using unicode 
see issue #756
 2015-07-30 11:32:24 -07:00
Leonardo de Moura
cc4f18c062 feat(frontends/lean): add "--info" command line option for extracting identifier/keyword information 
see issue #756
 2015-07-30 10:18:03 -07:00
Leonardo de Moura
be61fb0566 feat(frontends/lean/elaborator): add "noncomputable theory" command, display "noncomputable" when printing definitions 
When the command "noncomputable theory" is used, Lean will not sign an
error when a noncomputable definition is not marked as noncomputable
 2015-07-29 17:54:35 -07:00
Leonardo de Moura
b3707ab54a feat(library/tactic/unfold_rec): fixes #753 2015-07-29 17:13:02 -07:00
Leonardo de Moura
ed41a01a51 fix(frontends/lean/elaborator): fixes #755 2015-07-29 16:41:30 -07:00
Leonardo de Moura
bbd6946a15 refactor(library/logic/axioms): we have only one extra axiom 2015-07-29 13:36:23 -07:00
Leonardo de Moura
6dbcf86fd4 feat(library/logic/axioms): use diaconescu to prove em 
With the new "noncomputable" feature we can use Hilbert's choice without
being concerned it may accidentaly "leak" inside definitions we don't
want to use it.
 2015-07-29 13:01:07 -07:00
Leonardo de Moura
0bda39c8ac feat(frontends/lean): check for noncomputability when moving theorems from theorem_queue to environment 2015-07-29 13:01:07 -07:00
Leonardo de Moura
69ead0ddd8 feat(frontends/lean/decl_cmds): reject unnecessary "noncomputable" annotations 2015-07-29 13:01:07 -07:00
Leonardo de Moura
74be3031b1 feat(frontends/lean/decl_cmds): sign an error if "noncomputable" keyword is used in the HoTT library or with non-definitions 2015-07-29 13:01:06 -07:00
Leonardo de Moura
308af87b69 feat(library): add 'noncomputable' keyword for the standard library 2015-07-28 21:56:35 -07:00
Leonardo de Moura
7e8a394caf chore(tests/lean): fix style and adjust tests 2015-07-28 18:15:25 -07:00
Leonardo de Moura
b81d4d50f1 feat(frontends/lean/bultin_cmds): add 'print axioms <declname>' command that prints axioms a giving declaration depends on 2015-07-28 18:15:25 -07:00
Leonardo de Moura
80e3da0526 fix(library/util): fixes #751 2015-07-28 16:30:20 -07:00
Leonardo de Moura
8ee1d35bed fix(tests/lean/unfold_crash): fixed regression test for bug reported by Rob 2015-07-28 12:51:42 -07:00
Leonardo de Moura
cfa9412f96 fix(frontends/lean): "show goal" localization, add "position", support "by tactic" 2015-07-28 12:48:12 -07:00
Leonardo de Moura
0dc8dc999e fix(library/tactic/rewrite_tactic): crash when trying to unfold constructor 2015-07-28 12:43:56 -07:00
Leonardo de Moura
08b23d8b4f test(tests/lean/extra): add test for "show goal" feature 2015-07-27 21:03:16 -07:00
Leonardo de Moura
a3b570c852 test(tests/lean/extra): test for Soonho 2015-07-27 19:32:27 -07:00
Leonardo de Moura
8c06803f54 test(tests/lean): add regression for issue #737 2015-07-27 07:59:18 -07:00
Leonardo de Moura
f7440ff068 fix(tests/lean): adjust tests to reflect changes in the standard library 2015-07-24 09:59:49 -07:00
Leonardo de Moura
bcf057f4f3 feat(frontends/lean): display '[congr]' attribute when printing theorems 2015-07-23 18:52:59 -07:00
Leonardo de Moura
3e6b80d38c feat(library/util): disable local constant purification when pretty printing goals 
This feature generates confusion.
 2015-07-23 18:52:59 -07:00
Leonardo de Moura
f1a19a10c4 fix(library/util): incorrect hypothesis renaming when pretty printing goals 2015-07-23 18:52:59 -07:00
Leonardo de Moura
e221d38790 feat(library/tactic/assert_tactic): allow duplicate names for hypotheses in assert tactic 2015-07-23 18:52:59 -07:00
Leonardo de Moura
e0209a1532 feat(frontends/lean): better error localization for 'have'-expressions in tactic mode 2015-07-23 18:52:59 -07:00
Leonardo de Moura
faab1e449f fix(tests/lean/rw_set3): update test to reflect changes in the standard library 2015-07-23 18:52:59 -07:00
Leonardo de Moura
5f4576a7f7 test(tests/lean): add test for '[congr]' attribute validation 2015-07-23 18:52:59 -07:00
Leonardo de Moura
844caf32e4 feat(frontends/lean/bultin_cmds): add 'print [congr]' command for displaying active congruence rules 2015-07-23 18:52:59 -07:00
Leonardo de Moura
933f056fff feat(library/simplifier): add API for extracting simplification rules defined in a given namespace 2015-07-22 18:47:56 -07:00
Leonardo de Moura
8085123119 refactor(library/simplifier): rename 'rewrite_rule' to 'simp_rule' 2015-07-22 10:39:30 -07:00
Leonardo de Moura
092c8d05b9 feat(frontends/lean,library): rename '[rewrite]' to '[simp]' 2015-07-22 09:01:42 -07:00
Leonardo de Moura
23dd47d27f fix(tests/lean): adjust tests to recent changes to the standard library 2015-07-19 21:32:42 -07:00
Leonardo de Moura
5112232d6d fix(tests/lean/run/finset): adjust test to recent changes to the 
standard library
 2015-07-19 11:53:21 -07:00
Leonardo de Moura
3ab0e07ba9 feat(frontends/lean): add simp tactic frontend stub 
This commit also removes the fake_simplifier. It doesn't work anymore
because simp is now a reserved word.
 2015-07-14 09:54:53 -04:00
Leonardo de Moura
589f9df103 fix(tests/lean): adjust tests to reflect recent changes in the standard library 2015-07-13 21:46:09 -04:00
Leonardo de Moura
267545ca0c feat(frontends/lean): parse 'with_options' tactical 
see issue #492
 2015-07-13 19:13:41 -04:00
Leonardo de Moura
f8d472c9f1 feat(frontends/lean/parse_rewrite_tactic): change the semantics of rewrite[↑f] when f is recursive 
After this commit it behaves like 'unfold f'.
That is, it will unfold f even if it fails to fold recursive
applications. Now, only 'esimp[f]' will not unfold f-applications when
it cannot fold the recursive applications.

This commit also closes #692. It is part of a series of commits that
addresses this issue.

closes #692
 2015-07-12 13:20:21 -04:00
Leonardo de Moura
4c0a656ecc fix(library/tactic/unfold_rec): support indexed families + brec_on at unfold_rec 
see issue #692
 2015-07-12 12:45:05 -04:00
Leonardo de Moura
7fa5c3e5da feat(library/tactic/unfold_rec): take '[recursor]' annotations into account at unfold_rec 2015-07-12 11:33:40 -04:00
Leonardo de Moura
f0e3eef38a test(tests/lean/unfold_rec2): add example from #692 2015-07-11 19:45:27 -04:00
Leonardo de Moura
8e8e08cfe7 feat(library/tactic): use occurrence object in unfold tactic family 2015-07-11 18:53:45 -04:00
Leonardo de Moura
554a42b407 fix(library/tactic/unfold_rec): add annother brec pattern that should be checked in the unfold recursive definition tactic 2015-07-10 22:16:23 -04:00
Leonardo de Moura
a9515ac7a4 feat(library/tactic/rewrite_tactic): try to fold nested recursive applications after unfolding a recursive function 
See issue #692.
The implementation still has some rough spots.
It is not clear what the right semantic is.
Moreover, the folds in e_closure could not be eliminated automatically.
 2015-07-08 21:19:18 -04:00
Leonardo de Moura
26574e29a9 feat(library/normalize,frontends/lean): allow multiple arguments in [unfold] hint 
closes #693
 2015-07-07 18:01:57 -07:00
Leonardo de Moura
a27b20cd9c feat(frontends/lean/notation_cmd): allow local notation to override reserved notation 
closes #712
 2015-07-07 17:30:46 -07:00
Leonardo de Moura
4b1b3e277f feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]' 
see issue #693
 2015-07-07 16:37:06 -07:00
Leonardo de Moura
b0c56273e2 fix(frontends/lean/elaborator): fixes #724 2015-07-06 15:19:19 -07:00
Leonardo de Moura
7e0844a9e6 fix(tests): to reflect recent changes in the standard library 2015-07-06 15:05:01 -07:00
Leonardo de Moura
c843690d27 fix(frontends/lean/elaborator): fixes #719 2015-07-03 12:37:28 -07:00
Leonardo de Moura
aa338f6002 test(tests/lean/run): add test showing new coercion module addresses issue #668 2015-07-01 16:41:19 -07:00
Leonardo de Moura
4ae9f3ea81 feat(library/coercion): new coercion manager 
closes #668
 2015-07-01 16:32:34 -07:00
Leonardo de Moura
cf574d0127 feat(library): assign priorities to notation declarations in the standard library 
Now, even if the user opens the namespaces in the "wrong" order, the
notation + coercions will behave as expected.
 2015-06-30 17:38:13 -07:00
Leonardo de Moura
cabe30ba71 feat(frontends/lean): allow user to assign priorities to notation declarations 2015-06-30 17:10:27 -07:00
Leonardo de Moura
0fc2efe88e fix(library/tactic/rewrite_tactic): fixes #702 2015-06-28 20:37:17 -07:00
Leonardo de Moura
95720b1670 fix(frontends/lean/elaborator): fixes #687 2015-06-28 19:58:57 -07:00
Leonardo de Moura
ecfc01b2d0 test(tests/lean/run): add test for <d notation 
see issue #695

remark: we have to fix the tutorial the ASCII notation for fold is `<d`
instead of `<D`
 2015-06-28 13:10:15 -07:00
Leonardo de Moura
1b864a838f fix(library/tactic/induction_tactic.cpp): condition for checking whether 'induction' tatic is applicable or not 
fixes #690
 2015-06-28 13:07:02 -07:00
Leonardo de Moura
2f75768243 feat(library/tactic/rewrite_tactic): fail when nothing is rewritten 
fixes #686
 2015-06-28 12:05:00 -07:00
Leonardo de Moura
d1eaa7bcda feat(frontends/lean/parse_rewrite_tactic): accept trailing comman in rewrite tactic 
see issue #695
 2015-06-28 11:45:30 -07:00
Leonardo de Moura
4a4ef48344 fix(frontends/lean/parse_rewrite_tactic): fixes #691 2015-06-28 11:28:05 -07:00
Leonardo de Moura
869ad261c5 fix(frontends/lean/elaborator): fixes #689 2015-06-27 16:19:38 -07:00
Leonardo de Moura
97b3fd45ce fix(library/logic/axioms/prop_decidable): fixes #704 2015-06-26 19:14:36 -07:00
Leonardo de Moura
2aa64034df fix(tests/lean): adjust tests to reflect changes in the elaboration process 2015-06-26 17:18:30 -07:00
Floris van Doorn
9ef1ae0848 fix(tests): update tests to reflect the change of notation from \~ to ~ 2015-06-25 22:55:05 -04:00
Leonardo de Moura
1b414d36e7 refactor(library/init): define prod as an inductive datatype 
Motivation: prod is used internally in the definitional package.
If we define prod as a structure, then Lean will tag pr1 and pr2 as
projections. This creates problems when we add special support for
projections in the elaborator. The heuristics avoid some case-splits
that are currently performed, and without them some files break.
 2015-06-25 17:59:06 -07:00
Floris van Doorn
fa1979c128 feat(datatypes): let the type of unit be the lowest non-Prop universe 
The definitional package (brec_on and cases_on) now use poly_unit instead of unit

closes #698
 2015-06-25 17:33:46 -07:00
Leonardo de Moura
a4c0699e81 feat(library/tactic/constructor_tactic): restore 'constructor' tactic old semantics, add 'fconstructor' tactic 
See issue #676

Add new test demonstrating why it is useful to have the old semantics
for 'constructor'
 2015-06-17 23:48:54 -07:00
Leonardo de Moura
bf71d9f342 fix(library/tactic/rewrite_tactic): fixes #682 2015-06-17 18:49:02 -07:00
Leonardo de Moura
ce8f2a1674 feat(library/class): allow any constant to be marked as a class 
closes #679
 2015-06-17 16:26:45 -07:00
Leonardo de Moura
9e6e406f73 feat(frontends/lean): add '#compose' command for testing composition manager 2015-06-17 14:42:25 -07:00
Leonardo de Moura
0ae24faae3 feat(library/tactic/constructor_tactic): use 'fapply' in 'constructor' tactic 
closes #676
 2015-06-16 12:03:31 -07:00
Leonardo de Moura
0dc674e350 fix(tests/lean/630): adjust test to reflect changes in the standard library 2015-06-16 11:33:26 -07:00
Jeremy Avigad
a4a8253f50 refactor(library,hott,tests): rename succ_inj to succ.inj, add abbreviation eq_of_succ_eq_succ 2015-06-15 22:52:38 +10:00
Leonardo de Moura
d8620ef4c9 fix(kernel,library,frontends/lean): improve error messages 
see #669
 2015-06-14 19:44:00 -07:00
Leonardo de Moura
8a85e4ee87 feat(frontends/lean/builtin_cmds): improve print <id> when <id> is a not yet revealed theorem 
We add a remark saying the command `reveal <id>` should be used to
access `<id>` definition.
 2015-06-13 12:12:22 -07:00
Leonardo de Moura
591fb91f34 fix(frontends/lean/builtin_cmds): fixes #671 2015-06-13 11:35:03 -07:00
Leonardo de Moura
9fbf267a3f feat(library/tactic/rewrite_tactic): when 'rewrite' step fails apply esimp and try again 
closes #670
 2015-06-12 19:48:58 -07:00
Leonardo de Moura
3d9b557cfd feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions 
closes #484
 2015-06-12 17:49:26 -07:00
Leonardo de Moura
7bad9fe554 feat(library/error_handling/error_handling): set 'pp.beta' to false when displaying errors 
see issue #669
 2015-06-12 14:46:51 -07:00
Leonardo de Moura
69be4c720c fix(library/tactic/subst_tactic): bug in 'subst' tactic 2015-06-12 12:11:44 -07:00
Leonardo de Moura
8aa634378e fix(tests/lean): adjust tests to reflect changes in the standard library 2015-06-10 17:00:47 -07:00
Leonardo de Moura
0b335230d7 test(tests/lean): add test for eta at postprocessing 2015-06-10 16:33:27 -07:00
Leonardo de Moura
8b7dc4e03a feat(frontends/lean): apply eta-reduction in postprocessing step 
Perhaps, we should add an option to disable this new feature.

Remark: this commit makes commit 46d418a redundant.
I'm keeping 46d418a because we may retract this commit in the future.
 2015-06-10 16:29:30 -07:00
Leonardo de Moura
4b91cfccff feat(frontends/lean/builtin_exprs): make notation ( e : T ) builtin 
In the previous approach, the following (definitionally equal) term was being generated

       (fun (A : Type) (a : A), a) T e
 2015-06-10 14:52:59 -07:00
Leonardo de Moura
cff7b7474a test(tests/lean/run): add examples showing how to prove (using tactics) that direct_subterm relation is well-founded 
see issue #347
 2015-06-09 16:17:29 -07:00