add simple instances for lookup of list that results in an evar

theories/lithium/simpl_instances.v

@@ -455,6 +455,18 @@ Proof.
   rewrite list_lookup_insert_Some. naive_solver.
 Qed.
 
+Global Instance simpl_and_lookup_protected {A} (l : list A) (i : nat) v `{!IsProtected v} `{Inhabited A}:
+  SimplAndRel (=) (l !! i) (Some v) (λ T, i < length l ∧ v = l !!! i ∧ T).
+Proof.
+  split.
+  - move => -[? [-> ?]]. split; [|done]. apply: list_lookup_lookup_total_lt. lia.
+  - move => [/list_lookup_alt ?]. naive_solver lia.
+Qed.
+
+Global Instance simpl_and_lookup_lookup_total {A} (l : list A) (i : nat) `{Inhabited A}:
+  SimplBothRel (=) (l !! i) (Some (l !!! i)) (i < length l).
+Proof. rewrite /SimplBothRel list_lookup_alt. naive_solver lia. Qed.
+
 Global Instance simpl_learn_insert_some_len_impl {A} l i (x : A) :
   (* The false is important here as we learn additional information,
   but don't want to get stuck in an endless loop. *)

tutorial/t07_arrays.c

@@ -16,6 +16,15 @@ void permute(int* ar, int i, int j){
   ar[j] = k;
 }
 
+[[rc::parameters("ar : loc", "elts : {list Z}", "n : nat")]]
+[[rc::args("ar @ &own<array<i32, {elts `at_type` (int i32)}>>", "n @ int<i32>")]]
+[[rc::requires("{2 < length elts}")]]
+[[rc::ensures("own ar : array<i32, {elts `at_type` (int i32)}>")]]
+void use_permute(int* ar, int n) {
+  permute(ar, 1, 2);
+  permute(ar, 1, 2);
+}
+
 [[rc::parameters("ar : loc", "elts : {list Z}", "n : nat")]]
 [[rc::args("ar @&own<array<i32, {elts `at_type` (int i32)}>>")]]
 [[rc::args("n @ int<i32>")]]