How to prove properties about multiset?

[ChuyueSun]

predicate post_original<a(==)>(a: array<a>,key: a,b:bool)
reads a
{
( (multiset(a[..])[key] ==1 ) <==> b)
}

predicate post_gen<a(==)>(a: array<a>,key: a,b:bool)
reads a
{
(b <==> (exists i :: 0 <= i < a.Length && a[i] == key 
&& forall j :: 0 <= j < a.Length && j != i ==> a[j] != key))
}

lemma post_eq<a(==)>(a: array<a>,key: a,b:bool) 
        ensures post_original(a,key,b ) <==> post_gen(a,key,b ) 
 {
}

How to prove the lemma?

[rdivyanshu]

Hi @ChuyueSun, Please look into following code snippet to achieve this.
Few modifications I have done

• Renamed type parameter a to T for better readability
• Removed parameter b from both predicate. These two encoding are equivalent.

predicate post_original<T(==)>(a: array<T>, key: T)
  reads a
{
  (multiset(a[..])[key] == 1)
}

predicate post_gen<T(==)>(a: array<T>, key: T)
  reads a
{
  (exists i :: 0 <= i < a.Length && a[i] == key && (forall j :: 0 <= j < a.Length && j != i ==> a[j] != key))
}

lemma post_eq<T>(a: array<T>, key: T)
  ensures post_original(a, key) <==> post_gen(a, key)
{
  if post_original(a, key) {
    var i :| 0 <= i < a.Length && a[i] == key;
    assert a[..] == a[..i] + [a[i]] + a[(i+1)..];
  }
  if post_gen(a, key) {
    var i :| 0 <= i < a.Length && a[i] == key && (forall j :: 0 <= j < a.Length && j != i ==> a[j] != key);
    assert a[..] == a[..i] + [a[i]] + a[(i+1)..];
  }
}