nat.v 2.88 KB
 Xiaojie Guo committed Dec 14, 2017 1 ``````Require Import rt.util.tactics rt.util.ssromega. `````` Felipe Cerqueira committed May 05, 2016 2 ``````From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div. `````` Felipe Cerqueira committed Mar 31, 2016 3 4 5 6 7 8 9 10 11 `````` (* Additional lemmas about natural numbers. *) Section NatLemmas. Lemma subh1 : forall m n p, m >= n -> m - n + p = m + p - n. Proof. by ins; ssromega. Qed. `````` Sergey Bozhko committed Nov 19, 2019 12 13 14 15 16 17 18 `````` Lemma subh2 : forall m1 m2 n1 n2, m1 >= m2 -> n1 >= n2 -> (m1 + n1) - (m2 + n2) = m1 - m2 + (n1 - n2). Proof. by ins; ssromega. Qed. `````` Sergey Bozhko committed Apr 05, 2019 19 `````` `````` Sergey Bozhko committed May 19, 2019 20 `````` Lemma subh3: `````` Sergey Bozhko committed Apr 05, 2019 21 22 23 24 25 26 `````` forall m n p, m + p <= n -> m <= n - p. Proof. clear. intros. `````` Sergey Bozhko committed May 19, 2019 27 28 29 30 `````` rewrite <- leq_add2r with (p := p). rewrite subh1 //. - by rewrite -addnBA // subnn addn0. - by apply leq_trans with (m+p); first rewrite leq_addl. `````` Sergey Bozhko committed Apr 05, 2019 31 32 `````` Qed. `````` Björn Brandenburg committed Aug 13, 2019 33 34 35 36 37 38 39 40 41 42 43 44 45 46 `````` (* Simplify n + a - b + b - a = n if n >= b. *) Lemma subn_abba: forall n a b, n >= b -> n + a - b + b - a = n. Proof. move=> n a b le_bn. rewrite subnK; first by rewrite -addnBA // subnn addn0 //. rewrite -[b]addn0. apply leq_trans with (n := n + 0); rewrite !addn0 //. apply leq_addr. Qed. `````` Xiaojie Guo committed Dec 14, 2017 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 `````` Lemma add_subC: forall a b c, a >= c -> b >=c -> a + (b - c ) = a - c + b. Proof. intros* AgeC BgeC. induction b;induction c;intros;try ssromega. Qed. Lemma ltn_subLR: forall a b c, a - c < b -> a < b + c. Proof. intros* AC. ssromega. Qed. `````` Björn Brandenburg committed Aug 13, 2019 64 `````` `````` Björn Brandenburg committed Aug 21, 2019 65 66 67 68 69 70 71 72 73 74 75 `````` (* We can drop additive terms on the lesser side of an inequality. *) Lemma leq_addk: forall m n k, n + k <= m -> n <= m. Proof. move=> m n p. apply leq_trans. by apply leq_addr. Qed. `````` Björn Brandenburg committed Aug 13, 2019 76 77 ``````End NatLemmas. `````` Björn Brandenburg committed Aug 13, 2019 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 ``````Section Interval. (* Trivially, points before the start of an interval, or past the end of an interval, are not included in the interval. *) Lemma point_not_in_interval: forall t1 t2 t', t2 <= t' \/ t' < t1 -> forall t, t1 <= t < t2 -> t <> t'. Proof. move=> t1 t2 t' EXCLUDED t /andP [GEQ_t1 LT_t2] EQ. subst. case EXCLUDED => [INEQ | INEQ]; eapply leq_ltn_trans in INEQ; eauto; by rewrite ltnn in INEQ. Qed. End Interval. `````` Björn Brandenburg committed Aug 13, 2019 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 ``````Section NatOrderLemmas. (* Mimic the way implicit arguments are used in ssreflect. *) Set Implicit Arguments. Unset Strict Implicit. (* ltn_leq_trans: Establish that m < p if m < n and n <= p, to mirror the lemma leq_ltn_trans in ssrnat. NB: There is a good reason for this lemma to be "missing" in ssrnat -- since m < n is defined as m.+1 <= n, ltn_leq_trans is just m.+1 <= n -> n <= p -> m.+1 <= p, that is (@leq_trans n m.+1 p). Nonetheless we introduce it here because an additional (even though arguably redundant) lemma doesn't hurt, and for newcomers the apparent absence of the mirror case of leq_ltn_trans can be somewhat confusing. *) Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p. Proof. exact (@leq_trans n m.+1 p). Qed. End NatOrderLemmas.``````