Commit graph

399 commits

Author SHA1 Message Date
Leonardo de Moura
9dc86e3cf5 fix(builtin/kernel): rename generalized proof_irrel axiom to hproof_irrel, and derive the restricted one
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-04 10:06:29 -08:00
Leonardo de Moura
4fcc292332 feat(frontends/lean): parse and pretty print pair/tuple projection operators proj1 and proj2, fix bug in the type checker
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 22:10:01 -08:00
Leonardo de Moura
cc96b50644 feat(frontends/lean): support for nary-tuples, improve notation for non-dependent tuples, add support in the elaborator for sigma types
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 20:53:11 -08:00
Leonardo de Moura
5c991f8fbf feat(frontends/lean): parse and pretty print tuples/pairs
This commit also fixes a bug in the type checker when processing dependent pairs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 20:10:30 -08:00
Leonardo de Moura
640ebcc040 test(tests/lean/exp): add example for Steve
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 11:35:40 -08:00
Leonardo de Moura
e4afa3dc43 fix(tests/lean/map): incorrect output
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-03 00:05:19 -08:00
Leonardo de Moura
87f9c9b27e fix(tests/lean/map): make sure the unit test produce the same result in different platforms
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 20:29:34 -08:00
Leonardo de Moura
e2add5c9f2 test(tests/lean): add heterogeneous equality simplification example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 20:27:39 -08:00
Leonardo de Moura
6be50f0133 refactor(builtin/heq): merge cast and heq modules
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 15:01:48 -08:00
Leonardo de Moura
c56df132b8 refactor(kernel): remove semantic attachments from the kernel
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-02 14:48:27 -08:00
Leonardo de Moura
2b7bc7b673 test(tests/lean/exp): simulating HOL constructions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 17:59:57 -08:00
Leonardo de Moura
e3dc552c39 fix(library/simplifier): nontermination
The example tests/lua/simp1.lua demonstrates the issue.
The higher-order matcher matches closed terms that are definitionally equal.
So, given a definition

    definition a := 1

it will match 'a' with '1' since they are definitionally equal.

Then, if we have a theorem

    theorem a_eq_1 : a = 1

as a rewrite rule, it was triggering the following infinite loop when simplifying the expression "a"

   a --> 1 --> 1 --> 1 ...

The first simplification is expected. The other ones are not.
The problem is that "1" is definitionally equal to "a", and they match.
The rewrite_rule_set manager accepts the rule a --> 1 since the left-hand-side does not occur in the right-hand-side.

To avoid this loop, we test if the new expression is not equal to the previous one.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 15:55:21 -08:00
Leonardo de Moura
1d85267d26 fix(library/simplifier): assumptions/context may contain equations where the left-hand-side is a metavariable or semantic attachment
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 15:38:22 -08:00
Leonardo de Moura
110ca84984 feat(library/simplifier): allow the user to associate a simplifier monitor with the lua_State object
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-31 13:49:24 -08:00
Leonardo de Moura
759aa61f70 refactor(builtin/kernel): define if-then-else using Hilbert's operator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-30 19:28:42 -08:00
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
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
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
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
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
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
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
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
b26035fcf6 feat(kernel/type_checker): improve application type mismatch error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-27 09:45:17 -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
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
e8bba1ebf3 fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f
Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.

For example, if we had

variable f {A : Type} : A -> Bool

Then, the definition of @f was

definition @f (A : Type) (a : A) : Bool := f A a

This definition is equivalent to
     fun A a, f A a
which is not definitionally equal to
     f
since definitionally equality in Lean ignores Eta conversion.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 20:34:28 -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
5b13ef1b90 test(tests/lean): new simplifier test
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-25 10:56:49 -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
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
35ad156a46 fix(tests/lean): make sure pretty print and parse test passes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:23:55 -08:00
Leonardo de Moura
8f455f5965 fix(frontends/lean): bug in scope construct
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:23:29 -08:00
Leonardo de Moura
7f3e2b3ef4 fix(frontends/lean/parser): bug in 'using' construct
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-24 17:09:46 -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
1a3660180e test(tests/lean): add new simplifier test
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
cd87cb3de4 test(tests/lean): add test for congruence theorem that uses an argument before simplification
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 13:26:09 -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
5ba2525eab test(tests/lean): add test disabling contextual simplifications
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-23 12:57:05 -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
1638a7bb02 fix(frontends/lean/pp): compute local shared nodes, and avoid unnecessary let's
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-22 21:44:24 -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
331b5846c6 test(library/simplifier): add test for the single_pass option in the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-21 13:47:54 -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
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
d1bd56b3d3 fix(tests/lean): adjust test to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 14:47:03 -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
5224df56a3 test(tests/lean): add example showing how to 'sort' argumentes of AC operators using the simplifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-20 08:36:48 -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
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
bcede6925f fix(tests/lean): add expected result file
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 16:31:35 -08:00
Leonardo de Moura
19f3c281c3 test(tests/lean): matrix multiplication example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 16:29:32 -08:00
Leonardo de Moura
999984e701 fix(tests/lean): remove unnecessary theorems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 12:55:33 -08:00
Leonardo de Moura
cc11b9e125 test(tests/lean): rewriting proof example
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-19 12:53:21 -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
7a3aab60c6 chore(builtin/kernel): remove \bowtie as notation for transitivity
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-18 21:11:12 -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
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
fc4c6454a7 chore(tests/lean): adjust tests to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-17 14:36:55 -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
57e58c598c fix(tests/lean): adjust tests to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 16:35:33 -08:00
Leonardo de Moura
91e1f9fc02 fix(tests/lean): adjust test to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 10:20:35 -08:00
Leonardo de Moura
3ab2d2a441 fix(frontends/lean/parser): memory leak due to g++ bug
g++ implementation of std::initializer_list has bug.
http://gcc.gnu.org/ml/gcc-bugs/2013-06/msg00095.html

This commit memory leaks triggered by this bug.
It also adds minimal tests to expose three different instances of the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 10:15:04 -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
12451e4a35 feat(frontends/lean/pp): display implicit arguments when expression contains metavariables
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-13 12:42:05 -08:00
Leonardo de Moura
b85b45b40f test(tests/lean): When and Cond tactical tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 20:43:39 -08:00
Leonardo de Moura
65bdb9c7e0 fix(frontends/lean): unprotected call to Lua API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 19:56:20 -08:00
Leonardo de Moura
a339a53f50 feat(util/options): 'verbose' as a system option, add -q (quiet) option
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 15:31:58 -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
52e11dbbee test(tests/lean): 'using' command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:21:14 -08:00
Leonardo de Moura
fdeb457a81 feat(kernel/pos_info_provider): add support for file names in pos_info_provider
The idea is to include the file name when displaying justification objects.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 12:19:30 -08:00
Leonardo de Moura
84e211b81b fix(frontends/lean): missing ':' in error messages
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:19:58 -08:00
Leonardo de Moura
f7c7dd4ed4 feat(frontends/lean): include filename in error messages, use GNU error message style
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 11:01:27 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 08:33:52 -08:00
Leonardo de Moura
e42b616438 fix(kernel/normalizer): equality between semantic attachments
Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 19:10:30 -08:00
Leonardo de Moura
a4b3d6d6c8 refactor(builtin/kernel): prove eta using function extensionality, and rename abst and abstpi to funext and allext
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 17:25:14 -08:00
Leonardo de Moura
a6e0dcc96c fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-08 16:19:11 -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
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
d12d0f036f feat(kernel/environment): universe variables now live in their own namespace
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-07 15:57:36 -08:00