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$ i*)
Require Import Le Plus.
Open Local Scope nat_scope.
Implicit Types m n : nat.
(** * Maximum of two natural numbers *)
Fixpoint max n m {struct n} : nat :=
match n, m with
| O, _ => m
| S n', O => n
| S n', S m' => S (max n' m')
end.
(** * Inductive characterization of [max] *)
Lemma max_case_strong : forall n m (P:nat -> Type),
(m<=n -> P n) -> (n<=m -> P m) -> P (max n m).
Proof.
induction n; destruct m; simpl in *; auto with arith.
intros P H1 H2; apply IHn; intro; [apply H1|apply H2]; auto with arith.
Qed.
(** Propositional characterization of [max] *)
Lemma max_spec : forall n m, m <= n /\ max n m = n \/ n <= m /\ max n m = m.
Proof.
intros n m; apply max_case_strong; auto.
Qed.
(** * [max n m] is equal to [n] or [m] *)
Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.
Proof.
induction n; destruct m; simpl; auto.
destruct (IHn m) as [-> | ->]; auto.
Defined.
(** [max n m] is equal to [n] or [m], alternative formulation *)
Lemma max_case : forall n m (P:nat -> Type), P n -> P m -> P (max n m).
Proof.
intros n m; destruct (max_dec n m) as [-> | ->]; auto.
Defined.
(** * Compatibility properties of [max] *)
Lemma succ_max_distr : forall n m, S (max n m) = max (S n) (S m).
Proof.
auto.
Qed.
Lemma plus_max_distr_l : forall n m p, max (p + n) (p + m) = p + max n m.
Proof.
induction p; simpl; auto.
Qed.
Lemma plus_max_distr_r : forall n m p, max (n + p) (m + p) = max n m + p.
Proof.
intros n m p; repeat rewrite (plus_comm _ p).
apply plus_max_distr_l.
Qed.
(** * Semi-lattice algebraic properties of [max] *)
Lemma max_idempotent : forall n, max n n = n.
Proof.
intros; apply max_case; auto.
Qed.
Lemma max_assoc : forall m n p : nat, max m (max n p) = max (max m n) p.
Proof.
induction m; destruct n; destruct p; trivial.
simpl; auto.
Qed.
Lemma max_comm : forall n m, max n m = max m n.
Proof.
induction n; destruct m; simpl; auto.
Qed.
(** * Least-upper bound properties of [max] *)
Lemma max_l : forall n m, m <= n -> max n m = n.
Proof.
induction n; destruct m; simpl; auto with arith.
Qed.
Lemma max_r : forall n m, n <= m -> max n m = m.
Proof.
induction n; destruct m; simpl; auto with arith.
Qed.
Lemma le_max_l : forall n m, n <= max n m.
Proof.
induction n; simpl; auto with arith.
destruct m; simpl; auto with arith.
Qed.
Lemma le_max_r : forall n m, m <= max n m.
Proof.
induction n; simpl; auto with arith.
induction m; simpl; auto with arith.
Qed.
Hint Resolve max_r max_l le_max_l le_max_r: arith v62.
Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
Proof.
intros n m p; eapply le_trans. apply le_max_l.
Qed.
Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
Proof.
intros n m p; eapply le_trans. apply le_max_r.
Qed.
Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
Proof.
intros n m p; apply max_case; auto.
Qed.
(* begin hide *)
(* Compatibility *)
Notation max_case2 := max_case (only parsing).
Notation max_SS := succ_max_distr (only parsing).
(* end hide *)
|
