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

5019 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Leonardo de Moura
72c607846a test(tests/lean): add Jeremy's proof to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 16:05:46 -08:00
Leonardo de Moura
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
b55aee1efd doc(demo): add another example into demo set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 10:11:58 -08:00
Leonardo de Moura
9bdf076342 doc(demo): add files for making demos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 09:59:16 -08:00
Leonardo de Moura
7f53cb9601 feat(frontends/lean/parser): add_rewrite take the 'using' command into account 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 01:15:28 -08:00
Leonardo de Moura
b31ef34787 feat(library/simplifier): preserve binder names when applying higher-order rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:50:27 -08:00
Leonardo de Moura
6da1b447f0 fix(library/hop_match): do not match iff with = 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:21:05 -08:00
Leonardo de Moura
db45d02078 fix(tests/lean): test discrepancy on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 23:31:35 -08:00
Leonardo de Moura
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
7b88d68afb test(tests/lean): add test using simplifier monitor for tracking failures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 15:11:16 -08:00