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
|
(************************************************************************)
(* 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: Le.v 9245 2006-10-17 12:53:34Z notin $ i*)
(** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
<<
Inductive le (n:nat) : nat -> Prop :=
| le_n : n <= n
| le_S : forall m:nat, n <= m -> n <= S m
where "n <= m" := (le n m) : nat_scope.
>>
*)
Open Local Scope nat_scope.
Implicit Types m n p : nat.
(** * [le] is a pre-order *)
(** Reflexivity *)
Theorem le_refl : forall n, n <= n.
Proof.
exact le_n.
Qed.
(** Transitivity *)
Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
Proof.
induction 2; auto.
Qed.
Hint Resolve le_trans: arith v62.
(** * Properties of [le] w.r.t. successor, predecessor and 0 *)
(** Comparison to 0 *)
Theorem le_O_n : forall n, 0 <= n.
Proof.
induction n; auto.
Qed.
Theorem le_Sn_O : forall n, ~ S n <= 0.
Proof.
red in |- *; intros n H.
change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
Qed.
Hint Resolve le_O_n le_Sn_O: arith v62.
Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n.
Proof.
induction n; auto with arith.
intro; contradiction le_Sn_O with n.
Qed.
Hint Immediate le_n_O_eq: arith v62.
(** [le] and successor *)
Theorem le_n_S : forall n m, n <= m -> S n <= S m.
Proof.
induction 1; auto.
Qed.
Theorem le_n_Sn : forall n, n <= S n.
Proof.
auto.
Qed.
Hint Resolve le_n_S le_n_Sn : arith v62.
Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
Proof.
intros n m H; apply le_trans with (S n); auto with arith.
Qed.
Hint Immediate le_Sn_le: arith v62.
Theorem le_S_n : forall n m, S n <= S m -> n <= m.
Proof.
intros n m H; change (pred (S n) <= pred (S m)) in |- *.
destruct H; simpl; auto with arith.
Qed.
Hint Immediate le_S_n: arith v62.
Theorem le_Sn_n : forall n, ~ S n <= n.
Proof.
induction n; auto with arith.
Qed.
Hint Resolve le_Sn_n: arith v62.
(** [le] and predecessor *)
Theorem le_pred_n : forall n, pred n <= n.
Proof.
induction n; auto with arith.
Qed.
Hint Resolve le_pred_n: arith v62.
Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
Proof.
destruct n; simpl; auto with arith.
destruct m; simpl; auto with arith.
Qed.
(** * [le] is a order on [nat] *)
(** Antisymmetry *)
Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m.
Proof.
intros n m H; destruct H as [|m' H]; auto with arith.
intros H1.
absurd (S m' <= m'); auto with arith.
apply le_trans with n; auto with arith.
Qed.
Hint Immediate le_antisym: arith v62.
(** * A different elimination principle for the order on natural numbers *)
Lemma le_elim_rel :
forall P:nat -> nat -> Prop,
(forall p, P 0 p) ->
(forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) ->
forall n m, n <= m -> P n m.
Proof.
induction n; auto with arith.
intros m Le.
elim Le; auto with arith.
Qed.
|
