refactor(library/logic): rename connectives -> core, basic -> connectives

library/data/bool.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.basic logic.classes.decidable logic.classes.inhabited
+import logic.core.connectives logic.classes.decidable logic.classes.inhabited
 
 using eq_ops decidable
 

library/data/option.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.basic logic.connectives.eq logic.classes.inhabited logic.classes.decidable
+import logic.core.eq logic.classes.inhabited logic.classes.decidable
 using eq_ops decidable
 
 namespace option

library/data/prod.lean

@@ -7,7 +7,7 @@
 
 -- The cartesian product.
 
-import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
+import logic.classes.inhabited logic.core.eq logic.classes.decidable
 
 using inhabited decidable
 

library/data/quotient/basic.lean

@@ -5,8 +5,8 @@
 -- Theory data.quotient
 -- ====================
 
-import logic tools.tactic ..subtype logic.connectives.cast struc.relation data.prod
-import logic.connectives.instances
+import logic tools.tactic ..subtype logic.core.cast struc.relation data.prod
+import logic.core.instances
 import .aux
 
 using relation prod inhabited nonempty tactic eq_ops

library/data/sigma.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.classes.inhabited logic.connectives.eq
+import logic.classes.inhabited logic.core.eq
 
 using inhabited
 

library/data/subtype.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
+import logic.classes.inhabited logic.core.eq logic.classes.decidable
 
 using decidable
 

library/data/sum.lean

@@ -7,7 +7,7 @@
 
 -- The sum type, aka disjoint union.
 
-import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
+import logic.core.prop logic.classes.inhabited logic.classes.decidable
 
 using inhabited decidable
 
@@ -81,4 +81,4 @@ rec_on s1
         show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 
-end sum
+end sum

library/logic/axioms/classical.lean

@@ -1,10 +1,8 @@
-----------------------------------------------------------------------------------------------------
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-----------------------------------------------------------------------------------------------------
 
-import logic.connectives.basic logic.connectives.quantifiers logic.connectives.cast struc.relation
+import logic.core.quantifiers logic.core.cast struc.relation
 
 using eq_ops
 

library/logic/axioms/funext.lean

@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.connectives.eq struc.function
+import logic.core.eq struc.function
 using function
 
 -- Function extensionality

library/logic/axioms/hilbert.lean

@@ -8,7 +8,7 @@
 -- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the
 -- constructive one).
 
-import logic.connectives.eq logic.connectives.quantifiers
+import logic.core.quantifiers
 import logic.classes.inhabited logic.classes.nonempty
 import data.subtype data.sum
 

library/logic/axioms/piext.lean

@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.classes.inhabited logic.connectives.cast
+import logic.classes.inhabited logic.core.cast
 
 using inhabited
 

library/logic/classes/decidable.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.basic logic.connectives.eq
+import logic.core.connectives
 
 namespace decidable
 

library/logic/classes/inhabited.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import logic.connectives.basic
+import logic.core.connectives
 
 inductive inhabited (A : Type) : Type :=
 inhabited_mk : A → inhabited A

library/logic/classes/nonempty.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import logic.connectives.basic .inhabited
+import .inhabited
 
 using inhabited
 

library/logic/core/core.md

@@ -4,8 +4,8 @@ logic.connectives
 Logical operations and connectives.
 
 * [prop](prop.lean) : the type Prop
-* [basic](basic.lean) : propositional connectives
 * [eq](eq.lean) : equality and disequality
+* [connectives](connectives.lean) : propositional connectives
 * [cast](cast.lean) : casts and heterogeneous equality
 * [quantifiers](quantifiers.lean) : existential and universal quantifiers
 * [if](if.lean) : if-then-else

library/logic/core/identities.lean

@@ -8,13 +8,10 @@
 -- Useful logical identities. In the absence of propositional extensionality, some of the
 -- calculations use the type class support provided by logic.connectives.instances
 
-import logic.connectives.instances
+import logic.core.instances
 
 using relation
 
--- TODO: delete when calc bug is fixed
-calc_subst subst_iff
-
 theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
 calc
   (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
@@ -38,6 +35,3 @@ calc
   a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff_symm (and_assoc _ _ _)
     ... ↔ (b ∧ a) ∧ c : {and_comm a b}
      ... ↔ b ∧ (a ∧ c) : and_assoc _ _ _
-
--- TODO: delete when calc bug is fixed
-calc_subst subst

library/logic/core/instances.lean

@@ -2,7 +2,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.connectives.basic logic.connectives.eq struc.relation
+import logic.core.connectives struc.relation
 
 namespace relation
 

library/logic/core/quantifiers.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import .basic .eq ..classes.nonempty
+import .connectives ..classes.nonempty
 
 using inhabited nonempty
 

library/logic/default.lean

@@ -2,8 +2,8 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.connectives.basic logic.connectives.eq logic.connectives.cast 
-import logic.connectives.quantifiers logic.connectives.if 
+import logic.core.connectives logic.core.eq logic.core.cast 
+import logic.core.quantifiers logic.core.if 
 import logic.classes.decidable logic.classes.inhabited logic.classes.nonempty
-import logic.connectives.instances
-import logic.connectives.identities
+import logic.core.instances
+import logic.core.identities

library/logic/logic.md

@@ -4,7 +4,7 @@ logic
 Logical constructions and axioms. By default, `import logic` does not
 import any additional axioms.
 
-* [connectives](connectives/connectives.md) : logical connectives
+* [core](core/core.md) : logical connectives
 * [axioms](axioms/axioms.md) : additional axioms
 * [classes](classes/classes.md) : classes for inhabited types, 
 decidable types, etc.  

library/struc/binary.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.connectives.eq
+import logic.core.eq
 using eq_ops
 
 namespace binary

library/struc/relation.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 
-import logic.connectives.prop
+import logic.core.prop
 
 
 -- General properties of relations

library/struc/struc.md

@@ -6,5 +6,4 @@ Axiomatic properties and structures.
 * [function](function.lean)
 * [relation](relation.lean)
 * [binary](binary.lean) : binary operations
-* [equivalence](equivalence.lean) : equivalence relations
 * [wf](wf.lean) : well-founded relations

tests/lean/run/congr_imp_bug.lean

@@ -3,7 +3,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
-import logic.connectives.basic struc.function
+import logic.core.connectives struc.function
 using function
 
 namespace congr
@@ -44,4 +44,4 @@ theorem congr_and_comp [instance] {T : Type} {R : T → T → Prop} {f1 f2 : T
      (C1 : struc R iff f1) (C2 : struc R iff f2) :
    congr.struc R iff (λx, f1 x ∧ f2 x) := congr.compose21 congr_and C1 C2
 
-end congr
+end congr

tests/lean/run/sum_bug.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
+import logic.core.prop logic.classes.inhabited logic.classes.decidable
 
 using inhabited decidable
 
@@ -67,4 +67,4 @@ rec_on s1
         show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff_symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 
-end sum
+end sum