(* Exercise 1: A Simple Ambient Logic Proof *) prover [""]. (* no use of SMT solvers *) (* consider and carefully study this proof: *) lemma negb_exists (P : 'a -> bool) : (! exists (x : 'a), P x) <=> (forall (x : 'a), ! (P x)). proof. split => [not_ex x | all_not]. case (P x) => [P_x | //]. have // : exists x, P x by exists x. case (exists x, P x) => [[] x P_x | //]. have // : ! (P x) by apply all_not. qed. (* we can use negb_exists to prove: *) lemma negb_forall (P : 'a -> bool) : ! (forall (x : 'a), P x) <=> (exists (x : 'a), ! P x). proof. have H : (! exists (x : 'a), ! (P x)) <=> (forall (x : 'a), ! (! (P x))). apply negb_exists. by rewrite -H. qed. (* instead, write a direct proof of negb_forall, not using any lemmas of the EasyCrypt Library or SMT solvers *) lemma negb_forall' (P : 'a -> bool) : ! (forall (x : 'a), P x) <=> (exists (x : 'a), ! P x). proof. (* BEGIN FILL IN *) (* END FILL IN *) qed.