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

461 commits

Author SHA1 Message Date
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
413391b2b4 chore(tests/lean/sig2): remove unnecessary parenthesis from test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 11:37:08 -08:00
Leonardo de Moura
c9b72df34b fix(frontends/lean/parser): bug when applying tactics to synthesize remaining meta-variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 11:36:26 -08:00
Leonardo de Moura
96c9c7505a test(tests/lean): add another sigma-type test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-02-04 10:12:39 -08:00
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
dd6aae378f fix(library/simplifier): must use metavar_env in is_ceq, otherwise it may ceqs that contain metavariables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 13:29:20 -08:00
Leonardo de Moura
4dc3aa46c3 feat(frontends/lean): allow tactics to be used in axiom/variable declarations and in the type of definitions/theorems; add a new test showing the need for this feature 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 12:02:12 -08:00
Leonardo de Moura
069e5edf6b fix(library/simplifier): include flag indicating if the proof generated by simplifier is a homogenous or heterogenous equality, use flag to fix bug in the simp_tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-29 12:01:01 -08:00
Leonardo de Moura
62408a6adc test(tests/lean): move simp_loop test to slow subdirectory 
This example produces a stackoverflow on Valgrind.
We don't execute Valgrind on tests in the slow subdirectory.

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