Bijective 4

Stream: new members

[Răzvan Flavius Panda]

Trying to prove: https://github.com/hrmacbeth/math2001/blob/e660f42b13ddcb6d12b52ba036d6bd071a0cfb9b/Math2001/08_Functions/02_Bijective.lean#L191

Haven't got much:

example : ∀ f : Subatomic → Subatomic, Injective f → Bijective f := by
  intro f h
  constructor
  · exact h
  · dsimp [Surjective]
    dsimp [Injective] at h
    intro b

I don't know how to proceed further.

[Aaron Liu]

you have to start casing on b

[Răzvan Flavius Panda]

I tried cases b but did not know how to solve the sub-goals. Do I need to treat every possible implementation of function f?

[Aaron Liu]

yes, unless you want to develop the theory of finiteness

[Aaron Liu]

you can choose to do that instead, but be warned it is quite tricky

[Răzvan Flavius Panda]

I'll try every implementation of f. How do I do that?

[Aaron Liu]

what you want to do is do cases on f u where u is running through all the constructors of Subatomic

[Răzvan Flavius Panda]

That sounds like the code is insulting me haha

[Aaron Liu]

do cases helec : f .electron so you can remember what you're casing on

[Răzvan Flavius Panda]

Didn't quite get exactly what to do, I tried:

    cases b
    cases helec : f .electron

f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
helec : f electron = proton
⊢ ∃ a, f a = proton
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
helec : f electron = neutron
⊢ ∃ a, f a = proton
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
helec : f electron = electron
⊢ ∃ a, f a = proton
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
⊢ ∃ a, f a = neutron
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
⊢ ∃ a, f a = electron

[Răzvan Flavius Panda]

I see first sub-goal is solvable but not the 2nd sub-goal.

[Aaron Liu]

Well you need to case on f neutron and f proton too

[Răzvan Flavius Panda]

Like so?

    cases b
    cases helec1 : f .electron
    cases helec2 : f .proton
    cases helec3 : f .neutron

[Aaron Liu]

idk maybe save the cases b for last

[Aaron Liu]

Also each cases generates multiple subgoals so you should immediately indent them with the focusing dot

[Răzvan Flavius Panda]

Aaron Liu said:

Also each cases generates multiple subgoals so you should immediately indent them with the focusing dot

I don't get how that works. Could you show me?

[Răzvan Flavius Panda]

These goals are clearly not all the possibilities:

f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
helec1 : f electron = proton
helec2 : f proton = proton
helec3 : f neutron = proton
⊢ ∃ a, f a = proton
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
helec1 : f electron = proton
helec2 : f proton = proton
helec3 : f neutron = proton
⊢ ∃ a, f a = neutron
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
helec1 : f electron = proton
helec2 : f proton = proton
helec3 : f neutron = proton
⊢ ∃ a, f a = electron
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
b : Subatomic
helec1 : f electron = proton
helec2 : f proton = proton
helec3 : f neutron = neutron
⊢ ∃ a, f a = b
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
b : Subatomic
helec1 : f electron = proton
helec2 : f proton = proton
helec3 : f neutron = electron
⊢ ∃ a, f a = b
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
b : Subatomic
helec1 : f electron = proton
helec2 : f proton = neutron
⊢ ∃ a, f a = b
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
b : Subatomic
helec1 : f electron = proton
helec2 : f proton = electron
⊢ ∃ a, f a = b
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
b : Subatomic
helec1 : f electron = neutron
⊢ ∃ a, f a = b
f : Subatomic → Subatomic
h : ∀ ⦃a₁ a₂ : Subatomic⦄, f a₁ = f a₂ → a₁ = a₂
b : Subatomic
helec1 : f electron = electron
⊢ ∃ a, f a = b

[Răzvan Flavius Panda]

Also cases b doesn't seem to do anything to the last few goals, it stays f a = b

[Aaron Liu]

like I said, there are multiple goals

[Aaron Liu]

here's a sample

    cases helec1 : f .electron with
    | proton =>
      cases helec2 : f .proton with
      | proton =>
        exfalso
        sorry
      | neutron =>
        cases helec3 : f .neutron with
        | proton =>
          exfalso
          sorry
        | neutron =>
          exfalso
          sorry
        | electron =>
          cases b with
          | proton =>
            sorry
          | neutron =>
            sorry
          | electron =>
            sorry
      | electron =>
        sorry
    | neutron =>
      sorry
    | electron =>
      sorry

[Răzvan Flavius Panda]

Yes, I see that but

[Aaron Liu]

you have to run your tactic on every goal

[Aaron Liu]

by default it only runs on the first goal

[Aaron Liu]

you can also just use the focusing dot like this

    cases helec1 : f .electron
    · sorry
    · sorry
    · sorry

but then you don't get to control what order they come out in

[Răzvan Flavius Panda]

This is some Cartesian product stuff. Trying to understand, I still don't get how to fill what you provided.

[Aaron Liu]

somehow I don't see cartesian products anywhere

[Răzvan Flavius Panda]

It's everything combined with everything.

[Aaron Liu]

oh yeah it is

[Aaron Liu]

the proof size blows up the more constructors you add

[Aaron Liu]

the advantage of developing finiteness is that you can reuse the same proof over and over

[Răzvan Flavius Panda]

Is this 3 ^ 4 total goals after I fill up everything above?

[Aaron Liu]

some of the branches get cut off early for being impossible

[Aaron Liu]

so it's a bit less than that

[Aaron Liu]

in particular every branch I put exfalso on is impossible without having to do any more casing

[Răzvan Flavius Panda]

What makes the branches be impossible?

[Aaron Liu]

the hypotheses you have can make a contradiction with h : Injective f

[Răzvan Flavius Panda]

So 2 argument values resolving to same function value?

[Aaron Liu]

yes

[Răzvan Flavius Panda]

What does exfalso do?

[Răzvan Flavius Panda]

I see you still put sorry after exfalso

[Aaron Liu]

changes the goal to False

[Aaron Liu]

the reason I still put sorry is because you still need to prove a contradiction

[Răzvan Flavius Panda]

Oh

[Aaron Liu]

I think probably after you finish the proofs you can remove the exfalso

[Răzvan Flavius Panda]

This proof is driving me insane.
I chose the wrong way to solve it.

[Răzvan Flavius Panda]

Aaron Liu said:

yes, unless you want to develop the theory of finiteness

How would this proof work?

[Aaron Liu]

developing finiteness takes probably at least twice as long depending on the exact way you do it

[Răzvan Flavius Panda]

The thing is, next exercise is the same thing but with a type that has 4 constructors:

example : ∀ f : Element → Element, Injective f → Bijective f := by

[Răzvan Flavius Panda]

Going through 4 ^ 4 combinations even with dead ends is a lot.

[Răzvan Flavius Panda]

I don't understand why the book did not choose an exercise with 2 constructors only. That would have been a gentle introduction to solving it.

[Răzvan Flavius Panda]

And in the end 2, 3, 4, etc. same thing just more work.

[Aaron Liu]

Răzvan Flavius Panda said:

Aaron Liu said:

yes, unless you want to develop the theory of finiteness

How would this proof work?

lots of steps, I had a go at this once (exact same problem), this is the plan I came up with

• define a type as finite if you can put all its elements into a List without missing any
• prove that finite type can't admit an injection from Nat
• prove that if f^[a + c] x = f^[b + c] x then f^[a] x = f^[b] x if f is injective
• prove that iterating an injective function from a finite type to itself sends every element in a loop
• show injective functions from a finite type to itself are surjective
• show that Subatomic and Element are finite

[Răzvan Flavius Panda]

Wow, yeah, that is a lot of things to prove.

[Răzvan Flavius Panda]

Ok, I think I will just skip this exercise for now and maybe come back to it when I get better at LEAN.

[Răzvan Flavius Panda]

I am kind of looking forward to working on another book. This book was good but felt like it was missing a lot of explanations.

[Răzvan Flavius Panda]

Thank you for the explanations.