reimplementation of `allperms` uncovered EasyCrypt (?) error

[alleystoughton]

PR #970 gives us the following behavior. Seems like a bug in EasyCrypt itself?

require import AllCore List Perms.

print allperms_r.
(*
op allperms_r ['a] (n : unit list)
  (s : 'a list) : 'a list list = 
  with n = "[]" => [[]]
  with n = (::) x n0 => flatten
                          (map
                             (fun (x0 : 'a) =>
                                map ((::) x0) (allperms_r n0 (rem x0 s)))
                             (undup s)).
*)

lemma foo (ns ms : int list) :
  ms \in allperms ns.
proof.
rewrite /allperms.
(* ms \in allperms_r (nseq (size ns) tt) ns *)
smt().
(* Ident Top_Perms_allperms_r is not yet declared *)

[alleystoughton]

Not sure if it'll help, but here is an even more minimal example:

require import AllCore List.

op g (x : int list) : int = 3.

op f (n : unit list) : int = 
  with n = "[]"    => 3
  with n = _ :: n0 => g (map (fun (_ : unit) => f n0) [tt]).

lemma foo  : f (nseq 0 tt) = 4.
proof.
smt().
(* Ident Top_f is not yet declared *)

Almost anything I do to this causes the problem to go away. E.g., replacing neq 0 tt with [].

[oskgo]

I think this is #334. I'll make a PR changing the definition of allperms to use the workaround I mentioned in that issue.

Closing as duplicate.