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

1985 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
ee4344076e feat(library/simplifier): improve error message when simplifier is looping 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 19:36:31 -08:00
Leonardo de Moura
72c607846a test(tests/lean): add Jeremy's proof to test suite 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 16:05:46 -08:00
Leonardo de Moura
b6985bd713 feat(builtin/kernel): add another rewrite rule 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 15:56:26 -08:00
Leonardo de Moura
e2540b68db fix(src/builtin/tactic): add default rule set if none is provided 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 15:56:01 -08:00
Leonardo de Moura
b55aee1efd doc(demo): add another example into demo set 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 10:11:58 -08:00
Leonardo de Moura
9bdf076342 doc(demo): add files for making demos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 09:59:16 -08:00
Leonardo de Moura
7f53cb9601 feat(frontends/lean/parser): add_rewrite take the 'using' command into account 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 01:15:28 -08:00
Leonardo de Moura
b31ef34787 feat(library/simplifier): preserve binder names when applying higher-order rewrite rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:50:27 -08:00
Leonardo de Moura
6da1b447f0 fix(library/hop_match): do not match iff with = 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-28 00:21:05 -08:00
Leonardo de Moura
db45d02078 fix(tests/lean): test discrepancy on OSX 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 23:31:35 -08:00
Leonardo de Moura
dbdbd211e3 fix(library/simplifier): compilation warning 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 23:29:53 -08:00
Leonardo de Moura
55fde28954 feat(kernel/type_checker): optionally provide metavariable environment in the methods: is_definitionally_equal, is_convertible and ensure_pi 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 17:47:03 -08:00
Leonardo de Moura
160dc71cb5 refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 17:38:06 -08:00
Leonardo de Moura
05b4d8411b refactor(kernel/normalizer): normalizer only needs read access to metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 17:03:36 -08:00
Leonardo de Moura
3b152d1a9e refactor(kernel): use ro_metavar_env instead of metavar_env in places where we only need to read the metavariable environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 16:44:43 -08:00
Leonardo de Moura
7b88d68afb test(tests/lean): add test using simplifier monitor for tracking failures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-27 15:11:16 -08:00
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
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
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
ceff335bb8 doc(doc/lean/tutorial): update tutorial 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-26 22:58:44 -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
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
6bc1537e25 feat(frontends/lean/parser): allow the user to write (Type) without providing a level 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-25 20:17:36 -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
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
2bb33c55fe feat(builtin/kernel): add more theorems useful for simplification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 18:52:50 -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
009217b499 feat(builtin/hep): replace hallext axiom with theorem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-01-24 17:09:20 -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