Leonardo de Moura
|
6bbe72190d
|
fix(library/congr_lemma_manager): bug in congruence lemma generator
|
2015-12-03 14:21:30 -08:00 |
|
Leonardo de Moura
|
038369533e
|
fix(library/blast/recursor_action): indexed families
|
2015-12-02 23:43:15 -08:00 |
|
Leonardo de Moura
|
87995b96e3
|
fix(library/blast/congruence_closure): is_relation_app ==> is_equivalence_relation_app
|
2015-12-02 23:28:57 -08:00 |
|
Daniel Selsam
|
42dcbebd1c
|
fix(library/blast/forward/ematch): typo
|
2015-12-02 23:17:24 -08:00 |
|
Daniel Selsam
|
139536896c
|
feat(library/light_lt_manager): light wrappers for ordered rewriting
|
2015-12-02 22:56:54 -08:00 |
|
Daniel Selsam
|
c064f0cd82
|
fix(library/blast/simplifier/ceqv): typos
|
2015-12-02 22:56:00 -08:00 |
|
Daniel Selsam
|
aac50873fe
|
fix(library/num): fix memory leak
|
2015-12-02 22:55:18 -08:00 |
|
Leonardo de Moura
|
acb5b969c6
|
fix(library/blast/subst_action): missing occurs check
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
d2054bb65c
|
chore(library/blast): fix style
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
028ef47c84
|
feat(frontends/lean,library/blast/forward/pattern): check whether patterns can be inferred at declaration time
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
f84c6a6cfa
|
fix(library/blast,frontends/lean): handling pattern hints after unfolding
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
950f356d9a
|
refactor(library/blast,frontends/lean): forward pattern index
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
562d7b3e4a
|
feat(library/blast/blast): add support in blast for controlling whether macros are unfolded or not at whnf/normalize
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
24e4dbe353
|
feat(src/library/type_context): add support for preserving macros at type_context whnf
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
39429251c6
|
chore(library/blast/forward/ematch): fix style
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
af9180b35c
|
fix(library/blast/forward/qcf): compilation warning
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
a83a7f8356
|
feat(library/blast/forward/pattern): remove redundant multi-patterns
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
ec7c38d847
|
feat(library/blast/forward/pattern): add minimal pattern validation
|
2015-12-02 22:52:55 -08:00 |
|
Leonardo de Moura
|
72bd4a8f5a
|
fix(library/blast/options): typo
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
32ad59adc1
|
feat(library/blast/forward/ematch): add support for multi-patterns
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
9260be01b2
|
feat(library/blast): add blast.backward option for disabling/enabling backward chaining
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
a8bb4ba109
|
fix(library/blast/congruence_closure): bug in congruence closure proof extraction
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
08bb966581
|
feat(library/blast/forward/ematch): generate new instances
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
d5b2efc74f
|
feat(library/idx_metavar): add has_idx_metavar
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
4d63a27f13
|
feat(library/blast/forward/ematch): use type class resolution to infer missing arguments
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
37ad850455
|
fix(library/type_context): improve on_is_def_eq_failure
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
3d7831284b
|
fix(library/blast/forward/ematch): extract lemma using target expression instead of pattern
Reason: pattern contains temporary universe meta-variables.
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
9f3f24b46c
|
fix(src/library/blast/forward/ematch): use head_index at m_apps
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
2296168bda
|
feat(library/blast): add blast.ematch option, and ematching search procedure
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
4c624206f4
|
feat(library/blast/forward/pattern): save meta-variables
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
7fa2b7cace
|
feat(library/blast/forward/ematch): ematching skeleton
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
001f8084a9
|
chore(library/blast/forward/forward_extension): rename procedure
|
2015-12-02 22:52:54 -08:00 |
|
Leonardo de Moura
|
05477d34bb
|
fix(library/blast/forward/pattern): missing case
|
2015-12-02 22:52:54 -08:00 |
|
Soonho Kong
|
ff8f24a29b
|
fix(library/blast/backward/backward_rule_set.cpp): fully annotate the use of map2
Close #904
|
2015-12-01 13:42:25 -05:00 |
|
Leonardo de Moura
|
41ff4bc193
|
feat(library/blast/forward/pattern): pattern inference and heuristic instantiation index
|
2015-11-25 23:45:08 -08:00 |
|
Leonardo de Moura
|
996a660de8
|
feat(library/blast): add is_hi_lemma
|
2015-11-25 17:52:59 -08:00 |
|
Leonardo de Moura
|
2becc0367d
|
feat(library/blast/forward/pattern): add add_hi_lemma
|
2015-11-25 17:44:27 -08:00 |
|
Leonardo de Moura
|
87c31acf8c
|
feat(library/blast/forward/pattern): basic indexing for heuristic instantiation
|
2015-11-25 17:30:24 -08:00 |
|
Leonardo de Moura
|
3335c1782d
|
feat(library/blast/forward/pattern): extract trackable and residue hypotheses
|
2015-11-25 13:43:27 -08:00 |
|
Leonardo de Moura
|
edd1b34143
|
doc(library/blast/forward/pattern): describe pattern inference heuristic
|
2015-11-25 11:57:30 -08:00 |
|
Daniel Selsam
|
ca71a2eb12
|
feat(library/blast/unit): conjunctive conclusions
|
2015-11-24 22:45:39 -08:00 |
|
Daniel Selsam
|
eac1ebbf72
|
feat(library/blast/unit): propagate clauses
|
2015-11-24 21:16:01 -08:00 |
|
Leonardo de Moura
|
c923120db5
|
feat(library/blast/congruence_closure): expose mk_ext_congr_lemma
|
2015-11-24 18:48:23 -08:00 |
|
Leonardo de Moura
|
651e3834ba
|
feat(library/blast/congruence_closure): allow meta-variables in the congruence closure module after partitions have been frozen
|
2015-11-24 18:48:23 -08:00 |
|
Leonardo de Moura
|
67a4cd3972
|
feat(frontends/lean): add print [no_pattern] command
|
2015-11-24 18:48:22 -08:00 |
|
Leonardo de Moura
|
8c729d1620
|
feat(library/blast/forward): start 'pattern' module
|
2015-11-24 18:48:22 -08:00 |
|
Leonardo de Moura
|
c50d7ac4b8
|
feat(library/blast/congruence_closure): add add/assume API
|
2015-11-23 15:21:28 -08:00 |
|
Leonardo de Moura
|
f0ccffe968
|
feat(library/blast/congruence_closure): track mod-time
|
2015-11-23 15:03:46 -08:00 |
|
Leonardo de Moura
|
712f60d003
|
feat(library/blast/congruence_closure): expose get_cc()
|
2015-11-23 14:41:22 -08:00 |
|
Leonardo de Moura
|
11f838c13a
|
perf(library/blast/congruence_closure): only copy parents that are still congruence roots
|
2015-11-23 14:38:31 -08:00 |
|
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
|
fc461ce832
|
feat(library/app_builder): avoid redundant proof terms at mk_of_iff_true and mk_not_of_iff_false
|
2015-11-22 15:49:17 -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
|
5e9914ef45
|
feat(library/blast/congruence_closure): avoid eq.rec if major premise is eq.refl
|
2015-11-21 19:00:16 -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
|
c76b04719c
|
feat(library/app_builder): add lift_from_eq
|
2015-11-20 10:27:58 -08:00 |
|
Leonardo de Moura
|
f6ba746b03
|
chore(library/blast/trace): fix signature
|
2015-11-20 08:55:44 -08:00 |
|
Leonardo de Moura
|
ffacf70230
|
chore(library/io_state_stream): remove unused variable
|
2015-11-20 08:20:29 -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
|
86ad8c348e
|
fix(library/norm_num): memory leaks
|
2015-11-19 14:32:47 -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 |
|