(* ASSIGNMENT 1 Due on Gradescope by 5pm on Friday, February 12 *) require import AllCore. (* QUESTION 1 prove the following lemma without using the tactics `case` or `smt`, and without using any lemmas from the EasyCrypt Library: *) lemma sub (a b c : bool) : (a => b => c) => (a => b) => a => c. proof. (* BEGIN FILL IN *) move => H1 H2 a_true. apply H1 => //. by apply H2. (* END FILL IN *) qed. lemma sub' (a b c : bool) : (a => b => c) => (a => b) => a => c. proof. (* BEGIN FILL IN *) move => H1 H2 a_true. by rewrite H1 2:H2. (* END FILL IN *) qed. (* QUESTION 2 prove the following lemma without using the tactics `case` or `smt`, and without using any lemmas from the EasyCrypt Library: *) lemma peirce (a b : bool) : (a \/ !a) => ((a => b) => a) => a. proof. (* BEGIN FILL IN *) move => [// | a_false] H. by apply H. (* END FILL IN *) qed. lemma peirce' (a b : bool) : (a \/ !a) => ((a => b) => a) => a. proof. (* BEGIN FILL IN *) move => [// | -> //]. (* END FILL IN *) qed. (* QUESTION 3 prove the following lemma without using the `smt` tactic, and without using any lemmas from the EasyCrypt Library (you may use the `case` tactic): *) lemma not_exists (P : 'a -> bool) : (! exists (x : 'a), P x) <=> (forall (x : 'a), ! (P x)). proof. (* BEGIN FILL IN *) 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). apply all_not. (* END FILL IN *) qed. (* QUESTION 4 This question is about proving the equivalence of two definitions of when an integer is prime. *) require import IntDiv StdOrder. (* lemmas for integer mod and div *) import IntOrder. (* lemmas about <, <= on int *) (* n %/ x is the integer division of n by x, discarding any remainder n %% x is the remainder of integer division of n by x x %| n tests whether x divides n, i.e., n %% x = 0 %/ and %% are actually abbreviations, defined in terms of edivz; consequently, when using `search` to look for lemmas involving these abbreviations, one must search for `edivz` instead. But we've provided (below) the lemma that needs such facts *) (* here are two ways of defining when an integer is prime, which you will prove are equivalent: *) op is_prime1 (n : int) : bool = 2 <= n /\ ! exists (x : int), x %| n /\ 1 < x /\ x < n. op is_prime2 (n : int) : bool = 2 <= n /\ forall (x : int), x %| n => x <= 1 \/ x = n. (* you may use the following lemma in your proof (it should probably be provided by IntDiv): *) lemma div_le (x n : int) : 1 <= x => 1 <= n => x %| n => x <= n. proof. move => ge1_x ge1_n x_div_n. have n_eq : n = (n %/ x) * x. by rewrite eq_sym -dvdz_eq. rewrite n_eq -{1}mul1z ler_pmul // (lez_trans 1) //. case (1 <= n %/ x) => //. rewrite -ltrNge => lt1_n_div_x. have le0_n : n <= 0. by rewrite n_eq mulr_le0_ge0 1:-ltzS // (lez_trans 1). have // : 1 <= 0. by apply (lez_trans n). qed. (* When proving the following lemma, this lemma from the EasyCrypt Library will be helpful: lemma forall_iff (P P' : 'a -> bool) : (forall x, P x <=> P' x) => (forall (x : 'a), P x) <=> (forall (x : 'a), P' x). *) (* prove the following lemma without using the `smt` tactic; you may use the `case` tactic as well as any lemmas from the EasyCrypt Library hint: you can use your solution to QUESTION 3, and you can use `search` to look for needed lemmas in the EasyCrypt Library. E.g., search [!] (/\) searches for lemmas involving negation and conjunction for *partial credit*, you can use `smt` or even `admit` for parts of your proof *) lemma prime_equiv_ge2 (n : int) : 2 <= n => (! (exists (x : int), x %| n /\ 1 < x /\ x < n) <=> (forall (x : int), x %| n => x <= 1 \/ x = n)). proof. (* BEGIN FILL IN *) move => ge2_n. have ge1_n : 1 <= n. by apply (lez_trans 2). rewrite not_exists /=. apply forall_iff => x /=. rewrite 2!negb_and. split => [[] // [not_lt1_x x_div_n | not_lt_x_n x_div_n] | rhs_impl]. left; by rewrite lezNgt. right. have ge1_x : 1 <= x. rewrite -lerNgt in not_lt_x_n. by apply (lez_trans n). have not_n_lt_x : ! n < x. by rewrite ler_gtF 1:div_le. case (x = n) => [// | x_ne_n]. rewrite neq_ltz in x_ne_n. by elim x_ne_n. case (x %| n) => [x_div_n /= | //]. have [le1_x | -> //] : x <= 1 \/ x = n. by rewrite rhs_impl. left; by rewrite ltzNge. (* END FILL IN *) qed. (* use prime_equiv_ge2 (but not the `smt` tactic) to prove the following lemma asserting the equivalence of the two definitions of primality (you won't need `case` or lemmas from the EasyCrypt Library, but you may use them) *) lemma prime_equiv (n : int) : is_prime1 n <=> is_prime2 n. proof. (* BEGIN FILL IN *) rewrite /is_prime1 /is_prime2. split => [[] ge2_n H | [] ge2_n H]. split => //. by rewrite -prime_equiv_ge2. split => //. by rewrite prime_equiv_ge2. (* END FILL IN *) qed.