From 31cf6cb44f0fd455858d706d1fcf1a136d8e2e11 Mon Sep 17 00:00:00 2001
From: Oskar Goldhahn <oskar.goldhahn@ntnu.no>
Date: Thu, 9 Apr 2026 19:54:07 +0200
Subject: [PATCH] implement allperms to get rid of some unneeded axioms

---
 theories/algebra/Perms.ec | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

diff --git a/theories/algebra/Perms.ec b/theories/algebra/Perms.ec
index 5423d79128..1ebc0e1d70 100644
--- a/theories/algebra/Perms.ec
+++ b/theories/algebra/Perms.ec
@@ -3,19 +3,13 @@ require import AllCore List IntDiv Binomial Ring StdOrder.
 (*---*) import IntID IntOrder.
 
 (* -------------------------------------------------------------------- *)
-op allperms_r (n : unit list) (s : 'a list) : 'a list list.
-
-axiom allperms_r0 (s : 'a list) :
-  allperms_r [] s = [[]].
-
-axiom allperms_rS (x : unit) (n : unit list) (s : 'a list) :
-  allperms_r (x :: n) s = flatten (
+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 allperms (s : 'a list) = allperms_r (nseq (size s) tt) s.
 
-hint rewrite ap_r : allperms_r0 allperms_rS.
-
 (* -------------------------------------------------------------------- *)
 lemma allperms_rP n (s t : 'a list) : size s = size n =>
   (mem (allperms_r n s) t) <=> (perm_eq s t).
@@ -51,7 +45,7 @@ qed.
 (* -------------------------------------------------------------------- *)
 lemma uniq_allperms_r n (s : 'a list) : uniq (allperms_r n s).
 proof.
-elim: n s => [|? n ih] s; rewrite ?ap_r  //.
+elim: n s => [|? n ih] s; rewrite ?ap_r  //=.
 apply/uniq_flatten_map/undup_uniq.
   by move=> x /=; apply/map_inj_in_uniq/ih => a b _ _ [].
 move=> x y; rewrite !mem_undup => sx sy /= /hasP[t].
@@ -79,7 +73,7 @@ require import StdBigop.
 lemma size_allperms_uniq_r n (s : 'a list) : size s = size n => uniq s =>
   size (allperms_r n s) = fact (size s).
 proof.
-elim: n s => /= [|? n ih] s; rewrite ?ap_r /=.
+elim: n s => /= [s|n ih s].
   by move/size_eq0=> -> /=; rewrite fact0.
 case: s=> [|x s]; first by rewrite addz_neq0 ?size_ge0.
 (pose s' := undup _)=> /=; move/addrI=> eq_sz [Nsz uqs].