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

1591 commits

Author SHA1 Message Date
Leonardo de Moura
0963ce336f feat(library/blast): add 'grind' and 'grind_simp' blast strategies 
The use [intro] [intro!] [elim] [simp] lemmas.
The [simp] lemmas are only used by grind_simp.
 2016-01-01 17:32:13 -08:00
Leonardo de Moura
4f1415174e refactor(library/data): "union." ==> "union_", "inter." ==> "inter_" 2016-01-01 16:13:44 -08:00
Leonardo de Moura
4e2494f12e refactor(library/init/nat): minor cleanup 2016-01-01 15:56:46 -08:00
Leonardo de Moura
ac9d6c2021 refactor(library/data/bool): cleanup bool proofs and fix bxor definition 2016-01-01 13:52:42 -08:00
Leonardo de Moura
52ec7e6d57 feat(library/blast/recursor): add 'blast.recursor.max_rounds' options and iterative deepening for recursor_strategy 2016-01-01 13:09:37 -08:00
Leonardo de Moura
712e19e22a fix(library/blast/forward/ematch): bug in the ematching procedure 2015-12-31 21:26:44 -08:00
Leonardo de Moura
54f2c0f254 feat(library/blast/forward): inst_simp should use the left-hand-side as a pattern (if none is provided by the user) 
The motivation is to reduce the number of instances generated by ematching.

For example, given

   inv_inv:  forall a, (a⁻¹)⁻¹ = a

the new heuristic uses ((a⁻¹)⁻¹) as the pattern.
This matches the intuition that inv_inv should be used a simplification
rule.

The default pattern inference procedure would use (a⁻¹). This is bad
because it generates an infinite chain of instances whenever there is a
term (a⁻¹) in the proof state.
By using (a⁻¹), we get
   (a⁻¹)⁻¹ = a
Now that we have (a⁻¹)⁻¹, we can match again and generate
   ((a⁻¹)⁻¹)⁻¹ = a⁻¹
and so on
 2015-12-31 20:20:39 -08:00
Jeremy Avigad
0fb398c217 fix(library/data/nat/bigops): delete some blank lines 2015-12-31 15:16:57 -08:00
Jeremy Avigad
7f25dd6646 feat(library/data/nat/bigops): sums and products over intervals of natural numbers 2015-12-31 15:16:57 -08:00
Jeremy Avigad
12a69bad04 refactor(library/data/finset/basic,library/*): get rid of finset singleton 2015-12-31 15:16:57 -08:00
Jeremy Avigad
8a00a431e8 refactor(library/data/finset/basic): rename theorem 2015-12-31 15:16:57 -08:00
Jeremy Avigad
a28ded641c refactor(library/algebra/interval): rename intervals to interval 2015-12-31 15:16:57 -08:00
Jeremy Avigad
86b64cf43b feat(library/data/set/*,library/algebra/group_bigops): better finiteness lemmas, reindexing for big operations 2015-12-31 15:16:57 -08:00
Leonardo de Moura
c3dfabf741 feat(library/blast/strategies/portfolio): add 'rec_simp' 
recursors followed by simplification
 2015-12-31 15:00:38 -08:00
Leonardo de Moura
4134fdd925 feat(library/blast/strategies/rec_strategy): give priority to user defined recursors 2015-12-31 14:55:00 -08:00
Leonardo de Moura
bd03619b5c refactor(library/data/list/basic): test 'rec_inst_simp' blast strategy 
recursor + instantiate [simp] lemmas + congruence closure
 2015-12-31 13:03:47 -08:00
Leonardo de Moura
b35abcc6a8 refactor(library): rename strategy "msimp" ==> "inst_simp" 
"inst_simp" means "instantiate simplification lemmas"
The idea is to make it clear that this strategy is *not* a simplifier.
 2015-12-31 12:45:48 -08:00
Leonardo de Moura
dc6a3e30c0 refactor(library): test simp and msimp in the standard library 2015-12-30 11:22:58 -08:00
Leonardo de Moura
41a01bb606 feat(library/blast/forward/ematch): add option 'blast.ematch.max_instances' 2015-12-29 20:36:11 -08:00
Leonardo de Moura
0148bb08fd feat(library/blast): add 'ematch_simp' strategy for blast and msimp shortcut for it. 
This strategy is based on ematching and congruence closure, but it uses
the [simp] lemmas instead of [forward] lemmas.
 2015-12-29 20:04:31 -08:00
Leonardo de Moura
7462874a4a refactor(library): cleanup nat/int proofs 2015-12-29 12:39:53 -08:00
Leonardo de Moura
a307a0691b refactor(library/data/nat/basic): cleanup some of the nat proofs 2015-12-29 11:43:56 -08:00
Leonardo de Moura
726867a8fb refactor(library/algebra/ring): minor cleanup 2015-12-29 11:16:18 -08:00
Leonardo de Moura
3557bd36e7 refactor(library/algebra/group): cleanup proofs using simp and add [simp] attribute 2015-12-29 10:48:47 -08:00
Leonardo de Moura
b117a10f82 refactor(library/blast/simplifier): use priority_queue to store simp/congr lemmas, use name convention used at forward/backward lemmas, normalize lemmas when blast starts, cache get_simp_lemmas 2015-12-28 17:52:57 -08:00
Leonardo de Moura
f177082c3b refactor(*): normalize metaclass names 
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).

Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write

   definition foo [coercion] ...
   definition bla [forward] ...

and

  open [coercion] nat
  open [forward] nat

It is easier to remember and is uniform.
 2015-12-28 10:39:15 -08:00
Jeremy Avigad
c52ffda0e0 feat(library/algebra/intervals): add notation for intervals 2015-12-26 10:45:53 -08:00
Jeremy Avigad
395eab7c2c feat(library/theories/topology/basic): start on topology (with Jacob Gross) 2015-12-26 10:29:58 -08:00
Jeremy Avigad
549feb5d7f feat(library/data/set/basic): add notation and theorems for large unions and intersections 2015-12-26 08:02:04 -08:00
Jeremy Avigad
d83e5d25fc feat(library/theories/measure_theory/extended_real): start on extended reals 2015-12-24 16:27:48 -05:00
Jeremy Avigad
84cdf3d36d feat(library/theories/analysis/normed_space): start theory of normed spaces for analysis 2015-12-22 16:39:13 -05:00
Jeremy Avigad
08fbf127c6 feat(library/theories/analysis/metric_space,real_limit): define complete metric space, make real an instance 2015-12-22 16:39:13 -05:00
Jeremy Avigad
5b3fbf1618 feat(library/algebra/module): make a start on modules and vector spaces (with material from Nathaniel Thomas) 2015-12-22 16:39:13 -05:00
Jeremy Avigad
6913eb0c76 refactor(library/init/subtype.lean): put subtype notation in the namespace 
The notation { x : A | P x } is overloaded in set, and is ambiguous.
 2015-12-22 16:39:13 -05:00
Jeremy Avigad
8ccafc4267 fix(library/init/function): fix typo 2015-12-22 16:39:13 -05:00
Jeremy Avigad
baf11d0018 feat(library/algebra/ring_bigops): make start on file with more properties of sums and products 2015-12-22 16:39:13 -05:00
Jeremy Avigad
0e3b13f1a0 refactor(library/algebra): combine group_bigops and group_set_bigops 2015-12-22 16:39:13 -05:00
Soonho Kong
f1daf8f24e fix(algebra/group.lean): remove unnecessary use of add.assoc from theorem bit0_add_bit1_helper 2015-12-22 09:12:57 -05:00
Floris van Doorn
da5f10ce63 feat(hott): minor fixes. allow the usage of numerals for trunc_index 2015-12-17 12:46:16 -08:00
Leonardo de Moura
61ecf018e9 feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ... 2015-12-17 12:18:32 -08:00
Leonardo de Moura
c824a0e050 chore(library,hott): enforce naming conventions 2015-12-17 11:36:58 -08:00
Leonardo de Moura
13419d1561 chore(hott/library): cleanup 2015-12-17 11:31:07 -08:00
Leonardo de Moura
42eda36225 chore(library/algebra/ordered_ring): use 'note' 2015-12-15 09:33:57 -08:00
Sebastian Ullrich
2185ee7e95 feat(library/tactic): make let tactic transparent, introduce new opaque note tactic 
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
 2015-12-14 10:14:02 -08:00
Leonardo de Moura
193a9d8cde refactor(library/norm_num): avoid manual constant name initialization 
@rlewis1988 We group all Lean constants used in the C++ code at
src/library/constants.txt

Jeremy and Floris check this file before renaming constants in the
library. So, they can quickly decide whether C++ code will be affected
or not.

We also have a python script for initializing the C++ name objects.
To use the script:
   - go to src/library
   - execute
       python ../../script/gen_constants_cpp.py constants.txt

It will create the boring initialization and finalization code, and
declare a procedure get_<id>_name() for each constant in the file constants.txt.

I also move the norm_num1.lean to the set of unit tests that are
executed whenever we push a commit to the main branch.

I found an assertion violation at line 606. Could you take a look?

Best,
Leo
 2015-12-13 21:38:59 -08:00
Leonardo de Moura
e3a35ba4fd feat(frontends/lean): add 'with_attributes' tactical 
closes #494
 2015-12-13 18:27:44 -08:00
Leonardo de Moura
d4e49a8434 feat(library/tactic/intros_tactic): intro without argument should introduce a single variable 
see #695
 2015-12-13 16:28:39 -08:00
Leonardo de Moura
49eae56db4 test(library/theories/group_theory): test auto-include in the group theory library 2015-12-13 13:40:54 -08:00
Leonardo de Moura
ef546c5c5b refactor(library): use anonymous instance implicit arguments 2015-12-13 11:46:48 -08:00
Floris van Doorn
2325d23f68 feat(hott): port nat and int from the standard library 2015-12-09 12:36:11 -08:00