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

8555 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
797905b803 feat(library/theories/topology/order_topology): add order_topology, from Jacob Gross 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
03cd2c0013 feat/refactor(library/algebra/interval): use i for infinite, add some 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
Floris van Doorn
6cdbc0f79f feat(pointed/equiv): add more theorems 
The theorems are mostly about the interaction between pointed equivalences and pointed homotopies
Some of these theorems were missing for (unpointed) equivalences, so I also added them there
 2016-02-22 11:15:39 -08:00
Floris van Doorn
eea2a1ac91 feat(hott): add some more abstracts 2016-02-22 11:15:39 -08:00
Floris van Doorn
b2181497fd fix(tests): fix delta_issue2 2016-02-22 11:15:38 -08:00
Floris van Doorn
facd94a1b4 feat(hott): various changes 
more about pointed truncated types, including pointed sets.
also increase the priority of some basic instances that nat/num/pos_num/trunc_index have 0, 1 and + (in both libraries)
also move the notation + for sum into the namespace sum, to (sometimes) avoid overloading with add
 2016-02-22 11:15:38 -08:00
Floris van Doorn
087c44d614 style(hott): rename instances of pType using pfoo instead of Foo 
For example, the pointed suspension operation was called Susp before this commit, but now is called psusp
 2016-02-22 11:15:38 -08:00
Floris van Doorn
c64e5a114c feat(circle): add missing facts that the circle is 1-truncated and 0-connected 2016-02-22 11:15:38 -08:00
Floris van Doorn
bac6d99cc7 style(hott): rename Pointed to pType 
also rename sigma_equiv_sigma_id to sigma_equiv_sigma_right and similarly for pi
 2016-02-22 11:15:38 -08:00
Floris van Doorn
43cf2ad23d style(hott): replace all other occurrences of hprop/hset 
They are replaced by either Prop/Set or prop/set
 2016-02-22 11:15:38 -08:00
Floris van Doorn
4e2cc66061 style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
Floris van Doorn
816237315c feat(hott): various additions, especially for pointed maps/homotopies/equivalences 2016-02-22 11:15:38 -08:00
Floris van Doorn
ecc141779a feat(init.path): update init.path to use tactics, also some additions 
Now the file hardly uses eq.rec explicitly anymore.
Also add the fact that horizontal and vertical inverses of paths are equal
Make one more argument explicit in eq.cancel_left and eq.cancel_right (to make it nicer to write 'apply cancel_right p')
 2016-02-22 11:15:38 -08:00
Floris van Doorn
7f09ba328e feat(hott): small changes 2016-02-22 11:15:38 -08:00
Floris van Doorn
78092af27f feat(hott): add some attributes 2016-02-22 11:15:38 -08:00
Floris van Doorn
cd74b6bff0 fix(hott): abstract some equivalence proofs 
Note: this is important. I proved a quite complicated equivalence with calc, by chaining these
equivalences. Now if I want to know the underlying function of this composite equivalence, I have to
unfold all these instances. Without the abstracts, this took 14 seconds, and afterwards, it took 2
seconds.
 2016-02-22 11:15:38 -08:00
Jacob Gross
db8ed5dd08 feat (library/theories/topology/basic) : add separation theorems 
add T0, T1, T2 separation theorems and add closed singleton theorem for T1 spaces
 2016-02-22 11:11:54 -08:00
Sean Leather
7852524370 fix(library/data/list/sorted): incorrect name 2016-02-22 11:06:39 -08:00
Daniel Selsam
859a3d35ea feat(library/defeq_simplifier): no need to reverse args 2016-02-22 11:01:36 -08:00
Daniel Selsam
d521063dfb feat(library/defeq_simplifier): new simplifier that uses only definitional equalities 2016-02-22 11:01:36 -08:00
Leonardo de Moura
20f70035dd fix(frontends/lean/util): fixes #1007 2016-02-22 10:54:55 -08:00
Soonho Kong
994815bc77 fix(bin/linja.in): roll back d8fb6f5 
The previous fix d8fb6f5 creates a problem in Linux platform.

Related issue: #986
 2016-02-15 14:31:15 -05:00
Soonho Kong
ca1901bb2c feat(emacs/lean-project.el): ask 'project type' in lean-project-create 
close #999
 2016-02-12 22:02:24 -05:00
Rob Lewis
b047c9c037 refactor(theories/{analysis, topology}): clean up proofs connecting open balls and open sets 2016-02-12 11:50:11 -08:00
Rob Lewis
68bc41b5fe feat(data/set): add missing set theorems 2016-02-12 11:50:11 -08:00
Rob Lewis
4a41e78124 fix(theories/analysis): make variables implicit in continuous_at_intro 2016-02-12 11:50:10 -08:00
Rob Lewis
2c56a2c48b feat(theories/{analysis, topology}): show eps-delta and topological continuity coincide on metric spaces 2016-02-12 11:50:10 -08:00
Rob Lewis
eb05741ce6 feat(data/set): add missing set membership theorems 2016-02-12 11:50:10 -08:00
Rob Lewis
685049988c feat(theories/analysis): define metric topology 2016-02-12 11:50:10 -08:00
Rob Lewis
b8d86ffe48 feat(theories/topology): add theorem for proving sets open 2016-02-12 11:50:10 -08:00
Daniel Selsam
bb4b8da582 feat(library/unification_hint): basic handling of user-supplied unification hints 2016-02-12 11:48:51 -08:00
Soonho Kong
d8fb6f5082 fix(bin/linja.in): wrap args.cache to avoid problems handling fullpath with space 
related issue: #986
 2016-02-12 13:25:23 -05:00
Leonardo de Moura
632d4fae36 chore(library): rename local_context to old_local_context 2016-02-11 18:15:16 -08:00
Leonardo de Moura
74192b0cb8 chore(library): remove dead code 2016-02-11 18:08:44 -08:00
Leonardo de Moura
c9e9fee76a refactor(*): remove name_generator and use simpler mk_fresh_name 2016-02-11 18:05:57 -08:00
Leonardo de Moura
9cbda49297 chore(frontends/lean): remove script blocks 2016-02-11 17:26:44 -08:00
Leonardo de Moura
f67181baf3 chore(*): remove support for Lua 2016-02-11 17:17:55 -08:00
Daniel Selsam
3de4ec1a6c fix(library/blast/imp_extension): do not use the name 'assert' 
Closes #994
 2016-02-10 14:11:17 -08:00
Floris van Doorn
42b78962f9 feat(init/wf): simplify definition acc.drec 2016-02-09 10:03:48 -08:00
Floris van Doorn
e14d4a4c0c feat(init/wf): port from standard library to HoTT library 
After this commit we need some more advanced theorems in init/wf, notably function extenstionality.
For this reason I had to refactor the init folder a little bit.
To keep the init folders in both libraries similar, I did the same refactorization in the standard library, even though that was not required for the standard library
 2016-02-09 10:03:48 -08:00
Jakob von Raumer
c0abcc7722 chore(hott): fix signature of previous lemma 2016-02-09 09:59:03 -08:00
Jakob von Raumer
3c7536cff8 chore(hott): clean up cancellability proof a bit 2016-02-09 09:58:57 -08:00
Jakob von Raumer
4d6c516c01 feat(hott): add lemma: equivalent fin sets come from equal numbers, sums with fin sets are cancellable 2016-02-09 09:58:52 -08:00
Jakob von Raumer
4edb6d7765 feat(hott): finish cancelling law for sums with unit 2016-02-09 09:58:31 -08:00