(* logic-examp2.ec *)

require import AllCore.

(* we'll prove this lemma from scratch *)

lemma not_forall (P : 'a -> bool) :
  (! forall (x : 'a), P x) <=> (exists (x : 'a), ! (P x)).
proof.
split => [not_all | [x not_P_x]].
case (exists x, ! P x) => [// | not_ex_not].
have // : forall x, P x.
  move => x.
  case (P x) => [// | not_P_x].
  have // : exists x, ! (P x) by exists x.
case (forall x, P x) => [all | //].
have // : P x by apply all.
qed.

(* below, we'll allow ourselves to use lemmas from the EasyCrypt
   Library (.opam/.../lib/easycrypt/theories), but not to use `smt`

   hint: use `search` (see the Ambient Logic slides) to find applicable
   lemmas *)

(* In .../theories/prelude/Logic.ec:

lemma nosmt exists_iff (P P' : 'a -> bool) :
  (forall x, P x <=> P' x) =>
  (exists (x : 'a), P x) <=> (exists (x : 'a), P' x).
*)

lemma foo (P : int -> bool, y : int) :
  (! forall (x : int), y <= x => P x) <=>
  (exists (x : int),  y <= x /\ ! (P x)).
proof.
rewrite not_forall /=.
apply exists_iff => x /=.
by rewrite negb_imply.
qed.