Chapter 4
From mathcomp Require Import all_ssreflect. (* 4.1.1 Pulling from the stack *) Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => xy pr_x odd_y. Abort. Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] pr_x odd_y. Abort. Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] /= pr_x odd_y. Abort. Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] /= /prime_gt1-x_gt1 odd_y. Abort. Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x [//|z]] /= /prime_gt1-x_gt1. Abort. Print odd. (* Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false. *) Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. by move=> [x [//|z]] /= /prime_gt1-x_gt1 _; apply: ltn_addl x_gt1. Qed. About ltn_addl. (* 4.1.2 Working on the stack *) Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] /= /prime_gt1. Abort. Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] /= /prime_gt1/ltnW. Abort. Goal (forall n, n * 2 = n + n) -> 6 = 3 + 3. move => /(_ 3). Abort. Goal (forall n, n * 2 = n + n) -> 6 = 3 + 3. move => /(_ 3) <-. Abort. (* 4.1.3 Pushing to the stack *) Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] /= /prime_gt1-x_gt1 odd_y. move: y odd_y. case. Abort. Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] /= /prime_gt1-x_gt1 odd_y. case: y odd_y. Abort. Goal forall xy, prime xy.1 -> odd xy.2 -> 2 < xy.2 + xy.1. move => [x y] /= /prime_gt1-x_gt1 odd_y. case: y odd_y => [|y']. Abort. (* 4.2.1 Primes, a never ending story *) (* Inductive ex2 A P Q : Prop := ex_intro2 x of P x & Q x. *) (* Notation "exists2 x , p & q" := (ex2 (fun x => p) (fun x => q)). *) (* Notation "n ` !" := (factorial n). *) (* Lemma fact_gt0 n : 0 < n`!. *) (* Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!. *) (* Lemma pdivP n : 1 < n -> exists2 p, prime p & p %| n, *) (* Lemma dvdn_addr m d n : d %| m -> (d %| m + n) = (d %| n). *) (* Lemma gtnNdvd n d : 0 < n -> n < d -> (d %| n) = false. *) Goal forall m, exists2 p, m < p & prime p. move => m; have m1_gt1 : 1 < m`! + 1. by rewrite addn1 ltnS fact_gt0. Abort. Goal forall m, exists2 p, m < p & prime p. move => m; have m1_gt1 : 1 < m`! + 1. by rewrite addn1 ltnS fact_gt0. case: (pdivP m1_gt1) => [p pr_p p_dv_m1]. Abort. Lemma prime_above m : exists2 p, m < p & prime p. Proof. have /pdivP[p pr_p p_dv_m1]: 1 < m`! + 1. by rewrite addn1 ltnS fact_gt0. exists p => //; rewrite ltnNge; apply: contraL p_dv_m1 => p_le_m. by rewrite dvdn_addr ?dvdn_fact ?prime_gt0 // gtnNdvd ?prime_gt1. Qed. (* 4.2.2 Order and max, a matter of symmetry *) (* Lemma orP {a b : bool} : a || b -> a \/ b. *) (* Lemma orb_idr (a b : bool) : (b -> a) -> (a || b) = a. *) (* Lemma orbC a b : a || b = b || a. *) (* Lemma maxn_idPl {m n} : n <= m -> maxn m n = m. *) (* Lemma maxnC m n : maxn m n = maxn n m. *) (* Lemma leq_total m n : (m <= n) || (n <= m). *) Lemma leq_max4 m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2). Proof. case: (orP (leq_total n2 n1)) => [le_n21|le_n12]. rewrite (maxn_idPl le_n21) orb_idr // => le_mn2. by apply: leq_trans le_mn2 le_n21. rewrite maxnC orbC. rewrite (maxn_idPl le_n12) orb_idr // => le_mn1. by apply: leq_trans le_mn1 le_n12. Qed. Lemma leq_max3 m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2). Proof. have th_sym x y: y <= x -> (m <= maxn x y) = (m <= x) || (m <= y). move=> le_yx; rewrite (maxn_idPl le_yx) orb_idr // => le_my. by apply: leq_trans le_my le_yx. by case: (orP (leq_total n2 n1)) => /th_sym; last rewrite maxnC orbC. Qed. Lemma leq_max2 m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2). Proof. suff th_sym x y: y <= x -> (m <= maxn x y) = (m <= x) || (m <= y). by case: (orP (leq_total n2 n1)) => /th_sym; last rewrite maxnC orbC. move=> le_yx; rewrite (maxn_idPl le_yx) orb_idr // => le_my. by apply: leq_trans le_my le_yx. Qed. Lemma leq_max1 m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2). Proof. wlog le_n21: n1 n2 / n2 <= n1 => [th_sym|]. by case: (orP (leq_total n2 n1)) => /th_sym; last rewrite maxnC orbC. rewrite (maxn_idPl le_n21) orb_idr // => le_mn2. by apply: leq_trans le_mn2 le_n21. Qed. Lemma leq_max m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2). Proof. wlog le_n21: n1 n2 / n2 <= n1 => [th_sym|]. by case: (orP (leq_total n2 n1)) => /th_sym; last rewrite maxnC orbC. by rewrite (maxn_idPl le_n21) orb_idr // => /leq_trans->. Qed.