inverse_add_const_neg_const: ∀ (k : ℤ), inverse (int.add k) (int.add (-k))

inverse.lean

open function
open int

namespace inverse
  universes u₁ u₂
  variables {α : Sort u₁} {β : Sort u₂}
  /- For reference
     I have inlined, the standard definitions i rely upon,
     these come from open function above.
     
  def left_inverse (g : β → α) (f : α → β) := ∀ x, g(f x) = x
  def right_inverse (g : β → α) (f : α → β) := ∀ y, f(g y) = y

  def injective (f : α → β) : Prop  := ∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
  def surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
  def bijective (f : α → β) : Prop  := injective f ∧ surjective f
  -/
  /- End of standard definitions -/

  def inverse (g : β → α) (f : α → β) := left_inverse g f ∧ right_inverse g f

  lemma inverse_iff (f : α → β) (g : β → α) :
    (∀ a b, f a = b ↔ a = g b) ↔ inverse g f :=
  ⟨assume h, ⟨λ a, eq.symm $ (h a $ f a).1 rfl, λ b, (h (g b)  b).2 rfl⟩,
  assume ⟨hl, hr⟩ a b, ⟨λ h, hl a ▸ congr_arg g h, λ h, eq.symm (congr_arg f h) ▸ (hr b)⟩⟩

  def inverse_rev {g : β → α} {f : α → β} (gf_inv : inverse g f)
  : inverse f g
  := ⟨gf_inv.right,gf_inv.left⟩

  def inverse_comp (f : α → β) (g : β → α) (gf_inv : inverse g f)
  : (∀ a, (g ∘ f) a = a) ∧ (∀ b, (f ∘ g) b = b) :=
    ⟨gf_inv.left, gf_inv.right⟩

  def inverse_comp_id {f : α → β} {g : β → α} (gf_inv  : inverse g f)
  : (g ∘ f = id) ∧ (f ∘ g = id)
  := ⟨funext (λ a, by rw [(inverse_comp f g gf_inv).left, id]),
      funext (λ b, by rw [(inverse_comp f g gf_inv).right, id])⟩

  def inverse_bijective (f : α → β) (g : β → α) (gf_inv  : inverse g f)
  : bijective f ∧ bijective g
  := have fg_inv : inverse f g, from inverse_rev gf_inv,
    have injective f,
      from (λ x₁ x₂, λ (h : f x₁ = f x₂),
            show x₁ = x₂, by rw [<- gf_inv.left x₁, h, gf_inv.left]),
    have surjective f, from (λ y, exists.intro (g y) (gf_inv.right y)),
    have injective g,
      from (λ y₁ y₂, λ (h : g y₁ = g y₂),
        show y₁ = y₂, by rw [<- fg_inv.left y₁, h, fg_inv.left]),
    have surjective g, from (λ x, exists.intro (f x) (fg_inv.right x)),
    ⟨⟨‹injective f›, ‹surjective f›⟩, ⟨‹injective g›, ‹surjective g ›⟩⟩


  theorem inverse_id_self {α : Type*} : inverse (@id α) (@id α)
  := have injective (@id α), from injective_id,
    have surjective (@id α), from surjective_id,
    have h : ∀ x : α, id(id x) = x,
      from (λ x,
        calc id(id x) = id x : by rw id
                  ... = x : by rw id
      ),
    show inverse (id) (id), from and.intro h h

  /-
     The following proof is kind of dumb, it is basically inverse_id_self above
     routed through inverse_comp_id, 

     The intent was to explore a little weirdness
     We have f ∘ g = id ∧ g ∘ f = id, but 
     and can show that inverse f g → inverse (f ∘ g) (f ∘ g)
     However since the types differ:
     g ∘ f : α → α 
     f ∘ g : β → β
     we cannot show inverse (f ∘ g) (g ∘ f)
     even though equality is transitive and we have f ∘ g = id and id = g ∘ f
     f ∘ g cannot be shown equal to g ∘ f because the types α and β differ. 
     I guess if you first assume α = β, however that may not be the case.
     Anyhow it seemed like a weird edge case.
   -/
  def inverse_comp_inv {α : Type*} {β : Type*}
  : ∀ (f : α → β) (g : β → α), inverse f g → inverse (f ∘ g) (f ∘ g)
  := (λ f g, λ inv,
      have fog_eq_id : (f ∘ g = id), from (inverse_comp_id inv).left,
      have gof_eq_id : (id = g ∘ f), from eq.symm ((inverse_comp_id inv).right),
      -- As per above this is commented out due to it's failure to typecheck
      -- have fog_eq_gof : f ∘ g = g ∘ f, from eq.trans fog_eq_id gof_eq_id,            
      have fog_comp_id : ∀ x, (f ∘ g)((f ∘ g) x) = x,
        from (λ x, calc (f ∘ g) ((f ∘ g) x) = (id (id x)) : by rw (inverse_comp_id inv).left
                          ... = id x : by refl
                          ... = x : by refl),
      and.intro fog_comp_id fog_comp_id)

  -- Here we partially apply addition by any k, and also by it's negation -k
  -- once we have all the values available we can use infix..
  theorem inverse_add_const_neg_const
  : ∀ (k : ℤ), inverse (int.add k) (int.add (-k))
  := (λ k,
      have l : ∀ (x : ℤ), int.add (k) (int.add (int.neg k) x) = x,
        from (λ x,
              calc  int.add (k) (int.add (int.neg k) x)
                  = k + (-k + x) : by refl
              ... = k + -k + x   : by rw add_assoc
              ... = 0 + x        : by rw add_right_neg
              ... = x            : by rw zero_add),
      -- Basically the same except using add_left_neg instead of right.
      have r : ∀ (x : ℤ), int.add (-k) (int.add (k) x) = x,
        from (λ x,
              calc  int.add (-k) (int.add (k) x)
                  = -k + (k + x) : by refl
              ... = -k + k + x : by rw add_assoc
              ... = 0 + x : by rw add_left_neg
              ... = x : by rw zero_add),
      show inverse (int.add k) (int.add (-k)),
        from and.intro l r)

#check inverse_add_const_neg_const

  def neg : bool → bool
  | tt := ff
  | ff := tt
  
  def nand : bool → bool → bool
  | tt tt := ff
  | ff ff := tt
  | ff tt := tt
  | tt ff := tt

  theorem neg_inverse_self
  : inverse (neg) (neg) 
  := have h : ∀ x : bool, neg(neg x) = x,
      from (λ x,
        begin
        cases x,
          {show neg(neg ff) = ff, by refl},
          {show neg(neg tt) = tt, by refl}
        end
      ),
      and.intro h h
end inverse