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

1115 commits

Author SHA1 Message Date
Rob Lewis
b1aea149db chore(library/data/real): update md 2015-06-09 15:43:43 +10:00
Rob Lewis
e112468f99 feat(library/data/real): prove reals are Cauchy complete 2015-06-09 15:39:51 +10:00
Rob Lewis
3749a8ad04 chore(library/data/real): update real.md 2015-06-09 15:39:51 +10:00
Leonardo de Moura
1c5c79fbc1 refactor(library/data/list/perm): use improved 'obtain' to cleanup proof 2015-06-08 11:58:21 -07:00
Haitao Zhang
6949e2d422 feat(library/data/fintype): add finite function related theories 
develop kth related techniques, all_lists_of_len, all_funs, map between lists and functions, finite inverse and cardinality
remove function module from default import list for now
 2015-06-08 10:48:22 -07:00
Leonardo de Moura
35eae96aa5 chore(library/data/int/gcd): remove 'TODO' 
The 'TODO' was fixed by commit 496189feed
 2015-06-08 10:45:05 -07:00
Jeremy Avigad
e59400b58c feat(library/data/int/{div,gcd}): add some theorems, to reduce rationals 2015-06-08 22:43:51 +10:00
Jeremy Avigad
1c93c5bbb2 feat(library/logic/{connectives.lean,quantiers.lean}): add iff congruence rules 2015-06-08 16:58:08 +10:00
Jeremy Avigad
feb385748f refactor(library/data/set/map.lean): put map into set namespace 
This is needed to repair a conflict in the tutorial, but it is the right thing to do anyhow. The type "map A B" should not be a top-level identifier.
 2015-06-06 18:58:33 -07:00
Leonardo de Moura
17f2c240e1 refactor(library/init/wf): cleanup wf proofs using tactics 
add dependent elimination for acc.
 2015-06-06 16:58:24 -07:00
Leonardo de Moura
7db84c7036 refactor(library/data): replace 'fin' with Haitao's 'less_than' 
The commit also fixes vector to use the new definition.
 2015-06-05 10:33:19 -07:00
Jeremy Avigad
453da48dd5 feat(library/data/less_than.lean): add finite ordinals from Haitao Zhang 2015-06-05 09:32:00 -07:00
Jeremy Avigad
370860e1b0 feat(library/data/fintype,finset): add cardinality for finite types from Haitao Zhang 2015-06-05 09:32:00 -07:00
Jeremy Avigad
f475408f4c feat(library/data/list/*): add theorems from Haitao Zhang and clean up 2015-06-05 09:32:00 -07:00
Jeremy Avigad
4db89e16dc feat(library/theories): create theories folder 2015-06-05 09:32:00 -07:00
Jeremy Avigad
c2aa8c6720 feat(library/data/finset/partition.lean): add theory of partitions into finsets by Haitao Zhang 2015-06-05 09:32:00 -07:00
Leonardo de Moura
4d52d4c790 fix(library/init/quot): prove quot.exact 2015-06-05 08:04:55 -07:00
Floris van Doorn
dce257bccb fix(init/nat): remove exit 2015-06-04 20:23:44 -04:00
Floris van Doorn
ff41886a32 feat(nat/bquant): give instances for quantification bounded with le 
also add theorems c_iff_c to logic/connectives, where c is a connective
 2015-06-04 20:14:13 -04:00
Floris van Doorn
7f5caab694 feat(nat): redefine le and lt in the standard library 2015-06-04 20:14:13 -04:00
Floris van Doorn
37995edbd7 fix(tools.md): remove missing link 2015-06-04 20:14:13 -04:00
Floris van Doorn
876aa20ad6 feat(hott): Port remainder of §6.3 and §7.2 from the HoTT book 
Also prove a theorem similar to Lemma 7.3.1

There are still some sorry's in hit.suspension
 2015-06-04 20:14:12 -04:00
Leonardo de Moura
63f61a35f4 feat(library/data/list/set): cleanup nodup_map proof 2015-06-04 15:21:40 -07:00
Leonardo de Moura
9a7cff0e89 feat(library/data/list/comb): add length_product theorem 2015-06-04 15:11:09 -07:00
Jeremy Avigad
df69bb4cfc feat(library/*): add theorems from Haitao on sets and functions, clean up 2015-06-04 11:55:25 -07:00
Jeremy Avigad
03952ae12c feat(library/logic/{connectives,identities},library/algebra/function): cleanup and some additions from Haitao Zhang 2015-06-04 11:55:25 -07:00
Leonardo de Moura
dce86b3a84 feat(library/init/logic): add 'eq.drec' (in standard Lean) with a signature very similar to eq.rec in the HoTT library 2015-06-03 17:29:26 -07:00
Leonardo de Moura
c841e63649 refactor(library/data/fintype): create 'fintype' subdirectory 2015-06-03 16:43:55 -07:00
Leonardo de Moura
2a6ea2c6fb feat(library/data/finset/to_set): add to_set.inj 2015-06-03 14:05:43 -07:00
Leonardo de Moura
16d03c17ee refactor(library/logic/eq): use 'substvars' tactic 2015-06-02 23:55:51 -07:00
Leonardo de Moura
a8c9121d2e feat(library/data/vec): add vector as list subtype 2015-06-02 22:09:23 -07:00
Leonardo de Moura
7a39d5aaa3 feat(library/data): add auxiliary definitions 2015-06-02 22:08:25 -07:00
Leonardo de Moura
228a99af7e feat(library/data/subtype): cleanup proof 2015-06-02 19:51:28 -07:00
Leonardo de Moura
70d0dea02d feat(library/init/logic): add more congruence theorems 
Remark: the simplifier should be able to select the "right" one.
 2015-06-02 14:06:15 -07:00
Leonardo de Moura
2f9005827c feat(library/init/logic): 'if-then-else' and 'dependent-if-then-else' congruence theorems 
We will use these theorems to test the new simplifier.
 2015-06-02 13:27:50 -07:00
Leonardo de Moura
50fe4ec6c0 feat(library/data/encodable): add quot.rep definition for choosing equivalence class representative for equivalence classes of encodable types 2015-06-02 11:03:24 -07:00
Leonardo de Moura
e7448ca77e feat(library/init/quot): add exists_rep theorem for quotients 2015-06-02 10:52:07 -07:00
Leonardo de Moura
1ea56038e3 feat(library/init/quot): add has_decidable_eq definition for quotients 2015-06-02 10:47:20 -07:00
Rob Lewis
b1404c5943 feat(library/data/real): fill in sorrys in proof that R is l.o. field 2015-06-01 23:00:53 +10:00
Rob Lewis
9843e61583 feat(library/data/real): define inverses of reals, prove (classically) that R is a discrete linear ordered field 2015-06-01 23:00:53 +10:00
Jeremy Avigad
82142b60f0 refactor(library/data/finset/basic.lean): remove finset / finset.finset duplicate 2015-06-01 12:35:44 +10:00
Jeremy Avigad
dcae29a253 feat(library/data/int/gcd.lean): add gcd for the integers 2015-06-01 12:35:44 +10:00
Jeremy Avigad
ffa648a090 feat/refactor(library/*): various additions and improvements 2015-06-01 12:35:44 +10:00
Jeremy Avigad
cdecc309b3 fix(library/data/finset/to_set.lean): to_set does not require decidable equality 2015-06-01 12:35:44 +10:00
Leonardo de Moura
1238f43575 feat(library/logic/examples): add "double-negation translation" example 2015-05-31 18:18:10 -07:00
Leonardo de Moura
ca110012d8 feat(library/tactic): automate "generalize-intro-induction/cases" idiom 
closes #645
 2015-05-30 21:57:28 -07:00
Jeremy Avigad
b76445df39 feat(library/data/{nat,int}/div.lean,*): improve and extend div in nat and int 2015-05-30 22:10:21 +10:00
Jeremy Avigad
c986ee305b refactor(library/data/nat/gcd.lean): move gcd to a new file 2015-05-30 22:10:21 +10:00
Jeremy Avigad
cc0a620db1 feat(library/data/{nat,int}/div.lean): add to and improve div library 2015-05-30 22:10:21 +10:00
Rob Lewis
82f85a574d feat(library/data/real): prove reals form an ordered ring 2015-05-29 14:11:51 +10:00
Rob Lewis
2273dc669e feat(library/data): fill in sorrys in int and rat orderings 2015-05-29 14:11:51 +10:00
Rob Lewis
6dfcc4610b feat(data): update orderings on int and nat to conform to new algebraic hierarchy 2015-05-29 14:11:51 +10:00
Rob Lewis
4b67cd1f97 feat(library/algebra): update algebraic hierarchy to be more constructive 2015-05-29 14:11:50 +10:00
Leonardo de Moura
00232e70d6 feat(hott,library): auxiliary theorems for simplifier 2015-05-27 16:35:56 -07:00
Leonardo de Moura
85409a59d3 feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants 
closes #511
 2015-05-27 16:32:43 -07:00
Leonardo de Moura
dc6411b903 feat(library/inductive_unifier_plugin): restrict rule that was generating non-terminating behavior 
see issue #632
 2015-05-27 14:41:12 -07:00
Leonardo de Moura
5da4922397 feat(library/data/list/perm): cleanup proofs 
refl and symm were refering to the setoid.refl and setoid.symm.
Moreover, they were producing harder elaboration problems
 2015-05-27 12:30:56 -07:00
Leonardo de Moura
47e5633498 feat(frontends/lean/calc_proof_elaborator): avoid unnecessary unfolding in the calc tactic 2015-05-27 12:07:39 -07:00
Floris van Doorn
8056f326d7 feat(reserved_notation): make is_typeof parsing-only, add ^ to HoTT 2015-05-26 21:37:01 -07:00
Floris van Doorn
0c7e16e017 feat(library.data.int.basic): move theorems about successor and predecessor from HoTT to standard library 2015-05-26 21:37:01 -07:00
Leonardo de Moura
7f0951b8e7 feat(library/tactic): improve assumption tactic performance 2015-05-25 20:22:37 -07:00
Rob Lewis
393cefcf97 feat(library/data/real): define real numbers, prove they form a commutative ring 2015-05-26 12:05:53 +10:00
Rob Lewis
681f431d4b feat(library/data/rat): make rat subtraction reducible, fix migration of min/max 2015-05-26 11:52:34 +10:00
Rob Lewis
eb537daa1c feat(library/algebra): add min/max to ordered algebraic structures 2015-05-26 11:45:09 +10:00
Leonardo de Moura
4152ebfa23 refactor(library/data/nat): use new tactics 2015-05-25 18:14:52 -07:00
Jeremy Avigad
39129f112b refactor(library/*): do various renamings 2015-05-25 16:50:42 -07:00
Jeremy Avigad
a64c0ea845 feat/refactor(library/data/{int,rat}/*): improve casting from nat to int to rat 2015-05-25 16:50:42 -07:00
Jeremy Avigad
4ed9e46532 refactor(library/data/int/*): use better direction for of_nat theorems 2015-05-25 16:50:42 -07:00
Jeremy Avigad
fdc89cd285 refactor(library/algebra/order.lean,library/{data,algebra}/*): use better names for order theorems 2015-05-25 16:50:42 -07:00
Jeremy Avigad
81c0ef8c89 refactor(library/data/nat/*): cleanup, additions, renaming 2015-05-25 16:50:42 -07:00
Jeremy Avigad
7c92161e49 refactor(library/data/finset/basic.lean): change order of arguments to induction tactic 2015-05-25 16:50:42 -07:00
Jeremy Avigad
716da2488b fix(hott/*.md,library/*.md): use the word 'file' instead of 'module' 2015-05-25 16:50:42 -07:00
Leonardo de Moura
6db08c5519 test(library): test new tactics in the standard library 2015-05-25 16:48:33 -07:00
Leonardo de Moura
d0987eb3ac feat(library/tactic): add 'subtvars' tactic 2015-05-25 16:36:44 -07:00
Leonardo de Moura
7e875c8d85 refactor(library): simplify theorems using improved tactics 2015-05-25 10:43:28 -07:00
Leonardo de Moura
88975927e6 fix(library/tactic/relation_tactics): beta-reduce goal before trying to extract head symbol 2015-05-24 18:56:35 -07:00
Leonardo de Moura
c453bb52a9 feat(library/data/stream): add notation and commonly used definitions 2015-05-24 16:53:58 -07:00
Leonardo de Moura
880027ea0e feat(library/data/stream): define stream mem predicate and prove basic theorems 2015-05-24 15:47:33 -07:00
Leonardo de Moura
607a5fbb86 feat(library/data/stream): define cycle, inits, tails for streams and prove basic theorems 2015-05-24 13:42:51 -07:00
Leonardo de Moura
3181471024 feat(library/data/list/basic): add nth_eq_some aux theorem 2015-05-24 10:10:23 -07:00
Leonardo de Moura
32a2425e02 feat(library/data/stream): prove take lemma for infinite streams 2015-05-23 23:01:54 -07:00
Leonardo de Moura
75901157a1 feat(library/data/stream): add more declarations and examples demonstrating how to use eq_of_bisim 2015-05-23 22:03:17 -07:00
Leonardo de Moura
d987d6cc84 feat(library/data/stream): simplify corecursion proofs, define interleave operation by corecursion, add one example of proof by bisimulation 2015-05-23 16:00:08 -07:00
Leonardo de Moura
8685e8ad7e feat(library/data/stream): define corec for infinite streams 2015-05-23 14:32:52 -07:00
Leonardo de Moura
dd4dd154ec feat(library/data/stream): add bisimulation for streams 2015-05-23 12:07:27 -07:00
Jeremy Avigad
8bebd104ff refactor(library/*): remove 'Module:' lines 2015-05-23 20:52:23 +10:00
Jeremy Avigad
db7bdce451 refactor(logic/funext.lean, algebra/function.lean): delete logic/funext, merge into algebra/function 2015-05-23 16:16:36 +10:00
Jeremy Avigad
f65a49b2c3 feat/fix(library/data/nat,int): add power to int, add trans attributes, power notation 2015-05-23 15:38:42 +10:00
Jeremy Avigad
a662f925cb refactor(library/data/quotient.lean): improve comments 2015-05-23 14:21:16 +10:00
Jeremy Avigad
d33c91d7b9 fix({hott,library}/algebra/*): fix names 2015-05-23 14:05:06 +10:00
Jeremy Avigad
4bc93b59e3 feat(library/data/rat/{basic,order}.lean): add property of of_int 2015-05-23 12:34:07 +10:00
Jeremy Avigad
59c1801921 refactor(library/data/{list,set,finset}/basic.lean): make subset reserved notation 2015-05-23 12:34:07 +10:00
Leonardo de Moura
fe32b9fa7f feat(library/data/stream): add infinite streams 2015-05-22 18:08:11 -07:00
Leonardo de Moura
1665ee39e8 feat(library/data/finset/card): test 'induction' tactic at finset 2015-05-19 15:56:51 -07:00
Leonardo de Moura
3e87f09d78 feat(library/tactic/induction_tactic): add support for user-defined recursors that contain parameters that should be synthesized by type class resolution 2015-05-19 15:33:46 -07:00
Leonardo de Moura
e1c2340db2 fix(frontends/lean): consistent behavior for protected declarations 
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608

closes #609
 2015-05-18 22:35:18 -07:00
Floris van Doorn
2144036cdb feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups 
Also many minor fixes at various places
 2015-05-18 15:59:55 -07:00
Leonardo de Moura
19361f0196 feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables 
see discussion at #604
 2015-05-18 15:45:23 -07:00
Leonardo de Moura
b1ece388a6 feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation 2015-05-18 09:25:07 -07:00
Jeremy Avigad
566acf4b31 feat(library/data/finset/card.lean): add card_Union_of_disjoint and other theorems 2015-05-17 19:06:10 +10:00