how to avoid 27 sub-proofs

Stream: new members

[rzeta0]

I'm doing an 8.2.8 ex 4 from MoP on Functions.

It seems I need to provide 27 sub-proofs! That can't be right.

Question: Normally I'd use the <;> structure to repeat a proof but that doesn't seem application here. Help!

The exercise asks us to use the approach from an earlier example which does indeed provide 4 sub-proofs covering all the possible combinations.

27 sub-proofs !

example : ∀ f : Subatomic → Subatomic, Injective f → Bijective f := by
  dsimp [Bijective, Injective, Surjective]
  intro f h
  constructor
  · -- injective
    exact h
  · -- surjective
    intro y
    match h_p : f proton, h_n: f neutron, h_e : f electron with
    | electron, electron, electron =>
      have x: electron = proton := by
        apply h
        rw [h_e, h_p]
      contradiction
      --
    | electron, electron, neutron => sorry
    | electron, electron, proton => sorry
    | electron, neutron, electron => sorry
    | electron, neutron, neutron => sorry
    | electron, neutron, proton => sorry
    | electron, proton, electron => sorry
    | electron, proton, neutron => sorry
    | electron, proton, proton => sorry
    | neutron, electron, electron => sorry
    | neutron, electron, neutron => sorry
    | neutron, electron, proton => sorry
    | neutron, neutron, electron => sorry
    | neutron, neutron, neutron => sorry
    | neutron, neutron, proton => sorry
    | neutron, proton, electron => sorry
    | neutron, proton, neutron => sorry
    | neutron, proton, proton => sorry
    | proton, electron, electron => sorry
    | proton, electron, neutron => sorry
    | proton, electron, proton => sorry
    | proton, neutron, electron => sorry
    | proton, neutron, neutron => sorry
    | proton, neutron, proton => sorry
    | proton, proton, electron => sorry
    | proton, proton, neutron => sorry
    | proton, proton, proton => sorry

---

for clarity, Subatomic is defined as

inductive Subatomic
  | proton
  | neutron
  | electron
  deriving DecidableEq

[Eric Wieser]

(inside a spoiler block, you need a ```lean4 - can you edit your post?)

[rzeta0]

(deleted)

[rzeta0]

Hi @Eric Wieser done

[Kyle Miller]

rzeta0 said:

It seems I need to provide 27 sub-proofs! That can't be right.

I don't know, the parenthetical here seems consistent with that:

This is like Example 8.2.6 and the previous exercise, but with even more (frankly, way too many ….) cases to check.

(From the exercises)

[Eric Wieser]

That parenthetical is from the exercise after the one in question, but indeed it is surely asking you to find a different way

[Kyle Miller]

Ah, you're right.

[Eric Wieser]

rzeta0 said:

Normally I'd use the <;> structure to repeat a proof but that doesn't seem application here. Help!

You can use cases h_p : f proton <;> cases h_n : f neutron <;> cases h_e : f electron to get yourself in a state where you can add more <;>s or use all_goals

[Kyle Miller]

Question for you @rzeta0: It suggests following the solution to https://hrmacbeth.github.io/math2001/08_Functions.html#bij-card2, which does cases on two values, but you do cases on three values. Both are Injective f → Bijective f proofs. Why is the number of discriminants different in your solution?

Should two versus three need to depend on the specific type?

[rzeta0]

@Kyle - yes the type has 3 elements. (I updated the OP to list them)

inductive Subatomic
  | proton
  | neutron
  | electron
  deriving DecidableEq

[Kyle Miller]

Oh, I see, I misread the solution's structure. Never mind. I thought something different was going on.

[Kyle Miller]

What I was trying to get at is, if it's proved in a different way, the number of columns in the match depends only on the number of quantifiers, not the number of constructors for the type.

[rzeta0]

I think you may be onto something there. I can see that if two of the variables are the same, the proof is always by contradiction but I can't see how to use that to reduce the size of the proof.

[rzeta0]

I'm 99% certain the course author doesn't want us to write 27 proofs. The final exercise has $4^4=256$ cases !

I'm pretty sure she is encouraging us to be "lazy in a good way" mathematicians. I will sleep on this and try again tomorrow.

[Eric Wieser]

I was able to get the <;> version working; do you want a hint?

This tactic, and others like it, is quite helpful when repeated on every goal

all_goals
  try have := h_p.trans h_n.symm

[Aaron Liu]

There are like 5 levels of automation you can do here

[Derek Rhodes]

By the way, MoP has a tactic called "exhaust" which is based on "duper" (as mentioned in the transitioning section)

[rzeta0]

Hi Derek - yes we've been introduced to exhaust using the following pattern:

intro x
  cases x <;> exhaust

however here the cases would need to be the 'same' in the sense they can all be resolved by exhaust which we're told can resolve true/false.
.
Sadly I can't see how it is applicable here. I'll keep trying

[Damiano Testa]

I realise that this is probably not the intended solution, but, since I imagine that this is a learning exercise, this is how I would do it:

-- this instance is used in the `example` below
deriving instance Fintype for Subatomic

example : ∀ f : Subatomic → Subatomic, Injective f → Bijective f :=
  fun _ => Finite.injective_iff_bijective.mp

[Derek Rhodes]

Here's a take in a direction towards the spirit of MoP restrictions. (Looking back through my work, I did not manage to solve the case for an inductive type with three constructors.) But here is a smaller example.

This finds two groups of cases and uses all_goals and try. (I was trying to find a way to reorder the goals into groups then take them out in batches, but all_goals and try seems like the way to go).

It does not solve the problem to my satisfaction because it uses tauto at the end. But I think with some more work it may generalize to the 3 element problem.

import Mathlib

inductive Alpha | A | B deriving DecidableEq
open Function Alpha

example : ∀ f : Alpha → Alpha, Injective f → Bijective f := by
  intro f hf
  constructor
  · -- `f` is injective by assumption
    apply hf
  . -- show that `f` is surjective
    intro c
    cases ha : f A <;> cases hb : f B

    -- cases for when f A = f B
    all_goals try
      have : A = B := by
        apply hf
        rw [ha, hb]
      contradiction

    -- cases for when f A ≠ f B
    all_goals try
      cases c <;> tauto  --<-- cheating with tauto