Refutation by exhaustion for loop with early exit

Stream: general

[Mathias Sven]

There is a simple coding exercise that asks:

You are given an integer array nums with the following properties:

• nums.length == 2 * n.
• nums contains n + 1 unique elements.
• Exactly one element of nums is repeated n times.
  Return the element that is repeated n times.

Plus some additional constraints. My goal here was to take this Python solution:

def repeatedNTimes(nums: list[int]) -> int:
    for i in range(len(nums)):
        if nums[i - 1] == nums[i] or nums[i - 2] == nums[i]:
            return nums[i]

And prove that it is correct as is. Where "as is" would be a translation padded with additional witnesses to induce the proof.

def repeatedNTimes
  (nums : Array Int32)
  {n : ℕ}
  {h1 : 2 ≤ n ∧ n ≤ 5000}
  {h2 : nums.size = 2 * n}
  {h3 : ∀ i : Fin nums.size, 0 ≤ nums[i] ∧ nums[i] ≤ 10^4}
  {h4 : #nums.toList.toFinset = n + 1 ∧ ∃ v : Int32, nums.count v = n}
  : { v : Int32 // nums.count v = n } := Id.run do
  have instNeZero : NeZero nums.size := ⟨by omega⟩

  for h : i in [:nums.size] do
    -- Casting `i : ℕ` to `i : Fin nums.size` for wrap around
    let i := Fin.ofNat nums.size i
    if hf : nums[i - 1] == nums[i] || nums[i - 2] == nums[i] then
      return ⟨nums[i], is_solution nums (by omega) h2 h4 hf⟩

  have for_loop_concluded_no_return : ¬∃ i : Fin nums.size,
    nums[i - 1] == nums[i] || nums[i - 2] == nums[i] := by admit

  ⟨unreachable!, False.elim
    <| for_loop_concluded_no_return
    <| repeated_n_on_2n_prop nums h1.left h2 h4.right
  ⟩

This is at line 237 of my Proof. As I see it, the "interesting" parts of the proof were is_solution and repeated_n_on_2n_prop which asserts that given the constraints and for_loop_concluded_no_return, we have a contradiction.

My question then is, is it possible to arrive at for_loop_concluded_no_return while maintaining the for loop? Or would that require one to restructure the solution? From what I have seen, this should be possible with some sort of state added to the for loop, but I am not really sure where to start.

[Kim Morrison]

I think it is better (and also plausible!) to actually prove this really "as is", where you just write the function in Lean, with early return and no verification conditions, and then write the theorem you want about it as a separate declaration.

[Mathias Sven]

By separate declaration, do you mean a lemma that relates to the solution via "argumentation" and in which the wanted properties are proved? If that is the case, then I would say I am done, since I have already proved:

theorem repeated_n_on_2n_prop
  {α : Type} [DecidableEq α]
  (xs : Array α) [NeZero xs.size] {n : ℕ}
  (h1 : 2 ≤ n) (h2 : xs.size = 2 * n) (h3 : ∃ v : α, xs.count v = n) :
  ∃ i : Fin xs.size, xs[i - 1] == xs[i] || xs[i - 2] == xs[i]

And

theorem is_solution
  {α : Type} [DecidableEq α]
  (xs : Array α) [NeZero xs.size]
  {n : ℕ} {i : Fin xs.size}
  (h1 : 2 < xs.size)
  (h2 : xs.size = 2 * n)
  (h3 : #xs.toList.toFinset = n + 1 ∧ ∃ v : α, xs.count v = n)
  (h4 : xs[i - 1] == xs[i] || xs[i - 2] == xs[i]) :
  xs.count xs[i] = n

Which from what I can tell, is all you would need to show to "argue" the correctness of the solution. However, for this I thought it would be more interesting to code up a solution that is type checked correct onto itself. By "also plausible", do you mean to say that it is not possible to have for_loop_concluded_no_return while still keeping the for loop, or that it is impractical and would require a lot of work?

[Robin Arnez]

Here's how I'd solve this:

-- the lemmas `repeated_n_on_2n_prop` and `is_solution`
-- ...
def repeatedNTimes (nums : Array Int32) : Int32 := Id.run do
  for h : i in *...nums.size do
    -- Casting `i : ℕ` to `i : Fin nums.size` for wrap around
    have : NeZero nums.size := by constructor; rw [Std.Rio.mem_iff] at h; grind
    let i := Fin.ofNat nums.size i
    if nums[i - 1] == nums[i] || nums[i - 2] == nums[i] then
      return nums[i]
  unreachable!

open Std.Do
set_option mvcgen.warning false in
theorem repeatedNTimes_correct {nums : Array Int32} {n : Nat} {v : Int32}
    (h₁ : nums.size = 2 * n) (hn : 2 ≤ n)
    (h₂ : #nums.toList.toFinset = n + 1)
    (hv : nums.count v = n) :
    nums.count (repeatedNTimes nums) = n := by
  have : NeZero nums.size := by constructor; grind
  generalize h : repeatedNTimes nums = x
  apply Id.of_wp_run_eq h
  mvcgen invariants
  · Invariant.withEarlyReturn (onReturn := fun r _ => ⌜nums.count r = n⌝)
      (onContinue := fun xs _ => ⌜∀ i ∈ xs.prefix, let i := Fin.ofNat nums.size i;
        (nums[i - 1]! == nums[i]! || nums[i - 2]! == nums[i]!) = false⌝)
  case vc1.step.isTrue i hi _ =>
    suffices nums.count nums[i] = n by simpa
    exact is_solution nums (by grind) h₁ ⟨h₂, v, hv⟩ hi
  case vc2.step.isFalse => grind
  case vc3.a.pre => simp
  case vc4.a.post.success.h_1 h h' =>
    obtain ⟨i, hi⟩ := repeated_n_on_2n_prop nums hn h₁ ⟨v, hv⟩
    absurd hi
    simp only [h, Nat.toList_rio_eq_toList_rco, Std.Rco.mem_toList_iff_mem, Std.Rco.mem_iff,
      zero_le, true_and, Fin.ofNat_eq_cast, Fin.is_lt, getElem!_pos, Fin.getElem_fin,
      Fin.getElem!_fin, Fin.val_natCast, Bool.or_eq_false_iff, beq_eq_false_iff_ne, ne_eq,
      reduceCtorEq, false_and, exists_const, or_false] at h'
    specialize h' i.1 i.2
    simpa [Nat.mod_eq_of_lt] using h'
  case vc5.a.post.success.h_2 => grind

[Robin Arnez]

You can read more at https://lean-lang.org/doc/reference/latest/The--mvcgen--tactic/Tutorial___-Verifying-Imperative-Programs-Using--mvcgen/#mvcgen-tactic-tutorial

[Mathias Sven]

I didn't know about mvcgen until now. I haven't read much into it yet, but it seems to be exactly* what I was looking for... Thanks for giving this example

*I mean I just wanted a principled way to prove properties of imperative programs. It would still be nice to somehow do it like I did and have a feature that would bring that kinda of statement in or state keeping track of things. But given that it seems the purpose of this tool is to address this kinda of problem, it seems silly to try to hack something together

[Kim Morrison]

mvcgen is fairly new, and while it's hopefully a good robust foundation, we're still hoping to make it much more user friendly (and have more and better tutorials!)