feat(logic/function): define function.involutive (#1474)

* feat(logic/function): define `function.involutive`

* Prove that `inv`, `neg`, and `complex.conj` are involutive.

* Move `inv_inv'` to `algebra/field`

src/algebra/field.lean

@@ -19,6 +19,14 @@ instance division_ring.to_domain [s : division_ring α] : domain α :=
       division_ring.mul_ne_zero (mt or.inl hn) (mt or.inr hn) h
   ..s }
 
+@[simp] theorem inv_inv' [discrete_field α] (x : α) : x⁻¹⁻¹ = x :=
+if h : x = 0
+then by rw [h, inv_zero, inv_zero]
+else division_ring.inv_inv h
+
+lemma inv_involutive' [discrete_field α] : function.involutive (has_inv.inv : α → α) :=
+inv_inv'
+
 namespace units
 variables [division_ring α] {a b : α}
 

src/algebra/group/basic.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Simon Hudon, Mario Carneiro
 
 Various multiplicative and additive structures.
 -/
-import algebra.group.to_additive
+import algebra.group.to_additive logic.function
 
 universe u
 variable {α : Type u}
@@ -241,3 +241,6 @@ section add_monoid
   show 0+0+1=(1:α), by rw [zero_add, zero_add]
 
 end add_monoid
+
+@[to_additive]
+lemma inv_involutive {α} [group α] : function.involutive (has_inv.inv : α → α) := inv_inv

src/algebra/group_power.lean

@@ -19,9 +19,6 @@ variable {α : Type u}
 
 @[simp] theorem inv_one [division_ring α] : (1⁻¹ : α) = 1 := by rw [inv_eq_one_div, one_div_one]
 
-@[simp] theorem inv_inv' [discrete_field α] {a:α} : a⁻¹⁻¹ = a :=
-by rw [inv_eq_one_div, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_one]
-
 /-- The power operation in a monoid. `a^n = a*a*...*a` n times. -/
 def monoid.pow [monoid α] (a : α) : ℕ → α
 | 0     := 1

src/analysis/complex/polynomial.lean

@@ -57,7 +57,7 @@ have hF₁ : F.eval z' = f.eval z₀ - f.eval z₀ * (g.eval z₀).abs * δ ^ n
       neg_mul_eq_neg_mul_symm, mul_one, div_eq_mul_inv];
     simp only [mul_comm, mul_left_comm, mul_assoc],
 have hδs : (g.eval z₀).abs * δ ^ n / (f.eval z₀).abs < 1,
-  by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← @inv_inv' _ _ (complex.abs _ * _), mul_inv',
+  by rw [div_eq_mul_inv, mul_right_comm, mul_comm, ← inv_inv' (complex.abs _ * _), mul_inv',
       inv_inv', ← div_eq_mul_inv, div_lt_iff hfg0, one_mul];
     calc δ ^ n ≤ δ ^ 1 : pow_le_pow_of_le_one (le_of_lt hδ0) hδ1 hn0
       ... = δ : pow_one _

src/data/complex/basic.lean

@@ -122,9 +122,9 @@ ext_iff.2 $ by simp
 @[simp] lemma conj_conj (z : ℂ) : conj (conj z) = z :=
 ext_iff.2 $ by simp
 
-lemma conj_bijective : function.bijective conj :=
-⟨function.injective_of_has_left_inverse ⟨conj, conj_conj⟩,
- function.surjective_of_has_right_inverse ⟨conj, conj_conj⟩⟩
+lemma conj_involutive : function.involutive conj := conj_conj
+
+lemma conj_bijective : function.bijective conj := conj_involutive.bijective
 
 lemma conj_inj {z w : ℂ} : conj z = conj w ↔ z = w :=
 conj_bijective.1.eq_iff

src/data/equiv/basic.lean

@@ -22,13 +22,16 @@ structure equiv (α : Sort*) (β : Sort*) :=
 (left_inv  : left_inverse inv_fun to_fun)
 (right_inv : right_inverse inv_fun to_fun)
 
+infix ` ≃ `:25 := equiv
+
+def function.involutive.to_equiv {f : α → α} (h : involutive f) : α ≃ α :=
+⟨f, f, h.left_inverse, h.right_inverse⟩
+
 namespace equiv
 
 /-- `perm α` is the type of bijections from `α` to itself. -/
 @[reducible] def perm (α : Sort*) := equiv α α
 
-infix ` ≃ `:25 := equiv
-
 instance : has_coe_to_fun (α ≃ β) :=
 ⟨_, to_fun⟩
 

src/data/real/hyperreal.lean

@@ -33,7 +33,7 @@ localized "notation `ω` := hyperreal.omega" in hyperreal
 
 lemma epsilon_eq_inv_omega : ε = ω⁻¹ := rfl
 
-lemma inv_epsilon_eq_omega : ε⁻¹ = ω := @inv_inv' _ _ ω
+lemma inv_epsilon_eq_omega : ε⁻¹ = ω := inv_inv' ω
 
 lemma epsilon_pos : 0 < ε :=
 have h0' : {n : ℕ | ¬ n > 0} = {0} :=

src/data/real/nnreal.lean

@@ -368,7 +368,7 @@ nnreal.eq $ inv_mul_cancel $ mt (@nnreal.eq_iff r 0).1 h
 @[simp] lemma mul_inv_cancel {r : ℝ≥0} (h : r ≠ 0) : r * r⁻¹ = 1 :=
 by rw [mul_comm, inv_mul_cancel h]
 
-@[simp] lemma inv_inv {r : ℝ≥0} : r⁻¹⁻¹ = r := nnreal.eq inv_inv'
+@[simp] lemma inv_inv {r : ℝ≥0} : r⁻¹⁻¹ = r := nnreal.eq $ inv_inv' _
 
 @[simp] lemma inv_le {r p : ℝ≥0} (h : r ≠ 0) : r⁻¹ ≤ p ↔ 1 ≤ r * p :=
 by rw [← mul_le_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h]

src/logic/function.lean

@@ -259,4 +259,22 @@ lemma uncurry'_bicompr (f : α → β → γ) (g : γ → δ) :
   uncurry' (g ∘₂ f) = (g ∘ uncurry' f) := rfl
 end bicomp
 
+/-- A function is involutive, if `f ∘ f = id`. -/
+def involutive {α} (f : α → α) : Prop := ∀ x, f (f x) = x
+
+lemma involutive_iff_iter_2_eq_id {α} {f : α → α} : involutive f ↔ (f^[2] = id) :=
+funext_iff.symm
+
+namespace involutive
+variables {α : Sort u} {f : α → α} (h : involutive f)
+
+protected lemma left_inverse : left_inverse f f := h
+protected lemma right_inverse : right_inverse f f := h
+
+protected lemma injective : injective f := injective_of_left_inverse h.left_inverse
+protected lemma surjective : surjective f := λ x, ⟨f x, h x⟩
+protected lemma bijective : bijective f := ⟨h.injective, h.surjective⟩
+
+end involutive
+
 end function