feat (Data/Equiv/Basic): add equiv (leanprover#13)

* add lemma macro

* port init/function

* equiv is an equivalence relation

* a bit more equiv

* functors send equivs to equivs

* more tinkering

* add changes suggested by review

* add missing imports

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Mathlib.lean

@@ -5,10 +5,14 @@ import Mathlib.Algebra.Ring.Basic
 import Mathlib.Data.Array.Basic
 import Mathlib.Data.ByteArray
 import Mathlib.Data.Char
+import Mathlib.Data.Equiv.Basic
+import Mathlib.Data.Equiv.Functor
 import Mathlib.Data.List.Basic
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.UInt
+import Mathlib.Function
 import Mathlib.Logic.Basic
+import Mathlib.Logic.Function.Basic
 import Mathlib.Mem
 import Mathlib.Set
 import Mathlib.Tactic.Basic

Mathlib/Data/Equiv/Basic.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Mario Carneiro
+-/
+import Mathlib.Logic.Function.Basic
+/-!
+# Equivalence between types
+
+* `equiv α β` a.k.a. `α ≃ β`: a bijective map `α → β` bundled with its inverse map; we use this (and
+  not equality!) to express that various `Type`s or `Sort`s are equivalent.
+
+## Tags
+
+equivalence, congruence, bijective map
+-/
+
+open Function
+
+universes u v w
+variable {α : Sort u} {β : Sort v} {γ : Sort w}
+
+/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
+structure equiv (α : Sort u) (β : Sort v) :=
+(to_fun    : α → β)
+(inv_fun   : β → α)
+(left_inv  : left_inverse inv_fun to_fun)
+(right_inv : right_inverse inv_fun to_fun)
+
+infix:25 " ≃ " => equiv
+
+namespace equiv
+
+/-- `perm α` is the type of bijections from `α` to itself. -/
+@[reducible] def perm (α : Sort u) := equiv α α
+
+instance : CoeFun (α ≃ β) (λ _ => α → β):=
+⟨to_fun⟩
+
+@[simp] theorem coe_fn_mk (f : α → β) (g l r) : (equiv.mk f g l r : α → β) = f :=
+rfl
+
+def refl (α) : α ≃ α := ⟨id, id, λ _ => rfl, λ _ => rfl⟩
+
+def symm (e : α ≃ β) : β ≃ α := ⟨e.inv_fun, e.to_fun, e.right_inv, e.left_inv⟩
+
+def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
+⟨e₂ ∘ (e₁ : α → β), e₁.symm ∘ (e₂.symm : γ → β),
+  e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
+
+@[simp] theorem apply_symm_apply  (e : α ≃ β) (x : β) : e (e.symm x) = x :=
+e.right_inv x
+
+@[simp] theorem symm_apply_apply (e : α ≃ β) (x : α) : e.symm (e x) = x :=
+e.left_inv x
+
+@[simp] theorem symm_comp_self (e : α ≃ β) : e.symm ∘ (e : α → β) = id := funext e.symm_apply_apply
+
+@[simp] theorem self_comp_symm (e : α ≃ β) : e ∘ (e.symm : β → α) = id := funext e.apply_symm_apply
+
+end equiv

Mathlib/Data/Equiv/Functor.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2019 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin, Simon Hudon, Scott Morrison
+-/
+import Mathlib.Data.Equiv.Basic
+
+/-!
+
+# Functors can be applied to `equiv`s.
+
+```
+def functor.map_equiv (f : Type u → Type v) [functor f] [is_lawful_functor f] :
+  α ≃ β → f α ≃ f β
+```
+
+-/
+
+open equiv
+
+namespace Functor
+
+variable (f : Type u → Type v) [Functor f] [LawfulFunctor f]
+
+-- this is in control.basic in Lean 3
+theorem map_map (m : α → β) (g : β → γ) (x : f α) :
+  g <$> (m <$> x) = (g ∘ m) <$> x :=
+(comp_map _ _ _).symm
+
+/-- Apply a functor to an `equiv`. -/
+def map_equiv (h : α ≃ β) : f α ≃ f β where
+  to_fun    := map h
+  inv_fun   := map h.symm
+  left_inv x := by simp [map_map]
+  right_inv x := by simp [map_map]
+
+@[simp]
+lemma map_equiv_apply (h : α ≃ β) (x : f α) :
+  (map_equiv f h : f α ≃ f β) x = map h x := rfl
+
+@[simp]
+lemma map_equiv_symm_apply (h : α ≃ β) (y : f β) :
+  (map_equiv f h : f α ≃ f β).symm y = map h.symm y := rfl
+
+end Functor

Mathlib/Function.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura, Jeremy Avigad, Haitao Zhang
+-/
+-- a port of core Lean `init/function.lean`
+
+/-!
+# General operations on functions
+-/
+
+universes u₁ u₂ u₃ u₄
+
+namespace Function
+
+variable {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ : Sort u₁}
+
+@[reducible] def comp_right (f : β → β → β) (g : α → β) : β → α → β :=
+λ b a => f b (g a)
+
+@[reducible] def comp_left (f : β → β → β) (g : α → β) : α → β → β :=
+λ a b => f (g a) b
+
+/-- Given functions `f : β → β → φ` and `g : α → β`, produce a function `α → α → φ` that evaluates
+`g` on each argument, then applies `f` to the results. Can be used, e.g., to transfer a relation
+from `β` to `α`. -/
+@[reducible] def on_fun (f : β → β → φ) (g : α → β) : α → α → φ :=
+λ x y => f (g x) (g y)
+
+@[reducible] def combine (f : α → β → φ) (op : φ → δ → ζ) (g : α → β → δ)
+  : α → β → ζ :=
+λ x y => op (f x y) (g x y)
+
+@[reducible] def swap {φ : α → β → Sort u₃} (f : ∀ x y, φ x y) : ∀ y x, φ x y :=
+λ y x => f x y
+
+@[reducible] def app {β : α → Sort u₂} (f : ∀ x, β x) (x : α) : β x :=
+f x
+
+theorem left_id (f : α → β) : id ∘ f = f := rfl
+
+theorem right_id (f : α → β) : f ∘ id = f := rfl
+
+@[simp] theorem comp_app (f : β → φ) (g : α → β) (a : α) : (f ∘ g) a = f (g a) := rfl
+
+theorem comp.assoc (f : φ → δ) (g : β → φ) (h : α → β) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl
+
+@[simp] theorem comp.left_id (f : α → β) : id ∘ f = f := rfl
+
+@[simp] theorem comp.right_id (f : α → β) : f ∘ id = f := rfl
+
+theorem comp_const_right (f : β → φ) (b : β) : f ∘ (const α b) = const α (f b) := rfl
+
+/-- A function `f : α → β` is called injective if `f x = f y` implies `x = y`. -/
+@[reducible] def injective (f : α → β) : Prop := ∀ {a₁ a₂}, f a₁ = f a₂ → a₁ = a₂
+
+theorem injective.comp {g : β → φ} {f : α → β} (hg : injective g) (hf : injective f) :
+  injective (g ∘ f) :=
+λ h => hf (hg h)
+
+/-- A function `f : α → β` is calles surjective if every `b : β` is equal to `f a`
+for some `a : α`. -/
+@[reducible] def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
+
+theorem surjective.comp {g : β → φ} {f : α → β} (hg : surjective g) (hf : surjective f) :
+  surjective (g ∘ f) :=
+λ (c : φ) => Exists.elim (hg c) (λ b hb => Exists.elim (hf b) (λ a ha =>
+  Exists.intro a (show g (f a) = c from (Eq.trans (congrArg g ha) hb))))
+
+/-- A function is called bijective if it is both injective and surjective. -/
+def bijective (f : α → β) := injective f ∧ surjective f
+
+theorem bijective.comp {g : β → φ} {f : α → β} : bijective g → bijective f → bijective (g ∘ f)
+| ⟨h_ginj, h_gsurj⟩, ⟨h_finj, h_fsurj⟩ => ⟨h_ginj.comp h_finj, h_gsurj.comp h_fsurj⟩
+
+/-- `left_inverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
+def left_inverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
+
+/-- `has_left_inverse f` means that `f` has an unspecified left inverse. -/
+def has_left_inverse (f : α → β) : Prop := ∃ finv : β → α, left_inverse finv f
+
+/-- `right_inverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
+def right_inverse (g : β → α) (f : α → β) : Prop := left_inverse f g
+
+/-- `has_right_inverse f` means that `f` has an unspecified right inverse. -/
+def has_right_inverse (f : α → β) : Prop := ∃ finv : β → α, right_inverse finv f
+
+theorem left_inverse.injective {g : β → α} {f : α → β} : left_inverse g f → injective f :=
+λ h a b hf => h a ▸ h b ▸ hf ▸ rfl
+
+theorem has_left_inverse.injective {f : α → β} : has_left_inverse f → injective f :=
+λ h => Exists.elim h (λ finv inv => inv.injective)
+
+theorem right_inverse_of_injective_of_left_inverse {f : α → β} {g : β → α}
+    (injf : injective f) (lfg : left_inverse f g) :
+  right_inverse f g :=
+λ x => injf $ lfg $ f x
+
+theorem right_inverse.surjective {f : α → β} {g : β → α} (h : right_inverse g f) : surjective f :=
+λ y => ⟨g y, h y⟩
+
+theorem has_right_inverse.surjective {f : α → β} : has_right_inverse f → surjective f
+| ⟨finv, inv⟩ => inv.surjective
+
+theorem left_inverse_of_surjective_of_right_inverse {f : α → β} {g : β → α} (surjf : surjective f)
+  (rfg : right_inverse f g) : left_inverse f g :=
+λ y =>
+  let ⟨x, hx⟩ := surjf y
+  by rw [← hx, rfg]
+
+theorem injective_id : injective (@id α) := id
+
+theorem surjective_id : surjective (@id α) := λ a => ⟨a, rfl⟩
+
+theorem bijective_id : bijective (@id α) := ⟨injective_id, surjective_id⟩
+
+end Function
+
+namespace Function
+
+variable {α : Type u₁} {β : Type u₂} {φ : Type u₃}
+
+/-- Interpret a function on `α × β` as a function with two arguments. -/
+@[inline] def curry : (α × β → φ) → α → β → φ :=
+λ f a b => f (a, b)
+
+/-- Interpret a function with two arguments as a function on `α × β` -/
+@[inline] def uncurry : (α → β → φ) → α × β → φ :=
+λ f a => f a.1 a.2
+
+@[simp] theorem curry_uncurry (f : α → β → φ) : curry (uncurry f) = f :=
+rfl
+
+@[simp] theorem uncurry_curry (f : α × β → φ) : uncurry (curry f) = f :=
+funext (λ ⟨a, b⟩ => rfl)
+
+protected theorem left_inverse.id {g : β → α} {f : α → β} (h : left_inverse g f) : g ∘ f = id :=
+funext h
+
+protected theorem right_inverse.id {g : β → α} {f : α → β} (h : right_inverse g f) : f ∘ g = id :=
+funext h
+
+end Function

Mathlib/Logic/Function/Basic.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2016 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Mario Carneiro
+-/
+import Mathlib.Logic.Basic
+import Mathlib.Function
+
+namespace Function
+
+theorem left_inverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
+  (hf : left_inverse f g) (hh : left_inverse h i) : left_inverse (h ∘ f) (g ∘ i) :=
+λ a => show h (f (g (i a))) = a by rw [hf (i a), hh a]
+
+theorem right_inverse.comp {f : α → β} {g : β → α} {h : β → γ} {i : γ → β}
+  (hf : right_inverse f g) (hh : right_inverse h i) : right_inverse (h ∘ f) (g ∘ i) :=
+left_inverse.comp hh hf