[WP] adds an improvement of the simplifier for eq_sequence

src/plugins/wp/Vlist.ml

@@ -195,7 +195,14 @@ let rec leftmost a ms =
   | L.Fun( repeat , [ u ; n ] ) when repeat == f_repeat -> begin
       let exception RetryOnUnfold in
       try (* tries to perform some rolling that do not depend on [n] *)
-        raise RetryOnUnfold
+        match ms with
+        | b::ms ->
+            let b,ms = leftmost b ms in
+            let u,us = leftmost u [] in
+            if not (F.decide (F.e_eq u b)) then raise RetryOnUnfold;
+            (*  u=b ==>  ((u^us)*^n) ^ b ^ ms  == u ^ (us^b)*^n) ^ ms *)
+            u, v_repeat (v_concat (us@[b]) (F.typeof a)) n :: ms
+        | _ -> raise RetryOnUnfold
       with RetryOnUnfold ->
         if F.decide (F.e_lt F.e_zero n) then
           (* 0<n ==> (u*^n) ^ ms ==  u ^ (u*^(n-1)) ^ ms *)

src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle

@@ -33,7 +33,7 @@ Prove: (0<=k_0) -> (k_0<(3*(length x_0)))
 ------------------------------------------------------------
 
 Lemma concat_repeat_swap:
-Prove: let a_0 = (repeat x_0 k_0) in (concat a_0 x_0)=(concat x_0 a_0)
+Prove: (repeat x_0 k_0)=(repeat x_0 k_0)
 
 ------------------------------------------------------------