Make allperms_r opaque to work around #334

Add explicit unfolding lemmas and simplification hints to
restore definitional transparency for proofs.

Author: oskgo

theories/algebra/Perms.ec

@@ -3,11 +3,22 @@ require import AllCore List IntDiv Binomial Ring StdOrder.
 (*---*) import IntID IntOrder.
 
 (* -------------------------------------------------------------------- *)
-op allperms_r (n : unit list) (s : 'a list) : 'a list list =
-with n = [] => [[]]
-with n = x::n => flatten (
-    map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s)).
+op [smt_opaque] allperms_r (n : unit list) (s : 'a list) : 'a list list =
+  with n = [] =>
+    [[]]
+  with n = _ :: n =>
+    flatten (map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s)).
 
+lemma allperms_r0 (s : 'a list) :
+  allperms_r [] s = [[]]
+by done. 
+
+lemma allperms_rS (x : unit) (n : unit list) (s : 'a list) :
+  allperms_r (x :: n) s = flatten (
+    map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s))
+by done.
+
+(* -------------------------------------------------------------------- *)
 op allperms (s : 'a list) = allperms_r (nseq (size s) tt) s.
 
 (* -------------------------------------------------------------------- *)