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

2234 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
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
cbe89ca32e doc(doc/todo): update TODO list 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 19:19:49 -08:00
Leonardo de Moura
17eb2374ee doc(README): add link to tutorial in the main page 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 19:14:02 -08:00
Leonardo de Moura
9fa03db42b doc(doc/lean/tutorial): expand the tutorial 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-02 19:09:55 -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
a51530dca0 doc(examples/lean): improve dep_if example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-31 13:49:57 -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
4f22a3bfed doc(examples/lean): expand the dependent if-then-else example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 22:44:04 -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
5b810d11eb doc(examples/lean): "dependent" if-then-else example 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 22:14:41 -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
2368b4097c fix(examples/lean): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 12:36:10 -08:00
Leonardo de Moura
45b453873b doc(examples/lean): add well-founded induction theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-30 12:33:55 -08:00
Leonardo de Moura
41f5e2a067 feat(library/simplifier): statically check (conditional) equations (aka rewrite rules) to verify whether we can skip type checking when using them in the simplifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 18:32:40 -08:00
Leonardo de Moura
01259b1e84 feat(kernel): make sure U is the maximal universe 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 16:31:00 -08:00
Leonardo de Moura
ea6bf224e5 feat(frontends/lean): make the parser accept (Type -> ...) 
Before this commit, the parser would accept only a universe level or a ')' after '(' 'Type'

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 10:32:48 -08:00
Leonardo de Moura
92ba4e8b2d feat(library/simplifier): add support for metavariables in conditional rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 08:34:04 -08:00
Leonardo de Moura
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