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

914 commits

Author SHA1 Message Date
Sean Leather
4eee26eaee feat(library/data/sigma): add imp_sigma 2016-04-11 10:04:29 -07:00
Rob Lewis
5a640590cc feat(data/{list,fin}): add theorems for use in matrices 2016-04-11 09:46:46 -07:00
Leonardo de Moura
226f8bafeb fix(library/tactic/rewrite_tactic): do not allow projections to be unfolded 
fixes #1032

This is just a workaround. A better fix has been implemented in the
lean3 branch.
 2016-03-28 13:02:57 -07:00
Leonardo de Moura
0c4a6d3c5e chore(data/set): cleanup proofs to make them less dependent on unifier heuristics 2016-03-09 18:46:23 -08:00
Leonardo de Moura
5e14b4ebe8 fix(library,hott): avoid rewrite with patterns of the form (?M ...) 2016-03-09 15:39:17 -08:00
Floris van Doorn
e5d5ef9d55 feat(hott/library): various changes and additions. 
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
 2016-03-03 10:13:20 -08:00
Floris van Doorn
bf403e124a feat(nat/div): port to HoTT library 2016-03-03 10:13:20 -08:00
Jeremy Avigad
87252bbffe fix(library/data/set/basic): add spaces in notation for bounded quantifiers 2016-03-03 11:50:40 -05:00
Jeremy Avigad
4050892889 refactor(library/*): rename 'compose' to 'comp' 2016-03-02 22:48:05 -05:00
Jeremy Avigad
ebb3e60096 feat(library/algebra/monotone): add properties of monotone functions 2016-03-02 22:01:35 -05:00
Leonardo de Moura
fbe5188480 refactor(frontends/lean): remove 'by+' and 'begin+' tokens 2016-02-29 13:45:43 -08:00
Leonardo de Moura
79ba2638b7 fix(library/data/set/equinumerosity): add missing 'using' 2016-02-29 13:29:03 -08:00
Leonardo de Moura
faa0031d4e refactor(library,hott): remove 'by+' and 'begin+' 2016-02-29 13:15:48 -08:00
Leonardo de Moura
b41c65f549 feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking 2016-02-29 12:31:23 -08:00
Leonardo de Moura
deb1b3dc79 refactor(library): replace assert-exprs with have-exprs 2016-02-29 11:53:26 -08:00
Leonardo de Moura
101cf1ec4c feat(frontends/lean): remove difference between 'have' and 'assert' 2016-02-29 11:28:20 -08:00
Leonardo de Moura
768ba1c363 refactor(library/hott): remove more unnecessary annotations 2016-02-25 14:30:00 -08:00
Leonardo de Moura
510168a387 refactor(library,hott): remove unnecessary annotations 2016-02-25 12:26:20 -08:00
Leonardo de Moura
146edde5b3 feat(library/class): mark instances as quasireducible by default 
quasireducible are also known as lazyreducible.

There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.
 2016-02-25 12:11:29 -08:00
Sebastian Ullrich
3de216d302 chore(*.md): fix/remove broken links 2016-02-23 10:11:24 -08:00
Jeremy Avigad
1546c04154 feat(library/theories/analysis/complex_norm): instantiate complex numbers as a real normed vector space 2016-02-22 11:25:24 -08:00
Jeremy Avigad
158acf878d feat(library/data/set/filter): work in material from Jacob Gross 2016-02-22 11:25:23 -08:00
Jeremy Avigad
41342f53df refactor(library/data/set/filter): get filters working with complete lattice notation 2016-02-22 11:25:23 -08:00
Jeremy Avigad
7fe71c972f feat(library/data/set/basic): add theorems for bounded unions and intersections 2016-02-22 11:25:23 -08:00
Jeremy Avigad
518a77587a refactor(library/data/{set,finset},library/*): use compl for set and finset complement 2016-02-22 11:25:23 -08:00
Jeremy Avigad
8f83c78bc9 fix(library/logic/identities,library/*): fix implicit arguments, add implications. Closes #1002. 2016-02-22 11:25:23 -08:00
Jeremy Avigad
769ae6830d feat(library/data/set/function): add facts about preimages 2016-02-22 11:25:23 -08:00
Jeremy Avigad
a72f6666e8 feat(library/data/set/basic): add two theorems 2016-02-22 11:25:23 -08:00
Jeremy Avigad
b8d3f34d14 feat(library/data/set/basic): add a couple of theorems 2016-02-22 11:25:23 -08:00
Jeremy Avigad
e80559237a fix(library/data/real): tinker with instances 
Convert two instances of has_zero and has_one to local instance,
and change one "[instance]" to a "[trans_instance]". This (by
accident) fixed a problem Rob had a couple of weeks ago.
 2016-02-22 11:25:23 -08:00
Jeremy Avigad
15c9ec12cf fix(library/data/real/division): make temporary has_div only a local instance 2016-02-22 11:25:23 -08:00
Sean Leather
7852524370 fix(library/data/list/sorted): incorrect name 2016-02-22 11:06:39 -08:00
Rob Lewis
68bc41b5fe feat(data/set): add missing set theorems 2016-02-12 11:50:11 -08:00
Rob Lewis
eb05741ce6 feat(data/set): add missing set membership theorems 2016-02-12 11:50:10 -08:00
Leonardo de Moura
42fbc63bb6 fix(library/tc_multigraph): avoid name collisions 
@avigad, @fpvandoorn, @rlewis1988, @dselsam

I changed how transitive instances are named.
The motivation is to avoid a naming collision problem found by Daniel.
Before this commit, we were getting an error on the following file
tests/lean/run/collision_bug.lean.

Now, transitive instances contain the prefix "_trans_".
It makes it clear this is an internal definition and it should not be used
by users.

This change also demonstrates (again) how the `rewrite` tactic is
fragile. The problem is that the matching procedure used by it has
very little support for solving matching constraints that involving type
class instances. Eventually, we will need to reimplement `rewrite`
using the new unification procedure used in blast.

In the meantime, the workaround is to use `krewrite` (as usual).
 2016-02-04 13:15:42 -08:00
Rob Lewis
ffed988a34 feat(data/list): add missing theorems 2016-02-04 11:03:28 -08:00
Rob Lewis
cb4f71b16c feat(library/data/real): add more theorems concerning rationals embedded in reals 2016-02-04 11:03:28 -08:00
Leonardo de Moura
cb12b9b876 refactor(library): cleanup proofs 
Fixed proofs that broke when we tried to implement a "checkpoint" have.
 2016-02-03 19:52:23 -08:00
Jeremy Avigad
53b2d90c90 feat(library/data/{set,finset}): add some useful facts 2016-01-24 16:26:57 -08:00
Jeremy Avigad
1980baf784 feat(library/algebra/group_bigops): add Prod_semigroup, for cases without a unit 2016-01-24 16:26:57 -08:00
Leonardo de Moura
dc5ca99afa fix(library/data/real/basic): unnecessary level of indirection 
At real.comm_ring, `add` is `@add real real_has_add`.
This is bad for any tactic (e.g., blast) that only unfolds reducible definitions.
`add` is not reducible. So, the tactic will not be able to establish
that `@add real real_has_add` is definitionally equal to `real.add`.
 2016-01-24 13:37:15 -08:00
Leonardo de Moura
d3242a2068 refactor(library): rename heq.of_eq heq.to_eq auxiliary lemmas 2016-01-09 12:32:18 -08:00
Johannes Hölzl
6d6a00f48b refactor(library/algebra): fix theorem names 2016-01-06 10:57:55 -08:00
Johannes Hölzl
9c28552afb feat(library/algebra): add lattice instances for Prop, fun, and set 
Adds weak_order, lattice and complete_lattice instances for Prop, fun, and set. Adds supporting
theorems to various other places.
 2016-01-06 10:57:32 -08:00
Jeremy Avigad
4289daddcb refactor(library/data/{set,finset}/basic,library/*): change notation for image to tick mark 2016-01-03 18:52:25 -08:00
Jeremy Avigad
17f6ab3a71 fix(library/data/set/basic): fix spacing in notation 2016-01-03 18:52:25 -08:00
Jeremy Avigad
173368801b fix(library/algebra/interval): rename namespace, and move a theorem 2016-01-03 18:52:25 -08:00
Jeremy Avigad
721f6c87bf feat(library/data/set/basic): add some theorems 2016-01-03 18:52:25 -08:00
Leonardo de Moura
66a722ff5a feat(library/unifier): remove "eager delta hack", use is_def_eq when delta-constraint does not have metavariables anymore 
The "eager-delta hack" was added to minimize problems in the interaction
between coercions and delta-constraints.
 2016-01-03 12:39:32 -08:00
Leonardo de Moura
4f1415174e refactor(library/data): "union." ==> "union_", "inter." ==> "inter_" 2016-01-01 16:13:44 -08:00