Decidable equality for ImmutableArray type?

[mushrm88]

Is there any reason why the new ImmutableArray type can't have decidable equality?

As a workaround, for now I am just making an assumption:

val array_eq (a : Type) : Lemma
  (requires hasEq a)
  (ensures hasEq (FStar.ImmutableArray.t a))
  [SMTPat (FStar.ImmutableArray.t a)]

Is this safe and is there a better way of doing this?

I am using F* 2022.11.19~dev

[nikswamy]

This does look like a reasonable property to assume. ImmutableArray is implemented as an OCaml array and comparing them in F* with (=) will boil down to structural comparison element-wise in OCaml.

If you did not want to use this as an axiom, you can use something like what's below to prove the correctness of your own structural comparison of immutable arrays.

module IA = FStar.ImmutableArray
module L = FStar.List.Tot

let immutable_array_index_extensionality (#a:eqtype) (x y: IA.t a)
  : Lemma
    (requires
       IA.length x = IA.length y /\
      (forall (i:nat { i < IA.length x}). IA.index x i == IA.index y i))
    (ensures
      x == y)
  = let open IA in
    assert (forall (i:nat{ i < IA.length x}). L.index (to_list x) i == L.index (to_list y) i);
    L.index_extensionality (to_list x) (to_list y);
    of_list_to_list x;
    of_list_to_list y

let compare (#a:eqtype) (x: IA.t a) (y:IA.t a { IA.length x == IA.length y})
  : b:bool { b <==>  (x == y) }
  = let rec aux (i:nat {i <= IA.length x /\ (forall (j:nat { j < i }). IA.index x j == IA.index y j)})
      : Tot (b:bool { b <==>  (forall (j:nat { j < IA.length x }). IA.index x j == IA.index y j)})
            (decreases (IA.length x - i))
      = if i = IA.length x then true
        else if IA.index x i = IA.index y i
        then aux (i + 1)
        else false
    in
    let b = aux 0 in
    if b then immutable_array_index_extensionality x y;
    b

That said, since FStar.ImmutableArray is a primitive F* type, adding your assumed lemmas as an axiom about this type is likely to be broadly useful and more convenient to use than the compare function above. I'll add it to library.

[mushrm88]

That would be great! I have two other issues related to ImmutableArray:

1. Positivity checking doesn't work the way I'd expect.

noeq type test =
| Test : test
| Array : FStar.ImmutableArray.t test -> test

This doesn't work. Until recently I was able to work around this with a mutually inductive type but apparently that was a bug. It used to work inconsistently in other cases as well.

Is there a reason this doesn't pass the positivity checker?

2. Array members don't precede the array.

I ended up making some additional assumptions about precedence. For example, if something precedes a list, ls, then it should also precede ImmutableArray.of_list(ls).

Maybe it is possible to prove these properties without assumptions? Maybe the assumptions are incorrect?

I can open separate issues for these if that would be better.