Leonardo de Moura
|
f4a7268bd7
|
fix(library/blast/congruence_closure): bug in add_eqv_step
|
2015-11-23 14:26:33 -08:00 |
|
Leonardo de Moura
|
f1a3f8ec9d
|
feat(library/blast/congruence_closure): add blast.trace_cc option
|
2015-11-23 14:24:59 -08:00 |
|
Daniel Selsam
|
46e60abda6
|
feat(library/blast/forward): branch extension
|
2015-11-23 13:58:13 -08:00 |
|
Daniel Selsam
|
a8700e6778
|
refactor(library/blast/unit): rename unit propagation module
|
2015-11-23 13:58:13 -08:00 |
|
Leonardo de Moura
|
20cfe9e02e
|
feat(library/blast/state): improve lazy initialization
|
2015-11-23 11:32:45 -08:00 |
|
Leonardo de Moura
|
3ee32c02d8
|
feat(library/blast/congruence_closure): add freeze_partitions API for qcf procedure
|
2015-11-23 11:26:15 -08:00 |
|
Leonardo de Moura
|
565a294489
|
fix(library/blast/congruence_closure): bug at is_congr_root
|
2015-11-23 11:25:58 -08:00 |
|
Leonardo de Moura
|
8632b7ae27
|
chore(library/blast/backward/backward_strategy): remove unused param
|
2015-11-22 18:27:23 -08:00 |
|
Leonardo de Moura
|
b442fe66b2
|
chore(library/blast/simple_strategy): fix style
|
2015-11-22 18:24:59 -08:00 |
|
Leonardo de Moura
|
0fcf8ed7d2
|
refactor(library/blast): hypothesis activation protocol
|
2015-11-22 18:22:26 -08:00 |
|
Leonardo de Moura
|
1bd827dffc
|
feat(library/blast/simplifier/simplifier_actions): add simplify_hypothesis_action
|
2015-11-22 17:49:00 -08:00 |
|
Leonardo de Moura
|
8681b34129
|
fix(library/blast/simplifier/simplifier_actions): update target when simplifier produces a definitionally equal output that is not structurally equal
This update also uses the even target_updated to decide when the target
needs to be updated.
|
2015-11-22 17:25:54 -08:00 |
|
Leonardo de Moura
|
0c4fb6b3d5
|
feat(library/blast): add option 'blast.recursor' for disabling recursor action
|
2015-11-22 17:15:38 -08:00 |
|
Leonardo de Moura
|
56282a11f6
|
feat(library/blast/blast): use type_context normalizer
|
2015-11-22 17:04:04 -08:00 |
|
Leonardo de Moura
|
6b248f44eb
|
feat(library/blast): add option for showing the blast failure state
|
2015-11-22 16:32:07 -08:00 |
|
Leonardo de Moura
|
94f7b7f95d
|
feat(library/blast/congruence_closure): add support for propagating units in the congruence closure module
See blast_cc12.lean for example.
|
2015-11-22 15:39:44 -08:00 |
|
Leonardo de Moura
|
f326e731a0
|
fix(library/blast/subst_action): do not apply subst to (H : a = a), let the discard_action to get rid of it
|
2015-11-22 15:37:32 -08:00 |
|
Leonardo de Moura
|
6fc0e41439
|
fix(library/blast/congruence_closure): proof generation for congruences such as (a = b) <-> (b = a)
The congruence closure module treats these two terms as the same thing.
So, we should take this into account when building proofs
|
2015-11-21 19:50:59 -08:00 |
|
Leonardo de Moura
|
607552e51f
|
feat(library/blast): add target_updated event
|
2015-11-21 17:58:21 -08:00 |
|
Leonardo de Moura
|
091b0f0cc7
|
feat(library/blast): add option for disabling congruence closure
|
2015-11-21 17:45:25 -08:00 |
|
Leonardo de Moura
|
c4328aad3a
|
feat(library/blast/congruence_closure): missing case
|
2015-11-21 17:40:15 -08:00 |
|
Leonardo de Moura
|
c49caf3740
|
feat(library/blast/congruence_closure): add support for user-defined congruence lemmas in the congruence closure module
|
2015-11-21 14:43:51 -08:00 |
|
Leonardo de Moura
|
a61869ba1a
|
feat(library/blast): add option for disabling simplifier
|
2015-11-21 12:19:55 -08:00 |
|
Leonardo de Moura
|
85601c5a83
|
chore(library/blast/congruence_closure): fix style
|
2015-11-20 16:46:28 -08:00 |
|
Leonardo de Moura
|
8f368cebbf
|
feat(library/blast/congruence_closure): lift equalities
|
2015-11-20 13:48:22 -08:00 |
|
Leonardo de Moura
|
28970ef717
|
feat(library/blast/congruence_closure): proof extraction
|
2015-11-20 12:23:32 -08:00 |
|
Leonardo de Moura
|
1e3f549c39
|
feat(library/blast/subst_action): add option for disabling subst action
|
2015-11-20 10:53:02 -08:00 |
|
Leonardo de Moura
|
028a2ab785
|
feat(library/blast): add get_config()
|
2015-11-20 10:39:26 -08:00 |
|
Leonardo de Moura
|
f6ba746b03
|
chore(library/blast/trace): fix signature
|
2015-11-20 08:55:44 -08:00 |
|
Leonardo de Moura
|
628608ca7d
|
chore(library/blast/congruence_closure): fix style
|
2015-11-19 19:49:59 -08:00 |
|
Leonardo de Moura
|
d5b0a45aa4
|
chore(library/blast/simplifier/simplifier_actions): fix warnings
|
2015-11-19 19:47:04 -08:00 |
|
Daniel Selsam
|
21cb409e6c
|
refactor(library/blast/simplifier): move simplifier module into blast
|
2015-11-19 19:43:04 -08:00 |
|
Daniel Selsam
|
2c72f46adc
|
feat(library/blast/forward): opportunistically delete dead hypotheses
|
2015-11-19 19:40:40 -08:00 |
|
Leonardo de Moura
|
2d93fe4b76
|
feat(library/blast/congruence_closure): implement congruence closure
Proof extraction is still missing
|
2015-11-19 19:37:11 -08:00 |
|
Leonardo de Moura
|
968b615390
|
feat(library/blast/congruence_closure): add "add_eqv"
|
2015-11-19 15:56:21 -08:00 |
|
Leonardo de Moura
|
f9ced4b3e1
|
feat(library/blast): add "ppb" helper class for pretty printing expression in blast
|
2015-11-19 15:55:22 -08:00 |
|
Leonardo de Moura
|
ee3083c12c
|
feat(library/blast): add action based on congruence closure module
|
2015-11-19 12:30:45 -08:00 |
|
Daniel Selsam
|
5ada4312d7
|
feat(library/blast/forward): propositional forward chaining
|
2015-11-19 11:44:53 -08:00 |
|
Daniel Selsam
|
3523e32345
|
chore(library/blast/simplifier): use blast's app_builder
|
2015-11-19 10:57:33 -08:00 |
|
Daniel Selsam
|
e856de5ab4
|
chore(library/blast/simplifier): remove old comment
|
2015-11-19 10:57:33 -08:00 |
|
Leonardo de Moura
|
193c446fc4
|
fix(library/blast/blast): metavariable assignment validation
|
2015-11-19 10:52:18 -08:00 |
|
Leonardo de Moura
|
3bd83b8e41
|
feat(library/blast/backward/backward_strategy): don't try constructor action by default
|
2015-11-18 19:14:37 -08:00 |
|
Leonardo de Moura
|
aa1451888c
|
fix(library/blast): spurious trace messages, typo
|
2015-11-18 19:12:29 -08:00 |
|
Leonardo de Moura
|
d85e26898e
|
fix(library/blast): uninitialized variables
|
2015-11-18 18:56:19 -08:00 |
|
Leonardo de Moura
|
fbeee674b3
|
chore(library/blast/union_find): remove dead code
|
2015-11-18 18:35:00 -08:00 |
|
Leonardo de Moura
|
f8a20341cb
|
refactor(library/blast): get_hypothesis_decl return a reference
|
2015-11-18 18:20:02 -08:00 |
|
Leonardo de Moura
|
b61eb3ea0c
|
fix(library/blast): compilation errors in debug mode
|
2015-11-18 18:01:58 -08:00 |
|
Leonardo de Moura
|
808e6f0089
|
chore(library/blast/backward/backward_rule_set): unused variable
|
2015-11-18 17:59:31 -08:00 |
|
Daniel Selsam
|
413989afd6
|
feat(library/blast/backward): backward chaining strategy
|
2015-11-18 17:48:39 -08:00 |
|
Daniel Selsam
|
39a9ab6bf8
|
fix(library/blast/simplifier): misc cleanup
|
2015-11-18 17:32:08 -08:00 |
|
Leonardo de Moura
|
5251752b9c
|
chore(library/blast/state): document branch extension methods
|
2015-11-18 17:29:01 -08:00 |
|
Leonardo de Moura
|
70a1aebfe3
|
feat(library/blast/state): add initialized event handler for branch extensions.
|
2015-11-18 17:24:04 -08:00 |
|
Leonardo de Moura
|
107c155574
|
chore(library/blast/state): fix style
|
2015-11-18 15:50:24 -08:00 |
|
Leonardo de Moura
|
223e77c4a9
|
refactor(library/blast): use branch_extension for recursor_action
|
2015-11-18 15:49:02 -08:00 |
|
Leonardo de Moura
|
6823a34935
|
feat(library/blast): branch extensions
|
2015-11-18 15:30:59 -08:00 |
|
Leonardo de Moura
|
bf5fe8d180
|
feat(library/blast): add trace module
|
2015-11-18 12:59:53 -08:00 |
|
Leonardo de Moura
|
453e90261b
|
refactor(library/blast): make sure all actions return action_result, add macros for simplifying strategy definition
revert is not an action, but a procedure for helping us to build actions.
|
2015-11-18 12:29:43 -08:00 |
|
Leonardo de Moura
|
59e676e4fa
|
fix(library/blast/strategy): initialization
A strategy is supposed to solve the current branch.
|
2015-11-18 10:20:02 -08:00 |
|
Leonardo de Moura
|
93a0f62cd3
|
chore(library/blast/congruence_closure): fix style
|
2015-11-17 19:16:42 -08:00 |
|
Leonardo de Moura
|
dde4aa72f9
|
chore(library/blast/congruence_closure): fix warnings
|
2015-11-17 19:14:12 -08:00 |
|
Leonardo de Moura
|
3734cc671a
|
feat(library/blast/congruence_closure): add is_eqv
|
2015-11-17 19:10:00 -08:00 |
|
Leonardo de Moura
|
d833410f0d
|
feat(library/blast/congruence_closure): add proved/disproved aux methods
|
2015-11-17 19:06:23 -08:00 |
|
Leonardo de Moura
|
3f6b79227f
|
refactor(library/blast/congruence_closure,library/app_builder): add helper methods for theorems heavily used in the congruence closure module
|
2015-11-17 18:57:40 -08:00 |
|
Leonardo de Moura
|
3de9a89d93
|
feat(library/blast/congruence_closure): congruence_closure basics
|
2015-11-17 18:45:22 -08:00 |
|
Leonardo de Moura
|
491c7c55e1
|
feat(library/simplifier/simp_rule_set): add priorities for simp and congr rules
|
2015-11-16 22:34:06 -08:00 |
|
Daniel Selsam
|
a689c66b1e
|
fix(library/blast/simplifier): handle scalar in fusion
|
2015-11-16 20:39:15 -08:00 |
|
Daniel Selsam
|
49ff8640d9
|
fix(library/blast/simplifier): use ac rules for numerals
|
2015-11-16 20:39:15 -08:00 |
|
Daniel Selsam
|
8ca5d87f0b
|
feat(library/blast/simplifier): rely on norm_num for recursion
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
9f1dda5622
|
style(library/blast/simplifier): follow else brace rules
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
6ba42bb7bc
|
test(simplifier11.lean): add rule for (not P)
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
b9a516783c
|
fix(library/blast/simplifier): remove unnecessary casts
|
2015-11-16 20:33:22 -08:00 |
|
Daniel Selsam
|
550cac6065
|
feat(library/norm_num): use type_context
|
2015-11-16 20:33:22 -08:00 |
|
Leonardo de Moura
|
ab98be633a
|
fix(library/blast/simplifier): warning when compiling using clang on OSX
|
2015-11-16 18:56:35 -08:00 |
|
Leonardo de Moura
|
4dc27fb43b
|
chore(library/blast): use "override" consistently for proof_step objects
|
2015-11-16 18:30:59 -08:00 |
|
Leonardo de Moura
|
39ec756331
|
feat(library/blast): add congruence closure skeleton
|
2015-11-16 16:07:00 -08:00 |
|
Leonardo de Moura
|
60945e95b4
|
feat(library/blast): add 'discard' action for detecting irrelevant hypotheses
|
2015-11-16 11:43:51 -08:00 |
|
Leonardo de Moura
|
7abb0d6b96
|
chore(frontends/lean/builtin_cmds,library/blast/simplifier): fix style
|
2015-11-16 11:10:12 -08:00 |
|
Leonardo de Moura
|
a567cce685
|
fix(library/blast/simplify_actions): compilation error due to recent changes in the simplifier API
|
2015-11-16 10:13:27 -08:00 |
|
Daniel Selsam
|
5e8068b2b2
|
feat(library/blast/simplifier): draft of fusion
|
2015-11-16 09:13:07 -08:00 |
|
Daniel Selsam
|
c694d443d7
|
feat(library/blast/simplifier): placeholder for fusion
|
2015-11-16 09:13:07 -08:00 |
|
Daniel Selsam
|
f72da014d4
|
feat(library/blast/fusion): refactor
|
2015-11-16 09:13:07 -08:00 |
|
Daniel Selsam
|
d852be0d79
|
feat(library/blast/simplifier): option for fusing
|
2015-11-16 09:12:29 -08:00 |
|
Leonardo de Moura
|
db59c6829c
|
feat(library/blast): add basic support for non-recursive recursors/eliminators in the simple_strategy, fix bug at recursor_action
|
2015-11-15 18:39:12 -08:00 |
|
Leonardo de Moura
|
a545860aa1
|
feat(library/blast/intros_action): apply head_beta_reduce at intros
|
2015-11-15 18:14:12 -08:00 |
|
Leonardo de Moura
|
2e057477ef
|
feat(library/blast/recursor_action): ignore type class instances in the recursor action
|
2015-11-15 18:04:08 -08:00 |
|
Leonardo de Moura
|
24ed427c2f
|
feat(library/blast): add "recursor" (aka elimination/induction) action
|
2015-11-15 18:00:32 -08:00 |
|
Leonardo de Moura
|
9e8627380a
|
chore(library/blast/simple_strategy): fix style
|
2015-11-15 15:08:01 -08:00 |
|
Leonardo de Moura
|
1308c7c4e2
|
feat(library/blast): add action for not(a ~ a) when ~ is a reflexive relation
|
2015-11-15 15:00:25 -08:00 |
|
Leonardo de Moura
|
ffd0c2b09a
|
refactor(library/blast/simple_strategy): eliminate duplicated code
|
2015-11-15 14:30:24 -08:00 |
|
Leonardo de Moura
|
2549e49e72
|
feat(library/blast): add priority_queue for hypotheses we want to eliminate (apply recursion over)
|
2015-11-15 13:32:43 -08:00 |
|
Leonardo de Moura
|
4cd5e18bd0
|
refactor(library/blast): add strategy abstract object
|
2015-11-15 13:12:21 -08:00 |
|
Leonardo de Moura
|
bae37d287d
|
fix(library/blast/state): bad style warnings
|
2015-11-15 12:38:07 -08:00 |
|
Leonardo de Moura
|
fd41a4f76d
|
feat(library/blast): add simplify_target action
|
2015-11-14 16:18:12 -08:00 |
|
Leonardo de Moura
|
6a554f6ba7
|
fix(library/blast/simple_actions): missing include
|
2015-11-14 15:41:54 -08:00 |
|
Leonardo de Moura
|
b5db77961d
|
feat(library/blast): add "trivial" action
|
2015-11-14 15:02:14 -08:00 |
|
Leonardo de Moura
|
0803db21d3
|
refactor(library/blast): add "_action" suffix to files defining actions
|
2015-11-14 13:22:12 -08:00 |
|
Leonardo de Moura
|
9921228dd5
|
feat(library/blast): add simp_rule_sets to branch
|
2015-11-14 13:16:00 -08:00 |
|
Leonardo de Moura
|
0f4e59a84f
|
feat(library/blast): add "no_confusion" action
|
2015-11-13 18:19:05 -08:00 |
|
Leonardo de Moura
|
29d472788f
|
feat(library/blast/subst): avoid unnecessary proof step
|
2015-11-13 16:31:07 -08:00 |
|
Leonardo de Moura
|
3849aff674
|
fix(library/blast/subst): bug in subst action, add hypothesis_idx_buffer_set (helper class), refine revert_action interface
|
2015-11-13 16:10:25 -08:00 |
|