Commit graph

650 commits

Author SHA1 Message Date
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
f1b97b18b4 refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 15:54:53 -08:00
Leonardo de Moura
ba02132a90 feat(frontends/lean/parser): add command macros
The idea is to allow users to define their own commands using Lua.
The builtin command Find is now written in Lua.
This commit also fixes a bug in the get_formatter() Lua API.
It also adds String arguments to macros.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-26 13:00:28 -08:00
Leonardo de Moura
88235d2922 feat(library/tactic/apply_tactic): try other solutions produced by the elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-25 11:51:27 -08:00
Leonardo de Moura
8e45064f25 feat(library/tactic/apply_tactic): improved parametric apply_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 22:40:34 -08:00
Leonardo de Moura
75cf751959 feat(library/tactic/apply_tactic): allow apply_tac Lua binding to take expressions as argument
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 16:03:16 -08:00
Leonardo de Moura
6cc57cc4b5 fix(library/tactic/apply_tactic): bug in apply_tac
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 15:54:56 -08:00
Leonardo de Moura
cb95b14332 feat(library/tactic/apply_tactic): improve apply_tactic
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-24 14:23:06 -08:00
Soonho Kong
de018220e1 feat(*): use std::make_shared to create shared_ptr 2013-12-24 14:32:50 -05:00
Leonardo de Moura
00e89190c2 refactor(library/cast): use .lean file instead of .cpp file to define casting library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-23 22:04:19 -08:00
Leonardo de Moura
3e32d9bef2 feat(library/tactic): add support for Pi's at to_proof_state
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 16:40:55 -08:00
Leonardo de Moura
104bd990e1 feat(library/tactic): add normalize_tac, eval_tac and trivial_tac
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 14:10:42 -08:00
Leonardo de Moura
4229e498d2 refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-22 11:51:38 -08:00
Leonardo de Moura
9128a437b8 refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 18:23:37 -08:00
Leonardo de Moura
36b2ec9abb fix(library/cast): bugs in Cast semantic attachment
TODO: revise cast semantic attachment.
It should be axioms instead of semantic attachments.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 16:16:54 -08:00
Leonardo de Moura
aebff0b4d3 fix(library/type_inferer): bug in get_range method
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 14:55:07 -08:00
Leonardo de Moura
97145c0f88 fix(library/elaborator): bug in free variable normalization (lift was missing)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 06:41:09 -08:00
Leonardo de Moura
fddcdb8f40 fix(library/elaborator): bug in process_lower
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 04:13:14 -08:00
Leonardo de Moura
4d05a8b65b fix(library/tactic/apply_tactic): provide the metavar_env to instantiate, the goal is to avoid add_lift and add_inst local entries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 14:17:04 -08:00
Leonardo de Moura
1ed4aa391c fix(library/fo_unify): bug at function that extracts the lhs and rhs of homogeneous/heterogeneous equality
For homogeneous equality, arg #1 is the Type of the lhs/rhs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 14:14:20 -08:00
Leonardo de Moura
7772c16033 refactor(kernel): add unfold_opaque flag to normalizer, modify how type checker uses the opaque flag, remove hidden_defs, and mark most builtin definitions as opaque
After this commit, in the type checker, when checking convertability, we first compute a normal form without expanding opaque terms.
If the terms are convertible, then we are done, and saved a lot of time by not expanding unnecessary definitions.
If they are not, instead of throwing an error, we try again expanding the opaque terms.
This seems to be the best of both worlds.
The opaque flag is a hint for the type checker, but it would never prevent us from type checking  a valid term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 12:47:47 -08:00
Leonardo de Moura
812c1a2960 feat(library/elaborator): only expand definitions that are not marked as hidden
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression

 (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)

After, this commit it produces

 (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)

The expressions above are definitionally equal, but the second is easier to work with.

Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 02:16:49 -08:00
Leonardo de Moura
cb48fbf3c4 fix(library/elaborator): missing case
The elaborator was failing in the following scenario:
- Failing constraint of the form
     ctx |- ?m1 =:= ?m2
where
     ?m2 is assigned to ?m1,
     and ?m1 is unassigned.

has_metavar(?m2, ?m1) returns true, and a cycle is incorrectly reported.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 01:39:43 -08:00
Leonardo de Moura
3eb4de6760 fix(frontends/lean/parser): fix deadlock in macro parser
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 21:40:00 -08:00