From 4861470e7724049241554a4c4ac8c68030bc816c Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 10 Apr 2026 16:13:06 +0200 Subject: [PATCH] Make `allperms_r` opaque to work around #334 Add explicit unfolding lemmas and simplification hints to restore definitional transparency for proofs. --- theories/algebra/Perms.ec | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/theories/algebra/Perms.ec b/theories/algebra/Perms.ec index 1ebc0e1d7..8e2b65d18 100644 --- a/theories/algebra/Perms.ec +++ b/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. (* -------------------------------------------------------------------- *)