Questions: what proofs are needed to prove the equivalence between two sorted lists?

[RabbitDong-on]

Hi, i try to prove equivalence between two sorted lists, but the assertion fails. I looks like that i fail to provide some proofs.
Program

def test(numbers:List[int])->List[int]:
    Requires(list_pred(numbers))
    Requires(len(numbers)>0)
    Ensures(list_pred(numbers))
    Ensures(list_pred(Result()))
    Ensures(len(Result())==len(numbers))
    Ensures(Forall(int, lambda i: (Implies(i >= 0 and i < len(Result())-1, Result()[i]<=Result()[i+1]))))
    numbers_sorted:List[int]=sorted(numbers)
    Assert(len(numbers)>0)
    Assert(len(numbers)==len(Old(numbers)))
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(numbers),numbers[i]==Old(numbers)[i]))))
    numbers_sorted2:List[int]=sorted(numbers)
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(numbers_sorted)-1,numbers_sorted[i]<=numbers_sorted[i+1]))))
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(numbers_sorted2)-1,numbers_sorted2[i]<=numbers_sorted2[i+1]))))
    sort1=ToSeq(numbers_sorted)
    sort2=ToSeq(numbers_sorted2)
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(sort1)-1,sort1[i]<=sort1[i+1]))))
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(sort2)-1,sort2[i]<=sort2[i+1]))))
    Assert(Forall(int,lambda i: (Implies(i >= 0 and i < len(numbers), numbers_sorted[i]==sort1[i]), [[sort1[i]]])))
    Assert(Forall(int,lambda i: (Implies(i >= 0 and i < len(numbers), numbers_sorted2[i]==sort2[i]), [[sort2[i]]])))
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(sort1),sort1[i]==sort2[i])))) # this assertion fails
    return numbers_sorted

Error messages

Verification failed
Errors:
Assert might fail. Assertion Forall(int, (lambda i: Implies(((i >= 0) and (i < len(sort1))), (sort1[i] == sort2[i])))) might not hold. (learn_example.py@32.11--32.85).
Old store:
  numbers -> list<int>0
Old heap:
  list<int>0 -> { len(list<int>0) -> 2, list<int>0[0] -> 4419, list<int>0[1] -> 9698 }
Current store:
  numbers_sorted -> list<int>1,
  numbers_sorted2 -> list<int>2,
  sort1 -> Sequence: { len(sort1) -> 2, sort1[0] -> -11, sort1[1] -> 13275, sort1[(- 3062)] -> -8678, sort1[9699] -> -985, sort1[9698] -> -1814 },
  sort2 -> Sequence: { len(sort2) -> 2, sort2[9698] -> -8389, sort2[1] -> 13274, sort2[2] -> 19971, sort2[(- 3062)] -> -1, sort2[0] -> True, sort2[9699] -> -3064 },
  numbers -> list<int>0,
  Result() -> list<int>3
Current heap:
  list<int>2 -> { len(list<int>2) -> 2, list<int>2[9698] -> -8389, list<int>2[1] -> 13274, list<int>2[2] -> 19971, list<int>2[(- 3062)] -> -1, list<int>2[0] -> True, list<int>2[9699] -> -3064 },
  list<int>1 -> { len(list<int>1) -> 2, list<int>1[0] -> -11, list<int>1[1] -> 13275, list<int>1[(- 3062)] -> -8678, list<int>1[9699] -> -985, list<int>1[9698] -> -1814 },
  list<int>0 -> { len(list<int>0) -> 2, list<int>0[0] -> 4419, list<int>0[1] -> 9698 }

Verification took 86.36 seconds.

Question: What proofs are needed to prove the equivalence between two sorted lists?
Any suggestions are greatly appreciated.

[viper-admin]

Basically, you'd need to write a lemma (i.e. a function) somewhat like this:

def sortedEquivalentLemma(s1: PSeq[int], s2: PSeq[int]) -> None:
  Requires(ToMS(s1) == ToMS(s2))
  Requires(... both are sorted)
  Ensures(s1 == s2)
  # proof here, probably by induction (i.e. a recursive call of this lemma) somehow

[RabbitDong-on]

Thanks a lot! I will try this method.

[RabbitDong-on]

I have tried this method, but i failed to write a correct lemma.
Program:

def sorted_equivalence_lemma(s1:PSeq[int],s2:PSeq[int])->None:
    Requires(ToMS(s1)==ToMS(s2))
    Requires(Forall(int, lambda i:(Implies(i>=0 and i<len(s1)-1,s1[i]<=s1[i+1]))))
    Requires(Forall(int, lambda i:(Implies(i>=0 and i<len(s2)-1,s2[i]<=s2[i+1]))))
    Ensures(s1==s2)
    if len(s1)==1:
        Assert(s1[0]==s2[0])
    else:
        # prove that s1[0]==s2[0]
        Assert(s1[0]==s2[0])
        # prove that s1[1:...]==s2[1:...]
        sorted_equivalence_lemma(s1.drop(1),s2.drop(1))

def test(numbers:List[int])->List[int]:
    Requires(list_pred(numbers))
    Requires(len(numbers)>0)
    Ensures(list_pred(numbers))
    Ensures(list_pred(Result()))
    Ensures(len(Result())==len(numbers))
    Ensures(Forall(int, lambda i: (Implies(i >= 0 and i < len(Result())-1, Result()[i]<=Result()[i+1]))))
    numbers_sorted:List[int]=sorted(numbers)

    # numbers does not change
    Assert(len(numbers)>0)
    Assert(len(numbers)==len(Old(numbers)))
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(numbers),numbers[i]==Old(numbers)[i]))))
    numbers_sorted2:List[int]=sorted(numbers)

    # prove that array is sorted
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(numbers_sorted)-1,numbers_sorted[i]<=numbers_sorted[i+1]))))
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(numbers_sorted2)-1,numbers_sorted2[i]<=numbers_sorted2[i+1]))))

    sort1=ToSeq(numbers_sorted)
    sort2=ToSeq(numbers_sorted2)
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(sort1)-1,sort1[i]<=sort1[i+1]))))
    Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(sort2)-1,sort2[i]<=sort2[i+1]))))
    Assert(Forall(int,lambda i: (Implies(i >= 0 and i < len(numbers), numbers_sorted[i]==sort1[i]), [[sort1[i]]])))
    Assert(Forall(int,lambda i: (Implies(i >= 0 and i < len(numbers), numbers_sorted2[i]==sort2[i]), [[sort2[i]]])))
    sorted_equivalence_lemma(sort1,sort2)
    # Assert(Forall(int,lambda i:(Implies(i>=0 and i < len(sort1),sort1[i]==sort2[i])))) # this assertion fails
    return numbers_sorted

The error messages are confusing. Requires(ToMS(s1)==ToMS(s2)) cannot guarantee that elements in s1 and s2 are same.
Specifically, True in s1 and -975 in s2 are not equal.
Errors:

Verification failed
Errors:
Assert might fail. Assertion (s1[0] == s2[0]) might not hold. (learn_example.py@66.15--66.27).
Old store:
  s1 -> Sequence: { len(s1) -> 1, s1[0] -> True },
  s2 -> Sequence: { len(s2) -> 1, s2[0] -> -975 }
Old heap: Empty.
Current store:
  s1 -> Sequence: { len(s1) -> 1, s1[0] -> True },
  s2 -> Sequence: { len(s2) -> 1, s2[0] -> -975 }
Current heap: Empty.

Verification took 47.13 seconds.

How to improve this lemma to prove s1==s2? Any suggestions are greatly appreciated.