lean2

Author	SHA1	Message	Date
Leonardo de Moura	633ed6bb69	fix(frontends/lean/parser): bug in add_rewrite Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 09:46:56 -08:00
Leonardo de Moura	b24c085cb0	feat(frontends/lean): avoid warning message Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-09 09:26:51 -08:00
Leonardo de Moura	d6167eae32	feat(builtin/num): define add and mul Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 22:28:15 -08:00
Leonardo de Moura	cc4148a98d	feat(builtin/num): primitive recursion theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 22:05:57 -08:00
Leonardo de Moura	f28c56b188	feat(builtin/num): add auxiliary definitions and theorems for proving the primitive recursion theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 19:36:17 -08:00
Leonardo de Moura	fa4b60963b	feat(builtin/num): define lt predicate, and prove basic theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 10:57:17 -08:00
Leonardo de Moura	1f3e0f7a38	chore(builtin/num): update object file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 09:16:52 -08:00
Leonardo de Moura	aeaa803f9a	feat(builtin): add num type (the base type that will be used to build nat, int, real) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 09:12:53 -08:00
Leonardo de Moura	1c43020fc9	fix(library/tactic/goal): bug creating main proof builder Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-08 09:11:07 -08:00
Leonardo de Moura	24528ff685	fix(library/elaborator): fix glitches in the elaborator that were forcing us to provide parameters explicitly Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 18:02:08 -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	6d7ec9d7b6	refactor(kernel): add heterogeneous equality back to expr The main motivation is that we will be able to move equalities between universes. For example, suppose we have A : (Type i) B : (Type i) H : @eq (Type j) A B where j > i We didn't find any trick for deducing (@eq (Type i) A B) from H. Before this commit, heterogeneous equality as a constant with type heq : {A B : (Type U)} : A -> B -> Bool So, from H, we would only be able to deduce (@heq (Type j) (Type j) A B) Not being able to move the equality back to a smaller universe is problematic in several cases. I list some instances in the end of the commit message. With this commit, Heterogeneous equality is a special kind of expression. It is not a constant anymore. From H, we can deduce H1 : A == B That is, we are essentially "erasing" the universes when we move to heterogeneous equality. Now, since A and B have (Type i), we can deduce (@eq (Type i) A B) from H1. The proof term is (to_eq (Type i) A B (to_heq (Type j) A B H)) : (@eq (Type i) A B) So, it remains to explain why we need this feature. For example, suppose we want to state the Pi extensionality axiom. axiom hpiext {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)} : A = A' → (∀ x x', x == x' → B x == B' x') → (∀ x, B x) == (∀ x, B' x) This axiom produces an "inflated" equality at (Type U) when we treat heterogeneous equality as a constant. The conclusion (∀ x, B x) == (∀ x, B' x) is syntax sugar for (@heq (Type U) (Type U) (∀ x : A, B x) (∀ x : A', B' x)) Even if A, A', B, B' live in a much smaller universe. As I described above, it doesn't seem to be a way to move this equality back to a smaller universe. So, if we wanted to keep the heterogeneous equality as a constant, it seems we would have to support axiom schemas. That is, hpiext would be parametrized by the universes where A, A', B and B'. Another possibility would be to have universe polymorphism like Agda. None of the solutions seem attractive. So, we decided to have heterogeneous equality as a special kind of expression. And use the trick above to move equalities back to the right universe. BTW, the parser is not creating the new heterogeneous equalities yet. Moreover, kernel.lean still contains a constant name heq2 that is the heterogeneous equality as a constant. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-07 10:28:10 -08:00
Leonardo de Moura	354d5607af	chore(builtin/sum): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 21:25:57 -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	ff955f9830	chore(frontends/lean/parser): update comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 20:56:31 -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	4b4b5e3345	fix(frontends/lean): import explicit versions when using the command 'using' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 17:33:58 -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	e85b1f1ac0	feat(library/elaborator): expose elaborator configuration options 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	581ae0c83b	chore(build): fix build dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 09:30:33 -08:00
Leonardo de Moura	db3bcdba55	refactor(builtin): move pair definition and theorems to pair.lean Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 09:20:52 -08:00
Leonardo de Moura	daf7075ce4	refactor(builtin/sum): use new 'have' expression to formalize optional-types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 09:15:12 -08:00
Leonardo de Moura	5d698a60a7	refactor(builtin/sum): use new 'have' expression to formalize sum-types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 08:59:05 -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	90f5a4f813	feat(builtin/sum): cleanup, and avoid unicode character that is not available in some platforms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-06 00:20:49 -08:00
Leonardo de Moura	c01f82aeb7	feat(builtin): add sum types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-05 23:04:44 -08:00
Leonardo de Moura	87da23649b	feat(builtin/optional): prove dichotomy and induction theorems for optional types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-05 19:49:50 -08:00
Leonardo de Moura	30570c843f	feat(builtin): add optional type Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-05 17:33: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	493007b7bc	fix(frontends/lean/pp): bug in tuple/pair pretty printing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 13:58:01 -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	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	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	9a677331da	feat(builtin): simulate subtypes using sigma types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-04 01:46:50 -08:00
Leonardo de Moura	61d0c792ff	fix(frontends/lean/parser): bug in tuple/proj1/proj2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 22:46: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	5e5ab1429d	feat(frontends/lean): parse and pretty print sigma types This commit also fixes some bugs in the implementation of Sigma types. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 18:16:00 -08:00
Leonardo de Moura	8eec289ce1	feat(kernel): add dependent pairs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-02-03 16:52:49 -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	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	0ed35e2133	fix(build): kernel.lean depends on tactic.lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 23:15:44 -08:00
Leonardo de Moura	2aaded261e	fix(kernel/environment): imported predicate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 23:02:19 -08:00
Leonardo de Moura	bc2d504ccc	feat(builtin/kernel): add rewrite rules for if-then-else Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 22:38:35 -08:00
Leonardo de Moura	b444756d20	fix(library/simplifier): missing condition in implication simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 22:14:01 -08:00
Leonardo de Moura	4d533c6a25	feat(builtin/kernel): add nonempty_range theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 22:13:34 -08:00
Leonardo de Moura	ddaf948c72	feat(builtin/kernel): add nonempty_fun theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-30 19:38:51 -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	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	f0a2d3627e	refactor(frontends/lean): use ascii prefix for auxiliary let-declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 11:58:09 -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	f101554e93	fix(util/script_exception): make sure a script_nested_exception may have a nested script_nested_exception, use LEAN_THREAD_LOCAL macro instead of thread_local Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-29 08:07:52 -08:00
Leonardo de Moura	24452289dd	feat(library/simplifier): make sure the simplifier can handle meta-variables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 20:30:47 -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	b6985bd713	feat(builtin/kernel): add another rewrite rule Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 15:56:26 -08:00
Leonardo de Moura	e2540b68db	fix(src/builtin/tactic): add default rule set if none is provided Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-28 15:56:01 -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	dbdbd211e3	fix(library/simplifier): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 23:29:53 -08:00
Leonardo de Moura	55fde28954	feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 17:47:03 -08:00
Leonardo de Moura	160dc71cb5	refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 17:38:06 -08:00
Leonardo de Moura	05b4d8411b	refactor(kernel/normalizer): normalizer only needs read access to metavariable environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 17:03:36 -08:00
Leonardo de Moura	3b152d1a9e	refactor(kernel): use ro_metavar_env instead of metavar_env in places where we only need to read the metavariable environment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 16:44:43 -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	c088825ef0	feat(library/simplifier): add simplifier_monitor interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-27 11:46:28 -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	579b751e01	fix(library/simplifier): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 23:16:24 -08:00
Leonardo de Moura	ceff335bb8	doc(doc/lean/tutorial): update tutorial Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 22:58:44 -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	5e6c1d4904	refactor(builtin/heq): remove axiom hpiext since we don't use it anymore Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 13:11:17 -08:00
Leonardo de Moura	50df761d90	refactor(library/simplifier): remove the is_typem hack, it is not needed anymore now that we don't use hpiext anymore Now, we are again using the following invariant for simplifier_fn::result The type of in the equality of the result is definitionally equal to the type of the resultant expression. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 12:21:23 -08:00
Leonardo de Moura	29e448f034	fix(library/simplifier): remove support in the simplifier for (forall x : A, B x) when it is not a proposition, the problem is that hpiext axiom produces an equality in a too big universe For example, in the hpiext axiom, the resultant equality if for (Type M+1) axiom hpiext {A A' : TypeM} {B : A -> TypeM} {B' : A' -> TypeM} : A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x) even if the actual arguments A, A’, B, B’ "live" in a much smaller universe (e.g., Type). So, it would be great if we could move the resultant equality back to the right universe. I don't see how to do it right now. The other solution would require a major rewrite of the code base. We would have to support universe level arguments like Agda, and write the axiom hpiext as: axiom hpiext {l : level} {A A' : (Type l)} {B : A -> (Type l)} {B' : A' -> (Type l)} : A = A' -> (∀ x x', x == x' -> B x = B' x') -> (∀ x, B x) = (∀ x, B' x) This is the first instance I found where it is really handy to have this feature. I think this would be a super clean solution, but it would require a big rewrite in the code base. Another problem is that the actual semantics that Agda has for this kind of construction is not clear to me. For instance, sometimes Agda reports that the type of an expression is (Set omega). An easier to implement hack is to support "axiom templates". We create instances of hipext "on-demand" for different universe levels. This is essentially what Coq does, since the universe levels are implicit in Coq. This is not as clean as the Agda approach, but it is much easier to implement. A super dirty trick is to include some instances of hpiext for commonly used universes (e.g., Type and (Type 1)). Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 12:10:34 -08:00
Leonardo de Moura	52ee9b35dd	feat(library/simplifier): add support for simplifying even when heq module is not available Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 11:29:36 -08:00
Leonardo de Moura	fafaa7e78e	fix(library/simplifier): remove hack for handling some constants that expect an argument of type TypeU, the new approach is general Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 10:10:57 -08:00
Leonardo de Moura	89bb5fbf19	chore(library/simplifier): fix style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-26 00:36:17 -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	6bc1537e25	feat(frontends/lean/parser): allow the user to write (Type) without providing a level Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 20:17:36 -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	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	df3129e80d	fix(library/hop_match): typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-25 10:08:53 -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	2bb33c55fe	feat(builtin/kernel): add more theorems useful for simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 18:52:50 -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	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	009217b499	feat(builtin/hep): replace hallext axiom with theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-24 17:09:20 -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	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	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	6cb4d165c9	feat(builtin/kernel): dependent version of axiom of choice Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 11:04:27 -08:00
Leonardo de Moura	88b6778a1f	fix(emacs): syntax highlight Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 09:44:12 -08:00
Leonardo de Moura	66553268d0	feat(builtin/kernel): add skolem_th, we need it to justify skolemization preprocessing step Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 09:41:07 -08:00
Leonardo de Moura	d9b5ebc738	refactor(builtin/kernel): cleanup Hilbert operator definition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 09:18:40 -08:00
Leonardo de Moura	bcf60db23b	fix(builtin/kernel): Hilbert operator only for non-empty types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 08:52:31 -08:00
Leonardo de Moura	94a3136904	feat(builtin/kernel): add Hilbert's operator, and derive axiom of choice using it Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-22 08:21:11 -08:00
Leonardo de Moura	425d31f513	chore(library/simplifier): fix style warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 21:45:55 -08:00
Leonardo de Moura	cca15f1390	feat(library/simplifier): congruence theorem compilation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 21:16:23 -08:00
Leonardo de Moura	029d74ec11	chore(kernel): remove comment, we decided to have Eta as a simplification rule Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:35:05 -08:00
Leonardo de Moura	95b6e61738	feat(kernel/max_sharing): check for imminent stack overflows and interruptions in the expression sharing maximizer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:33:49 -08:00
Leonardo de Moura	2089b85532	refactor(kernel/instantiate): remove code duplication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:30:38 -08:00
Leonardo de Moura	7299b2d5d6	chore(kernel): remove dead file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:21:13 -08:00
Leonardo de Moura	fbaf6e887f	refactor(builtin/kernel): put the congruence theorems in a format that is easier for the simplifier to process Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-21 14:03:51 -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	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	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	217e56ea03	feat(kernel/expr): make sure semantic attachments are smaller than other kinds of expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 14:10:44 -08:00
Leonardo de Moura	abfeacb8f0	fix(tests/library/expr_lt): adjust is_lt unit tests to reflect recent modifications Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:44:44 -08:00
Leonardo de Moura	56f5657ee7	fix(library/simplifier): ordered rewriting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:13:16 -08:00
Leonardo de Moura	5060bdbf14	fix(kernel/expr): compilation warning Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:12:49 -08:00
Leonardo de Moura	6a63ef3bc5	feat(library/expr_lt): make sure the total order on terms is monotonic Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-20 13:07:18 -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	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	8e90d17a0b	fix(library/hop_match): style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 23:28:12 -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	08053c1172	feat(library/hop_match): make the higher order pattern matcher slightly stronger It now can handle (?m t) where t is not a locally bound variable, but ?m and all free variables in t are assigned. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 20:35:50 -08:00
Leonardo de Moura	90ffb9d5ec	fix(frontends/lean/pp): bug in pp_abstraction_core Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 19:47:40 -08:00
Leonardo de Moura	6db10c577b	feat(builtin/kernel): add proof irrelevance axiom Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 12:20:09 -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	3bbadddc94	chore(library/simplifier): cleanup and add comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:54:09 -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	475df3d94e	chore(builtin/kernel): add theorem for rewriter/simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:34:18 -08:00
Leonardo de Moura	e512241c8f	fix(emacs): missing keyword Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-19 10:32:45 -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	2753a0ffc0	fix(builtin/kernel): add ascii notation for transitivity Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 20:56:35 -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	466285c577	refactor(library/simplifier): rewriter_rule_set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 17:26:01 -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	eae79877ae	feat(library/simplifier): add rewrite_rule_set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 12:50:46 -08:00
Leonardo de Moura	27ab49ae9d	feat(library/simplifier): bottom-up simplifier skeleton Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-18 12:49:41 -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	534838a36c	chore(build): update automatically generated files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 18:30:45 -08:00
Leonardo de Moura	d711ca4d1b	feat(builtin/heq): add heq C++/Lean interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 18:30:21 -08:00
Leonardo de Moura	20c8b91d07	feat(builtin/if_then_else): add more theorems for rewriting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 18:11:23 -08:00
Leonardo de Moura	2434024272	fix(library/rewriter): warning in release mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 15:46:49 -08:00
Leonardo de Moura	ba88a3b05a	chore(builtin/heq): remove unnecessary import Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 15:40:56 -08:00
Leonardo de Moura	70828af6db	refactor(builtin/heq): cleanup universes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 14:52:09 -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	0660cdbdb7	feat(builtin/cast): use heq in the cast library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 14:31:45 -08:00
Leonardo de Moura	52756c50fc	fix(builtin/heq): extensionality axioms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 12:56:36 -08:00
Leonardo de Moura	64795c6c42	feat(builtin): add heterogeneous equality theory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 12:32:49 -08:00
Leonardo de Moura	baed98d5be	chore(builtin/kernel): adjust emacs mode and fix typo Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-17 10:14:57 -08:00
Leonardo de Moura	5bee259a00	refactor(kernel): remove unnecessary universe Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 18:06:25 -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	1da4294793	refactor(builtin): more theorems, fix iff notation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 09:26:50 -08:00
Leonardo de Moura	398d83b6d5	chore(builtin/Nat): use iff Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 02:06:53 -08:00
Leonardo de Moura	4dc98bc73b	refactor(builtin/kernel): use iff instead of = for Booleans Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 02:05:09 -08:00
Leonardo de Moura	d063828ff9	feat(library/kernel_bindings): expose abst_name, abst_domain and abst_body in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-16 00:03:16 -08:00
Leonardo de Moura	8d73fb5699	fix(library/hop_match): Lua bindings gotcha See http://www.luafaq.org/gotchas.html#T6.4 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 23:51:26 -08:00
Leonardo de Moura	14c6218bdc	chore(kernel): file name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 20:06:29 -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	7fb0aa4800	chore(kernel/expr): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:24:31 -08:00
Leonardo de Moura	438fa8251b	test(kernel/expr): check if the serializer works for metavariables Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:15:56 -08:00
Leonardo de Moura	5058e403b5	test(kernel/expr): check if the serializer works for applications with many argumets Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:09:46 -08:00
Leonardo de Moura	c096eec1d6	chore(kernel/expr): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 17:09:04 -08:00
Leonardo de Moura	8c2f78a756	feat(builtin): minimize use of heterogenous equality in the kernel, add simpler version of congruence theorems for non-dependent types Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 16:34:23 -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	1176093afa	refactor(library/simplifier): simplifier should only use homogeneous equalities Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 14:58:32 -08:00
Leonardo de Moura	f177c8d1ec	fix(library/elaborator): missing condition The elaborator was failing in the following higher-order constraint ctx \|- (?M a) = (?M b) This constraint has solution, but the missing condition was making the elaborator to reduce this problem to ctx \|- a = b That does not have a solution. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 14:11:36 -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	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	83efa644d1	fix(frontends/lean/parser): uninitialized var error reported by valgrind Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-15 08:43:43 -08:00
Leonardo de Moura	28eb980484	fix(build): C++ module dependency problem, and style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 18:30:31 -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	07059b0531	feat(library): add if_then_else Lean/C++ interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 16:10:49 -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	acfb11e290	fix(kernel/instantiate): relax apply_beta pre-condition Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 14:36:51 -08:00
Leonardo de Moura	a968a43487	fix(kernel/free_vars): make sure has_free_var does not return incorrect result due to arithmetic overflows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-14 14:36:14 -08:00
Leonardo de Moura	f8eaae7218	feat(builtin/kernel): add new useful theorems for the simplifier Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-13 18:21:22 -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	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	e6c322d97f	feat(kernel/free_vars): make free_vars module functions more robust Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:44:28 -08:00
Leonardo de Moura	29fec3fecc	fix(builtin/util): bug incorrect encoding of \t and \n in regular expression, and missing local Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:40:41 -08:00
Leonardo de Moura	915644f3b3	fix(util/debug): avoid infinite loop when Ctrl-D is pressed after an assertion violation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:20:35 -08:00
Leonardo de Moura	5d9a95addd	refactor(kernel/free_vars): replace max_free_var with relaxed free_var_range Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 17:06:57 -08:00
Leonardo de Moura	582569b793	feat(frontends/lean): allow the user to set the trust_imported flag when creating environments using Lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 16:46:53 -08:00
Leonardo de Moura	4d9eb4ac6c	feat(kernel): add max_free_var function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-12 16:45:34 -08:00
Leonardo de Moura	6508e63a17	feat(builtin/macros): add assume/take macros for making proof scripts more readable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 18:36:37 -08:00
Leonardo de Moura	781720a26a	feat(builtin/kernel): add left_comm theorem Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 18:08:08 -08:00
Leonardo de Moura	a1a467a65f	refactor(builtin): move congruence theorems to kernel/if_then_else modules Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 13:48:28 -08:00
Leonardo de Moura	a0a92f11b7	feat(builtin/congr): add congruence theorems for contextual simplification Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 13:37:36 -08:00
Leonardo de Moura	53537d0684	feat(builtin/kernel): 'implication' simplification theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 13:35:20 -08:00
Leonardo de Moura	50f281b430	feat(builtin/kernel): add eqf_intro and eqf_elim theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 11:13:54 -08:00
Leonardo de Moura	4057f0d2fe	feat(emacs): minor improvements to emacs mode Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-11 11:13:20 -08:00
Leonardo de Moura	745c702ffb	fix(build): dependency problem on some platforms Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-10 19:06:15 -08:00
Leonardo de Moura	d4a7d796a5	feat(builtin): prove strong induction theorem, add < theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-10 18:46:33 -08:00
Leonardo de Moura	5fb718c03a	fix(build): broken dependencies between lean executable and .olean, _decls.cpp and _decls.h files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-10 10:58:35 -08:00
Leonardo de Moura	9e8b083673	feat(emacs): more highlighting Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 20:44:01 -08:00
Leonardo de Moura	3008cad151	feat(emacs): highlight tactics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 20:10:57 -08:00
Leonardo de Moura	2cf73fc4d2	feat(emacs): useful abbreviations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 19:57:00 -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	8c41b4e899	feat(build): run tests using -t Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 14:12:32 -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	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	dff0b9011b	chore(builtin/cast): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 12:06:22 -08:00
Leonardo de Moura	3e18cdfeec	feat(util/format): do not use colors by default Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:56:58 -08:00
Leonardo de Moura	6fe362ef07	feat(emacs): include lean-mode Emacs files in the distribution Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 11:50:07 -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	87b238efcd	chore(builtin/kernel): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-09 09:00:05 -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	25086947fa	fix(builtin/kernel): incorrect comment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 19:14:11 -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	8e9d88c2cf	refactor(builtin/kernel): prove iff::intro, and add a new name for it boolext (Boolean extensionality) Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 18:31:45 -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	9c8026b86e	refactor(builtin/macros): remove 'take', 'discharge' and 'instantiate' macros Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 16:58:01 -08:00
Leonardo de Moura	bdec4c8799	refactor(builtin/Nat): mark constants as opaque Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 16:53:08 -08:00
Leonardo de Moura	2e3b92ef36	refactor(builtin/kernel): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 16:52:43 -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	57640ecf19	fix(library/elaborator): array bounds Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 13:18:49 -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	cfe576f551	fix(library/elaborator): bug in the elaborator The elaborator was not handling correctly constraints of the form ctx \|- ?m << (Pi x : A, B) and ctx \|- (Pi x : A, B) << ?m Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 12:10:50 -08:00
Leonardo de Moura	dd6c13abb0	fix(util/buffer): warning produced by clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 11:27:11 -08:00
Leonardo de Moura	85de05e5cf	chore(kernel/unification_constraint): update max_constraint comment to reflect its new semantics Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-08 01:09:47 -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	e12d6e44cd	fix(util/name): bug in Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:52:51 -08:00
Leonardo de Moura	8ce6266e6b	feat(library/kernel_bindings): add new predicates for kernel objects in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:36:54 -08:00
Leonardo de Moura	6f4ca7bd2a	feat(frontends/lean): expose is_explicit function in the Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:36:27 -08:00
Leonardo de Moura	4fdc0406be	feat(util/name): additional methods to name Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 17:35:34 -08:00
Leonardo de Moura	248d55d454	chore(util/script_state): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 16:59:50 -08:00
Leonardo de Moura	2cd2527d9f	refactor(shell): move read-eval-loop script to repl.lua Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 16:56:22 -08:00
Leonardo de Moura	0bc2c51c9c	fix(build): put back the dependency on lean executable for .olean files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 16:13:58 -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	95515ca5df	chore(*): fix warnings produced by clang++ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:39:49 -08:00
Leonardo de Moura	a3af87f8d3	chore(frontends/lean/frontend): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:28:21 -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	fb73514913	fix(frontends/lean/parser): parser aborted if the scanner throws an exception in the first call to scan(); position information was being shown twice for scanner exceptions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:04:30 -08:00
Leonardo de Moura	f12a76a5cd	test(frontends/lean/scanner): missing tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 15:03:46 -08:00
Leonardo de Moura	c7338a8eab	chore(frontends/lean/scanner): remove dead code Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:37:28 -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	f67eab000b	fix(util/serializer): nontermination on corrupted files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:21:54 -08:00
Leonardo de Moura	d5ddb186d9	feat(library/kernel_bindings): add load method to Lua API Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 14:21:24 -08:00
Leonardo de Moura	6077dc61b7	feat(builtin): remove lean executable as a dependency for builtin .lean files Otherwise, we have to rebuild all .lean files whenever we change the executable. This commit also adds a test for each .lean file. This is useful for increasing coverage and having a log on how long does it take to process these files. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 13:53:30 -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	0bdecb6aa4	style(builtin/Nat): name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-07 00:05:51 -08:00
Leonardo de Moura	c5d13abd6f	refactor(builtin/Nat): rename destruct to discriminate Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 23:05:27 -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	4424a314e0	feat(kernel): add get_universe_distance method Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 17:13:13 -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	b5a30855f8	feat(kernel/universe_constraints): add new class for managing universe constraints Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 15:01:28 -08:00
Leonardo de Moura	68832dc6f2	fix(builtin/macros): comments Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 12:07:13 -08:00
Leonardo de Moura	929a536e2f	fix(builtin/README): update documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 12:03:11 -08:00
Leonardo de Moura	62bb2ab2f9	fix(builtin/Nat): name convention Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:14 -08:00
Leonardo de Moura	645e748302	feat(frontends/lean): add 'using' command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-06 11:41:14 -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	771b099c0c	fix(frontends/lean): must invoke lua GC before closing a scope, reason: we may still have references to the current environment inside of the Lua state object Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 16:38:29 -08:00
Leonardo de Moura	9d6bd7501c	feat(doc/lean): include lean documentation scripts in the test set Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-05 13:16:47 -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	f5cc2458a9	fix(frontends/lean/parser_calc): missing save calls Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 18:26:30 -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	66ec538c63	doc(doc/lean/calc.md): calculational proof documentation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 11:52:21 -08:00
Leonardo de Moura	5b5cebe750	refactor(builtin/Nat): use obtain-from instead of ExistsElim, and use more user-friendly argument order for Induction Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 10:33:57 -08:00
Leonardo de Moura	9f3706e365	feat(builtin/macros): add obtain-from macro for ExistsElim Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-03 10:32:49 -08:00
Leonardo de Moura	d7efdff83d	feat(builtin/Nat): add more leq theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 22:48:10 -08:00
Leonardo de Moura	cf35e7bed7	feat(frontends/lean): add support for disequalities in calculational proofs Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 22:47:45 -08:00
Leonardo de Moura	6329d1828d	feat(frontends/lean): reuse name expression Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 20:08:21 -08:00
Leonardo de Moura	92c7145d7f	feat(kernel/expr): maximize sharing before serializing Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 20:03:42 -08:00
Leonardo de Moura	2d5800ace4	feat(builtin/Nat): leq axiom, and some theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 18:24:32 -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	ecc5d1bc3a	refactor(kernel): move printer to library, cleanup io_state interface Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 13:37:50 -08:00
Leonardo de Moura	0592261847	refactor(kernel/io_state): move io_state_stream to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 13:14:21 -08:00
Leonardo de Moura	b81d3309b9	fix(kernel): remove ios hack Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 13:03:25 -08:00
Leonardo de Moura	9c5fa72f56	fix(library/elaborator): avoid unused variable warning in release build Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 12:40:41 -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	307099b1cb	refactor(builtin/Nat): cleanup all proofs using calculational proof style Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 12:13:26 -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	0cb741285c	chore(*): do not type check imported modules when running .cpp tests Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 07:11:55 -08:00
Leonardo de Moura	d7493ea86c	refactor(frontends/lean/parser): use std::function Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 06:53:34 -08:00
Leonardo de Moura	5540fc861a	refactor(frontends/lean/parser): break parser in smaller chunks Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 06:48:40 -08:00
Leonardo de Moura	7d18e9b32e	refactor(frontends/lean/parser): cleanup Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-02 04:37:21 -08:00
Leonardo de Moura	49425f1a5b	feat(builtin/Nat): multiplication axioms and theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 21:32:07 -08:00
Leonardo de Moura	d72b165db4	feat(builtin/Nat): cleanup and add PlusAssoc Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 17:19:12 -08:00
Leonardo de Moura	aa009b6b05	feat(builtin/Nat): add basic axioms and theorems Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 15:53:53 -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	43909ca66b	feat(frontends/lean/pp): pretty print SetOpaque command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 13:16:44 -08:00
Leonardo de Moura	770145a361	feat(builtin): use namespaces when defining nat, int and real. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 12:55:09 -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	74cae2a154	refactor(library/elaborator): remove hackish rule After the recent fixes, the hack in process_metavar is not needed anymore. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 10:55:39 -08:00
Leonardo de Moura	5f29146e0b	feat(library/elaborator): use is_convertible for constraints without metavariables in the elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2014-01-01 03:14:01 -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	0d815b8594	refactor(kernel/context): hide that the context is implemented using lists Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-31 19:43:50 -08:00
Leonardo de Moura	1cb7408c46	fix(kernel/normalizer): metavariable reification was incorrect, add tst11 at tests/kernel/normalizer.cpp to expose the bug Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-31 16:24:36 -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	c485b4bc4c	fix(kernel/environment): binary file reader, force the file to be read in binary mode We need this flag to be able to read the file on Windows. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 18:20:40 -08:00
Leonardo de Moura	1f6e959139	feat(deserializer): protect against corrupted binary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 18:05:38 -08:00
Leonardo de Moura	c473a484bb	feat(util/object_serializer): protect against corrupted files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 17:58:20 -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	909b10f515	fix(builtin): dependency Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 15:31:19 -08:00
Leonardo de Moura	931e196e83	fix(build): problem with reading LEAN_PATH on cygwin Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 15:12:31 -08:00
Leonardo de Moura	cc07c440e1	refactor(builtin): move pre-compiled object files to subdirectory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 13:46:39 -08:00
Leonardo de Moura	49698bd053	chore(library/all): remove unnecessary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 13:37:25 -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	a017801983	chore(builtin): cleanup dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 12:40:42 -08:00
Leonardo de Moura	a80fccea93	chore(*): cleanup builtin registration Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 12:19:00 -08:00
Leonardo de Moura	2a2f0b0d89	refactor(kernel/builtin): move helper decl macros to a separate file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:51:30 -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	72761f14e4	refactor(library/io_state): move to the kernel Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-30 11:20:23 -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	097b10e424	refactor(kernel/builtin): move builtin declarations to basic There is a lot to be done. We should do the same for Nat, Int and Real. We also should cleanup the file builtin.cpp and builtin.h. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 22:00:03 -08:00
Leonardo de Moura	37e8738a5f	refactor(kernel/expr): value deserializer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 20:47:14 -08:00
Leonardo de Moura	9b7d596e6b	chore(builtin/basic): simplify UnfoldExists2 proof Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 20:33:31 -08:00
Leonardo de Moura	a7654cfdbe	chore(builtin/basic): remove unnecessary parentheses Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 20:16:01 -08:00
Leonardo de Moura	de77851a00	refactor(util/object_serializer): add methods write_core and read_core that allows to pack information in the byte used to indicate whether an object is already in the cache or not Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 19:59:53 -08:00
Leonardo de Moura	dbd122301a	feat(kernel/object): compact object serialization kind ids Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 19:19:24 -08:00
Leonardo de Moura	d0fdc3619b	feat(kernel/expr): compress application serialization Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 19:11:57 -08:00
Leonardo de Moura	63a4a2f288	feat(builtin/basic): add UnfoldExists and neq Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 18:30:41 -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	14c3e11289	refactor(kernel/builtin): emove mk_bin_rop and mk_bin_lop to library Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 15:23:18 -08:00
Leonardo de Moura	92404c511c	refactor(kernel/builtin): Bool type does not need to be a semantic attachment Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 15:12:08 -08:00
Leonardo de Moura	8ff919ef2a	chore(build): remove dead dependency Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 14:49:22 -08:00
Leonardo de Moura	6633dff46f	fix(build): githash generation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 14:41:28 -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	b1efdac07b	feat(frontends/lean/parser): universe declarations Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 13:15:09 -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	1b300d3598	chore(kernel/builtin): remove unnecessary functions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 12:55:51 -08:00
Leonardo de Moura	f7889511f9	fix(build): cycle triggered by githash.h dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 12:47:25 -08:00
Leonardo de Moura	df3686634d	refactor(kernel/builtin): remove unnecessary predicates Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 12:20:29 -08:00
Leonardo de Moura	ac9801c7d7	feat(builtin): add support for cross-compilation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 11:58:55 -08:00
Leonardo de Moura	5b7d254e52	feat(builtin): add pre-compiled .lean builtin files to repository Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 11:49:17 -08:00
Leonardo de Moura	ba592c845c	fix(builtin): dependencies Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 11:19:17 -08:00
Leonardo de Moura	9fdf2a3f55	feat(kernel): add trust_imported flag, it skips type checking of 'pre-compiled' Lean modules "Pre-compiled" .olean files were already type checked. The flag -t instructs to Lean to skip type checking when importing these files. TODO: add a check-sum. Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-29 03:43:53 -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	a05c815d31	chore(builtin): cleanup cmake file Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 22:27:36 -08:00
Leonardo de Moura	66178ae65a	refactor(extra): move extra to builtin Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 22:06:11 -08:00
Leonardo de Moura	5e0b344871	fix(kernel/object): uninitialized variable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 21:57:56 -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	aee1c6d3f3	feat(kernel): export/import (.olean) binary files Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 17:31:35 -08:00
Leonardo de Moura	22bebbf242	feat(kernel/object): serializer for kernel objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 14:39:10 -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	755e8b735f	feat(kernel/expr): serializer for kernel expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-28 01:23:21 -08:00
Leonardo de Moura	0ef8ba2939	feat(kernel/level): serializer for level objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 23:30:13 -08:00
Leonardo de Moura	b94503ab20	chore(util/sexpr): remove unnecessary decls Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 23:24:31 -08:00
Leonardo de Moura	3715b10ce7	feat(util/sexpr/options): serialization for options Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 20:40:00 -08:00
Leonardo de Moura	dbebb4a4a1	feat(util/sexpr): serialization for sexpr Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 20:19:56 -08:00
Leonardo de Moura	9c6dc5d230	feat(util/serializer): add hackish write_double/read_double Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 19:46:45 -08:00
Leonardo de Moura	abc370a011	feat(util/numerics): serialization for mpz and mpq Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 18:32:01 -08:00
Leonardo de Moura	49df0c435d	feat(util/serializer): make sure the read/write is portable Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>	2013-12-27 18:07:19 -08:00

... 6 7 8 9 10 ...

2132 commits