1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Properties of subtraction between natural numbers.
This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead.
[minus] is now an alias for [Nat.sub], which is defined in [Init/Nat.v] as:
<<
Fixpoint sub (n m:nat) : nat :=
match n, m with
| S k, S l => k - l
| _, _ => n
end
where "n - m" := (sub n m) : nat_scope.
>>
*)
Require Import PeanoNat Lt Le.
Local Open Scope nat_scope.
(** * 0 is right neutral *)
Lemma minus_n_O n : n = n - 0.
Proof.
symmetry. apply Nat.sub_0_r.
Qed.
(** * Permutation with successor *)
Lemma minus_Sn_m n m : m <= n -> S (n - m) = S n - m.
Proof.
intros. symmetry. now apply Nat.sub_succ_l.
Qed.
Theorem pred_of_minus n : pred n = n - 1.
Proof.
symmetry. apply Nat.sub_1_r.
Qed.
Register pred_of_minus as num.nat.pred_of_minus.
(** * Diagonal *)
Notation minus_diag := Nat.sub_diag (only parsing). (* n - n = 0 *)
Lemma minus_diag_reverse n : 0 = n - n.
Proof.
symmetry. apply Nat.sub_diag.
Qed.
Notation minus_n_n := minus_diag_reverse.
(** * Simplification *)
Lemma minus_plus_simpl_l_reverse n m p : n - m = p + n - (p + m).
Proof.
now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub.
Qed.
(** * Relation with plus *)
Lemma plus_minus n m p : n = m + p -> p = n - m.
Proof.
symmetry. now apply Nat.add_sub_eq_l.
Qed.
Lemma minus_plus n m : n + m - n = m.
Proof.
rewrite Nat.add_comm. apply Nat.add_sub.
Qed.
Lemma le_plus_minus_r n m : n <= m -> n + (m - n) = m.
Proof.
rewrite Nat.add_comm. apply Nat.sub_add.
Qed.
Lemma le_plus_minus n m : n <= m -> m = n + (m - n).
Proof.
intros. symmetry. rewrite Nat.add_comm. now apply Nat.sub_add.
Qed.
(** * Relation with order *)
Notation minus_le_compat_r :=
Nat.sub_le_mono_r (only parsing). (* n <= m -> n - p <= m - p. *)
Notation minus_le_compat_l :=
Nat.sub_le_mono_l (only parsing). (* n <= m -> p - m <= p - n. *)
Notation le_minus := Nat.le_sub_l (only parsing). (* n - m <= n *)
Notation lt_minus := Nat.sub_lt (only parsing). (* m <= n -> 0 < m -> n-m < n *)
Lemma lt_O_minus_lt n m : 0 < n - m -> m < n.
Proof.
apply Nat.lt_add_lt_sub_r.
Qed.
Theorem not_le_minus_0 n m : ~ m <= n -> n - m = 0.
Proof.
intros. now apply Nat.sub_0_le, Nat.lt_le_incl, Nat.lt_nge.
Qed.
(** * Hints *)
#[global]
Hint Resolve minus_n_O: arith.
#[global]
Hint Resolve minus_Sn_m: arith.
#[global]
Hint Resolve minus_diag_reverse: arith.
#[global]
Hint Resolve minus_plus_simpl_l_reverse: arith.
#[global]
Hint Immediate plus_minus: arith.
#[global]
Hint Resolve minus_plus: arith.
#[global]
Hint Resolve le_plus_minus: arith.
#[global]
Hint Resolve le_plus_minus_r: arith.
#[global]
Hint Resolve lt_minus: arith.
#[global]
Hint Immediate lt_O_minus_lt: arith.
|
