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

1701 commits

Author SHA1 Message Date
Leonardo de Moura
e4e9c30e66 fix(frontends/lean/builtin_cmds): print patterns 2015-12-02 22:52:54 -08:00
Leonardo de Moura
fdd442bd38 feat(frontends/lean/decl_attributes): turn on [forward] if pattern hints have been provided 2015-12-02 22:52:54 -08: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
84b54ad027 test(tests/lean/run): disable recursor tactic and add tests for unit+cc 2015-11-25 06:43:48 -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
67a4cd3972 feat(frontends/lean): add print [no_pattern] command 2015-11-24 18:48:22 -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
0bd417bc2a test(tests/lean/run/blast23): missing test 2015-11-22 18:23:01 -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
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
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
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
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
c280ddb2b0 fix(tests,doc): adjust tests and documentation 2015-11-20 17:03:17 -08:00
Leonardo de Moura
1a4068878e fix(tests/lean/run): adjust tests 2015-11-20 16:46: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
6bd92e144a test(tests/lean/run/blast20): uncomment example that can now be solved 2015-11-19 11:46:22 -08:00
Daniel Selsam
5ada4312d7 feat(library/blast/forward): propositional forward chaining 2015-11-19 11:44:53 -08:00
Leonardo de Moura
f78e57fd52 feat(shell,frontends/lean): add command line option --dir 
See #821
See #788
 2015-11-19 08:34:23 -08:00
Leonardo de Moura
093a212ed4 test(tests/lean/run/blast21): another blast test 2015-11-18 19:20:32 -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
3f6ec66b36 test(tests/lean/run/blast20): more tests 2015-11-18 19:12:58 -08:00
Daniel Selsam
413989afd6 feat(library/blast/backward): backward chaining strategy 2015-11-18 17:48:39 -08:00
Leonardo de Moura
e580e6cdb1 fix(tests/lean/interactive/findp): adjust test 2015-11-18 10:10:46 -08:00
Leonardo de Moura
de67288305 fix(library/app_builder): mk_rel supports relations where the lhs and rhs are not necessarily the last two arguments (e.g., heq) 2015-11-17 18:45:22 -08:00
Leonardo de Moura
f363975856 feat(frontends/lean): add command #congr_rel for testing new congruence lemma for equivalence relations 2015-11-17 18:45:22 -08:00
Leonardo de Moura
a96aed6dfe test(tests/lean): add tests for simp priorities 2015-11-16 22:41:04 -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
Leonardo de Moura
5095f05303 fix(tests/lean/interactive/findp): adjust test to recent changes in the standard lib 2015-11-16 21:30:28 -08:00
Daniel Selsam
835e8995b4 test(simplifier19): nested fusion 2015-11-16 20:39:16 -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
7cd15aaecd test(simplifier11): add necessary simp rule 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
a02459fe5e test(simplifier9.lean): fix order of congr rules 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
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
b3ca5faa49 fix(tests/lean): some of the simplifier tests 2015-11-16 11:01:53 -08:00
Daniel Selsam
5e8068b2b2 feat(library/blast/simplifier): draft of fusion 2015-11-16 09:13:07 -08:00