(* 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.

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.

qed.