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

657 commits

Author SHA1 Message Date
Leonardo de Moura
862c5e354d feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 13:08:09 -07:00
Leonardo de Moura
40b3129e7b refactor(kernel): improve names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:28:05 -07:00
Leonardo de Moura
d6d72ba80e refactor(kernel): add binder structure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 10:51:54 -07:00
Leonardo de Moura
c0d8a3195c fix(library/kernel_serializer): style 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 18:00:09 -07:00
Leonardo de Moura
660b9299ad refactor(kernel): (de)serialization procedures don't need to be in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 17:23:36 -07:00
Leonardo de Moura
2e3ffea2ec feat(library): add new coercion API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 16:50:12 -07:00
Leonardo de Moura
1be758e4ef feat(library/resolve_macro.cpp): add macro to encode propositional resolution proofs compactly 
This is also a test for the macro_definition infrastructure that we have in the kernel.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
e644419463 feat(library/bin_app): add simpler is_bin_app predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:11 -07:00
Leonardo de Moura
24d8092a73 feat(library): add goodies for binary functions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
6f8f074f20 feat(library/kernel_bindings): make mk_arrow nary in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
0edcea55de fix(library/kernel_bindings): clang++ compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:48:04 -07:00
Leonardo de Moura
6e78256b87 feat(library/kernel_bindings): expose is_bi_equal predicate in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 17:24:49 -07:00
Leonardo de Moura
2e1a0bd50c feat(kernel/expr): add is_contextual binder info 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:54:27 -07:00
Leonardo de Moura
ab1a89e24c refactor(library): remove dead files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:44:52 -07:00
Leonardo de Moura
956b775c48 feat(library/kernel_bindings): add let field accessors in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 14:17:30 -07:00
Leonardo de Moura
2bb537f3fb feat(library/kernel_bindings): add sugar for creating Let expressions from Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 12:28:10 -07:00
Leonardo de Moura
f903626b78 feat(library/kernel_bindings): allow a list of level params/globals to be provided to declarations (instead of a list of names) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-14 09:45:48 -07:00
Leonardo de Moura
9ed700a5a6 feat(kernel/environment): add forget method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-13 08:40:46 -07:00
Leonardo de Moura
c883c638d6 feat(library/kernel_bindings): expose expression tags in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 16:50:43 -07:00
Leonardo de Moura
6f03064c46 fix(library/kernel_bindings): bug in mk_definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 12:56:50 -07:00
Leonardo de Moura
ff9004dae2 refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-11 18:05:02 -07:00
Leonardo de Moura
e942aecca6 refactor(kernel/type_checker): remove method is_conv 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:29:35 -07:00
Leonardo de Moura
9d96f24766 refactor(kernel): remove convertability constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:25:27 -07:00
Leonardo de Moura
aaea298839 refactor(library/kernel_bindings): remove level pair and list of level pairs from Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:13:10 -07:00
Leonardo de Moura
7b6d555433 refactor(kernel): remove level constraints from definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:11:50 -07:00
Leonardo de Moura
a650a4f9b5 fix(library/kernel_bindings): bug in mk_app, add expr_lt tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 19:54:52 -07:00
Leonardo de Moura
9676f48470 feat(library/kernel_bindings): add list of certified_definitions in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:51:34 -07:00
Leonardo de Moura
c843243f64 feat(library/kernel_bindings): add add_decl and type_check functions to Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 18:08:32 -07:00
Leonardo de Moura
95262fb68d feat(library/kernel_bindings): add remaining type_checker constructors in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 17:13:06 -07:00
Leonardo de Moura
3aa1afdf51 refactor(util): file name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 14:15:28 -07:00
Leonardo de Moura
bf57f951ea refactor(util): move Lua named parameter support to a different file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-08 13:20:37 -07:00
Leonardo de Moura
f3c7bc948a feat(library/kernel_bindings): type_checker Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 19:04:15 -07:00
Leonardo de Moura
62db010ba3 feat(library/kernel_bindings): add optional arguments to empty_environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 17:06:27 -07:00
Leonardo de Moura
4c5f88e63b feat(library/kernel_bindings): global level constructor/accessor/recognizer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:22:45 -07:00
Leonardo de Moura
8ae0e46e9d feat(library/kernel_bindings): add new global level methods to environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-07 16:17:04 -07:00
Leonardo de Moura
503d8dfa9e feat(kernel): add global universe level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-06 16:13:29 -07:00
Leonardo de Moura
8095783c36 refactor(library/kernel_bindings): use new functions for simulating python-like named arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:42:16 -07:00
Leonardo de Moura
850ec69538 feat(kernel): add flag for disabling impredicativity of Prop/Bool in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-05 14:09:17 -07:00
Leonardo de Moura
10d8840cac feat(library/kernel_bindings): add environment Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:53:32 -07:00
Leonardo de Moura
4f3fad5d65 feat(library/kernel_bindings): add certified_definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:46:59 -07:00
Leonardo de Moura
8f5491447a feat(library/kernel_bindings): add environment_id Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:42:27 -07:00
Leonardo de Moura
fc2d5f1595 feat(library/kernel_bindings): add definition Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 17:00:59 -07:00
Leonardo de Moura
b83410f042 fix(library/kernel_bindings): g++ compilation error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 14:34:56 -07:00
Leonardo de Moura
dc627c9965 test(lua): add constraint API tests, and fix minor bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:37:46 -07:00
Leonardo de Moura
6ef161824d feat(library/kernel_bindings): constraint Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 13:17:00 -07:00
Leonardo de Moura
802edd77d1 feat(kernel/justification): add is_eqp predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:15:29 -07:00
Leonardo de Moura
94ca82ec85 fix(library/kernel_bindings): incorrect use of pushinteger, and improve justification Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-02 12:03:43 -07:00
Leonardo de Moura
a5229e5283 chore(util/lua): name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:40:18 -07:00
Leonardo de Moura
7cd892464f feat(library/definition): macro definition and application Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 18:29:34 -07:00
Leonardo de Moura
9f5122b4c7 feat(library/kernel_bindings): justification Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 16:04:30 -07:00
Leonardo de Moura
340c0e0945 feat(library/kernel_bindings): substitution Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 15:30:30 -07:00
Leonardo de Moura
686c307976 feat(library/kernel_bindings): expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 12:25:49 -07:00
Leonardo de Moura
305815cb56 feat(library/kernel_bindings): expose expr_binder_info in the Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 11:23:37 -07:00
Leonardo de Moura
884b3f9b53 refactor(library/kernel_bindings): part of expr Lua API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 16:37:26 -07:00
Leonardo de Moura
3e222e2f22 refactor(kernel/formatter): add environment as an extra argument to the formatter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-30 10:28:07 -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
cd30bb49c1 chore(library/arith): remove unnecessary library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 16:14:15 -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
412a3797f4 refactor(*): add pushboolean inline function, and replace lua_pushboolean with it 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 14:37:16 -07:00
Leonardo de Moura
f7e705badb refactor(library/kernel_bindings): reactive some of the kernel Lua bindings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-29 11:52:09 -07:00
Leonardo de Moura
e769c26800 refactor(kernel): move files that don't need to be in the kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 18:30:40 -07:00
Leonardo de Moura
4842ae4fc7 refactor(kernel): store macro arguments in the macro_expr 
Before this commit, we "stored" macro arguments using applications.
This representation had some issues. Suppose we use [m a] to denote a macro
application. In the old representation, ([m a] b) and [m a b] would have
the same representation. Another problem is that some procedures (e.g., type inference)
would not have a clean implementation.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-25 15:02:56 -07:00
Leonardo de Moura
984ac03ac7 refactor(kernel): replace kernel object with definition, disable affected files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 16:10:47 -07:00
Leonardo de Moura
bc8379256a refactor(kernel): remove pairs from kernel 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-04-17 10:52:07 -07:00
Leonardo de Moura
0b3599851d refactor(library): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
d836e45452 refactor(library): remove unnecessary files 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:57 -07:00
Leonardo de Moura
4b7fe064fe refactor(kernel): finish formatter interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
28516a8dc2 refactor(library): remove unnecessary file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
e0ef6b2e9a refactor(library): monotonic total order on terms 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
8cd78e00f1 refactor(library): deep_copy procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-03-18 10:27:56 -07:00
Leonardo de Moura
1d10953da4 fix(library/elaborator): add hack for experimenting with algebraic hierarchy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-25 11:20:40 -08:00
Leonardo de Moura
309e7ba880 fix(library/elaborator): temporary fix for bug reported by Jeremy 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-24 15:26:21 -08:00
Leonardo de Moura
bfe64a7031 fix(library/elaborator): hack for fixing a bug due to pairs/projs, this is temporary fix until we build a new elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-11 21:30:26 -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
57982135d9 fix(library/simplifier): bug using congr1 theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 16:24:29 -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
2d70e2f4f2 fix(library/tactic/goal): bug in the proof builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-09 15:02:36 -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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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