Leonardo de Moura
|
565a294489
|
fix(library/blast/congruence_closure): bug at is_congr_root
|
2015-11-23 11:25:58 -08:00 |
|
Floris van Doorn
|
c44ad80e4e
|
feat(homotopy/torus): give recursion and induction principle for the torus
also change the surface of the torus to a square instead of an equality between paths
|
2015-11-22 18:29:37 -08:00 |
|
Floris van Doorn
|
fe8a858d79
|
feat(hott): add recursor to refl_quotient
|
2015-11-22 18:29:37 -08:00 |
|
Floris van Doorn
|
ae92e8c94d
|
feat(hit/two_quotient): give dependent eliminator for two_quotients
|
2015-11-22 18:29:37 -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
|
0bd417bc2a
|
test(tests/lean/run/blast23): missing test
|
2015-11-22 18:23:01 -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
|
989a2e077b
|
fix(tests/lean): adjust tests
|
2015-11-22 17:15:28 -08:00 |
|
Leonardo de Moura
|
a0284b0e82
|
fix(tests/lean/simplifier11): contextual ite lemma has been renamed
|
2015-11-22 17:08:15 -08:00 |
|
Leonardo de Moura
|
d240b06ba2
|
feat(library/init/logic): add new simp rules
|
2015-11-22 17:04:25 -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 |
|
Floris van Doorn
|
0537ef2bd9
|
chore(*): add me as author to files where I made nontrivial contributions
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
74aff044ef
|
feat(group): port three more theorems from the standard library
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
482c68b387
|
feat(*/list): add some computation rules for lists in both libraries
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
93283a4cf8
|
feat(list): also port part of list.comb
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
cc03ca9c6d
|
fix(reserved_notation): make :: bind stronger than ++
this allows us to write l1 ++ a :: l2 without parentheses
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
5abc450fad
|
feat(list): port list.basic from the standard library
|
2015-11-22 14:21:26 -08:00 |
|
Floris van Doorn
|
88a62f8e74
|
feat(algebra|types): small additions
add to markdown file for algebra, and add some definitions in types/
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
5328486d49
|
feat(hit): add elimination rule to propositions
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
5b8486a34f
|
feat(set_quotient): add some properties for set_quotients
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
45d808ce7f
|
feat(homotopy/circle): give all higher homotopy groups of the circle
|
2015-11-22 14:21:25 -08:00 |
|
Floris van Doorn
|
810a399699
|
style(homotopy/circle): clean-up encode-decode proof
|
2015-11-22 14:21:25 -08:00 |
|
Leonardo de Moura
|
564e8f947d
|
refactor(library): cleanup
|
2015-11-22 14:10:02 -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
|
962a61801e
|
test(tests/lean/run/blast_cc8): add card based on finite_set test for congruence closure module
|
2015-11-21 15:04:16 -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
|
c280ddb2b0
|
fix(tests,doc): adjust tests and documentation
|
2015-11-20 17:03:17 -08:00 |
|
Leonardo de Moura
|
85601c5a83
|
chore(library/blast/congruence_closure): fix style
|
2015-11-20 16:46:28 -08:00 |
|
Leonardo de Moura
|
1a4068878e
|
fix(tests/lean/run): adjust tests
|
2015-11-20 16:46:10 -08:00 |
|
Leonardo de Moura
|
5a98a2538c
|
refactor(library): move basic simp/congr rules to init folder, delete some legacy files
|
2015-11-20 16:38:10 -08:00 |
|
Leonardo de Moura
|
eb3d73873a
|
test(tests/lean/run/blast_cc4): congruence_closure and type classes
|
2015-11-20 14:01:15 -08:00 |
|
Leonardo de Moura
|
2627eade8b
|
test(tests/lean/run/blast_cc3): add test for congruence_closure with dependent types
|
2015-11-20 13:55:22 -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 |
|