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

441 commits

Author SHA1 Message Date
Leonardo de Moura
e1d909455c refactor(library/tactic): add namespace 'tactic', improve expr_to_tactic failure error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 10:45:09 -07:00
Leonardo de Moura
7593ee1468 refactor(library/standard): remove parameter from 'tactic' inductive type 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-02 08:09:24 -07:00
Leonardo de Moura
b2b76b078f feat(frontends/lean): remove build_tactic_cmds, and use expressions for representing tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 20:43:53 -07:00
Leonardo de Moura
cbac21ec7f feat(library/tactic): add trick for 'embedding' tactics inside Lean expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 19:05:22 -07:00
Leonardo de Moura
2df92b0701 refactor(library/tactic): simplify proof_state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 18:02:17 -07:00
Leonardo de Moura
4cb5f97038 refactor(library/tactic): simplify tactic framework, no more proof builders 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-01 16:11:19 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 11:37:46 -07:00
Leonardo de Moura
c2ab31113f refactor(library/tactic): remove cex_builder and 'precision' for proof_state's 
These two features make sense for solvers, but not in a general purpose tactic framework for building proofs like the one in Lean.

In most cases, we cannot build a counterexample anyway. These two features should be added in a custom framework for combining preprocessing techniques like in Z3.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 08:48:07 -07:00
Leonardo de Moura
8d584e54da feat(frontends/lean): add exact_apply 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 00:51:11 -07:00
Leonardo de Moura
360e9b9486 feat(library/tactic): add apply tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 18:33:53 -07:00
Leonardo de Moura
a8f9594046 refactor(kernel/instantiate): rename instantiate_params to instantiate_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 12:09:55 -07:00
Leonardo de Moura
937d7b2813 fix(library/tactic): unfold tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 12:04:58 -07:00
Leonardo de Moura
6d09d82a7c feat(frontends/lean): add notation for orelse tactic, add show and now tactics 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 11:39:18 -07:00
Leonardo de Moura
a1bbb09de4 feat(frontends/lean): add notation for then tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 11:24:56 -07:00
Leonardo de Moura
15f270d9f3 fix(library/tactic): memory leak that only happens when compiling with clang++ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 11:07:06 -07:00
Leonardo de Moura
e408998e06 fix(library/tactic): name convention 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 18:42:59 -07:00
Leonardo de Moura
fa72e7b874 refactor(library/tactic): simplify tactic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 18:35:59 -07:00
Leonardo de Moura
5524c6c3d8 refactor(library/tactic/proof_state): simplify proof state 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 14:49:48 -07:00
Leonardo de Moura
c6ac89d967 refactor(library/tactic/proof_builder): simplify proof builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 12:25:04 -07:00
Leonardo de Moura
aaa7960b75 refactor(library/tactic/goal): use local names for hypotheses 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 11:11:12 -07:00
Leonardo de Moura
d84b745241 refactor(library/tactic/cex_builder): simplify cex_builder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 07:14:33 -07:00
Leonardo de Moura
b4e4c4d610 chore(library/tactic): remove unnecessary file 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 07:02:13 -07:00
Leonardo de Moura
f1d8d8dcf9 chore(library/tactic): update goal objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 07:00:12 -07:00
Leonardo de Moura
ad70044ae1 chore(library/tactic): remove dead code 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-27 07:00:12 -07:00
Leonardo de Moura
77c5319c4a chore(*): remove Lua 'migrate' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-18 07:01:34 -07: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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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