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

886 commits

Author SHA1 Message Date
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
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
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
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
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
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
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
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
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
Floris van Doorn
da5f10ce63 feat(hott): minor fixes. allow the usage of numerals for trunc_index 2015-12-17 12:46:16 -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
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
Leonardo de Moura
1b80dc0df6 feat(library/data/real/basic): improve performance 2015-12-09 10:57:16 -08:00
Jacob Gross
ab91f8dd5f feat(library/data/set/basic): add sInter_insert 
add sInter supporting lemma
 2015-12-07 21:39:30 -08:00
Leonardo de Moura
b94e31a72c refactor(library): remove algebra namespace 2015-12-05 23:50:01 -08:00
Jacob Gross
dd6bed371a feat(library/data/set/basic): Added a supporting lemma for sUnion, which will be essential for proofs by induction on finite sets 2015-12-02 23:05:59 -08:00