ImmutableArray: add positivity, hasEq, decreases, new qualifier

tests/micro-benchmarks/TestImmutableArray.fst

@@ -5,6 +5,14 @@ open FStar.Tactics
 
 let test1 () = IA.of_list [0;1;2]
 
+// Decidable equality
+let _ = assert (test1 () = test1 ())
+
+let test_f () = IA.of_list [fun (x:int) -> x]
+
+[@@expect_failure]
+let _ = assert (test_f () = test_f ())
+
 let test2 () = assert_norm (IA.index (IA.of_list [0;1;2]) 1 == 1)
 
 let goal_is_true () : Tac unit = 
@@ -51,3 +59,6 @@ let test_length_correspondence (l:list 'a) = assert (IA.length (IA.of_list l) ==
 
 let test_index_correspondence (l:list 'a) (i:nat{ i < L.length l }) = assert (IA.index (IA.of_list l) i == L.index l i)
 
+noeq type test_pos =
+| Test : test_pos
+| Array : IA.t test_pos -> test_pos

ulib/FStar.ImmutableArray.Base.fsti

@@ -38,7 +38,14 @@
 module FStar.ImmutableArray.Base
 
 (* The main type of immutable arrays *)
-val t (a:Type u#a) : Type u#a
+new
+val t ([@@@strictly_positive] a:Type u#a) : Type u#a
+
+(* An array supports equality when its elements also do. *)
+val array_has_eq (a : Type) : Lemma
+  (requires hasEq a)
+  (ensures hasEq (t a))
+  [SMTPat (hasEq (t a))]
 
 (* Creating an immutable array from a list *)
 val of_list (#a:Type u#a) (l:list a) : Tot (t a)

ulib/FStar.ImmutableArray.fsti

@@ -60,3 +60,22 @@ val length_spec (#a:Type u#a) (s:t a)
 val index_spec (#a:Type u#a) (s:t a) (i:nat{ i < length s })
   : Lemma (index s i == FStar.List.Tot.index (to_list s) i)
           [SMTPat (index s i)]
+
+(* The list of elements precedes the array.*)
+val to_list_precedes (#a:Type u#a) (s:t a)
+  : Lemma (to_list s << s)
+
+(* Idem. *)
+let of_list_precedes (#a:Type u#a) (l:list a)
+  : Lemma (l << of_list l)
+  = to_list_precedes (of_list l)
+
+(* An explicit proof that elements of the array precede the array. *)
+let elem_precedes (#a:Type u#a) (s:t a) (i : nat{i < length s})
+  : Lemma (index s i << s)
+  = FStar.List.Tot.(
+      to_list_precedes s;
+      let l = to_list s in
+      assert (memP (index l i) l);
+      memP_precedes (index l i) l
+    )