Proving the jealous mathematician riddle

Stream: new members

[Willem vanhulle]

I am working on solving the jealous mathematician riddle. I have managed to state the problem, the required properties of the solution and a solution.

I can prove that individual steps of the solution to the problem are mostly correct on first sight.

When I try to prove that each step in the solution does not break the contract, I run into a problem. I don't know how to proof that all elements of a generated state vector satisfy some property.

The source code is here:
https://github.com/wvhulle/riddle-proofs/blob/main/RiddleProofs/JealousMath.lean

I am stuck with the proof

theorem all_states_safe : ∀ i : Fin 11, safe (solution_states.get i) := by
  sorry

I have tried rcases and fin_cases (from Mathlib) but it does not work out. I feel like I am doing something wrong?

[Aaron Liu]

Did you intro i first?

[Willem vanhulle]

Aaron Liu zei:

Did you intro i first?

Yes, I have done that

[Aaron Liu]

What exactly is being a problem?

[Willem vanhulle]

I have tried many different styles of proofs. I would like to prove that the solution state at time i is always correct. (No notebooks left-behind for other mathematicians). I am struggling with the inductive step.

[Willem vanhulle]

I have a feeling the recursive statement of the solution might be causing problems

[Willem vanhulle]

I can prove that the first state in the problem and the last step are safe, but not the 9 intermediate states.

[Aaron Liu]

Sorry, I still don't quite understand. What about the nine intermediate states makes it hard to show they are safe? Did you try unfolding everything?

By the way, I noticed that your solution_state_at function has its termination shown by well-founded recursion. This makes it irreducible, which could be a problem for automation.

[Willem vanhulle]

So the solution to mathematician riddle looks like this

def solution_cross_vec : Vector (State → State) 11 :=
  Vector.ofFn (fun
    | 0 => move_math 0 right ▷ move_notebook 0 right ▷ move_boat right
    | 1 => move_math 0 left ▷ move_notebook 0 left ▷ move_boat left
    | 2 => move_math 1 right ▷ move_notebook 1 right ▷ move_boat right
    | 3 => move_math 0 right ▷ move_notebook 0 right ▷ move_boat right
    | 4 => move_math 2 right ▷ move_notebook 2 right ▷ move_boat right
    | 5 => move_math 0 left ▷ move_notebook 0 left ▷ move_boat left
    | 6 => move_math 0 right ▷ move_notebook 0 right ▷ move_boat right
    | 7 => move_math 1 left ▷ move_notebook 1 left ▷ move_boat left
    | 8 => move_math 1 right ▷ move_notebook 1 right ▷ move_boat right
    | 9 => move_math 0 left ▷ move_notebook 0 left ▷ move_boat left
    | 10 => move_math 0 right ▷ move_notebook 0 right)

I am trying to prove by induction or fin_cases on the step but unfolding always get stuck I think

[Willem vanhulle]

Solution state is computed recursively based on these "crossings"

def solution_state_at : Fin 11 → State
| ⟨0, _⟩ => all_left
| ⟨n+1, h⟩ =>
  have n_lt_9 : n < 11 := by
    have : n + 1 < 11 := h
    cases Nat.lt_or_ge n 11 with
    | inl hlt => exact hlt
    | inr hge =>
      exact Nat.lt_of_succ_lt h
  (solution_cross_vec.get ⟨n, n_lt_9⟩) (solution_state_at ⟨n, Nat.lt_of_succ_lt h⟩)

[Willem vanhulle]

Did I do something wrong?

[Aaron Liu]

What goes wrong during unfolding?

[Willem vanhulle]

When I try this:

theorem all_states_safe : ∀ i : Fin 11, safe (solution_states.get i) := by
  intro state_i
  fin_cases state_i <;> (
    simp
    unfold solution_states
  )

I get these leftover cases

unsolved goals
case «0»
⊢ safe ((Vector.ofFn solution_state_at).get 0)


case «1»
⊢ safe ((Vector.ofFn solution_state_at).get 1)


case «2»
⊢ safe ((Vector.ofFn solution_state_at).get 2)

I don't know whether I should use unfold or simp

[Willem vanhulle]

Also, the fact my safe property expects i, j i \neq j makes it very nested

[Aaron Liu]

docs#Vector.get_ofFn

[Willem vanhulle]

I tried this

theorem all_states_safe : ∀ i : Fin 11, safe (solution_states.get i) := by
  intro i
  simp [Vector.get_ofFn]

Also imported the module but it cant make any progress

[Willem vanhulle]

I made a little progress with

theorem all_states_safe : ∀ i : Fin 11, safe (solution_states.get i) := by
  intro i
  fin_cases i <;> (
    unfold solution_states
    simp [Vector.get_ofFn _]
    repeat
      unfold solution_state_at
      unfold solution_cros_vec
      simp [Vector.get_ofFn _]


  )

[Aaron Liu]

etc etc

def solution_state_atAux : (n : Nat) → n < 11 → State
| 0, _ => all_left
| n+1, h =>
  have n_lt_9 : n < 11 := by
    have : n + 1 < 11 := h
    cases Nat.lt_or_ge n 11 with
    | inl hlt => exact hlt
    | inr hge =>
      exact Nat.lt_of_succ_lt h
  (solution_cross_vec.get ⟨n, n_lt_9⟩) (solution_state_atAux n <| Nat.lt_of_succ_lt h)
-- Helper function to compute state at step i
def solution_state_at : Fin 11 → State := fun f => solution_state_atAux f.val f.isLt

etc etc

instance : DecidablePred safe := by
  unfold safe
  infer_instance

theorem all_states_safe : ∀ i : Fin 11, safe (solution_states.get i) := by
  decide

[Willem vanhulle]

Thanks a lot @Aaron Liu that seems to fix it. What was the main thing you changed?

[Willem vanhulle]

Is it because you made safe decidable?

[Aaron Liu]

maybe?

[Willem vanhulle]

Now I can clean it up. I probably will try to get rid of the constant numeral 11

[Notification Bot]

This topic was moved here from #metaprogramming / tactics > Proving the jealous mathematician riddle by Patrick Massot.

[Willem vanhulle]

@Aaron Liu do you know why your solution works with aux but when I merge the two functions I get problems with decidability?

[Aaron Liu]

It's because when you merge the two you are now defining the function by well founded recursion which is irreducible

[Willem vanhulle]

What exactly is breaking well founded recursion?

[Aaron Liu]

I don't understand what you mean by that, can you elaborate a bit?

[Willem vanhulle]

Isn’t welfounded recursion just checking that recursive calls are only applied to a smaller part of the outer argument? When I merge both I still see n+1 and at the end n as argument so it seems to me like it is still well founded recursion?

[Aaron Liu]

No, it was using structural recursion when they're separated (which is not irreducible) but when you merge them it switches to using well-founded recursion (which is irreducible)

[Aaron Liu]

decide will not unfold irreducible things