lean2

Author	SHA1	Message	Date
Leonardo de Moura	9b6b162a7c	fix(library/scope): bug when abstracting inductive declaration in the end of a section Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-02 13:46:16 -07:00
Leonardo de Moura	2a101657c8	test(lua): add section+inductive_family test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-02 13:07:13 -07:00
Leonardo de Moura	6ee272477a	fix(library/private): bug when preserving private names at end_section Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-02 11:32:14 -07:00
Leonardo de Moura	936ca80b9b	fix(library/scope): bug in add_definition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-02 11:04:34 -07:00
Leonardo de Moura	e56307f006	fix(library/scope): bug in end_scope procedure Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-02 10:43:28 -07:00
Leonardo de Moura	6e113206b6	feat(library/scope): add support for inductive datatypes in sections Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-02 10:28:07 -07:00
Leonardo de Moura	d36ef5dcbe	feat(library/private): preserve 'hidden/private name => user name' map when section is closed Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-01 18:09:11 -07:00
Leonardo de Moura	585f3adde1	feat(library/scope): add sections Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-06-01 17:55:11 -07:00
Leonardo de Moura	286d7f0e64	feat(library): add namespace management Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-31 15:41:01 -07:00
Leonardo de Moura	3145cee51f	refactor(library/aliases): move replace_prefix to util/name Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-31 15:11:22 -07:00
Leonardo de Moura	37b5570e99	test(lua): add .olean corrupted file tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-31 12:51:33 -07:00
Leonardo de Moura	7bd10c2d2d	feat(library/module): export global universe level declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-31 12:12:41 -07:00
Leonardo de Moura	1b5366cfb7	feat(library): add module for implementing aliases and 'using' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-30 21:42:40 -07:00
Leonardo de Moura	6902d8cb05	feat(library): add simple placeholder module Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-30 20:28:28 -07:00
Leonardo de Moura	72f9e26dab	refactor(library/private): add hidden_to_user_name and user_to_hidden_name functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-30 17:52:01 -07:00
Leonardo de Moura	cba52b76c7	test(lua): add integer datatype test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-30 16:30:33 -07:00
Leonardo de Moura	6587d0f8f3	test(lua): add is_sorted inductive predicate example Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-30 16:30:32 -07:00
Leonardo de Moura	128d668f03	feat(library): add support for creating 'private/hidden' names Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-29 18:37:09 -07:00
Leonardo de Moura	bfa9b90af0	feat(library/kernel_bindings): used 'named' parameters in import_modules API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-29 11:03:44 -07:00
Leonardo de Moura	ade5d99023	feat(library/modules): add option for discarding the proof of imported theorems (after checking them) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-29 10:56:28 -07:00
Leonardo de Moura	0f894f4618	chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-27 17:47:53 -07:00
Leonardo de Moura	162fa25250	test(lua): move slow tests to tests/lua/slow Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-27 10:24:18 -07:00
Leonardo de Moura	3608826e4c	test(lua): add inductive decl serialization test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-26 15:54:41 -07:00
Leonardo de Moura	bb9830f10c	test(shell): add command line tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-26 04:53:04 -07:00
Leonardo de Moura	dbe55bf84a	test(lua): add Lua State tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-26 04:43:44 -07:00
Leonardo de Moura	701b60d2d9	test(lua): add Lua 'yield' test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-26 04:39:53 -07:00
Leonardo de Moura	38a826013c	test(lua): add import Lua file test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-26 04:34:34 -07:00
Leonardo de Moura	2d31c6c0b2	feat(library/coercion): improve get_user_coercions API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 11:35:47 -07:00
Leonardo de Moura	bb6db41414	test(lua): add 'multiple inheritance' test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 11:15:25 -07:00
Leonardo de Moura	e058839d24	fix(library/coercion): allow cycles in the coercion graph Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 11:08:49 -07:00
Leonardo de Moura	71b555ab15	test(lua): coercion module error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 10:01:04 -07:00
Leonardo de Moura	ef14c3d67e	fix(library/coercion): coercion replacement Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 09:49:26 -07:00
Leonardo de Moura	fc1819aadd	test(lua): coercion serialization Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 08:38:50 -07:00
Leonardo de Moura	0d02f933cb	test(lua): add coercion sort-class tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 08:29:47 -07:00
Leonardo de Moura	e28446710e	test(lua): add coercion to function-class tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 08:22:28 -07:00
Leonardo de Moura	a9a5f8628f	test(lua): add coercion module tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-25 07:45:49 -07:00
Leonardo de Moura	69e5156034	test(lua): add import 'diamond' tst Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-23 16:49:43 -07:00
Leonardo de Moura	879572ee7e	fix(kernel/module): non-termination Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-23 15:12:47 -07:00
Leonardo de Moura	e4f09335ce	test(lua): new module system test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-23 14:54:20 -07:00
Leonardo de Moura	46c292be71	test(lua): add simple module export/import test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-23 11:26:28 -07:00
Leonardo de Moura	69f6930bd7	test(lua): add Acc datatype declaration test Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-05-23 11:26:02 -07:00
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

... 6 7 8 9 10 ...

961 commits