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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
<<
Fixpoint minus (n m:nat) : nat :=
match n, m with
| O, _ => n
| S k, O => S k
| S k, S l => k - l
end
where "n - m" := (minus n m) : nat_scope.
>>
*)
Require Import Lt.
Require Import Le.
Open Local Scope nat_scope.
Implicit Types m n p : nat.
(** * 0 is right neutral *)
Lemma minus_n_O : forall n, n = n - 0.
Proof.
induction n; simpl in |- *; auto with arith.
Qed.
Hint Resolve minus_n_O: arith v62.
(** * Permutation with successor *)
Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
Proof.
intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
auto with arith.
Qed.
Hint Resolve minus_Sn_m: arith v62.
Theorem pred_of_minus : forall n, pred n = n - 1.
Proof.
intro x; induction x; simpl in |- *; auto with arith.
Qed.
(** * Diagonal *)
Lemma minus_diag : forall n, n - n = 0.
Proof.
induction n; simpl in |- *; auto with arith.
Qed.
Lemma minus_diag_reverse : forall n, 0 = n - n.
Proof.
auto using minus_diag.
Qed.
Hint Resolve minus_diag_reverse: arith v62.
Notation minus_n_n := minus_diag_reverse.
(** * Simplification *)
Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
Proof.
induction p; simpl in |- *; auto with arith.
Qed.
Hint Resolve minus_plus_simpl_l_reverse: arith v62.
(** * Relation with plus *)
Lemma plus_minus : forall n m p, n = m + p -> p = n - m.
Proof.
intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *;
intros.
replace (n0 - 0) with n0; auto with arith.
absurd (0 = S (n0 + p)); auto with arith.
auto with arith.
Qed.
Hint Immediate plus_minus: arith v62.
Lemma minus_plus : forall n m, n + m - n = m.
symmetry in |- *; auto with arith.
Qed.
Hint Resolve minus_plus: arith v62.
Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n).
Proof.
intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *;
auto with arith.
Qed.
Hint Resolve le_plus_minus: arith v62.
Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m.
Proof.
symmetry in |- *; auto with arith.
Qed.
Hint Resolve le_plus_minus_r: arith v62.
(** * Relation with order *)
Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p.
Proof.
intros n m p; generalize n m; clear n m; induction p as [|p HI].
intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial.
intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith.
intros q r H _. simpl. auto using HI.
Qed.
Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n.
Proof.
intros n m p; generalize n m; clear n m; induction p as [|p HI].
trivial.
intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
intros q; destruct q; auto with arith.
simpl.
apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
auto with arith.
intros q r Hqr _. simpl. auto using HI.
Qed.
Corollary le_minus : forall n m, n - m <= n.
Proof.
intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
Qed.
Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
Proof.
intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
auto using le_minus with arith.
intros; absurd (0 < 0); auto with arith.
Qed.
Hint Resolve lt_minus: arith v62.
Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n.
Proof.
intros n m; pattern n, m in |- *; apply nat_double_ind; simpl in |- *;
auto with arith.
intros; absurd (0 < 0); trivial with arith.
Qed.
Hint Immediate lt_O_minus_lt: arith v62.
Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0.
Proof.
intros y x; pattern y, x in |- *; apply nat_double_ind;
[ simpl in |- *; trivial with arith
| intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ]
| simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3;
apply H2; apply le_n_S; assumption ].
Qed.
|
