Commit graph

970 commits

Author SHA1 Message Date
Leonardo de Moura
ce634d4459 test(lua): well-founded induction
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-22 14:10:25 -07:00
Leonardo de Moura
1447d7e765 test(lua): add another inductive datatype example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-22 14:10:25 -07:00
Leonardo de Moura
6246fae32c fix(kernel/inductive): inductive datatype declaration validation bug pointed out by Cody Roux
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 16:29:25 -07:00
Leonardo de Moura
b9d7f8e867 test(lua): make sure bug reported by Floris does not happen in Lean 0.2
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 13:34:04 -07:00
Leonardo de Moura
203a59b682 test(lua): add more tests for the environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 12:36:04 -07:00
Leonardo de Moura
9f4bae6856 feat(library/kernel_bindings): add hott_environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:49:30 -07:00
Leonardo de Moura
4d1fecb21d refactor(library/kernel_bindings): rename empty_environment ==> bare_environment in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:24:24 -07:00
Leonardo de Moura
f08a852da8 feat(library/kernel_bindings): expose environment::add(declaration) method in the Lua API, and add example to demonstrate its usage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-21 11:12:55 -07:00
Leonardo de Moura
3726688711 test(lua): add test to demonstrate the different between list(A) where A is a parameter, and where A is an index
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 12:17:16 -07:00
Leonardo de Moura
11fc917102 test(lua): add tests for improving kernel_bindings coverage
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 12:16:12 -07:00
Leonardo de Moura
c5e8c10c9d fix(library/normalize): bug in normalize
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 11:53:58 -07:00
Leonardo de Moura
fae07771ec test(lua): add more universe level expression tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 11:41:17 -07:00
Leonardo de Moura
8872d4a531 refactor(kernel): rename definition class to declaration
The name was misleading since not every declaration is a definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 10:41:38 -07:00
Leonardo de Moura
00b1a84051 feat(library/kernel_bindings): expose environment::for_each method in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 10:16:19 -07:00
Leonardo de Moura
9e55c8766f test(lua): add normalize and type_check tests for terms containing metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 09:56:27 -07:00
Leonardo de Moura
ddccca529a test(lua): add test for mutually recursive inductive type recursor/eliminator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 09:41:50 -07:00
Leonardo de Moura
eb6807e1d3 test(lua): add another add_inductive example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 17:48:35 -07:00
Leonardo de Moura
4f15240a71 test(lua): add tests for new Pi/Fun notation in Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 17:17:15 -07:00
Leonardo de Moura
a72be5eea4 test(lua): add example suggested by Cody
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 17:06:19 -07:00
Leonardo de Moura
3e3d3c8380 feat(kernel/inductive): check in add_inductive whether the environment supports inductive datatypes or not
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 15:44:15 -07:00
Leonardo de Moura
a7aacaa782 feat(library/kernel_bindings): improve list_level support in the Lua interface
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 15:18:48 -07:00
Leonardo de Moura
48b436c1c8 test(lua): add Martin-lof identity type test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 13:42:49 -07:00
Leonardo de Moura
f3ed20a229 feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 12:52:25 -07:00
Leonardo de Moura
2aacb769dd feat(kernel/inductive): generate computational rules RHS for inductive datatypes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-19 09:08:19 -07:00
Leonardo de Moura
28b70b4e04 feat(kernel/inductive): use nondependent elimination when the datatype is in Bool/Prop
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-18 15:39:48 -07:00
Leonardo de Moura
45252e2229 feat(kernel/inductive): add eliminator/recursor for inductive datatype declarations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-18 14:17:57 -07:00
Leonardo de Moura
f53254b389 test(lua): fix n6.lua, and add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-18 13:52:16 -07:00
Leonardo de Moura
405b24861c feat(util/name): add methods append_after and append_before
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-18 13:49:24 -07:00
Leonardo de Moura
fcf94ad7c2 test(lua): add test for inductive datatype positivity check
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 20:12:55 -07:00
Leonardo de Moura
950d69b977 test(lua): add tests for exercising datatype validation code
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 20:10:45 -07:00
Leonardo de Moura
b5d07bec2e test(lua): add some comments to inductive datatype test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 19:30:43 -07:00
Leonardo de Moura
8fcb84c8f2 feat(kernel/inductive): finish inductive datatype declaration validation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 19:19:32 -07:00
Leonardo de Moura
d03e35aaac feat(kernel/inductive): add datatype and introduction rules declarations to environment, and fix tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 13:59:06 -07:00
Leonardo de Moura
53e02a902c test(lua): add is_geq (for universe level) tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 13:42:12 -07:00
Leonardo de Moura
a85a6b685b feat(kernel/formatter): add binding_body_fresh, let_body_fresh, and simplify formatter
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 12:30:03 -07:00
Leonardo de Moura
5ce134e24e chore(kernel): binder => binding where appropriate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 11:37:27 -07:00
Leonardo de Moura
3a0861bca7 test(lean): remove old test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 10:42:10 -07:00
Leonardo de Moura
9f06cd553e test(lean): remove tests using Lean old syntax and kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 10:38:53 -07:00
Leonardo de Moura
989bcdc7ad test(lua): add inductive datatype simple tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 09:25:03 -07:00
Leonardo de Moura
4ec89e8561 feat(library/kernel_bindings): add sugar for level expressions in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-17 08:10:36 -07:00
Leonardo de Moura
755fac8114 test(lua): add test simulating HoTT compatible environment
Type.{0} is predicative
   Type.{0} is proof relevant
   Id       is proof irrelevant
   Path     is proof relevant

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:32:01 -07:00
Leonardo de Moura
69e72c278d feat(kernel): add proof irrelevance for classes
We can use this feature to implement proof irrelevance for Identity types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 15:30:32 -07:00
Leonardo de Moura
193aa4a83f feat(library/kernel_bindings): improve Pi and Fun Lua APIs, and allow users to provide binder information
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 14:09:00 -07:00
Leonardo de Moura
40b3129e7b refactor(kernel): improve names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-16 11:28:05 -07:00
Leonardo de Moura
924b2344af fix(lua/res1): make sure the test works with Lua 5.1
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 14:47:42 -07:00
Leonardo de Moura
da31e60b02 test(lua): add more tests for type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 14:17:58 -07:00
Leonardo de Moura
90c4957071 test(lua): add tests for resolve macro
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:11 -07:00
Leonardo de Moura
7c0cc3111a fix(kernel/type_checker): we must use different caches for infer_type and check
The new test tc4.lua exposes the problem being fixed.
We need separate caches otherwise we may mistakenly assume that an expression was already checked by the type checker, while only its type was inferred.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 13:53:11 -07:00
Leonardo de Moura
6e78256b87 feat(library/kernel_bindings): expose is_bi_equal predicate in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 17:24:49 -07:00
Leonardo de Moura
606e6226c2 fix(kernel/type_checker): the type checker cache was not taking into account binder information
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 17:14:57 -07:00
Leonardo de Moura
2e1a0bd50c feat(kernel/expr): add is_contextual binder info
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 14:54:27 -07:00
Leonardo de Moura
52d682b832 test(lua): unit tests for let expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 14:29:44 -07:00
Leonardo de Moura
e57b943adf test(lua): add constraint generation test when type checking with metavars
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-14 11:06:48 -07:00
Leonardo de Moura
eea561c74b test(lua): add more expr API unit tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-13 09:20:25 -07:00
Leonardo de Moura
cfa9520655 test(lua): add more level API unit tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-13 09:20:10 -07:00
Leonardo de Moura
9ed700a5a6 feat(kernel/environment): add forget method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-13 08:40:46 -07:00
Leonardo de Moura
7b15e558a2 refactor(kernel/converter): implement eta in whnf instead of is_def_eq.
Without cumulativity, we do not have problems with Eta at whnf anymore.
When we had cumulativity, we could not not simply reduce
     (fun x : A, f x) ==> f
This step is correct only if domain(f) was definitionally equal to f.
Here is a problematic example for systems with cumulativity
Given, f : Type.{2} -> Bool
     (fun x : Type.{1}, f x)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 17:49:53 -07:00
Leonardo de Moura
c883c638d6 feat(library/kernel_bindings): expose expression tags in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 16:50:43 -07:00
Leonardo de Moura
20947de2f1 test(lua): add replace method test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 15:51:22 -07:00
Leonardo de Moura
9f86aa73c8 test(lua): add basic universe level tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-12 14:51:18 -07:00
Leonardo de Moura
ff9004dae2 refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-11 18:05:02 -07:00
Leonardo de Moura
9d96f24766 refactor(kernel): remove convertability constraints
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:25:27 -07:00
Leonardo de Moura
7b6d555433 refactor(kernel): remove level constraints from definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 20:11:50 -07:00
Leonardo de Moura
a650a4f9b5 fix(library/kernel_bindings): bug in mk_app, add expr_lt tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-09 19:54:52 -07:00
Leonardo de Moura
21e3e22017 test(lua/threads): re-activate Lua thread examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:52:15 -07:00
Leonardo de Moura
129d108d0b test(lua): add example for testing is_descendant
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:50:24 -07:00
Leonardo de Moura
c843243f64 feat(library/kernel_bindings): add add_decl and type_check functions to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 18:08:32 -07:00
Leonardo de Moura
5a7f181efc feat(util/name_set): improve name_set Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-08 17:17:00 -07:00
Leonardo de Moura
f3c7bc948a feat(library/kernel_bindings): type_checker Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 19:04:15 -07:00
Leonardo de Moura
1a8d75c4f0 feat(util): name_set Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 18:32:53 -07:00
Leonardo de Moura
7fe61bc69c feat(util): name_generator Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 17:28:11 -07:00
Leonardo de Moura
62db010ba3 feat(library/kernel_bindings): add optional arguments to empty_environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 17:06:27 -07:00
Leonardo de Moura
4c5f88e63b feat(library/kernel_bindings): global level constructor/accessor/recognizer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 16:22:45 -07:00
Leonardo de Moura
8ae0e46e9d feat(library/kernel_bindings): add new global level methods to environment Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-07 16:17:04 -07:00
Leonardo de Moura
9bf83390dc test(lua): add definition API tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 17:01:22 -07:00
Leonardo de Moura
dc627c9965 test(lua): add constraint API tests, and fix minor bugs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 13:37:46 -07:00
Leonardo de Moura
7b4b862faa test(lua): add justification API tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-02 12:16:24 -07:00
Leonardo de Moura
340c0e0945 feat(library/kernel_bindings): substitution Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 15:30:30 -07:00
Leonardo de Moura
305815cb56 feat(library/kernel_bindings): expose expr_binder_info in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-01 11:23:37 -07:00
Leonardo de Moura
97e7e4e762 test(lua): remove obsolete test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 17:08:50 -07:00
Leonardo de Moura
fd034521dc feat(library/kernel_bindings): cleanup level Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 17:05:25 -07:00
Leonardo de Moura
93a61748e9 fix(kernel/level): bug in optional<level>() constructor
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 17:00:57 -07:00
Leonardo de Moura
984048f40d feat(library/kernel_bindings): new level Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 15:08:58 -07:00
Leonardo de Moura
a6116e3156 test(lua): reactivate some of the Lua unit tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-04-29 10:36:57 -07:00
Leonardo de Moura
e9dada5e14 refactor(builtin/kernel): use standard definition for 'or' and 'and'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-17 12:05:34 -08:00
Leonardo de Moura
1739b5c153 fix(kernel/type_checker): caching bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-12 10:43:01 -08:00
Leonardo de Moura
368fcb5ff9 refactor(builtin/kernel): rename refute to by_contradiction
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-12 08:49:19 -08:00
Leonardo de Moura
b7b868de85 fix(library/elaborator): bug reported by Jeremy Avigad
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-10 14:01:22 -08:00
Leonardo de Moura
a2d2e36f04 refactor(frontends/lean): remove notation for creating tuples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-10 09:03:42 -08:00
Leonardo de Moura
4317f67bd2 fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 18:57:33 -08:00
Leonardo de Moura
c45c1748d8 refactor(builtin/kernel): reorder congr1 arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 16:15:44 -08:00
Leonardo de Moura
8df7c7b02d feat(kernel/type_checker): remove fallback that expands opaque definitions in the type checker
We should not rely on this feature. It can be quite expensive.
We invoke is_convertible in several places, in particular, if we are using overloading. For example, the frontend uses is_convertible to check which overload should be used. Thus, it will make several calls such as

   is_convertible(num, Nat)

If is_convertible starts unfolding opaque definitions, we would keep expanding num.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 11:31:24 -08:00
Leonardo de Moura
1ec01f5757 refactor(builtin): merge pair.lean with kernel.lean, and add basic theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 16:04:44 -08:00
Leonardo de Moura
ad7b13104f feat(*): add support for heterogeneous equality in the parser, elaborator and simplifier, adjusts unit test to reflect changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-07 15:03:16 -08:00
Leonardo de Moura
d4b08fcf96 feat(library/elaborator): be 'lazy' when normalizing terms in the elaborator
Unification constraints of the form

         ctx |- ?m[inst:i v] == T

         and

         ctx |- (?m a1 ... an) == T

are delayed by elaborator because the produce case-splits.
On the other hand, the step that puts terms is head-normal form is eagerly applied.
This is a bad idea for constraints like the two above. The elaborator will put T in head normal form
before executing process_meta_app and process_meta_inst. This is just wasted work, and creates
fully unfolded terms for solvers and provers.

The new test demonstrates the problem. In this test, we mark several terms as non-opaque.
Without this commit, the produced goal is a huge term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 21:08:00 -08:00
Leonardo de Moura
593f1f2ebd fix(frontends/lean): allow user set constants defined in other namespaces as opaque
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 20:56:31 -08:00
Leonardo de Moura
363c4dc5c2 feat(library/elaborator): improve support for dependent pairs in the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 20:56:31 -08:00
Leonardo de Moura
ea06bb2885 feat(frontends/lean/pp): change how lift local entries are pretty printed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 17:26:38 -08:00
Leonardo de Moura
a51139e63b feat(frontends/lean): position information in error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 17:26:38 -08:00
Leonardo de Moura
e4579b93e4 fix(library/elaborator): try first projection before imitation in the higher-order unifier
Projections build more general solutions. This commit also adds a test that demonstrates the issue. Before this commit, the elaborator would produce the "constant" predicate (fun x, a + b = b + a).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 13:35:05 -08:00
Leonardo de Moura
ef321e730f feat(builtin/tactic): add the 'skip' (bogus) tactic for ignoring a proof hole in a big proof
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 12:47:23 -08:00
Leonardo de Moura
eab0456b27 test(tests/lean): test super opaque style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 11:33:27 -08:00
Leonardo de Moura
fdc4c9b53c test(tests/lean): add nested 'have' expression test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 08:13:04 -08:00
Leonardo de Moura
1d23d93e60 feat(frontends/lean): new 'have' expression
Add 'have' notation suggested by Jeremy Avigad.
Add his example to the test suite.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 08:03:59 -08:00
Leonardo de Moura
ba9a8f9d98 feat(frontends/lean): add 'show' expression syntax sugar
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-06 07:50:22 -08:00
Leonardo de Moura
419fb7464e fix(tests/lean): adjust tests to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-05 21:04:06 -08:00
Leonardo de Moura
aec9c84d0d fix(util/lua): deadlock
Errors in the Lua library produce longjmps.
The longjmp will not unwind the C++ stack.
In the new test, the lock was not being released, and the system was deadlocking in the next call that tried to lock the environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 15:16:29 -08:00
Leonardo de Moura
f4ec874c6e refactor(builtin): remove dead module heq
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 14:42:28 -08:00
Leonardo de Moura
0283887ee9 refactor(builtin/kernel): move the heq axioms into kernel.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 14:17:34 -08:00
Leonardo de Moura
f03c09c10b feat(library/elaborator): add support for proj/pair/sigma in the the higher-order unification procedure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 13:53:30 -08:00
Leonardo de Moura
413391b2b4 chore(tests/lean/sig2): remove unnecessary parenthesis from test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 11:37:08 -08:00
Leonardo de Moura
c9b72df34b fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 11:36:26 -08:00
Leonardo de Moura
96c9c7505a test(tests/lean): add another sigma-type test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 10:12:39 -08:00
Leonardo de Moura
9dc86e3cf5 fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 10:06:29 -08:00
Leonardo de Moura
4fcc292332 feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 22:10:01 -08:00
Leonardo de Moura
cc96b50644 feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 20:53:11 -08:00
Leonardo de Moura
5c991f8fbf feat(frontends/lean): parse and pretty print tuples/pairs
This commit also fixes a bug in the type checker when processing dependent pairs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 20:10:30 -08:00
Leonardo de Moura
640ebcc040 test(tests/lean/exp): add example for Steve
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 11:35:40 -08:00
Leonardo de Moura
e4afa3dc43 fix(tests/lean/map): incorrect output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 00:05:19 -08:00
Leonardo de Moura
87f9c9b27e fix(tests/lean/map): make sure the unit test produce the same result in different platforms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 20:29:34 -08:00
Leonardo de Moura
e2add5c9f2 test(tests/lean): add heterogeneous equality simplification example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 20:27:39 -08:00
Leonardo de Moura
6be50f0133 refactor(builtin/heq): merge cast and heq modules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 15:01:48 -08:00
Leonardo de Moura
c56df132b8 refactor(kernel): remove semantic attachments from the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 14:48:27 -08:00
Leonardo de Moura
2b7bc7b673 test(tests/lean/exp): simulating HOL constructions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 17:59:57 -08:00
Leonardo de Moura
e3dc552c39 fix(library/simplifier): nontermination
The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition

    definition a := 1

it will match 'a' with '1' since they are definitionally equal.

Then, if we have a theorem

    theorem a_eq_1 : a = 1

as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"

   a --> 1 --> 1 --> 1 ...

The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.

To avoid this loop, we test if the new expression is not equal to the previous one.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 15:55:21 -08:00
Leonardo de Moura
1d85267d26 fix(library/simplifier): assumptions/context may contain equations where the left-hand-side is a metavariable or semantic attachment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 15:38:22 -08:00
Leonardo de Moura
110ca84984 feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 13:49:24 -08:00
Leonardo de Moura
759aa61f70 refactor(builtin/kernel): define if-then-else using Hilbert's operator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 19:28:42 -08:00
Leonardo de Moura
b45ab9dc30 feat(library/elaborator): use equality constraints instead of convertability constraints on definitions
Convertability constraints are harder to solve than equality constraints, and it seems they don't buy us anything definitions. They are just increasing the search space for the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 14:13:21 -08:00
Leonardo de Moura
8c1f6b9055 fix(kernel/typechecker): allow elaborator to infer (Type U+1)
In the new test elab8.lean, the parameter B is in (Type U+1).
Before, this commit, the type checker was forcing all metavariables that must be types to be <= (Type U). This restriction was preventing the elaborator from succeeding in reasonable cases.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 14:00:01 -08:00
Leonardo de Moura
41f5e2a067 feat(library/simplifier): statically check (conditional) equations (aka rewrite rules) to verify whether we can skip type checking when using them in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 18:32:40 -08:00
Leonardo de Moura
01259b1e84 feat(kernel): make sure U is the maximal universe
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 16:31:00 -08:00
Leonardo de Moura
ea6bf224e5 feat(frontends/lean): make the parser accept (Type -> ...)
Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 15:23:20 -08:00
Leonardo de Moura
4f3127d3d5 fix(library/simplifier): check if the given types are convertible to ceq expected types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 15:15:55 -08:00
Leonardo de Moura
0bb8fe75b3 test(tests/lean): new simplifier test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 14:21:18 -08:00
Leonardo de Moura
a19f9d4846 feat(library/simplifier): discard conditional equations that are clearly non-terminating
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 13:56:45 -08:00
Leonardo de Moura
dd6aae378f fix(library/simplifier): must use metavar_env in is_ceq, otherwise it may ceqs that contain metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 13:29:20 -08:00
Leonardo de Moura
4dc3aa46c3 feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 12:02:12 -08:00
Leonardo de Moura
069e5edf6b fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 12:01:01 -08:00
Leonardo de Moura
62408a6adc test(tests/lean): move simp_loop test to slow subdirectory
This example produces a stackoverflow on Valgrind.
We don't execute Valgrind on tests in the slow subdirectory.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 10:32:48 -08:00
Leonardo de Moura
92ba4e8b2d feat(library/simplifier): add support for metavariables in conditional rewrite rules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-29 08:34:04 -08:00
Leonardo de Moura
ee4344076e feat(library/simplifier): improve error message when simplifier is looping
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 19:36:31 -08:00
Leonardo de Moura
72c607846a test(tests/lean): add Jeremy's proof to test suite
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 16:05:46 -08:00
Leonardo de Moura
7f53cb9601 feat(frontends/lean/parser): add_rewrite take the 'using' command into account
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 01:15:28 -08:00
Leonardo de Moura
b31ef34787 feat(library/simplifier): preserve binder names when applying higher-order rewrite rules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 00:50:27 -08:00
Leonardo de Moura
6da1b447f0 fix(library/hop_match): do not match iff with =
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-28 00:21:05 -08:00
Leonardo de Moura
db45d02078 fix(tests/lean): test discrepancy on OSX
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 23:31:35 -08:00
Leonardo de Moura
7b88d68afb test(tests/lean): add test using simplifier monitor for tracking failures
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 15:11:16 -08:00
Leonardo de Moura
8bccfb947a feat(library/simplifier): expose simplier and simplifier_monitor objects in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 15:02:05 -08:00
Leonardo de Moura
b26035fcf6 feat(kernel/type_checker): improve application type mismatch error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 09:45:17 -08:00
Leonardo de Moura
4d25cb7f47 feat(library/tactic): add simplify_tactic based on the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-26 18:53:18 -08:00
Leonardo de Moura
844572c382 feat(library/simplifier): support for dependent simplification in Pi/forall expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-26 00:32:05 -08:00
Leonardo de Moura
e8bba1ebf3 fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f
Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.

For example, if we had

variable f {A : Type} : A -> Bool

Then, the definition of @f was

definition @f (A : Type) (a : A) : Bool := f A a

This definition is equivalent to
     fun A a, f A a
which is not definitionally equal to
     f
since definitionally equality in Lean ignores Eta conversion.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 20:34:28 -08:00
Leonardo de Moura
9fb3ccb4c0 feat(library/simplifier): support for dependent simplification in lambda expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 16:54:42 -08:00
Leonardo de Moura
5b13ef1b90 test(tests/lean): new simplifier test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 10:56:49 -08:00
Leonardo de Moura
7015089734 fix(library/simplifier): move to locally nameless approach in the simplifier. Contextual simplification may add rewriting rules with free variables, and it is a mess to manage them when using de Bruijn indices
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 10:49:44 -08:00
Leonardo de Moura
7a4eb4b8ed feat(library/simplifier): contextual simplification for A -> B
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 22:32:55 -08:00
Leonardo de Moura
c2381e43f1 fix(library/simplifier): bug in cast elimination
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 21:25:09 -08:00
Leonardo de Moura
35ad156a46 fix(tests/lean): make sure pretty print and parse test passes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:23:55 -08:00
Leonardo de Moura
8f455f5965 fix(frontends/lean): bug in scope construct
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:23:29 -08:00
Leonardo de Moura
7f3e2b3ef4 fix(frontends/lean/parser): bug in 'using' construct
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:09:46 -08:00
Leonardo de Moura
8e0888828d fix(library/simplifier): missing check in mk_hcongr_th
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:09:46 -08:00
Leonardo de Moura
1a3660180e test(tests/lean): add new simplifier test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:09:46 -08:00
Leonardo de Moura
26bea77721 fix(library/simplifier): bug in heterogeneous equality support, and universe commutativity support in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:09:46 -08:00
Leonardo de Moura
dbc100cc2e feat(library/simplifier): cast elimination in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 17:28:14 -08:00
Leonardo de Moura
cd87cb3de4 test(tests/lean): add test for congruence theorem that uses an argument before simplification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 13:26:09 -08:00
Leonardo de Moura
180be5c4a2 feat(library/simplifier): improve contextual simplifications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 13:11:58 -08:00
Leonardo de Moura
5ba2525eab test(tests/lean): add test disabling contextual simplifications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 12:57:05 -08:00
Leonardo de Moura
33193e1ab3 feat(library/simplifier): improve contextual simplifications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 12:54:29 -08:00
Leonardo de Moura
d6692264e8 feat(library/simplifier): contextual simplifications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 12:23:22 -08:00
Leonardo de Moura
1638a7bb02 fix(frontends/lean/pp): compute local shared nodes, and avoid unnecessary let's
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 21:44:24 -08:00
Leonardo de Moura
17cce340f6 fix(library/elaborator): in optimization for metavariable free terms
The optimization was incorrect if the term indirectly contained a metavariable.
It could happen if the term contained a free variable that was assigned in the context to a term containing a metavariable.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 18:06:00 -08:00
Leonardo de Moura
8214c7add4 feat(library/elaborator): compensate the lack of eta-reduction (and eta-expanded normal forms) in the kernel normalizer
Before this commit, the elaborator was solving constraints of the form

       ctx |- (?m x) == (f x)
as
       ?m <- (fun x : A, f x)    where A is the domain of f.

In our kernel, the terms f and (fun x, f x) are not definitionally equal.
So, the solution above is not the only one. Another possible solution is

       ?m  <- f

Depending of the circumstances we want  ?m <- (fun x : A, f x) OR ?m <- f.
For example, when Lean is elaborating the eta-theorem in kernel.lean, the first solution should be used:
       ?m <- (fun x : A, f x)

When we are elaborating the axiom_of_choice theorem, we need to use the second one:
       ?m <- f

Of course, we can always provide the parameters explicitly and bypass the elaborator.
However, this goes against the idea that the elaborator can do mechanical steps for us.

This commit addresses this issue by creating a case-split
       ?m <- (fun x : A, f x)
       OR
       ?m <- f

Another solution is to implement eta-expanded normal forms in the Kernel.

With this change, we were able to cleanup the following "hacks" in kernel.lean:
     @eps_ax A (nonempty_ex_intro H) P w Hw
     @axiom_of_choice A B P H
where we had to explicitly provided the implicit arguments

This commit also improves the imitation step for Pi-terms that are actually arrows.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 13:28:54 -08:00
Leonardo de Moura
331b5846c6 test(library/simplifier): add test for the single_pass option in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-21 13:47:54 -08:00
Leonardo de Moura
ead54bbf57 feat(library/simplifier): enforce max_steps option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-21 12:12:17 -08:00
Leonardo de Moura
1ccfac5873 feat(library/simplifier): conditional rewriting
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 21:15:46 -08:00
Leonardo de Moura
1ef75a9ba6 test(tests/lua): add test/example that demonstrates how to collect statistics of used theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 18:04:22 -08:00
Leonardo de Moura
6bcd8e3ee5 fix(library/expr_lt): use expression depth instead of size to obtain a monotonic total order on terms
It is not incorrect to use size, but it can easily overflow due to sharing.
The following script demonstrates the problem:

local f = Const("f")
local a = Const("a")
function mk_shared(d)
   if d == 0 then
      return a
   else
      local c = mk_shared(d-1)
      return f(c, c)
   end
end
print(mk_shared(33):size())

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 17:40:49 -08:00
Leonardo de Moura
cd19d4da01 feat(library/simplifier): memoize intermediate results
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 17:03:44 -08:00
Leonardo de Moura
97ead50a3e feat(builtin/Nat): flip orientation of associativity axioms for + and *
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 15:38:00 -08:00
Leonardo de Moura
d1bd56b3d3 fix(tests/lean): adjust test to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 14:47:03 -08:00
Leonardo de Moura
ad219d43d9 refactor(*): semantic attachment parsing and simplification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 14:44:45 -08:00
Leonardo de Moura
ac9f8f340d feat(kernel/expr): add efficient get_size() function for expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 12:28:37 -08:00
Leonardo de Moura
5224df56a3 test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 08:36:48 -08:00
Leonardo de Moura
913d893204 feat(library/simplifier): add support for 'permutation' rewrite rules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 08:29:31 -08:00
Leonardo de Moura
69d7ee316f feat(library/simplifier): improve simplification by evaluation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 23:26:34 -08:00
Leonardo de Moura
bcede6925f fix(tests/lean): add expected result file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 16:31:35 -08:00
Leonardo de Moura
19f3c281c3 test(tests/lean): matrix multiplication example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 16:29:32 -08:00
Leonardo de Moura
999984e701 fix(tests/lean): remove unnecessary theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 12:55:33 -08:00
Leonardo de Moura
cc11b9e125 test(tests/lean): rewriting proof example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 12:53:21 -08:00
Leonardo de Moura
d322f63113 feat(frontends/lea): add commands for creating and managing rewrite rule sets
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 12:03:59 -08:00
Leonardo de Moura
bbf6e6a256 feat(builtin/kernel): create default rule set in the kernel, and adjust unit tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 11:24:20 -08:00
Leonardo de Moura
7492fd5a2c feat(library/simplifier): add support for simplification by evaluation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 10:34:55 -08:00
Leonardo de Moura
11719713ec feat(library/hop_match): optionally unfold constants when performing higher order matching
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 10:32:06 -08:00
Leonardo de Moura
39c3b17eb7 feat(library/simplifier): add support for Eta-reduction in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 00:40:35 -08:00
Leonardo de Moura
ed009f4c88 feat(kernel/simplifier): add support for Beta-reduction in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 00:40:20 -08:00
Leonardo de Moura
7a3aab60c6 chore(builtin/kernel): remove \bowtie as notation for transitivity
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-18 21:11:12 -08:00
Leonardo de Moura
32c5bc25e3 refactor(library/simplifier): cleanup rewrite_rule_set, and use it in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-18 20:52:33 -08:00
Leonardo de Moura
feea96e84d feat(library/simplifier): add rewrite_rule_set extension for managing rewrite rules in an environment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-18 15:43:24 -08:00
Leonardo de Moura
40b7ed13c2 fix(tests/lean): adjust tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-17 19:27:32 -08:00
Leonardo de Moura
fc4c6454a7 chore(tests/lean): adjust tests to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-17 14:36:55 -08:00
Leonardo de Moura
a43020b31b refactor(kernel): remove heterogeneous equality
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-16 17:39:12 -08:00
Leonardo de Moura
5453a8f2f1 test(tests/lua): hop_match experiment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-16 00:15:31 -08:00
Leonardo de Moura
3238c7e2a0 feat(library/simplifier): add is_permutation_ceq predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 19:53:52 -08:00
Leonardo de Moura
2368c936d3 test(tests/lua): exercise fields method for semantic attachments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 17:24:18 -08:00
Leonardo de Moura
57e58c598c fix(tests/lean): adjust tests to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 16:35:33 -08:00
Leonardo de Moura
c73398a0b8 refactor(library/simplifier): relax rule for conditional equalities
The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference.
For example, we will be able to have the eta theorem as rewrite rule:

theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 16:06:00 -08:00
Leonardo de Moura
3daac17ea8 feat(library/simplifier): convert disequalities (a ≠ b) into equations '(a = b) = false'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 15:30:16 -08:00
Leonardo de Moura
f67b5c4d00 test(tests/lua): more to_ceqs tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 13:50:35 -08:00
Leonardo de Moura
c651d3ea2d feat(library/simplifier): filter out propositions that cannot be used as conditional equations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 12:06:27 -08:00
Leonardo de Moura
94fa987814 fix(kernel/type_checker): is_proposition method was still assuming that a Pi never has type Bool
The method is_proposition was using an optimization that became incorrect after  we identified Pi and forall.
It was assuming that any Pi expression is not a proposition.
This is not true anymore. Now, (Pi x : A, B) is a proposition if B is a proposition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 11:02:52 -08:00
Leonardo de Moura
91e1f9fc02 fix(tests/lean): adjust test to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 10:20:35 -08:00
Leonardo de Moura
3ab2d2a441 fix(frontends/lean/parser): memory leak due to g++ bug
g++ implementation of std::initializer_list has bug.
http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html

This commit memory leaks triggered by this bug.
It also adds minimal tests to expose three different instances of the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 10:15:04 -08:00
Leonardo de Moura
97d9765992 fix(tests/lua/threads): increase timeout to make sure it passes the test on slow machines
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 08:46:14 -08:00
Leonardo de Moura
c8e1ec87d2 feat(library/simplifier): add to_ceqs function that converts a theorem into a sequence of conditional equations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 18:30:19 -08:00
Leonardo de Moura
7c2a4211a8 feat(kernel): expose imported predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 16:41:40 -08:00
Leonardo de Moura
8217a544cc fix(library/hop_match): bugs in the higher-order matching procedure, add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 14:37:28 -08:00
Leonardo de Moura
485ca842c9 test(tests/lua): extra tests for Lua hierachical name API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-14 11:38:10 -08:00
Leonardo de Moura
4595c50f7e fix(library/hop_match): in locally bound variable management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 18:06:23 -08:00
Leonardo de Moura
ccb9faf065 refactor(*): error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 16:54:21 -08:00
Leonardo de Moura
55aa4cbfa3 feat(frontends/lean): improve error message for expressions containing unsolved metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 13:21:44 -08:00
Leonardo de Moura
12451e4a35 feat(frontends/lean/pp): display implicit arguments when expression contains metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 12:42:05 -08:00
Leonardo de Moura
84f017f127 chore(tests/lua): use default environment instead of creating a new one
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 18:24:04 -08:00
Leonardo de Moura
35bacf95fc feat(shell): provide the default environment when parsing Lua files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 18:21:14 -08:00
Leonardo de Moura
7f818ecd92 feat(library): match procedure for higher-order patterns
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-12 17:45:24 -08:00
Leonardo de Moura
b85b45b40f test(tests/lean): When and Cond tactical tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 20:43:39 -08:00
Leonardo de Moura
65bdb9c7e0 fix(frontends/lean): unprotected call to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 19:56:20 -08:00
Leonardo de Moura
411f14415d feat(builtin): automatically generate Lean/C++ interface for builtin theories
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 18:09:53 -08:00
Leonardo de Moura
a339a53f50 feat(util/options): 'verbose' as a system option, add -q (quiet) option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 15:31:58 -08:00
Leonardo de Moura
2179e57db3 refactor(builtin): move if_then_else to its own module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 14:08:39 -08:00
Leonardo de Moura
52e11dbbee test(tests/lean): 'using' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:21:14 -08:00
Leonardo de Moura
fdeb457a81 feat(kernel/pos_info_provider): add support for file names in pos_info_provider
The idea is to include the file name when displaying justification objects.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:19:30 -08:00
Leonardo de Moura
84e211b81b fix(frontends/lean): missing ':' in error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:19:58 -08:00
Leonardo de Moura
f7c7dd4ed4 feat(frontends/lean): include filename in error messages, use GNU error message style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:01:27 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 08:33:52 -08:00
Leonardo de Moura
e42b616438 fix(kernel/normalizer): equality between semantic attachments
Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 19:10:30 -08:00
Leonardo de Moura
a4b3d6d6c8 refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 17:25:14 -08:00
Leonardo de Moura
a6e0dcc96c fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 16:19:11 -08:00
Leonardo de Moura
2b2aa228e3 refactor(builtin/kernel): start with small universes
The universe constraint manager is more flexible now.
We don't need to start with a huge universe  U >= 512.
We can start small, and increase it on demand.

If module mod1 needs it, it can always add

   universe U >= 3

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 12:35:00 -08:00
Leonardo de Moura
abf61be8f6 chore(library/tactic): remove imp_tac, it is not needed anymore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 00:57:04 -08:00
Leonardo de Moura
048151487e feat(kernel): use Pi as forall/implication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 00:38:39 -08:00
Leonardo de Moura
d12d0f036f feat(kernel/environment): universe variables now live in their own namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:57:36 -08:00
Leonardo de Moura
d29d23cade test(tests/lean): alias command error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:29:16 -08:00
Leonardo de Moura
9f4959fb64 test(tests/lean): kernel exception pp method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:19:52 -08:00
Leonardo de Moura
0363faeec8 fix(frontends/lean/scanner): assertion violation, and add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:12:34 -08:00
Leonardo de Moura
29db6accb8 test(tests/lean): new tests for exercising the environment object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 14:34:21 -08:00
Leonardo de Moura
0a20356a51 fix(kernel/environment): we should not add an universe contraint object to the set of object when an integer overflow occurs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 13:43:22 -08:00
Leonardo de Moura
17c4cce89c fix(library/elaborator): remove_detail procedure was keeping a lot of details when typeof_mvar_justification was being used
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 13:24:46 -08:00
Leonardo de Moura
0f1737d62c fix(frontends/lean): more precise position information for infix operators
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 13:19:26 -08:00
Leonardo de Moura
8f3c97ca98 test(tests/lean): standard induction
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 10:18:31 -08:00
Leonardo de Moura
abb9b8af83 fix(frontends/lean): bug in pop::context command, and add new tests for the universe command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 17:14:07 -08:00
Leonardo de Moura
5fe8c32da9 feat(kernel): use new universe contraints in the environment, allow new constraints to be added
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 16:46:11 -08:00
Leonardo de Moura
8c956280d9 chore(frontends/lean): rename setoption and setopaque commands to set::option and set::opaque
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-06 11:41:03 -08:00
Leonardo de Moura
7222a2d1a9 feat(builtin/kernel): use the same notation for mp, eq::mp and forall::elim
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 21:39:31 -08:00
Leonardo de Moura
935c2a03a3 feat(*): change name conventions for Lean builtin libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 19:21:44 -08:00
Leonardo de Moura
4ba097a141 feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 13:06:36 -08:00
Leonardo de Moura
6569b07b7c feat(frontends/lean/parser): rename 'show' expression to 'have'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 11:25:58 -08:00
Leonardo de Moura
0b4bdceb10 feat(builtin/macros): rename 'For' macro to 'take'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 11:08:55 -08:00
Leonardo de Moura
9f08156a73 feat(frontends/lean/parser): combine Echo and Show commands into the 'print' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 11:03:35 -08:00
Leonardo de Moura
ce1213a020 feat(frontends/lean): use '(* ... *)' instead of '(** ... **)' for script code blocks
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 10:32:47 -08:00
Leonardo de Moura
028a9bd9bd feat(frontends/lean/scanner): use Lua style comments in Lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 08:53:27 -08:00
Leonardo de Moura
fbe0bccf51 chore(*): name convention, proof construnction functions/macros start with upper-case
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-03 18:11:01 -08:00
Leonardo de Moura
9eb4dc4a81 feat(kernel, library/elaborator, frontends/lean): improve how elaborator_exceptions are displayed in the Lean frontend
This commit affects different modules.
I used the following approach:
1- I store the metavariable environment at unification_failure_justifications. The idea is to capture the set of instantiated metavariables at the time of failure.
2- I added a remove_detail function. It removes propagation steps from the justification tree object. I also remove the backtracking search space associated with higher-order unificiation. I keep only the search related to case-splits due to coercions and overloads.

3- I use the metavariable environment captured at step 1 when pretty printing the justification of an elaborator_exception.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-03 17:18:23 -08:00
Leonardo de Moura
502d9f47ac test(tests/lean): new test full of holes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 16:31:52 -08:00
Leonardo de Moura
9620b00e24 feat(kernel/metavar): is instantiate_metavars, we are also instantiating assigned metavariables that occur in the local context of unassinged ones.
This modification improves the effectiveness of the process_metavar_inst procedure in the Lean elaborator.

For example, suppose we have the constraint

   ctx |- ?M1[inst:0 ?M2] == a

If ?M1 and ?M2 are unassigned, then we have to consider the two possible solutions:

        ?M1 == a
    or
        ?M1 == #0 and ?M2 == a

On the other hand, if ?M2 is assigned to b, then we can ignore the second case.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 16:08:38 -08:00
Leonardo de Moura
430b75f38f test(tests/lean): add version of the Nat library full of holes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 12:31:13 -08:00
Leonardo de Moura
e714bd7982 feat(frontends/lean): add syntax sugar for applying Subst in calculational proofs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 11:23:55 -08:00
Leonardo de Moura
111949b9be feat(frontends/lean): calculational proofs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-02 10:53:14 -08:00
Leonardo de Moura
b2a8f4118d feat(library/elaborator): process ho-match before normalizing
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 14:46:19 -08:00
Leonardo de Moura
7726ccad28 chore(builtin): rename nat, int and real modules to Nat, Int and Real.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 13:52:25 -08:00
Leonardo de Moura
d633622d90 feat(frontends/lean/parser): namespaces
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 12:28:18 -08:00
Leonardo de Moura
c423198a69 feat(builtin/kernel): add Not.*Elim theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 11:35:21 -08:00
Leonardo de Moura
a8bc9fb4e0 refactor(builtin/kernel): mark exists as opaque after proving key theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 11:00:32 -08:00
Leonardo de Moura
cbd1f98365 fix(library/elaborator): bug at method process_metavar_inst, add new test that exposed the bug
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-01 03:02:41 -08:00
Leonardo de Moura
cd3bbb1ebf fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-31 10:14:17 -08:00
Leonardo de Moura
390a78a8d2 chore(frontends/lean/parser): remove 'Skipped' message
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 15:35:12 -08:00
Leonardo de Moura
08718e33dc refactor(builtin): only load the kernel and natural numbers by default
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 13:35:37 -08:00
Leonardo de Moura
ecd62a1783 refactor(builtin/basic): rename basic.lean to kernel.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:46:03 -08:00
Leonardo de Moura
4401b390fe refactor(library/arith): do not load specialfn by default
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:25:43 -08:00
Leonardo de Moura
46a8300a2d refactor(library/arith): move real and special function declarations to .lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 11:02:22 -08:00
Leonardo de Moura
c3bc6afb12 refactor(library/arith): move int and nat declarations to .lean files.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-30 10:32:14 -08:00
Leonardo de Moura
15621610e9 refactor(library/arith): replace Nat, Int, Real with simple variable decls instead of semantic attachments
This commit also fixes bugs in the Alias command.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 17:04:36 -08:00
Leonardo de Moura
a1a5fb101d feat(frontends/lean): add Alias command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 16:25:45 -08:00
Leonardo de Moura
dfe46b9d25 refactor(kernel/builtin): move definition and axioms to basic.lean
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 14:01:30 -08:00
Leonardo de Moura
f8b82d854e feat(builtin/basic): add TypeM alias
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 13:03:32 -08:00
Leonardo de Moura
411ebbc3c1 refactor(library/basic_thms): move the proof of all basic theorems to a .Lean file
This commit also adds several new theorems that are useful for implementing the simplifier.
TODO: perhaps we should remove the declarations at basic_thms.h?

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-29 03:04:49 -08:00
Leonardo de Moura
41c1010043 feat(frontends/lean/parser): make Import command use binary Lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 19:20:04 -08:00
Leonardo de Moura
1fd81dd3a1 feat(frontends/lean/parser): disable verbose messages when importing files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 12:24:13 -08:00
Leonardo de Moura
44a31dd8fb feat(frontends/lean/parser): improve Import command
- The extension does not have to be provided.
- It can also import Lua files.
- Hierachical names can be used instead of strings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-28 12:05:01 -08:00
Leonardo de Moura
8e86d6578c fix(tests/lean): adjust tests to reflect modifications in the pp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-27 18:38:45 -08:00
Leonardo de Moura
3f0279b88c refactor(frontends/lua): replace lean.lua.h with util.lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 19:49:26 -08:00
Leonardo de Moura
40eca048e0 feat(extra): replace parse_lean_tpl with improved parse_template, that is based on macros
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 19:28:02 -08:00
Leonardo de Moura
275f022d79 fix(tests/lean): ignore lines containing 'executing external script' in test scripts, these lines contain references to the path where Lean was built
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 18:41:01 -08:00
Leonardo de Moura
f1b97b18b4 refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 15:54:53 -08:00
Leonardo de Moura
ef18cc4a92 fix(frontends/lean/parser): add existing command macros when creating parser object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 13:38:14 -08:00
Leonardo de Moura
8e4560a866 feat(frontends/lean/parser): protect imported modules from Lua definitions and macros in the file importing the module
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 13:21:36 -08:00
Leonardo de Moura
ba02132a90 feat(frontends/lean/parser): add command macros
The idea is to allow users to define their own commands using Lua.
The builtin command Find is now written in Lua.
This commit also fixes a bug in the get_formatter() Lua API.
It also adds String arguments to macros.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 13:00:28 -08:00
Leonardo de Moura
480781d13e feat(frontends/lean/parser): provide environment as an argument to macros, allow macros to parse tactics
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 11:15:45 -08:00
Leonardo de Moura
3673f2ac1d feat(frontends/lean/parser): add Find command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 18:31:52 -08:00
Leonardo de Moura
a3dde29f3c feat(frontends/lua/parser): allow users to specify the precedence of macros
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 12:27:56 -08:00
Leonardo de Moura
88235d2922 feat(library/tactic/apply_tactic): try other solutions produced by the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 11:51:27 -08:00
Leonardo de Moura
8e45064f25 feat(library/tactic/apply_tactic): improved parametric apply_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 22:40:34 -08:00
Leonardo de Moura
c87e965f86 fix(tests/lean/tactic14.lean): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 21:36:49 -08:00
Leonardo de Moura
cb95b14332 feat(library/tactic/apply_tactic): improve apply_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 14:23:06 -08:00
Leonardo de Moura
879ab6924a tests(test/lean): remove 'Importing...' message, the tests using the Import command fail when running on a different machine
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 12:26:53 -08:00
Leonardo de Moura
00e89190c2 refactor(library/cast): use .lean file instead of .cpp file to define casting library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 22:04:19 -08:00
Leonardo de Moura
8c8cefcb0c feat(frontends/lean/parser): compact definitions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 21:24:50 -08:00
Leonardo de Moura
5043cc75f6 fix(frontends/lean/parser): allow parenthesis in level expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 13:31:55 -08:00
Leonardo de Moura
2c30b87f30 test(tests/lean): ExistsElim test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 12:57:25 -08:00
Leonardo de Moura
baf99779dc feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 17:57:51 -08:00
Leonardo de Moura
65f7217935 fix(tests/lean/norm_tac): display implicit parameters to make sure output can be parsed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 17:11:36 -08:00
Leonardo de Moura
3e32d9bef2 feat(library/tactic): add support for Pi's at to_proof_state
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 16:40:55 -08:00
Leonardo de Moura
104bd990e1 feat(library/tactic): add normalize_tac, eval_tac and trivial_tac
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 14:10:42 -08:00
Leonardo de Moura
4229e498d2 refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 11:51:38 -08:00
Leonardo de Moura
9128a437b8 refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 18:23:37 -08:00
Leonardo de Moura
df58eb132e feat(frontends/lean): simplify explicit version names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 17:05:25 -08:00
Leonardo de Moura
36b2ec9abb fix(library/cast): bugs in Cast semantic attachment
TODO: revise cast semantic attachment.
It should be axioms instead of semantic attachments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 16:16:54 -08:00
Leonardo de Moura
aebff0b4d3 fix(library/type_inferer): bug in get_range method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 14:55:07 -08:00
Leonardo de Moura
55d46b2f88 test(tests/lean): add new normalizer/elaborator test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 06:43:25 -08:00
Leonardo de Moura
9444c1f47f test(tests/lean): add example that cannot be elaborated
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 04:19:53 -08:00
Leonardo de Moura
fddcdb8f40 fix(library/elaborator): bug in process_lower
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 04:13:14 -08:00
Leonardo de Moura
66f106da8c test(tests/lean): new error msg test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 03:20:04 -08:00
Leonardo de Moura
ce84fe5d33 feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 22:00:50 -08:00
Leonardo de Moura
bb81311e0a feat(frontends/lean/parser): include proof state in exception for tactic failure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 17:15:12 -08:00
Leonardo de Moura
7772c16033 refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking  a valid term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 12:47:47 -08:00
Leonardo de Moura
812c1a2960 feat(library/elaborator): only expand definitions that are not marked as hidden
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression

 (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)

After, this commit it produces

 (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)

The expressions above are definitionally equal, but the second is easier to work with.

Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 02:16:49 -08:00
Leonardo de Moura
c77464703f feat(frontends/lean): macro definition using Lua
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 19:08:10 -08:00
Leonardo de Moura
b08c606696 fix(library/io_state): bug in the io_state Lua bindings
This commit also includes a new test that exposes the problem.
The options in the io_state object were being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 16:39:42 -08:00
Leonardo de Moura
2648f41eaa test(tests/lean): add new test script that checks if Lean can parse the output produced by its pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 16:16:56 -08:00
Leonardo de Moura
d9e692f506 feat(frontends/lean): improve coercion manangement
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:45:46 -08:00
Leonardo de Moura
f43db96e1f fix(frontends/lean/pp): pretty printer for Type
Add parenthesis around Type when it has a universe.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:24:45 -08:00
Leonardo de Moura
ae01d3818d fix(frontends/lean/parser): parse_type method
The parser had a nasty ambiguity. For example,
    f Type 1
had two possible interpretations
    (f (Type) (1))
or
    (f (Type 1))

To fix this issue, whenever we want to specify a particular universe, we have to precede 'Type' with a parenthesis.
Examples:
    (Type 1)
    (Type U)
    (Type M + 1)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 15:24:34 -08:00
Leonardo de Moura
46627289b8 fix(kernel/expr): avoid '_' as a binder name, we use '_' as a placeholder in the Lean frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:47:53 -08:00
Leonardo de Moura
d3d24696f4 feat(frontends/lean): hide builtin object in the 'Show Environment' command
The user can still display builtin objects by using

    Show Environment all

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 14:00:58 -08:00
Leonardo de Moura
ad3f771b1d feat(frontends/lean): hide 'explicit' version of objects with implicit arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 13:12:39 -08:00
Leonardo de Moura
bff5a6bfb2 fix(frontends/lean/pp): make sure pp and parser are using the same precedences
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 12:46:14 -08:00
Leonardo de Moura
dd72269b13 feat(frontends/lean): rename command Set to SetOption
It is not nice to have Set as a reserved keyword. See example examples/lean/set.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 21:18:48 -08:00
Leonardo de Moura
42cb5d1d3c fix(tests/lean): typo
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 20:11:49 -08:00
Leonardo de Moura
79fa6e4940 feat(frontends/lean): Scopes in the default Lean frontend
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 17:40:21 -08:00
Leonardo de Moura
2aaa9a5273 feat(frontends/lean/parser): change function application precedence
Now, we can write

  Pi (x y : A), R x y -> R y x

instead of

  Pi (x y : A), (R x y) -> (R y x)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-18 12:44:15 -08:00
Leonardo de Moura
10f28c7bec feat(kernel/replace_fn): non-recursive replace_fn
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 16:35:39 -08:00
Leonardo de Moura
c53233ea26 fix(kernel/normalizer): avoid svalue hack, use 'semantic attachments' for implementing closures, include context in the closure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-17 14:33:42 -08:00
Leonardo de Moura
09b51a0fb7 fix(library/elaborator): missing condition
The elaborator was missing solutions because of the missing condition at is_simple_ho_match.

This commit also adds a new test that exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 17:13:36 -08:00
Leonardo de Moura
5b29fd8d93 test(tests/lean): add ExistsElim test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 15:43:09 -08:00
Leonardo de Moura
8f5c2b7d9f feat(library/basic_thms): add Refute theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 12:03:31 -08:00
Leonardo de Moura
8f9405c8b3 fix(library/elaborator): tag meta_app constraints of the form 'ctx |- m?[inst:i v] t1 =:= t2' as expensive
This commits also adds a new unit test that demonstrates non-termination due to this kind of constraint.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-16 09:39:02 -08:00
Leonardo de Moura
2972fb9d8c test(tests/lean): new elaborator tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 22:00:26 -08:00
Leonardo de Moura
61bd27ff06 fix(library/elaborator): bug in simple_ho_match
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 21:48:55 -08:00
Leonardo de Moura
19ad39159e feat(library/basic_thms): add ForallIntro theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 17:35:31 -08:00
Leonardo de Moura
82dfb553d5 feat(library/basic_thms): add ExistsIntro theorem
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-15 16:26:23 -08:00
Leonardo de Moura
993bea8206 refactor(library/elaborator): improve elaborator state data-structure
The "quota" hack used before this commit was inefficient, and too hackish.
This commit uses two lists of constraints: active and delayed.
The delayed constraints are only processed when there are no active constraints.
We use a simple index to quickly find which delayed constraints have assigned metavariables.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

checkpoint

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 23:27:08 -08:00
Leonardo de Moura
3d30664611 feat(kernel/type_checker): provide the metavar_env to instantiate, it will minimize the number of local_entries needed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 15:13:56 -08:00
Leonardo de Moura
4357c9196e feat(kernel/metavar): make sure that a metavariable 'm' can only be assigned to a term that contains free variables available in the context associated with 'm'
This commit also simplifies the method check_pi in the type_checker and type_inferer.
It also fixes process_meta_app in the elaborator.
The problem was in the method process_meta_app and process_meta_inst.
They were processing convertability constrains as equality constraints.
For example, process_meta_app would handle

    ctx |- Type << ?f b

as

    ctx |- Type =:= ?f b

This is not correct because a ?f that returns (Type U) for b satisfies the first but not the second.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-14 12:25:00 -08:00
Leonardo de Moura
bbaa83e16a feat(frontends/lean): implement relaxed operator compatibility in the parser
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 15:42:43 -08:00
Leonardo de Moura
6b1b6c7bd1 feat(tests/lean): include standard error in the expected output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 12:52:57 -08:00
Leonardo de Moura
90f88acf42 feat(frontends/lean): relax compatible_denotation predicate
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 12:42:29 -08:00
Leonardo de Moura
abe2cf2fb5 feat(frontends/lean): simplify how implicit parameters are marked
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 12:11:04 -08:00
Leonardo de Moura
78ec4b152b feat(frontends/lean): relax restricitions on parsing applications of functions containing implicit arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-10 09:48:24 -08:00
Leonardo de Moura
0cd8e3e76b feat(split-stack): add support for split-stacks (no more stackoverflows)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-09 22:30:54 -08:00
Leonardo de Moura
0eaa98221b fix(shell/lean): Lua repl missing, incorrect exit code in interactive mode, missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-09 12:25:19 -08:00
Leonardo de Moura
3ea09daf44 fix(frontends/lean/frontend): is_coercion for environment objects that have parents
Bug was exposed by tests/lua/coercion_bug1.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 17:47:00 -08:00
Leonardo de Moura
2a80807fef refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 17:33:18 -08:00
Leonardo de Moura
68c2e5cc7d fix(frontends/lean/parser): reachable code
The new test nbug1.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 15:22:21 -08:00
Leonardo de Moura
04b67f8b14 refactor(kernel/object): remove 'null' object, and operator bool for kernel objects
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-08 14:37:38 -08:00
Leonardo de Moura
3e1fd06903 refactor(kernel/expr): remove 'null' expression, and operator bool for expression
After this commit, a value of type 'expr' cannot be a reference to nullptr.
This commit also fixes several bugs due to the use of 'null' expressions.

TODO: do the same for kernel objects, sexprs, etc.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 23:21:10 -08:00
Leonardo de Moura
1ff6013594 fix(frontends/lean/frontend_elaborator): must elaborate type attached to placeholder, it may also contain holes
The test tactic14.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 15:37:59 -08:00
Leonardo de Moura
e2999d3ff6 feat(*): add component name to check_stack and check_system
I also reduced the stack size to 8 Mb in the tests at tests/lean and tests/lean/slow. The idea is to simulate stackoverflow conditions.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 15:11:55 -08:00
Leonardo de Moura
33b72f1dd0 feat(frontends/lean/parser): apply type inference elaborator to fill remaining metavariables/holes (these are holes produced by tactics such as apply_tac)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-07 13:09:39 -08:00
Leonardo de Moura
a75d05fdb4 fix(tests/lean/interactive): test driver (to avoid discrepancy between Win and Linux version)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 17:03:12 -08:00
Leonardo de Moura
daadff548e fix(tests/lean): update expected result to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 16:31:13 -08:00
Leonardo de Moura
015bff8283 fix(library/tactic/goal): to_goal way of handling context_entries of the form (name, domain, body) where domain is null, and body is a proof term
This commit fixes a problem exposed by t13.lean.
It has a theorem of the form:

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

When to_goal creates a goal for the metavariable associated with (show B /\ A by auto) it receives a context and proposition of the form

 [ A : Bool, B : Bool, assumption : A /\ B, lemma1 := Conjunct1 assumption, lemma2 := Conjunct2 assumption ] |- B /\ A

The context_entries "lemma1 := Conjunct1 assumption" and "lemma2 := Conjunct2 assumption" do not have a domain (aka type).
Before this commit, to_goal would simply replace and references to "lemma1" and "lemma2" in "B /\ A" with their definitions.
Note that, "B /\ A" does not contain references to "lemma1" and "lemma2". Then, the following goal is created
     A : Bool, B : Bool, assumption : A /\ B |- B /\ A
That is, the lemmas are not available when solving B /\ A.
Thus, the tactic auto produced the following (weird) proof for T1, where the lemmas are computed but not used.

    Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
            let lemma1 := Conjunct1 assumption,
                lemma2 := Conjunct2 assumption
            in Conj (Conjunct2 assumption) (Conjunct1 assumption)

This commit fixed that. It computes the types of "Conjunct1 assumption" and "Conjunct2 assumption", and creates the goal
     A : Bool, B : Bool, assumption : A /\ B, lemma1 : A, lemma2 : B |- B /\ A

After this commit, the proof for theorem T1 is

Theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A :=
    let lemma1 := Conjunct1 assumption,
        lemma2 := Conjunct2 assumption
    in Conj lemma2 lemma1

as expected.

Finally, this example suggests that the encoding

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 : A := (by auto),
              lemma2 : B := (by auto)
          in (show B /\ A by auto)

is more efficient than

Theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
     fun assumption : A /\ B,
          let lemma1 := (show A by auto),
              lemma2 := (show B by auto)
          in (show B /\ A by auto)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 16:14:25 -08:00
Leonardo de Moura
0390f3c39b feat(library/tactic/boolean_tactics): avoid unnecessary Let expression in proof terms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 15:01:54 -08:00
Leonardo de Moura
1df9d18891 feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 14:49:39 -08:00
Leonardo de Moura
2ddcc32c1d fix(frontends/lean/notation): change the precedence of '->'
It should match the precedence of the implication '=>'.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 13:23:24 -08:00
Leonardo de Moura
fa03ae2a26 fix(library/elaborator): strength elaborator procedure for handling equality and convertability constraints
This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 13:04:34 -08:00
Leonardo de Moura
d46cf5fdd5 fix(frontends/lean/parser): display failed state in noninteractive mode, stop processing tactic commands when a Lean command is found
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-06 05:13:29 -08:00
Leonardo de Moura
13f9454fe1 feat(library/tactic/proof_state): add option tactic::proof_state::goal_names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 21:18:22 -08:00
Leonardo de Moura
e6fb6f7d1e feat(frontends/lean/parser): add assumption command, and allow Lean expressions (proof terms) to be used with apply tactic command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 20:08:51 -08:00
Leonardo de Moura
0c059a9917 feat(library/tactic): use _tac suffix instead of _tactic like Isabelle
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 20:06:32 -08:00
Leonardo de Moura
1b176204b4 feat(frontends/lean/parser): allow the user to use a theorem/axiom name as an argument for the apply tactic command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 19:03:12 -08:00
Leonardo de Moura
e1d44eec6b fix(frontends/lean/parser): bug in parse_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 17:40:55 -08:00
Leonardo de Moura
a564795fe6 fix(frontends/lean/parser): remove unnecessary '#' after error
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 17:27:08 -08:00
Leonardo de Moura
74a8b5f2f4 test(tests/lean/interactive): add back command test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 17:19:53 -08:00
Leonardo de Moura
e069ce640b feat(frontends/lean/parser): add tactic abort command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 17:15:19 -08:00
Leonardo de Moura
34654ad06b feat(tests/lean/interactive): add interactive mode test script
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 16:56:20 -08:00
Leonardo de Moura
e3848d43a2 feat(frontends/lean): improve tactic command parsing in interactive mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 16:28:08 -08:00
Leonardo de Moura
fa98c1358f feat(library/tactic): add disj_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 04:49:06 -08:00
Leonardo de Moura
029ef57abd feat(library/tactic): add apply_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-05 03:22:12 -08:00
Leonardo de Moura
e60e20a11d feat(frontends/lean): add Exit command
Remark: on Windows, Ctrl-D does not seem to work.
So, this commit also changes the Lean startup message.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-04 10:40:22 -08:00
Leonardo de Moura
8e53643b61 feat(library/fo_unify): first order unification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-03 12:21:21 -08:00
Leonardo de Moura
dd62af1641 feat(frontends/parser): simplified theorem definition using tactical proof
When using tactics for proving theorems, a common pattern is

     Theorem T : <proposition> := _.
          apply <tactic>.
          ...
          done.

This commit allows the user to write the simplified form:

     Theorem T : <proposition>.
          apply <tactic>.
          ...
          done.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 08:20:18 -08:00
Leonardo de Moura
25978118df feat(library/tactic): add beta-reduction tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-02 08:10:51 -08:00
Leonardo de Moura
1ec8f9d536 feat(kernel): add abstraction (aka function extensionality) axiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 13:57:14 -08:00
Leonardo de Moura
09f98ecddc feat(library/tactic): add unfold_tactic() that unfolds every non-hidden definition
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 10:41:05 -08:00
Leonardo de Moura
70e06f8e86 feat(library/hidden_defs): hidden definitions are just hints for tactics and solvers
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 10:27:27 -08:00
Leonardo de Moura
ca53a5a1cc feat(library/tactic): add unfold tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 08:51:56 -08:00
Leonardo de Moura
f91c4901e8 feat(library/tactic): add absurd_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 07:55:00 -08:00
Leonardo de Moura
bf2adb20e7 feat(library/tactic): add disj_hyp_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-01 07:55:00 -08:00
Leonardo de Moura
1a221d8bbe feat(library/tactic): add focus tactical
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-30 11:28:38 -08:00
Leonardo de Moura
98897b467d feat(frontends/lean/parser): add support for Lua expression code blocks
In expression code blocks, we do not have to write a "return".
After this commit, the argument of an apply command is a Lua expression instead of a Lua block of code. That is, we can now write

apply (** REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)

instead of

apply (** return REPEAT(ORELSE(imp_tactic, conj_tactic, conj_hyp_tactic, assumption_tactic)) **)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 10:21:24 -08:00
Leonardo de Moura
f9874cd675 feat(library/tactic): add to_tactic_ext, it allows functions that return tactics to be used where a tactic is expected
For example, after this commit, we can write

simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic

instead of

simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 09:40:21 -08:00
Leonardo de Moura
20a36e98ec feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition.
Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P.

For example, consider the constraint
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b))

Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet.
So, the elaborator would continue to process the constraint, and convert it into:

[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

Now, ?M::1 is assigned to the term
     if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

This is bad, since the original structure was lost.

This commit also contains an example that only works after the commit is applied.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 09:15:01 -08:00
Leonardo de Moura
b3f87e2e4f feat(library/tactic): make THEN, ORELSE, APPEND, PAR and INTERLEAVE nary combinators
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 22:11:07 -08:00
Leonardo de Moura
7ed78815e0 fix(tests/lua): incorrect assertion
The assertion got violated after a bug was fixed in the to_goal procedure.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 21:53:57 -08:00
Leonardo de Moura
5dfb3b8b56 feat(frontends/lean/parse): allow script-code blocks to be used in the apply command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 21:48:30 -08:00
Leonardo de Moura
c6b05bcfcb feat(library/tactic): modify assumption_tactic, it should fail if not applicable, and TRY tactical
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 18:23:38 -08:00
Leonardo de Moura
e3f3ec5553 feat(library/tactic): expose conj_tactic, imp_tactic, conj_hyp_tactic in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 18:17:15 -08:00
Leonardo de Moura
662fb71d59 chore(tests/lua/threads): fix type in file name
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 13:12:54 -08:00
Leonardo de Moura
ce674d2d43 feat(library/tactic): execute Lua tactics using coroutines
This is very important when several Lua tactics are implemented in the
same Lua State object.  In this case, even if we use the par
combinator, a Lua tactic will block the other Lua tactics running in
the same Lua State object.

With this commit, a Lua tactic can use yield to allow other tactics
in the same State object to execute.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 13:09:33 -08:00
Leonardo de Moura
09bc7ddf91 feat(library/tactic): add support for migratic tactic framework object between Lua states
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-28 08:03:05 -08:00
Leonardo de Moura
3dc7a856f0 refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 18:11:46 -08:00
Leonardo de Moura
b4a8418d38 feat(library/tactic): expose tactics in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 17:47:29 -08:00
Leonardo de Moura
0934d7b2f4 fix(frontends/lua): make sure Lua 'sleep' function support interruption
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 13:25:06 -08:00
Leonardo de Moura
d87ad9eb7e refactor(util/lua): propagate C++ Lean exceptions in Lua
The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++

The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.

Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-27 12:25:29 -08:00
Leonardo de Moura
99a811a586 feat(bindings/lua): expose io_state object in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 12:54:47 -08:00
Leonardo de Moura
861be072d8 feat(bindings/lua): add proof_state to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 11:34:58 -08:00
Leonardo de Moura
fd3b9e39f6 feat(bindings/lua): add cex_builder to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 09:17:57 -08:00
Leonardo de Moura
4d9075bdfd feat(bindings/lua): add proof_map, assignment and proof_builder to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-26 08:37:37 -08:00
Leonardo de Moura
3ebc099ec5 feat(bindings/lua/options): improve options Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-25 21:05:05 -08:00
Leonardo de Moura
feeb6d9105 feat(bindings/lua): add goal object to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-25 20:51:47 -08:00
Leonardo de Moura
7b8bd97699 feat(lua/expr): add method for extracting semantic attachment data
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 19:06:47 -08:00
Leonardo de Moura
a98fdd9be6 refactor(shell): combine lean and leanlua executables in a single executable
The main motivation is to allow users to configure/extend Lean using .lua files before loading the actual .lean files.
Example:
        ./lean extension1.lua extension2.lua file.lean

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-19 16:48:21 -08:00
Leonardo de Moura
87775cbc07 chore(build): include incorrect output in the logs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 15:39:55 -08:00
Soonho Kong
20756c382c test(*): split leantests, leanslowtests, leanluatests, leanluadocs into singletons 2013-11-18 18:27:11 -05:00
Leonardo de Moura
b2d1acd0b7 test(lua/environment): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 09:27:46 -08:00
Leonardo de Moura
1315378ebb test(*): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-18 09:13:34 -08:00
Leonardo de Moura
7976937e4c test(lua/metavar_env): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 19:18:47 -08:00
Leonardo de Moura
69be5f6c94 feat(kernel/environment): track which modules were already imported
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 18:15:44 -08:00
Leonardo de Moura
5f651d46e6 tests(lua/frontend_lean): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 13:48:29 -08:00
Leonardo de Moura
df94e44806 test(lua/expr): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 11:46:24 -08:00
Leonardo de Moura
e693c2de01 test(lua/name): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 11:25:21 -08:00
Leonardo de Moura
8a13df3ce1 test(lua/type_inferer): add missing tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 11:17:32 -08:00
Leonardo de Moura
f586e58ac3 test(lua/justification): add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 11:13:10 -08:00
Leonardo de Moura
d0bac61e74 fix(lua/numerics): bug in bindings, add more tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-17 11:02:44 -08:00
Leonardo de Moura
926ed0a02d feat(lua): add type_inferer object to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-16 19:18:15 -08:00
Leonardo de Moura
590b14570f feat(lua): improve error handling in Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-16 18:21:42 -08:00
Leonardo de Moura
390f7eaec8 test(kernel/typechecker): type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-16 15:01:39 -08:00
Leonardo de Moura
9398ea5a59 feat(util/shared_mutex): add support for recursive lock at shared_mutex
We need support for recursive locks. The main user of this class is
the environment object. This commit adds a test that demonstrates that
the shared_lock of the environment object may be recursively requested.
Before this fix, the Lean was deadlocking in this example.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-15 22:01:11 -08:00
Leonardo de Moura
209a2d10f7 fix(lua): replace std::mutex with std::recursive_mutex, add test that demonstrates the problem that is being fixed
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-15 21:26:16 -08:00
Leonardo de Moura
8525e8534b feat(lua): expose parse_expr and parse_commands from frontends/lean in the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-15 16:11:26 -08:00
Leonardo de Moura
a74412963a chore(build): only execute lua multi-threading tests when on cygwin or linux, and using g++
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-15 09:27:58 -08:00
Leonardo de Moura
5e170ce5fe chore(tests/lua): move examples that use threads to tests/lua/threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-15 09:11:58 -08:00
Leonardo de Moura
b5dcb93550 feat(lua): communication channels for threads
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 21:10:46 -08:00
Leonardo de Moura
3a924a5fb1 perf(lua/name): improve to_name_ext performance
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 18:06:09 -08:00
Leonardo de Moura
45858d54ae test(frontends/lean): add missing expected output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 15:51:47 -08:00
Leonardo de Moura
6b30ebab5e test(lua): use simplified Const creation
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 15:17:00 -08:00
Leonardo de Moura
09bed4786c feat(lua): add semantic attachments for builtin arithmetical values to Lua API, improve mk_constant
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 15:15:04 -08:00
Leonardo de Moura
abe93dfec0 fix(lua/splay_tree): for_each method was crashing if the map was updated during for_each
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 13:48:23 -08:00
Leonardo de Moura
64cce595a5 feat(lua): add splay_maps to the Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 13:35:36 -08:00
Leonardo de Moura
9e445d1917 feat(lua): interrupt and sleep Lua APIs
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-14 10:04:32 -08:00