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

385 commits

Author SHA1 Message Date
Jakob von Raumer
7dbd7b31f6 Added substitution lemma for equivalence calculations 2014-11-06 19:22:57 -05:00
Jakob von Raumer
fa9cbb1f6a chore(library/hott) adapted univalence axiom to suit notation in book and def in Coq. 2014-11-06 19:22:57 -05:00
Jakob von Raumer
d842be9c52 feat(library/hott) add univalence axiom 2014-11-06 19:22:57 -05:00
Jakob von Raumer
28d1c6c5e4 chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it 2014-11-06 19:22:57 -05:00
Jakob von Raumer
9ad75108a3 chore(library/hott) clean up file and add class inference 2014-11-06 15:57:30 -08:00
Jakob von Raumer
1f5be44f51 chore(library/hott) clean up Equiv namespace 2014-11-06 15:57:30 -08:00
Jakob von Raumer
8e1949e9aa feat(library/hott) add calc environment for equivalences 2014-11-06 15:57:29 -08:00
Jakob von Raumer
c50db9899d feat(library/hott) add thm: to give a section of a fibration it suffices to provide it for the image of an equivalence 2014-11-06 15:57:29 -08:00
Leonardo de Moura
781f709bb4 feat(library/logic): import wf.lean in logic/default.lean 
We will use well-founded recursion in the definitional package
 2014-11-06 15:03:13 -08:00
Leonardo de Moura
194247f75b refactor(library/logic/wf): minimize dependencies 2014-11-06 14:59:03 -08:00
Leonardo de Moura
b177c84b06 feat(library/logic): add well-founded recursion 
It also removes the old well-founded induction theorem based on
classical principles
 2014-11-06 14:49:53 -08:00
Leonardo de Moura
d306c42a1f refactor(library/logic): cleanup some of the proofs in cast.lean, remove piext axiom 
Remark: the main motivation for piext was Lean 0.1 simplifier.
We are using a different approach in Lean 0.2.
The axiom is not needed anymore.
It is also not used in any part of the standard library
 2014-11-05 16:43:31 -08:00
Jakob von Raumer
09b533a965 fix(library/hott) rename IsEquiv.ap to IsEquiv.ap_closed to avoid name clashes 2014-11-05 15:14:14 -08:00
Jakob von Raumer
02abc5c2ad chore(library/hott) fixed the copyright in equiv_precomp.lean 2014-11-05 15:14:14 -08:00
Jakob von Raumer
807224f3c1 chore(library/hott) cleaned up the proof a bit 2014-11-05 15:14:14 -08:00
Jakob von Raumer
2712b9b18f feat(library/hott) add theorem: if f is an equivalence, so is ap f 2014-11-05 15:14:14 -08:00
Jakob von Raumer
588ad210a2 feat(library/hott) add theorem: assuming function extensionality, precomposing and postcomposing of equivalences is an equivalence 2014-11-04 18:47:34 -08:00
Jakob von Raumer
efa33c5b52 chore(library/hott) move theorem about precomposition to its own file 2014-11-04 18:47:34 -08:00
Jakob von Raumer
0ed046ed80 fix(library/hott) fix funext.lean by making funext an instance 2014-11-04 18:47:34 -08:00
Leonardo de Moura
60eac0195d feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures 2014-11-04 09:10:25 -08:00
Leonardo de Moura
795f664964 fix(library/hott/funext): compilation error 2014-11-04 06:53:21 -08:00
Jakob von Raumer
261f8a014a feat(library/hott) use class inference for IsEquiv 2014-11-04 06:49:42 -08:00
Jakob von Raumer
479eabb416 feat(library/hott) add: if precompositions with f are equivalences, then f is 2014-11-04 06:49:42 -08:00
Leonardo de Moura
b24165dc7b feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on' 2014-11-03 23:06:33 -08:00
Leonardo de Moura
d2b5af237e refactor(library): use new 'structure' command to define prod and sigma 2014-11-03 18:57:55 -08:00
Floris van Doorn
d8a616fa70 refactor(library): major changes in the library 
I made some major changes in the library. I wanted to wait with pushing
until I had finished the formalization of the slice functor, but for
some reason that is very hard to formalize, requiring a lot of casts and
manipulation of casts. So I've not finished that yet.

Changes:

- in multiple files make more use of variables

- move dependent congr_arg theorems to logic.cast and proof them using heq (which doesn't involve nested inductions and fewer casts).

- prove some more theorems involving heq, e.g. hcongr_arg3 (which do not
  require piext)

- in theorems where casts are used in the statement use eq.rec_on
  instead of eq.drec_on

- in category split basic into basic, functor and natural_transformation

- change the definition of functor to use fully bundled
categories. @avigad: this means that the file semisimplicial.lean will
also need changes (but I'm quite sure nothing major).  You want to
define the fully bundled category Delta, and use only fully bundled
categories (type and ᵒᵖ are notations for the fully bundled
Type_category and Opposite if you open namespace category.ops). If you
want I can make the changes.

- lots of minor changes
 2014-11-03 18:45:12 -08:00
Leonardo de Moura
ae9d11c9c4 refactor(library/data): rename prod_ext and dpair_ext to prod.eta and sigma.eta 
Reason: they will be generated automatically by definitional package.
 2014-11-03 08:29:05 -08:00
Leonardo de Moura
4bdee07af2 refactor(library/algebra/category/basic): use calc assistant 2014-10-31 09:49:45 -07:00
Leonardo de Moura
8d3e9fdc20 refactor(library/data/nat/basic): remove unnecessary {} 2014-10-31 09:49:45 -07:00
Leonardo de Moura
8a4d4409cd feat(frontends/lean/calc_proof_elaborator): add '{...⁻¹}' if needed in calc proofs, closes #268 
This commit also simplifies library/data/nat/basic.lean
 2014-10-31 01:02:49 -07:00
Leonardo de Moura
5f23179388 refactor(library/data/nat): remove unnecessary ! and eq.symm 
The calc command automatically adds them now.
 2014-10-30 23:28:35 -07:00
Leonardo de Moura
591e566472 feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator 
This is part of #268
 2014-10-30 23:24:09 -07:00
Leonardo de Moura
09c6c05e26 chore(library/data/quotient): replace 'let' with 'have' and cleanup 2014-10-30 18:44:05 -07:00
Leonardo de Moura
407e35692b feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved 
Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268.

Remark: we don't wrap the proof if it is of the form

   - `by tactic`
   - `begin tactic-seq end`
   - `{ expr }`
 2014-10-30 18:33:47 -07:00
Leonardo de Moura
9547e2d077 feat(library/tactic): add rotate_left/rotate_right tactics, closes #278 2014-10-29 19:13:55 -07:00
Leonardo de Moura
e22eb3543c feat(library/tactic): add whnf tactic, closes #270 2014-10-28 23:18:49 -07:00
Leonardo de Moura
ea739100b3 fix(library/unifier): broken optimization in the unifier 
See new comments and tests for details.
 2014-10-28 16:09:41 -07:00
Leonardo de Moura
777aa63660 fix(kernel/inductive): relax eliminator generation rules for empty types 
This commit also removes the workaround false.rec_type. It is not needed anymore
 2014-10-28 10:31:00 -07:00
Leonardo de Moura
aafdbf57f0 fix(library/data/unit): missing file 2014-10-25 18:34:41 -07:00
Leonardo de Moura
c7f6a6b94e feat(library/definitional/cases_on): automatically add 'cases_on' 2014-10-25 17:22:02 -07:00
Leonardo de Moura
758a17ab23 refactor(library/data/unit): break unit.lean into smaller pieces 
The unit datatype is used by automation.

We want to be able to access its declaration without having to access
all dependencies (e.g., decidable, subsingleton, inhabited, ...).

This is *not* an optimization, but a way to make sure we can "import" unit
before we import other declarations.
 2014-10-25 14:57:33 -07:00
Jakob von Raumer
b575c972bd feat(library/hott) add the proof that the inverse of an equivalence is an equivalence 
This is done by changing the order of theorems and using the adjointification.
 2014-10-25 14:20:47 -07:00
Jakob von Raumer
e7aa5f65e7 fix(library/hott) close gaps and clean up adjointification proof 2014-10-25 14:16:24 -07:00
Jakob von Raumer
16a0e970f7 feat(library/hott) add adjointification proof up to two gaps 2014-10-25 14:16:24 -07:00
Leonardo de Moura
354b50a1f5 refactor(library/data/unit): make unit universe polymorphic 
Motivation: we need it for "padding".
Example 1: defining a n-ary tuple type.
Example 2: defining cases-on for mutually recursive datatypes
 2014-10-25 13:55:03 -07:00
Leonardo de Moura
cdcde661ef feat(library/definitional/induction_on): automatically add 'induction_on' 2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8 feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes 2014-10-25 13:08:59 -07:00
Soonho Kong
51125c1577 fix(library/data/quotient/default.lean): remove classical 2014-10-24 07:41:29 -07:00
Leonardo de Moura
79d0347721 feat(library/tactic): add generalize tactic, closes #34 
Remark: the intros tactic has been added in a different commit: 7d0100a340
 2014-10-23 22:40:15 -07:00
Leonardo de Moura
e750c9b67a feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode 2014-10-23 13:18:30 -07:00