refactor(library/logic): add basic definitions for relations at logic/relation.lean

We need them for wf and definitional package

library/data/prod/wf.lean

@@ -56,7 +56,7 @@ namespace prod
 
   -- The relational product of well founded relations is well-founded
   definition rprod.wf (Ha : well_founded Ra) (Hb : well_founded Rb) : well_founded (rprod Ra Rb) :=
-  subrel.wf (rprod.sub_lex) (lex.wf Ha Hb)
+  subrelation.wf (rprod.sub_lex) (lex.wf Ha Hb)
 
   end
 end prod

library/data/quotient/basic.lean

@@ -302,8 +302,8 @@ theorem representative_map_equiv_inj {A : Type} {R : A → A → Prop}
     (equiv : is_equivalence R) {f : A → A}
     (H1 : ∀a, R a (f a)) (H2 : ∀a b, R a b → f a = f b) {a b : A} (H3 : f a = f b) :
   R a b :=
-have symmR : symmetric R, from rel_symm R,
+have symmR : relation.symmetric R, from rel_symm R,
-have transR : transitive R, from rel_trans R,
+have transR : relation.transitive R, from rel_trans R,
 show R a b, from
   have H2 : R a (f b), from H3 ▸ (H1 a),
   have H3 : R (f b) b, from symmR (H1 b),

library/data/quotient/classical.lean

@@ -27,8 +27,8 @@ epsilon_spec (exists_intro a (reflR a))
 -- TODO: only needed: R PER
 theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence R) {a b : A}
   (H2 : R a b) : prelim_map R a = prelim_map R b :=
-have symmR : symmetric R, from is_symmetric.infer R,
+have symmR : relation.symmetric R, from is_symmetric.infer R,
-have transR : transitive R, from is_transitive.infer R,
+have transR : relation.transitive R, from is_transitive.infer R,
 have H3 : ∀c, R a c ↔ R b c, from
   take c,
     iff.intro

library/logic/relation.lean

@@ -0,0 +1,37 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Leonardo de Moura
+import logic.eq
+
+-- TODO(Leo): remove duplication between this file and algebra/relation.lean
+-- We need some of the following definitions asap when "initializing" Lean.
+
+variables {A B : Type} (R : B → B → Prop)
+infix [local] `≺`:50 := R
+
+definition reflexive := ∀x, x ≺ x
+
+definition symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x
+
+definition transitive := ∀⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
+
+definition irreflexive := ∀x, ¬ x ≺ x
+
+definition anti_symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x → x = y
+
+definition empty_relation := λa₁ a₂ : A, false
+
+definition subrelation (Q R : B → B → Prop) := ∀⦃x y⦄, Q x y → R x y
+
+definition inv_image (f : A → B) : A → A → Prop :=
+λa₁ a₂, f a₁ ≺ f a₂
+
+theorem inv_image.trans (f : A → B) (H : transitive R) : transitive (inv_image R f) :=
+λ (a₁ a₂ a₃ : A) (H₁ : inv_image R f a₁ a₂) (H₂ : inv_image R f a₂ a₃), H H₁ H₂
+
+theorem inv_image.irreflexive (f : A → B) (H : irreflexive R) : irreflexive (inv_image R f) :=
+λ (a : A) (H₁ : inv_image R f a a), H (f a) H₁
+
+inductive tc {A : Type} (R : A → A → Prop) : A → A → Prop :=
+base  : ∀a b, R a b → tc R a b,
+trans : ∀a b c, tc R a b → tc R b c → tc R a c

library/logic/wf.lean

@@ -1,7 +1,7 @@
 -- 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.eq
+import logic.eq logic.relation
 
 inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
 intro : ∀x, (∀ y, R y x → acc R y) → acc R x
@@ -70,15 +70,15 @@ end well_founded
 open well_founded
 
 -- Empty relation is well-founded
-definition empty.wf {A : Type} : well_founded (λa b : A, false) :=
+definition empty.wf {A : Type} : well_founded empty_relation :=
 well_founded.intro (λ (a : A),
   acc.intro a (λ (b : A) (lt : false), false.rec _ lt))
 
 -- Subrelation of a well-founded relation is well-founded
-namespace subrel
+namespace subrelation
 context
   parameters {A : Type} {R Q : A → A → Prop}
-  parameters (H₁ : ∀{x y}, Q x y → R x y)
+  parameters (H₁ : subrelation Q R)
   parameters (H₂ : well_founded R)
 
   definition accessible {a : A} (ac : acc R a) : acc Q a :=
@@ -89,10 +89,7 @@ context
   definition wf : well_founded Q :=
   well_founded.intro (λ a, accessible (H₂ a))
 end
-end subrel
+end subrelation
-
-definition inv_image {A B : Type} (R : B → B → Prop) (f : A → B) : A → A → Prop :=
-λa₁ a₂, R (f a₁) (f a₂)
 
 -- The inverse image of a well-founded relation is well-founded
 namespace inv_image
@@ -115,11 +112,6 @@ context
 end
 end inv_image
 
--- Transitive closure
-inductive tc {A : Type} (R : A → A → Prop) : A → A → Prop :=
-base  : ∀a b, R a b → tc R a b,
-trans : ∀a b c, tc R a b → tc R b c → tc R a c
-
 -- The transitive closure of a well-founded relation is well-founded
 namespace tc
 context