The opposite

Stream: general

[deepest recursion]

In lean I can write this

def fpres {f:A->B}: ∀ a b , a = b -> f a = f b := by
  intro a b p
  rw [p]

But I feel like I cant write this

def fcanc1 {f:A->B}: ∀ a b , f a = f b -> a = b := by
  intros a b p

  admit

Am I missing something obvious?

[Damiano Testa]

What should happen if f is constant and a and b are different?

[Damiano Testa]

Say B = Unit, A = Bool and a = true while b = false.

[deepest recursion]

My initial guess was that it would be true if f is continuous. How do I add this assumption?

[Damiano Testa]

Constant functions are usually continuous.

[Damiano Testa]

The property that is what you wrote is normally called injectivity.

[Damiano Testa]

If continuity is what you want, this sets up an environment with a continuous function floating around:

import Mathlib

variable {A B} [TopologicalSpace A] [TopologicalSpace B] {f : A → B} (hf : Continuous f)

[deepest recursion]

On second thought, it would be nice if somebody showed what to do to make fcanc1 work :)

[Ruben Van de Velde]

import Mathlib
def fcanc1 {f:A->B} (hf : Function.Injective f) : ∀ a b , f a = f b -> a = b := by
  intros a b p
  apply hf
  apply p

[deepest recursion]

But... thas just a restatement...

Maybe it's easier to show this somehow?

def l1 {f:A->B}{h:B->A}: (∀ a , a = h (f a)) -> (∀ b , b = f (h b)) := by
  intro p1 b
  let m := p1 (h b)

  admit

[Damiano Testa]

I don't think that is true either: if A = Unit and B = Bool, this will not hold.

[deepest recursion]

I cant state the case when A is Unit and B is bool

def tounit := fun (_:Bool) => ()
def fromunit := fun () => false
example : ∀ a:Bool , a = fromunit (tounit a) := by
  intro a
  cases a
  rfl
  unfold tounit fromunit; simp
  -- goal is false

[Edward van de Meent]

that is exactly the point, because it's not true. as a sidenote, why is it that you want to prove this? is there a more specific case in which you want to apply such a theorem (if there were one)?

[deepest recursion]

I have written this. it works, and lets me rewrite things by equivalence that is not strict

inductive sigmaprop (T:Type _)(P:T -> Prop) : Type _
| mksprop : (t:T) -> P t -> sigmaprop T P

def iscoh_map {A:Type _}{B:Type _} : (A -> B) -> Type _ :=
  fun f => sigmaprop (B -> A) fun r => ∀ a , a = r (f a)
def iso : Type _ -> Type _ -> Type _ :=
  fun A B => @Sigma (A -> B) fun f => iscoh_map f

def iso.bw : iso A B -> (B -> A) := fun (.mk _ d) => by
  unfold iscoh_map at d; let (.mksprop bw _) := d; exact bw

def p1 : (p:iso A B) -> ∀ a , sigmaprop B fun b => a = (p.bw b) := by
  intros p a; unfold iso iscoh_map at p
  let (Sigma.mk f k) := p;
  simp at k
  let (.mksprop h r) := k
  unfold iso.bw; simp
  exact (.mksprop (f a) (r a))

notation "~(" L "," R ")" => ⟨ L , R ⟩

def not_iso: iso Bool Bool := by
  unfold iso
  exact ~(not, by unfold iscoh_map; exact (.mksprop not (by intro i; cases i <;> rfl)))

def proof : (not a) = not (not (not a)) := by cases a <;> rfl

-- notice that 'proof' is not definitionally equal to the 'a = not (not a)'
example : a = not (not a) := by
  let (.mksprop b c) := p1 not_iso a
  unfold iso.bw not_iso at c;
  simp at c
  rw [c]
  exact proof

I then tried to define inversion for iso like this

def fcanc1 {f:A->B}: ∀ a b , f a = f b -> a = b := by
  intros a b p

  admit

def fcanc2 {h:B->A}{f:A->B}{k:B}: h k = h (f (h k)) -> k = f (h k) := by
  generalize (f (h _)) = r
  intro p
  apply @fcanc1 _ _ h
  exact p

def rev : iso A B -> iso B A := by
  intro (.mk f (.mksprop b coh))
  unfold iso
  refine .mk b (.mksprop f ?p)
  intro k
  let t1 := coh (b k)
  let t2 := fcanc2 t1
  exact t2

but I have stuck at fcanc1

[deepest recursion]

Here's another example

def f : Nat -> List Unit
| .zero => .nil
| .succ a => .cons () (f a)
def b : List Unit -> Nat
| .nil => .zero
| .cons .unit t => .succ (b t)
def coh : (a : Nat) -> a = b (f a) := by
  intro i
  match i with
  | .succ a => unfold b f; simp; exact (coh a)
  | .zero => unfold b f; simp;


def int_list : iso Nat (List Unit) := by
  unfold iso
  exact ~(
    f,
    by unfold iscoh_map
       exact (.mksprop b coh)
  )

-- a proof about integers
-- by doing pattern matching on a list!!!!
example : (a > 0) -> (a + 1 > 0) := by
  let (.mksprop k p) := p1 int_list a
  rw [p]
  cases k
  . case nil => intro; contradiction
  . case cons a b => simp

[Edward van de Meent]

i'm sorry to say that there is no proof of fcanc1, because it says that for every function f, if the result is the same, then the inputs are the same. this is the same as saying that the value of f a cannot be equal to f b when a and b are different, which is simply not true for all f. in particular, given that there are at least two values a and a', as well as some value b, the statement is not true for the function mapping both a and a' to b.

[Ruben Van de Velde]

What are you trying to do?

[Kyle Miller]

By the way, sigmatype is known as docs#Subtype

-- def sigmaprop (T : Type _) (P : T -> Prop) := {t : T // P t}

def iscoh_map {A B : Type _} (f : A -> B) : Type _ :=
  {r : B → A // ∀ a , a = r (f a)}
def iso (A B : Type _) : Type _ :=
  Σ (f : A -> B), iscoh_map f

def iso.bw {A B} : iso A B -> (B -> A) := fun (.mk _ d) => d.1
-- or: def iso.bw {A B} (p : iso A B) : B -> A := p.2.1

def p1 {A B} (p : iso A B) (a : A) : {b : B // a = p.bw b} :=
  let ⟨f, k⟩ := p;
  let ⟨_, r⟩ := k
  ⟨f a, r a⟩

notation "~(" L "," R ")" => ⟨ L , R ⟩

def not_iso: iso Bool Bool :=
  ~(not, ⟨not, (by intro i; cases i <;> rfl)⟩)

def proof {a : Bool} : (not a) = not (not (not a)) := by cases a <;> rfl

-- notice that 'proof' is not definitionally equal to the 'a = not (not a)'
example (a : Bool) : a = not (not a) := by
  let ⟨b, c⟩ := p1 not_iso a
  unfold iso.bw not_iso at c;
  simp at c
  rw [c]
  exact proof

[Kyle Miller]

The reason you're not able to define rev is that the definition of iso is not correct. You made the definition for "function with an explicit right inverse", which just means it's injective, not necessarily bijective.

def myIso : iso Bool Nat :=
  ⟨(fun b => if b then 1 else 0),
    ⟨fun n => n == 1, by
      intro b
      cases b <;> simp⟩⟩

[deepest recursion]

An illuminating simplification, thank you.
I thought that ∀ a , a = r (f a) defines a surjection rather than an injection, and would qualify as an equivalence.
Is it not the case?

[Kyle Miller]

As the example shows, no that's not the case.

That proposition implies these two things: (1) f is injective and (2) r is surjective.

[deepest recursion]

In the code below I can use p to rewrite itself to refl. Can I use this fact to show that because of this, f (h b) has to be id?

def i4 {f:A->B}{h:B->A}: ∀ b , h b = h (f (h b)) -> f (h b) = id b := by
  intro v p
  -- p : h v = h (f (h v))
  rw [<-p] at p
  -- p : h v = h v

  admit

[Kyle Miller]

No, being able to rewrite to refl is to expected. If you have a = b then you can rewrite to get a = a or b = b, but these are trivial conclusions that don't need a = b.

Having h v = h v in your local context doesn't give you anything, it's trivial. You can always introduce it with have : h v = hv := rfl without needing to make use of p at all.