Nits: choiceb induction principle

EasyCrypt · Oct 19, 2023 · 9249c67 · 9249c67
1 parent e945e0c
commit 9249c67
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 3 deletions.
diff --git a/theories/core/Core.ec b/theories/core/Core.ec
@@ -302,3 +302,15 @@ lemma nosmt predTofV (f : 'a -> 'b): predT \o f = predT.
 proof. by apply/fun_ext=> x. qed.
 
 lemma pred_0Vmem (p : 'a -> bool) : p = pred0 \/ exists x, p x by smt().
+
+(* -------------------------------------------------------------------- *)
+lemma choicebW (P : 'a -> bool) (x0 : 'a) (I : 'a -> bool) :
+     ((exists x, P x) => forall x, P x => I x)
+  => ((forall x, !P x) => I x0)
+  => I (choiceb P x0).
+proof.
+rewrite -negb_exists; case: (exists x, P x) => /=.
+- by move/choicebP=> /(_ x0) ?; apply.
+- by rewrite negb_exists => /choiceb_dfl ->.
+qed.
+
diff --git a/theories/structure/Finite.ec b/theories/structure/Finite.ec
@@ -35,9 +35,8 @@ case=> s fin_p; exists (filter p (undup s)); split.
 qed.
 
 (* -------------------------------------------------------------------- *)
-lemma uniq_to_seq (P : 'a -> bool):
-  is_finite P => uniq (to_seq P).
-proof. by move=>/to_seq_finite [-> _]. qed.
+lemma uniq_to_seq (P : 'a -> bool): uniq (to_seq P).
+proof. by apply: choicebW => //= _ s []. qed.
 
 lemma mem_to_seq (P : 'a -> bool) x:
   is_finite P => mem (to_seq P) x <=> P x.