From 5eedca08ea50c0ac1ac92bd73ed9cc17a95fbd73 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Mon, 25 Aug 2014 09:11:46 -0700 Subject: [PATCH] refactor(library): set up and document standard/classical/hott imports --- README.md | 2 +- library/classical.lean | 5 +++++ library/hott/default.lean | 10 ++++++++++ library/hott/hott.md | 23 ++++++++++++----------- library/library.md | 35 +++++++++++++++++++++++++++++++++++ library/standard.lean | 10 ++++++---- library/standard.md | 12 ------------ 7 files changed, 69 insertions(+), 28 deletions(-) create mode 100644 library/classical.lean create mode 100644 library/hott/default.lean create mode 100644 library/library.md delete mode 100644 library/standard.md diff --git a/README.md b/README.md index ffaa70dbe4..d8129cba2c 100644 --- a/README.md +++ b/README.md @@ -21,7 +21,7 @@ About - [To Do list](doc/todo.md) - [Authors](doc/authors.md) - [Tutorial](doc/lean/tutorial.org) -- [Standard Library](library/standard.md) +- [Library](library/library.md) Requirements ------------ diff --git a/library/classical.lean b/library/classical.lean new file mode 100644 index 0000000000..464f744fc4 --- /dev/null +++ b/library/classical.lean @@ -0,0 +1,5 @@ +-- Copyright (c) 2014 Jeremy Avigad. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Jeremy Avigad + +import standard logic.axioms \ No newline at end of file diff --git a/library/hott/default.lean b/library/hott/default.lean new file mode 100644 index 0000000000..4e38ab29c5 --- /dev/null +++ b/library/hott/default.lean @@ -0,0 +1,10 @@ +-- Copyright (c) 2014 Jeremy Avigad. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Author: Jeremy Avigad + +-- hott.default +-- ============ + +-- A library for homotopy type theory + +import ..standard .path .equiv .trunc .fibrant \ No newline at end of file diff --git a/library/hott/hott.md b/library/hott/hott.md index 2f8c21ef6c..55a1b8dd5e 100644 --- a/library/hott/hott.md +++ b/library/hott/hott.md @@ -1,18 +1,19 @@ standard.hott ============= -A library for Homotopy Type Theory, which avoid the use of prop. Many -standard types are imported from `data`, but then theorems -are proved about them using predicativee versions of the logical -operations. For example, we use the path type, products, sums, sigmas, -and the empty type, rather than equality, and, or, exists, and -false. These operations take values in Type rather than Prop. +A library for homotopy type theory. HoTT is consistent with the +existence of an imprediative, proof irrelevant `Prop`, but favors +"proof relevant," predicative versions of the usual logical +constructions. For example, we use the path type, products, sums, +sigmas, and the empty type, rather than equality, and, or, exists, and +false. These operations take values in `Type` rather than `Prop`. -We view Homotopy Theory Theory as compatible with the axiomatic -framework of Lean, simply ignoring the impredicative, proof irrelevant -Prop. This is o.k. as long as we do not import additional axioms like -propositional extensionality or Hilbert choice, which are incompatible -with HoTT. +Note that the univalence axiom is inconsistent with classical axioms +such as propositional extensionality or Hilbert choice, and we have to +ensure that the library does not import these. + +The modules imported by the command `import hott` are found in the +file [default](default.lean). * [path](path.lean) : the path type and operations on paths * [equiv](equiv.lean) : equivalence of types diff --git a/library/library.md b/library/library.md new file mode 100644 index 0000000000..1be3cf41d6 --- /dev/null +++ b/library/library.md @@ -0,0 +1,35 @@ +The Lean Library +================ + +The Lean library is contained in the following modules and directories: + +* [general_notation](general_notation.lean) : commonly shared notation +* [logic](logic/logic.md) : logical constructs and axioms +* [data](data/data.md) : concrete datatypes and type constructors +* [struc](struc/struc.md) : axiomatic structures +* [hott](hott/hott.md) : homotopy type theory +* [tools](tools/tools.md) : additional tools + +Modules can be loaded individually, but they are also be loaded by importing the +following packages: + +* [standard](standard.lean) : constructive logic and datatypes +* [classical](classical.lean) : classical mathematics +* [hott](hott/default.lean) : homotopy type theory + +Lean's default logical framework is a version of the Calculus of Constructions with: + +* an impredicative, proof-irrelevant type `Prop` of propositions +* a non-cumulative hierarchy of universes, `Type 1`, `Type 2`, ... above `Prop` +* inductively defined types + +The `standard` library does not rely on any axioms beyond this framework, and is +hence constructive. It includes theories of the natural numbers, integers, +lists, and so on. + +The `classical` library imports the law of the excluded middle, choice functions, +and propositional extensionality. See `logic/axioms` for details. + +The `hott` library is compatible with the standard library, but favors "proof +relevant" versions of the logical connectives, based on `Type` rather than +`Prop`. See `hott` for details. \ No newline at end of file diff --git a/library/standard.lean b/library/standard.lean index 692eaa9fc6..6e28175c65 100644 --- a/library/standard.lean +++ b/library/standard.lean @@ -1,8 +1,10 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Leonardo de Moura +-- Authors: Leonardo de Moura, Jeremy Avigad --- changing to this breaks some tests: --- import logic data tools.tactic +-- standard +-- ======== -import logic tools.tactic data.num data.string data.prod logic.connectives.cast \ No newline at end of file +-- The constructive core of Lean's library. + +import logic data tools.tactic diff --git a/library/standard.md b/library/standard.md deleted file mode 100644 index c0f4b38480..0000000000 --- a/library/standard.md +++ /dev/null @@ -1,12 +0,0 @@ -standard -======== - -The Lean standard library. By default, `import standard` does not -import any axioms. See logic.axioms. - -* [general_notation](general_notation.lean) : notation shared by all libraries -* [logic](logic/logic.md) : logical constructs and axioms -* [data](data/data.md) : various datatypes -* [struc](struc/struc.md) : axiomatic structures -* [hott](hott/hott.md) : homotopy type theory -* [tools](tools/tools.md) : various additional tools \ No newline at end of file