Commit graph

390 commits

Author SHA1 Message Date
Leonardo de Moura
4e2377ddfc refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
08ccd58eb6 feat(frontends/lean): add 'reducible' modifier for controlling which
definitions are unfolded during elaboration

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-19 15:54:32 -07:00
Leonardo de Moura
baf4c01de8 feat(frontends/lean): definitions are opaque by default 2014-09-19 15:54:32 -07:00
Leonardo de Moura
48dbd13eef feat(frontends/lean): allow transient classes/instances, i.e.,
classes/instances that are not saved in .olean files
2014-09-19 15:54:32 -07:00
Leonardo de Moura
e3e2370a38 feat(frontends/lean): split 'opaque_hint' command into 'opaque' and 'transparent'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-16 18:03:40 -07:00
Jeremy Avigad
74cb289d48 refactor(library): rename algebra directory to struc, move categories.lean to algebra 2014-09-16 13:13:01 -07:00
Jeremy Avigad
9988914189 refactor(library/logic): move files in classes directory to core 2014-09-16 13:13:01 -07:00
Leonardo de Moura
dffe9a6f17 fix(frontends/lean/elaborator): more robust support for coercions to
function-class that contains implicit arguments
2014-09-16 13:08:34 -07:00
Leonardo de Moura
d0d23eb525 fix(frontends/lean/inductive_cmd): improve name resolution in inductive
command

The new test demonstrates the problem being fixed by this commit
2014-09-16 09:48:51 -07:00
Leonardo de Moura
8e52c478b1 refactor(library/data/num): add 'succ', 'pred' and 'size' (aka number of bits),
rename is_inhabited theorems
2014-09-15 16:05:17 -07:00
Leonardo de Moura
edcbe6fe10 feat(frontends/lean): allow multiple coercions from class A to B, closes #187
See new tests (for examples)
tests/lean/run/coe10.lean
tests/lean/run/coe11.lean
tests/lean/run/coe9.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-14 12:59:43 -07:00
Leonardo de Moura
029acbd1df feat(library/coercion): better support for coercions to function-class. closes #185 2014-09-12 13:17:20 -07:00
Leonardo de Moura
a2e36e97f2 fix(frontends/lean/builtin_cmds): allow coercion command inside section, fixes #186 2014-09-12 12:13:29 -07:00
Leonardo de Moura
010ecebfea feat(frontends/lean): add proof-qed expression
Remark: we still have to add support to it in the elaborator.
Right now, it is just an embellished parenthesis.
2014-09-11 18:14:49 -07:00
Leonardo de Moura
7ffe73b8ca fix(frontends/lean): name clash inside section, fixes #181 2014-09-11 16:37:23 -07:00
Leonardo de Moura
5cff53c447 test(tests/lean/run): add section test 2014-09-11 15:33:20 -07:00
Leonardo de Moura
570879b55f feat(frontends/lean): add declaration to namespace without opening it, closes #161 2014-09-09 18:02:14 -07:00
Leonardo de Moura
efb14d906b chore(tests/lean): add untracked tests 2014-09-09 16:21:30 -07:00
Leonardo de Moura
9b9adf8831 refactor(library): replace decidable_eq with abbreviation 2014-09-09 16:09:05 -07:00
Leonardo de Moura
47e02342bb feat(frontends/lean/elaborator): use whnf in class-instance resolution, closes #160 2014-09-09 15:04:44 -07:00
Leonardo de Moura
abdd784729 feat(shell): start 'lean --server' with 'pp.beta = true' 2014-09-09 14:13:35 -07:00
Leonardo de Moura
187661aa6a feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs 2014-09-09 09:27:26 -07:00
Leonardo de Moura
4088cdc139 chore(frontend/lean/pp_options): use consistent name convention for pp option names 2014-09-09 09:27:26 -07:00
Leonardo de Moura
b4793df653 feat(frontends/lean): rename '[fact]' to '[visible]'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-08 07:47:42 -07:00
Leonardo de Moura
559dd586f2 feat(library): add 'decidable_eq' class
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-07 22:23:36 -07:00
Leonardo de Moura
cbdfb0dcdc feat(frontends/lean/elaborator): (Pi/forall) intro in class inference, closes #77 2014-09-07 19:59:34 -07:00
Leonardo de Moura
2631979f5c fix(library/scoped_ext): section/context should not affect namespace 2014-09-07 19:59:34 -07:00
Leonardo de Moura
3310eb3dfc feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-07 12:29:32 -07:00
Leonardo de Moura
5549295c47 fix(frontends/lean/inductive_cmd): bug when elaborating inductive tyoe parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 11:38:32 -07:00
Leonardo de Moura
bbff564a1c feat(frontends/lean): persistent notation in sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-06 11:14:20 -07:00
Leonardo de Moura
b5f595c432 fix(frontends/lean/inductive_cmd): bugs when declarating inductive datatypes in sections, fixes #141, fixes #142
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-05 19:17:09 -07:00
Leonardo de Moura
6632a50015 refactor(library): add namespaces 'or', 'and' and 'iff'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 21:25:21 -07:00
Leonardo de Moura
68d9bef860 refactor(library): add 'eq' and 'ne' namespaces
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 18:41:06 -07:00
Leonardo de Moura
2bc6f92d33 refactor(library): add 'and' namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:44:53 -07:00
Leonardo de Moura
364bba2129 feat(frontends/lean/inductive_cmd): prefix introduction rules with the name of the inductive datatype
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 17:26:36 -07:00
Leonardo de Moura
8743394627 refactor(kernel/inductive): replace recursor name, use '.rec' instead of '_rec'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
653141135d chore(tests/lean): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-04 15:04:57 -07:00
Leonardo de Moura
f9a90b9920 feat(frontends/lean): add 'export' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 18:37:01 -07:00
Leonardo de Moura
5e18e6609c feat(frontends/lean): add 'as' clause to 'open' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 17:37:02 -07:00
Leonardo de Moura
e51c4ad2e9 feat(frontends/lean): rename 'using' command to 'open'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-03 16:00:38 -07:00
Leonardo de Moura
0f9478d91e feat(frontends/lean): add 'class' command back
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-02 15:04:23 -07:00
Leonardo de Moura
8dec18018c refactor(library/data/list): avoid placeholders '_', make first argument of false_elim implicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-09-01 19:44:04 -07:00
Jeremy Avigad
6ffd719c1a refactor(library/logic): move identities from classical to identities 2014-08-29 22:28:22 -07:00
Leonardo de Moura
1e80a9dfe9 feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 16:27:52 -07:00
Leonardo de Moura
d536475e49 refactor(library): more implicit_args for: and_assoc, and_comm, or_assoc, or_comm, if_pos, if_neg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 11:10:04 -07:00
Leonardo de Moura
6b7e79b62f feat(library/data/nat): mark more arguments implicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-28 10:38:58 -07:00
Jeremy Avigad
00a049a667 refactor(library/logic): rename connectives -> core, basic -> connectives 2014-08-27 18:43:24 -07:00
Leonardo de Moura
2d78387541 refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 18:34:09 -07:00
Leonardo de Moura
477b7b4811 fix(tests/lean/run/class_coe): adjust test to reflect library changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-27 17:55:42 -07:00
Leonardo de Moura
a8d58fdd33 refactor(library): mark absurd_elim argument as implicit
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-26 18:27:39 -07:00
Leonardo de Moura
c11fd6b0d2 fix(tests/lean/run): adjust tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 21:39:46 -07:00
Leonardo de Moura
04d9eb17d1 feat(kernel/conveter): improve support for proof irrelevant in the converter
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 11:19:18 -07:00
Leonardo de Moura
42a8fb5965 chore(tests/lean/run/matrix): simplify same_dim_irrel proof
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 09:27:19 -07:00
Leonardo de Moura
60d5e87a66 test(tests/lean/run): add matrix test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-25 09:04:39 -07:00
Leonardo de Moura
cbc81ea6c5 chore(*): minimize dependencies on tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-24 19:58:48 -07:00
Leonardo de Moura
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-23 18:08:09 -07:00
Jeremy Avigad
47a1c00a6d refactor(library/standard): collect notation in general_notation 2014-08-23 17:53:02 -07:00
Leonardo de Moura
a5f0593df1 feat(*): change inductive datatype syntax
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:46:10 -07:00
Leonardo de Moura
626cd952e7 test(tests/lean/run): add overload test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-22 15:23:33 -07:00
Leonardo de Moura
937c465685 fix(library/unifier): too much reduction
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 21:37:51 -07:00
Leonardo de Moura
6cf73b51e2 fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 17:56:18 -07:00
Leonardo de Moura
725f5ba0a0 feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-21 16:58:25 -07:00
Jeremy Avigad
6264fb52d6 fix(lean/library/standard): fix tests, more cleanup 2014-08-20 18:04:31 -07:00
Leonardo de Moura
f5987b7bda refactor(library/unifier): make it easier to add new options to the unifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 17:30:08 -07:00
Leonardo de Moura
b60c9d9ecc test(tests/lean/run): add test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-20 16:46:19 -07:00
Leonardo de Moura
f0d50e0d33 feat(frontends/lean): change the name resolution rules: when in a namespace N that defines C, then C always refers to N.C (i.e., it overrides any alias)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
08ae17650b feat(frontends/lean): try overloaded notation and declarations in the order they were defined
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
919f02983e feat(frontends/lean/elaborator): case-split on coercions that cannot be resolved by postponing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
4a96fefd96 fix(library/unifier): bug in unifier priority queue
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-18 18:58:50 -07:00
Leonardo de Moura
1436212a34 fix(library/unifier): use depth-first search strategy for solving class-instance constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-16 13:51:24 -07:00
Leonardo de Moura
670bfe24f5 chore(build): remove hott library directory, and move hott tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 13:30:56 -07:00
Leonardo de Moura
094459504b fix(tests/lean/run): adjust test to changes in the library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-15 13:27:18 -07:00
Leonardo de Moura
60ab6d3bd8 feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-12 17:40:30 -07:00
Leonardo de Moura
70c0eda9fc feat(frontends/lean): make sure all scopes are closed in the end of the module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 17:08:59 -07:00
Leonardo de Moura
1a67e69678 feat(library/scoped_ext): force user to end a scope with an identifier matching the one used in beginning of scope, closes #30
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:59:08 -07:00
Leonardo de Moura
9e6c5695be fix(library/unifier): make sure the imitation step is type correct, fix ensure_sufficient_args
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 16:09:45 -07:00
Leonardo de Moura
4ad7e709aa feat(frontends/lean): default for inductive types, closes #32
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-07 07:52:37 -07:00
Leonardo de Moura
069f217215 fix(frontends/lean/elaborator): use full local context for metavariables due to coercions and overloads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 17:21:21 -07:00
Leonardo de Moura
d1924097d5 feat(library/match): add 'local' backtracking
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 10:09:00 -07:00
Leonardo de Moura
e6ffda0c51 feat(library/match): add basic match_plugin that just invokes whnf before failing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-05 08:37:03 -07:00
Leonardo de Moura
56d151ef7f feat(frontends/lean): 'partial' aliases. closes #24
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-04 22:08:10 -07:00
Leonardo de Moura
938b4e8421 test(tests/lean/run): add unicode in identifiers test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 20:05:46 -07:00
Leonardo de Moura
fbc4a7af3b feat(library/unifier): when unifier.expensive == true, then use only restrict higher-order unification (a fragment slightly more general than higher-order pattern matching) for solving class-instance constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 14:30:25 -07:00
Leonardo de Moura
5e2185cfbe feat(library/unifier): postpone as much as possible universe constraints of the form ?m1 =?= max(l1, l2) and ?m1 =?= imax(l1, l2) where ?m1 occurs in the right hand side. When there is nothing else to be done, try to solve them by reducing to ?m1 = l1 and ?m1 = l2.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-02 09:14:35 -07:00
Leonardo de Moura
3795d466c1 fix(frontends/lean/elaborator): provide type information for expressions using '@' operator, and strict function applications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-01 20:57:24 -07:00
Leonardo de Moura
4cb8fb20fe fix(frontends/lean/elaborator): bug when mixing string and non-strict implict arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-01 10:58:20 -07:00
Leonardo de Moura
8e6324185a fix(tests/lean): adjust tests to new library structure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-01 09:37:23 -07:00
Leonardo de Moura
6ca80b5000 feat(frontends/lean): add 'sorry'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-31 18:35:57 -07:00
Leonardo de Moura
de05c041c7 feat(library/unifier): add flag for enabling/disabling expensive extensions in the unifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-31 16:46:16 -07:00
Leonardo de Moura
f57fc33442 fix(library/unifier): bug that was making unifier miss solutions, and add a new case-split that tries to solve flex_rigid constraints by putting the rhs into whnf
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-31 16:46:16 -07:00
Leonardo de Moura
9637ceb86e feat(frontends/lean): allow user to provide a terminator for 'foldr' and 'foldl'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-30 15:04:44 -07:00
Leonardo de Moura
450131692a fix(library/converter): missing constraint on eta expansion
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-30 10:43:47 -07:00
Leonardo de Moura
936bb2744b fix(library/unifier): add a flag to sign that a choice constraint owns a metavariable ?m, that is, it has the right to assign ?m, and the unifier should postpone any other constraint that tries to assign ?m
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 17:32:55 -07:00
Leonardo de Moura
b15f1bb8c7 fix(frontends/lean/elaborator): apply coercions in definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 13:55:39 -07:00
Leonardo de Moura
501cae37e5 fix(frontends/lean/parser): bug in check_constant_next (when invoked inside of a section)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-29 13:04:58 -07:00
Leonardo de Moura
105c29b51e refactor(library/standard): use new coding style, rename bool.b0 and bool.b1 to bool.ff and bool.tt
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-28 19:59:38 -07:00
Leonardo de Moura
4b2e403023 test(tests/lean/run): add more tests sent by Cody
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:17:38 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 12:12:54 -07:00
Leonardo de Moura
6ca120bf77 test(tests/lean/run): add Cody's file to test suite
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-27 08:17:46 -07:00
Leonardo de Moura
23af5ab217 fix(library/unifier): eager whnf application
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-26 10:37:02 -07:00
Leonardo de Moura
e79b0b11cf test(tests/lean/run): another test for the unifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 20:55:05 -07:00
Leonardo de Moura
cf44c80ffb fix(library/inductive_unifier_plugin): do not try to solve type incorrect constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 16:00:38 -07:00
Leonardo de Moura
7b84503133 fix(library/unifier): do not let a unification plugin to 'prioritize' a flex-flex constraint, and add missing case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 15:03:57 -07:00
Leonardo de Moura
0f12e5a35b fix(library/inductive_unifier_plugin): unification problem failure on problems with inductive datatypes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 13:49:45 -07:00
Leonardo de Moura
21176c61fe fix(tests/lean): move crash.lean to different directory
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 08:48:35 -07:00
Leonardo de Moura
e7c7d5718a fix(frontends/lean/pp): fix bug in the pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-25 08:30:30 -07:00
Leonardo de Moura
15c1e39f88 feat(frontends/lean/elaborator): distribute application over choice, this feature improves the support for overloaded aliases
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-24 23:43:40 -07:00
Leonardo de Moura
905a1095f9 fix(tests/lean/run/tactic14): remove not_intro, it is not needed anymore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-24 23:41:23 -07:00
Leonardo de Moura
5529ef1056 feat(library/standard): add function 'helper' module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-24 16:29:39 -07:00
Leonardo de Moura
d998bf9300 test(tests/lean/run): add some 'lost' tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-23 08:22:53 -07:00
Leonardo de Moura
b522ea6f2d refactor(library/standard): rename bit to bool
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 09:49:54 -07:00
Leonardo de Moura
5eaf04518b refactor(*): rename Bool to Prop
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 09:43:18 -07:00
Leonardo de Moura
a9f7d87aae test(tests/lean/run/decidable): show implicit argument that is computed automatically
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 05:58:36 -07:00
Leonardo de Moura
5e8c128b00 feat(library/standard): add more decidable instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-20 01:10:49 +01:00
Leonardo de Moura
6b60db7b93 fix(frontends/lean/elaborator): bug when mixing implicit arguments and sections
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-19 09:55:34 +01:00
Leonardo de Moura
0f44e3c9f4 fix(frontends/lean): calc configuration commands, add check_constant_next auxiliary method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-15 01:19:47 +01:00
Leonardo de Moura
2e6184a721 fix(frontends/lean): more bugs in section management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 06:27:36 +01:00
Leonardo de Moura
8167ad329f fix(frontends/lean): bug in section management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 05:04:01 +01:00
Leonardo de Moura
fab7934265 refactor(frontends/lean/elaborator): modify when tactic_hints are invoked, add the notion of strict placeholder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-14 02:53:02 +01:00
Leonardo de Moura
e432e23115 test(tests/lean/run/class5): improve test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-13 22:39:16 +01:00
Leonardo de Moura
1d273fcfdd chore(frontends/lean): rename 'obtains' to 'obtain'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-12 06:35:24 +01:00
Leonardo de Moura
1230e942aa feat(library/unifier): handle 'first-order' flex-flex constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-11 04:51:28 +01:00
Leonardo de Moura
cf34f75ab5 feat(frontends/lean): add 'obtains' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-11 04:08:51 +01:00
Leonardo de Moura
92bb046854 test(tests/lean/run): add nested let-expr test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 15:56:15 +01:00
Leonardo de Moura
c13c75b93e feat(frontends/lean/pp): add option for displaying fully qualified names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 15:55:19 +01:00
Leonardo de Moura
06beff327f test(tests/lean/run): add more universe tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 14:43:55 +01:00
Leonardo de Moura
1a6d0784f2 feat(kernel/level): improve universe level normalization procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 13:49:41 +01:00
Leonardo de Moura
d9b2801eeb feat(frontends/lean): use the same universe in declarations such as (A B : Type)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 13:18:52 +01:00
Leonardo de Moura
12d89ea0b9 fix(kernel/level): is_geq predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-10 13:18:41 +01:00
Leonardo de Moura
aff766430d fix(frontends/lean/pp): universe pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 19:17:28 -07:00
Leonardo de Moura
43eba857cb feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-09 18:47:10 -07:00
Leonardo de Moura
2ad1a93657 test(tests/lean/run): add append tactic test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 18:21:22 -07:00
Leonardo de Moura
a1601e7a5f feat(library/tactic/apply_tactic): add option for 'refreshing' universe metavariables in the 'apply' tactic
The new test ../../tests/lean/run/tactic27.lean demonstrates why we need this feature. The tactic 'apply @refl' is actually 'apply @refl.{?l}'. It is used inside of a repeat tactical. Each iteration of the 'repeat' may need to use a different value for ?l. Before this commit, there was not way to say we want a fresh ?l each iteration.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 16:55:23 -07:00
Leonardo de Moura
4505016154 feat(frontends/lean): allow tactic_hints to be applied when class-instance mechanism fails
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -07:00
Leonardo de Moura
5e836092cc feat(frontends/lean): allow user to suppress proofs in theorems, and let them be inferred automatically using tactic_hints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -07:00
Leonardo de Moura
a3be63af73 feat(frontends/lean): add tactic_hint command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-08 15:08:13 -07:00
Leonardo de Moura
da4c1922e3 feat(frontends/lean): add '_root_' prefix for referencing names in the root namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 19:15:46 -07:00
Leonardo de Moura
b43fb7448c feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 19:00:06 -07:00
Leonardo de Moura
e6d4c01b88 feat(frontends/lean): check whether namespace exists or not in the 'using' command, add to_valid_namespace_name helper function
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 18:17:10 -07:00
Leonardo de Moura
bd1873f6b1 feat(frontends/lean): add coercion modifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 17:48:20 -07:00
Leonardo de Moura
08465f049a feat(frontends/lean): remove [class] annotation and 'class' command, they are redundant, we only need [instance] and 'instance'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 16:09:30 -07:00
Leonardo de Moura
112353861c feat(frontends/lean): rename command 'reset_proof_qed' to 'set_proof_qed'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 15:48:16 -07:00
Leonardo de Moura
c16951aba6 fix(library/aliases): aliasing behavior
The new test '../../tests/lean/run/alias3.lean' demonstrates the issue being fixed.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 15:40:55 -07:00
Leonardo de Moura
b9d08ff28c feat(frontends/lean/builtin_cmds): allow many namespaces in the same 'using' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 14:53:06 -07:00
Leonardo de Moura
d30f387e72 feat(library/standard): add namespace 'pair'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 14:48:19 -07:00
Leonardo de Moura
10b0dfeb37 feat(frontends/lean/class): allow many instances to provided with a single 'instance' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 14:41:14 -07:00
Leonardo de Moura
b956ce68d2 feat(frontends/lean/elaborator): keep postponing delayed coercions until the type can be inferred
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 12:50:43 -07:00
Leonardo de Moura
831de22bcd fix(frontends/lean): bugs in notation management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-07 09:31:42 -07:00
Leonardo de Moura
e8bd267a00 fet(frontends/lean): allow coercions to sort-class in the types of variable and definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 21:54:16 -07:00
Leonardo de Moura
48b28ad75c fix(library/unifier): missing test in flex_rigid
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 21:36:23 -07:00
Leonardo de Moura
dcf7cf00ff fix(*): bugs in the type checker, inductive datatypes, and unifier
The bugs were indentified when performing the tiny change in the file
tests/lean/run/group.lean
2014-07-06 18:44:56 -07:00
Leonardo de Moura
9a13bef4f3 fix(frontends/lean): fix (and simplify) parameter universe inference
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-06 16:56:54 -07:00
Leonardo de Moura
8e5ac54ae1 test(tests/lean/run): group experiments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 22:31:57 -07:00
Leonardo de Moura
55894f01e3 feat(frontends/lean): add 'opaque_hint' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 18:58:20 -07:00
Leonardo de Moura
e68a3e5251 test(tests/lean/run): add another class-instance example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 17:41:08 -07:00
Leonardo de Moura
59755289e4 feat(library/unifier): case split on constraints of the form (f ...) =?= (f ...), where f can be unfolded, and there are metavariables in the arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 15:52:40 -07:00
Leonardo de Moura
a52c9f4e2b feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 09:43:16 -07:00
Leonardo de Moura
efabd2280c feat(library/unifier): allow unifier to unfold opaque definitions of the current module
It is not clear whether this is a good idea or not. In some cases, it seems to do more harm than good.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-05 00:46:03 -07:00
Leonardo de Moura
99fb6431a6 fix(frontends/lean/elaborator): support for local instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 18:38:08 -07:00
Leonardo de Moura
8ab0b5bee3 feat(frontends/lean/elaborator): use local declarations as class instances
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 18:18:25 -07:00
Leonardo de Moura
00e1a7db23 feat(frontends/lean/elaborator): add class instance elaboration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 15:45:50 -07:00
Leonardo de Moura
b94ce412ae fix(library/unifier): non-termination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 10:32:01 -07:00
Leonardo de Moura
a97f82be1a fix(library/standard): orelse notation, avoid conflict with inductive datatype declaration
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 10:10:05 -07:00
Leonardo de Moura
e0501104e2 feat(library/tactic): add 'fixpoint' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-04 01:30:28 -07:00
Leonardo de Moura
7fb2b0f6d8 feat(kernel): add method 'may_reduce_later' to normalizer_extension, and improve unifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 22:31:05 -07:00
Leonardo de Moura
855ffcba34 feat(library/standard): add pairs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 20:43:16 -07:00
Leonardo de Moura
110b622b83 feat(library/unifier): add support for unification constraints of the form "(elim ... (?m ...)) =?= t", where elim is an eliminator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 20:41:51 -07:00
Leonardo de Moura
b5f63e78ca feat(frontends/lean/notation_cmd): reuse existing precedence to increase compatibility with existing notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 17:23:29 -07:00
Leonardo de Moura
fa1857e6a9 fix(frontends/lean/notation_cmd): fix default, add 'prev' action
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 16:44:44 -07:00
Leonardo de Moura
abbd054b51 feat(library/tactic): add eassumption tactic, and remove redundant 'subgoals' from apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 13:04:46 -07:00
Leonardo de Moura
d63ccbcf94 fix(library/unifier): missing case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 10:51:59 -07:00
Leonardo de Moura
0ff145e59b feat(library/tactic): add apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 09:20:01 -07:00
Leonardo de Moura
c1538bfc40 test(tests/lean/run): add 'apply subst' test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-03 09:07:56 -07:00
Leonardo de Moura
a7d660f875 feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 20:45:10 -07:00
Leonardo de Moura
5527955ba8 feat(frontends/lean): add 'proof-qed' notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 19:30:48 -07:00
Leonardo de Moura
60c637fb9d feat(library/tactic): add 'exact' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:37:32 -07:00
Leonardo de Moura
37b5b7c4c2 feat(library/tactic): rename 'exact' to 'assumption', 'exact' is a different tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 18:10:42 -07:00
Leonardo de Moura
ee531ec0e2 feat(frontends/parser): improve error message when an apply tactic refers a local constant that is not marked as [fact]
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 14:09:01 -07:00
Leonardo de Moura
0f27856e4a feat(library/tactic): new apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 13:14:50 -07:00
Leonardo de Moura
6ab46396d8 feat(library/tactic): expose 'trace' tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:52:45 -07:00
Leonardo de Moura
e1d909455c refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:45:09 -07:00
Leonardo de Moura
a66a08c89e feat(frontends/lean): parse strings as expressions of type 'string.string'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 10:00:55 -07:00
Leonardo de Moura
0198dfc7c5 feat(frontends/lean): parse numerals as expressions of type 'num.num'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:09:33 -07:00
Leonardo de Moura
7593ee1468 refactor(library/standard): remove parameter from 'tactic' inductive type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-02 08:09:24 -07:00
Leonardo de Moura
b2b76b078f feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 20:43:53 -07:00
Leonardo de Moura
5b69f88664 feat(frontends/lean/notation_cmd): make the notation for setting precedence uniform
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-01 16:55:41 -07:00
Leonardo de Moura
8d584e54da feat(frontends/lean): add exact_apply
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-30 00:51:11 -07:00
Leonardo de Moura
33cb9382aa feat(frontends/lean): add beta-reduction tactic command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 19:41:54 -07:00
Leonardo de Moura
360e9b9486 feat(library/tactic): add apply tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 18:33:53 -07:00
Leonardo de Moura
6645fdeae0 feat(frontends/lean): add repeat tactic command, refactor tactic sequence notation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 12:24:13 -07:00
Leonardo de Moura
2510d5722a feat(frontends/lean): add unfold tactic command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 12:05:45 -07:00
Leonardo de Moura
6d09d82a7c feat(frontends/lean): add notation for orelse tactic, add show and now tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 11:39:18 -07:00
Leonardo de Moura
a1bbb09de4 feat(frontends/lean): add notation for then tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 11:24:56 -07:00
Leonardo de Moura
ffa175009b feat(frontends/lean): use tactics for solving unassigned metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 09:50:16 -07:00
Leonardo de Moura
1e39a21823 feat(frontends/lean): add basic tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 09:03:51 -07:00
Leonardo de Moura
7d5522e36a chore(tests): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 09:03:51 -07:00
Leonardo de Moura
cf28981f45 feat(tests/lean/run): add test_single script that sets the LEAN_PATH
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-29 07:47:46 -07:00
Leonardo de Moura
193ce35419 refactor(frontends/lean/inductive_cmd): redesign inductive datatype elaboration, use the new elaborator, and use simpler algorithm to infer the resulting universe
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 15:33:56 -07:00
Leonardo de Moura
0adacb5191 feat(kernel): add infer implicit, and use it to infer implicit arguments of inductive datatype eliminators, and tag whether parameters should be implicit or not in introduction rules in the module inductive_cmd
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 13:57:36 -07:00
Leonardo de Moura
47ff300d1a fix(frontends/lean): '@' explicit mark
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-28 07:30:36 -07:00