From e27aae81f7efcf34b3631098aa2fe64584397ede Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Fri, 11 Aug 2017 18:06:23 -0400 Subject: [PATCH] introduce top level dir `order`: move `algebra.order` and content of `algebra.lattice` --- algebra/lattice/README.md | 20 ------------------- algebra/lattice/default.lean | 3 --- data/set/lattice.lean | 2 +- algebra/order.lean => order/basic.lean | 0 .../lattice => order}/boolean_algebra.lean | 2 +- .../lattice => order}/bounded_lattice.lean | 2 +- .../complete_boolean_algebra.lean | 2 +- .../lattice => order}/complete_lattice.lean | 2 +- order/default.lean | 3 +++ {algebra/lattice => order}/filter.lean | 2 +- {algebra/lattice => order}/fixed_points.lean | 2 +- .../lattice/basic.lean => order/lattice.lean | 2 +- {algebra/lattice => order}/zorn.lean | 0 tactic/converter/binders.lean | 2 +- topology/real.lean | 2 +- topology/topological_space.lean | 2 +- topology/uniform_space.lean | 2 +- 17 files changed, 15 insertions(+), 35 deletions(-) delete mode 100644 algebra/lattice/README.md delete mode 100644 algebra/lattice/default.lean rename algebra/order.lean => order/basic.lean (100%) rename {algebra/lattice => order}/boolean_algebra.lean (99%) rename {algebra/lattice => order}/bounded_lattice.lean (99%) rename {algebra/lattice => order}/complete_boolean_algebra.lean (96%) rename {algebra/lattice => order}/complete_lattice.lean (99%) create mode 100644 order/default.lean rename {algebra/lattice => order}/filter.lean (99%) rename {algebra/lattice => order}/fixed_points.lean (99%) rename algebra/lattice/basic.lean => order/lattice.lean (99%) rename {algebra/lattice => order}/zorn.lean (100%) diff --git a/algebra/lattice/README.md b/algebra/lattice/README.md deleted file mode 100644 index e5621adc9c888..0000000000000 --- a/algebra/lattice/README.md +++ /dev/null @@ -1,20 +0,0 @@ - -# Lattice theory - -Most here is translated from Isabelle 2016-1. - -The idea is to keep the theory constructive and only when instantiating `Prop` with -`boolean_algebra` and `complete_boolean_algebra` should be `classical` needed. - -Questions / Notes: - - * is the namespace `lattice` really needed? - Some names are overlapping like `neg_neg` for `boolean_algebra` and `group`. - - * should we keep the names `supr` and `infi`, what's with `Sup` and `Inf`? - At least `Sup` anf `Inf` violate the namespace conventions. - - * should we introduce syntax for `Inf` and `Sup`? - - * maybe introduce `heyting_algebra` and `complete_heyting_algebra` - diff --git a/algebra/lattice/default.lean b/algebra/lattice/default.lean deleted file mode 100644 index d2b179347252d..0000000000000 --- a/algebra/lattice/default.lean +++ /dev/null @@ -1,3 +0,0 @@ -import algebra.lattice.basic algebra.lattice.bounded_lattice - algebra.lattice.boolean_algebra algebra.lattice.complete_lattice - diff --git a/data/set/lattice.lean b/data/set/lattice.lean index 8bd4756058f44..deb01bb08ec81 100644 --- a/data/set/lattice.lean +++ b/data/set/lattice.lean @@ -6,7 +6,7 @@ Authors Jeremy Avigad, Leonardo de Moura, Johannes Hölzl -- QUESTION: can make the first argument in ∀ x ∈ a, ... implicit? -/ import logic.basic data.set.basic -import algebra.lattice algebra.order algebra.lattice.complete_boolean_algebra category.basic +import order.complete_boolean_algebra category.basic import tactic.finish open function tactic set lattice auto diff --git a/algebra/order.lean b/order/basic.lean similarity index 100% rename from algebra/order.lean rename to order/basic.lean diff --git a/algebra/lattice/boolean_algebra.lean b/order/boolean_algebra.lean similarity index 99% rename from algebra/lattice/boolean_algebra.lean rename to order/boolean_algebra.lean index cca9d8c9cbdab..c573846789e52 100644 --- a/algebra/lattice/boolean_algebra.lean +++ b/order/boolean_algebra.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl Type class hierarchy for Boolean algebras. -/ -import algebra.lattice.bounded_lattice +import order.bounded_lattice set_option old_structure_cmd true diff --git a/algebra/lattice/bounded_lattice.lean b/order/bounded_lattice.lean similarity index 99% rename from algebra/lattice/bounded_lattice.lean rename to order/bounded_lattice.lean index 9ed52b8ebb886..68f83050b83f2 100644 --- a/algebra/lattice/bounded_lattice.lean +++ b/order/bounded_lattice.lean @@ -8,7 +8,7 @@ Defines bounded lattice type class hierarchy. Includes the Prop and fun instances. -/ -import algebra.lattice.basic +import order.lattice set_option old_structure_cmd true diff --git a/algebra/lattice/complete_boolean_algebra.lean b/order/complete_boolean_algebra.lean similarity index 96% rename from algebra/lattice/complete_boolean_algebra.lean rename to order/complete_boolean_algebra.lean index 0bc329c349584..bedb4cba46065 100644 --- a/algebra/lattice/complete_boolean_algebra.lean +++ b/order/complete_boolean_algebra.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl Theory of complete Boolean algebras. -/ -import algebra.lattice.complete_lattice algebra.lattice.boolean_algebra data.set.basic +import order.complete_lattice order.boolean_algebra data.set.basic set_option old_structure_cmd true diff --git a/algebra/lattice/complete_lattice.lean b/order/complete_lattice.lean similarity index 99% rename from algebra/lattice/complete_lattice.lean rename to order/complete_lattice.lean index 20b8720aad461..ea5908d9373e4 100644 --- a/algebra/lattice/complete_lattice.lean +++ b/order/complete_lattice.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl Theory of complete lattices. -/ -import algebra.lattice.bounded_lattice data.set.basic +import order.bounded_lattice data.set.basic set_option old_structure_cmd true diff --git a/order/default.lean b/order/default.lean new file mode 100644 index 0000000000000..3cac438c4afe8 --- /dev/null +++ b/order/default.lean @@ -0,0 +1,3 @@ +import order.basic order.lattice order.bounded_lattice + order.boolean_algebra order.complete_lattice + diff --git a/algebra/lattice/filter.lean b/order/filter.lean similarity index 99% rename from algebra/lattice/filter.lean rename to order/filter.lean index 1299be2903b98..38985d993cde5 100644 --- a/algebra/lattice/filter.lean +++ b/order/filter.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl Theory of filters on sets. -/ -import algebra.lattice.complete_lattice data.set algebra.lattice.zorn +import order.complete_lattice data.set order.zorn open lattice set universes u v w x y diff --git a/algebra/lattice/fixed_points.lean b/order/fixed_points.lean similarity index 99% rename from algebra/lattice/fixed_points.lean rename to order/fixed_points.lean index 7f0ac3fc91e7c..5cf91d56f5237 100644 --- a/algebra/lattice/fixed_points.lean +++ b/order/fixed_points.lean @@ -6,7 +6,7 @@ Authors: Johannes Hölzl Fixed point construction on complete lattices. -/ -import algebra.lattice.complete_lattice +import order.complete_lattice universes u v w variables {α : Type u} {β : Type v} {γ : Type w} diff --git a/algebra/lattice/basic.lean b/order/lattice.lean similarity index 99% rename from algebra/lattice/basic.lean rename to order/lattice.lean index 897959c2878e3..4e507375293b2 100644 --- a/algebra/lattice/basic.lean +++ b/order/lattice.lean @@ -6,7 +6,7 @@ Authors: Johannes Hölzl Defines the inf/sup (semi)-lattice with optionally top/bot type class hierarchy. -/ -import algebra.order tactic.finish +import order.basic tactic.finish open auto set_option old_structure_cmd true diff --git a/algebra/lattice/zorn.lean b/order/zorn.lean similarity index 100% rename from algebra/lattice/zorn.lean rename to order/zorn.lean diff --git a/tactic/converter/binders.lean b/tactic/converter/binders.lean index f901af154842e..f0c00db062f2b 100644 --- a/tactic/converter/binders.lean +++ b/tactic/converter/binders.lean @@ -5,7 +5,7 @@ Authors: Johannes Hölzl Binder elimination -/ -import algebra.lattice tactic.converter.old_conv +import order tactic.converter.old_conv namespace old_conv open tactic monad diff --git a/topology/real.lean b/topology/real.lean index d99daff091803..14510a07cd407 100644 --- a/topology/real.lean +++ b/topology/real.lean @@ -22,7 +22,7 @@ generalizations: -/ -import topology.uniform_space data.rat algebra.field algebra.order +import topology.uniform_space data.rat algebra.field noncomputable theory open classical set lattice filter local attribute [instance] decidable_inhabited prop_decidable diff --git a/topology/topological_space.lean b/topology/topological_space.lean index 736bf75cad03c..87ab14995d198 100644 --- a/topology/topological_space.lean +++ b/topology/topological_space.lean @@ -10,7 +10,7 @@ Parts of the formalization is based on the books: I. M. James: Topologies and Uniformities A major difference is that this formalization is heavily based on the filter library. -/ -import algebra.lattice.filter +import order.filter open set filter lattice classical local attribute [instance] decidable_inhabited prop_decidable diff --git a/topology/uniform_space.lean b/topology/uniform_space.lean index 4cae19a7d5a47..964a4a791781f 100644 --- a/topology/uniform_space.lean +++ b/topology/uniform_space.lean @@ -27,7 +27,7 @@ The formalization is mostly based on the books: I. M. James: Topologies and Uniformities A major difference is that this formalization is heavily based on the filter library. -/ -import algebra.lattice.filter topology.topological_space topology.continuity +import order.filter topology.topological_space topology.continuity open set lattice filter classical local attribute [instance] decidable_inhabited prop_decidable