nat.v 2.72 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 Apr 05, 2019 12 `````` `````` Sergey Bozhko committed May 19, 2019 13 `````` Lemma subh3: `````` Sergey Bozhko committed Apr 05, 2019 14 15 16 17 18 19 `````` forall m n p, m + p <= n -> m <= n - p. Proof. clear. intros. `````` Sergey Bozhko committed May 19, 2019 20 21 22 23 `````` 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 24 25 `````` Qed. `````` Björn Brandenburg committed Aug 13, 2019 26 27 28 29 30 31 32 33 34 35 36 37 38 39 `````` (* 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 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 `````` 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 57 `````` `````` Björn Brandenburg committed Aug 21, 2019 58 59 60 61 62 63 64 65 66 67 68 `````` (* 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 69 70 ``````End NatLemmas. `````` Björn Brandenburg committed Aug 13, 2019 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 ``````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 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 ``````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.``````