Skip to content

Instantly share code, notes, and snippets.

@ratmice

ratmice/inverse.lean Secret

Last active Apr 4, 2020
Embed
What would you like to do?
inverse_add_const_neg_const: ∀ (k : ℤ), inverse (int.add k) (int.add (-k))
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.