1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: Minus.v 11072 2008-06-08 16:13:37Z herbelin $ i*)
11
(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
13
Fixpoint minus (n m:nat) {struct n} : nat :=
19
where "n - m" := (minus n m) : nat_scope.
26
Open Local Scope nat_scope.
28
Implicit Types m n p : nat.
30
(** * 0 is right neutral *)
32
Lemma minus_n_O : forall n, n = n - 0.
34
induction n; simpl in |- *; auto with arith.
36
Hint Resolve minus_n_O: arith v62.
38
(** * Permutation with successor *)
40
Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m.
42
intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
45
Hint Resolve minus_Sn_m: arith v62.
47
Theorem pred_of_minus : forall n, pred n = n - 1.
49
intro x; induction x; simpl in |- *; auto with arith.
54
Lemma minus_diag : forall n, n - n = 0.
56
induction n; simpl in |- *; auto with arith.
59
Lemma minus_diag_reverse : forall n, 0 = n - n.
61
auto using minus_diag.
63
Hint Resolve minus_diag_reverse: arith v62.
65
Notation minus_n_n := minus_diag_reverse.
67
(** * Simplification *)
69
Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m).
71
induction p; simpl in |- *; auto with arith.
73
Hint Resolve minus_plus_simpl_l_reverse: arith v62.
75
(** * Relation with plus *)
77
Lemma plus_minus : forall n m p, n = m + p -> p = n - m.
79
intros n m p; pattern m, n in |- *; apply nat_double_ind; simpl in |- *;
81
replace (n0 - 0) with n0; auto with arith.
82
absurd (0 = S (n0 + p)); auto with arith.
85
Hint Immediate plus_minus: arith v62.
87
Lemma minus_plus : forall n m, n + m - n = m.
88
symmetry in |- *; auto with arith.
90
Hint Resolve minus_plus: arith v62.
92
Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n).
94
intros n m Le; pattern n, m in |- *; apply le_elim_rel; simpl in |- *;
97
Hint Resolve le_plus_minus: arith v62.
99
Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m.
101
symmetry in |- *; auto with arith.
103
Hint Resolve le_plus_minus_r: arith v62.
105
(** * Relation with order *)
107
Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p.
109
intros n m p; generalize n m; clear n m; induction p as [|p HI].
110
intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial.
112
intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith.
113
intros q r H _. simpl. auto using HI.
116
Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n.
118
intros n m p; generalize n m; clear n m; induction p as [|p HI].
121
intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial.
122
intros q; destruct q; auto with arith.
124
apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O];
127
intros q r Hqr _. simpl. auto using HI.
130
Corollary le_minus : forall n m, n - m <= n.
132
intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith.
135
Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n.
137
intros n m Le; pattern m, n in |- *; apply le_elim_rel; simpl in |- *;
138
auto using le_minus with arith.
139
intros; absurd (0 < 0); auto with arith.
141
Hint Resolve lt_minus: arith v62.
143
Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n.
145
intros n m; pattern n, m in |- *; apply nat_double_ind; simpl in |- *;
147
intros; absurd (0 < 0); trivial with arith.
149
Hint Immediate lt_O_minus_lt: arith v62.
151
Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0.
153
intros y x; pattern y, x in |- *; apply nat_double_ind;
154
[ simpl in |- *; trivial with arith
155
| intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ]
156
| simpl in |- *; intros n m H1 H2; apply H1; unfold not in |- *; intros H3;
157
apply H2; apply le_n_S; assumption ].