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

492 commits

Author SHA1 Message Date
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