Proof on recursive function of List of Int

Stream: new members

[Gaëtan Serré]

Hello, I wrote a function that takes a List of Int and removes the consecutive elements that sum to 0 (if the list contains 0, it removes it):

def irre (l : List ℤ) :=
  let rec aux (l : List ℤ) (acc : List ℤ) :=
    match l with
    | [] => acc
    | hd::[] => if hd = 0 then acc else acc.concat hd
    | hd1::hd2::tl =>
      if hd1 + hd2 = 0 then aux tl acc
      else if hd1 = 0 then aux (hd2::tl) acc
      else if hd2 = 0 then aux (hd1::tl) acc
      else aux (hd2::tl) (acc.concat hd1)
  aux l []

I want to prove that my statement is true, that is:

example (l : List ℤ) :
  if h : 1 < (irre l).length then ∀ (i : Fin (irre l).length), ((irre l).get i) + ((irre l).get (i + {val:=1, isLt:=h})) ≠ 0
  else if h : (irre l).length = 1 then (irre l).get {val:=0, isLt:=by rw[h]; exact Nat.zero_lt_one} ≠ 0
  else l = [] := by
  induction l with
  | nil =>
    split
    · contradiction
    next h =>
      push_neg at h
      split
      · contradiction
      rfl
  | cons hd tl h =>
    sorry

I think the statement definition is pretty heavy and that my irre function could be simpler. Moreover, I started an induction on l, the initial case is easy but the induction step will be a mess, with a lot of nested cases. Do you have any advice on how to prove this more easely?

[Matt Diamond]

it might be easier if you define the function without using a second accumulator list:

def irre (l : List ℤ) :=
  match l with
  | [] => []
  | hd::[] => if hd = 0 then [] else [hd]
  | hd1::hd2::tl =>
    if hd1 + hd2 = 0 then irre tl
    else if hd1 = 0 then irre (hd2::tl)
    else if hd2 = 0 then irre (hd1::tl)
    else hd1::(irre (hd2::tl))

[Matt Diamond]

I'm also confused about your example proof, as it appears to be checking if the products of consecutive elements equal one, not that sums of consecutive elements equal 0

[Gaëtan Serré]

Thanks for the advice, indeed using an accumulator makes the proof more complicated

[Gaëtan Serré]

Matt Diamond said:

I'm also confused about your example proof, as it appears to be checking if the products of consecutive elements equal one, not that sums of consecutive elements equal 0

Indeed, sorry for that.. The reason is because I try to prove a generalised version of my statement for group and I forgot to change it when copy pasting the mwe. I edited it

[Matt Diamond]

@Gaëtan Serré I was thinking about this more and your irre function doesn't really accomplish what you want it to. For example, if you run irre [1, 1, -1, -1] you end up with [1, -1] because it only eliminates the middle two entries.

[Gaëtan Serré]

Oh yes you're totally right, thanks again for noticing that. I need a way to ensure thathd and tl.head do not cancel each other when constructing hd::tl. I did not had time to work on the proof neither the function today, but I'll try to provide a working function soon

[Gaëtan Serré]

Thank you again for your help

[Matt Diamond]

I think you'll have an easier time if you separate the task of filtering out zero from the task of filtering out pairs that sum to zero. This implementation seems to work correctly:

def irre_aux (l : List ℤ) :=
  match l with
  | [] => []
  | hd :: rest =>
    match irre_aux rest with
    | [] => [hd]
    | hd' :: rest' =>
    if hd + hd' = 0 then rest'
    else hd :: hd' :: rest'

def irre (l : List ℤ) := irre_aux (l.filter (· ≠ 0))

[Matt Diamond]

I also noticed that your theorem statement only seems to check for pairs that sum to 0 in the 1 < (irre l).length case, but it doesn't say anything about the absence of 0 more generally (except in the case where length = 1)

[Matt Diamond]

if you don't actually care about zeroes except in the length = 1 case, then my implementation isn't correct, as it filters out all zeroes

you said "if the list contains 0, it removes it"... did you mean "if the list only contains 0, it removes it"?

if so, it would be a pretty easy change to make... just replace irre_aux (l.filter (· ≠ 0)) with something like let result := irre_aux l; if l = [0] then [] else l

[Gaëtan Serré]

Thank you for your implementation, that's exactly what I need!

[Gaëtan Serré]

Matt Diamond said:

you said "if the list contains 0, it removes it"... did you mean "if the list only contains 0, it removes it"?

I meant that any 0 should be removed from the list (as l.filter (· ≠ 0) does). However, you're right, the statement do not check anything about that. The reason is that it is not necessary for what follows to remove the 0s, but it seemed to me more natural to remove it in the implementation (I hope that's makes sense)

[Markus Schmaus]

Especially for recursive functions, I find it easier to put the theorem in the function signature using Subtype and prove it when constructing the return values. docs#Nat.findX is an example of this in Mathlib.

[Gaëtan Serré]

That's a good idea, thank you!