Skip to content

implement allperms to get rid of some unneeded axioms#970

Merged
strub merged 1 commit intomainfrom
remove-axioms
Apr 9, 2026
Merged

implement allperms to get rid of some unneeded axioms#970
strub merged 1 commit intomainfrom
remove-axioms

Conversation

@oskgo
Copy link
Copy Markdown
Contributor

@oskgo oskgo commented Apr 9, 2026

No description provided.

@strub strub self-assigned this Apr 9, 2026
@strub strub added the library label Apr 9, 2026
@strub strub enabled auto-merge April 9, 2026 18:01
@fdupress
Copy link
Copy Markdown
Member

fdupress commented Apr 9, 2026

Make opaque and keep the axioms as lemmas?

@strub strub added this pull request to the merge queue Apr 9, 2026
Merged via the queue into main with commit ecb3395 Apr 9, 2026
16 checks passed
@strub strub deleted the remove-axioms branch April 9, 2026 18:36
@alleystoughton
Copy link
Copy Markdown
Member

I figured this was going to break one of my proofs.

@fdupress
Copy link
Copy Markdown
Member

fdupress commented Apr 9, 2026

If it does, please do feel free to layer an additional PR on. I was too late for this one.

@alleystoughton
Copy link
Copy Markdown
Member

Is this a bug in EasyCrypt (not the library)?

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 *)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants