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___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $Id$ *)
Require BinInt.
Require Zeven.
Require Zorder.
Require Zcompare.
Require ZArith_dec.
Require Zsyntax.
Require Sumbool.
(** The decidability of equality and order relations over
type [Z] give some boolean functions with the adequate specification. *)
Definition Z_lt_ge_bool := [x,y:Z](bool_of_sumbool (Z_lt_ge_dec x y)).
Definition Z_ge_lt_bool := [x,y:Z](bool_of_sumbool (Z_ge_lt_dec x y)).
Definition Z_le_gt_bool := [x,y:Z](bool_of_sumbool (Z_le_gt_dec x y)).
Definition Z_gt_le_bool := [x,y:Z](bool_of_sumbool (Z_gt_le_dec x y)).
Definition Z_eq_bool := [x,y:Z](bool_of_sumbool (Z_eq_dec x y)).
Definition Z_noteq_bool := [x,y:Z](bool_of_sumbool (Z_noteq_dec x y)).
Definition Zeven_odd_bool := [x:Z](bool_of_sumbool (Zeven_odd_dec x)).
(**********************************************************************)
(** Boolean comparisons of binary integers *)
Definition Zle_bool :=
[x,y:Z]Cases `x ?= y` of SUPERIEUR => false | _ => true end.
Definition Zge_bool :=
[x,y:Z]Cases `x ?= y` of INFERIEUR => false | _ => true end.
Definition Zlt_bool :=
[x,y:Z]Cases `x ?= y` of INFERIEUR => true | _ => false end.
Definition Zgt_bool :=
[x,y:Z]Cases ` x ?= y` of SUPERIEUR => true | _ => false end.
Definition Zeq_bool :=
[x,y:Z]Cases `x ?= y` of EGAL => true | _ => false end.
Definition Zneq_bool :=
[x,y:Z]Cases `x ?= y` of EGAL => false | _ => true end.
Lemma Zle_cases : (x,y:Z)if (Zle_bool x y) then `x<=y` else `x>y`.
Proof.
Intros x y; Unfold Zle_bool Zle Zgt.
Case (Zcompare x y); Auto; Discriminate.
Qed.
Lemma Zlt_cases : (x,y:Z)if (Zlt_bool x y) then `x<y` else `x>=y`.
Proof.
Intros x y; Unfold Zlt_bool Zlt Zge.
Case (Zcompare x y); Auto; Discriminate.
Qed.
Lemma Zge_cases : (x,y:Z)if (Zge_bool x y) then `x>=y` else `x<y`.
Proof.
Intros x y; Unfold Zge_bool Zge Zlt.
Case (Zcompare x y); Auto; Discriminate.
Qed.
Lemma Zgt_cases : (x,y:Z)if (Zgt_bool x y) then `x>y` else `x<=y`.
Proof.
Intros x y; Unfold Zgt_bool Zgt Zle.
Case (Zcompare x y); Auto; Discriminate.
Qed.
(** Lemmas on [Zle_bool] used in contrib/graphs *)
Lemma Zle_bool_imp_le : (x,y:Z) (Zle_bool x y)=true -> (Zle x y).
Proof.
Unfold Zle_bool Zle. Intros x y. Unfold not.
Case (Zcompare x y); Intros; Discriminate.
Qed.
Lemma Zle_imp_le_bool : (x,y:Z) (Zle x y) -> (Zle_bool x y)=true.
Proof.
Unfold Zle Zle_bool. Intros x y. Case (Zcompare x y); Trivial. Intro. Elim (H (refl_equal ? ?)).
Qed.
Lemma Zle_bool_refl : (x:Z) (Zle_bool x x)=true.
Proof.
Intro. Apply Zle_imp_le_bool. Apply Zle_refl. Reflexivity.
Qed.
Lemma Zle_bool_antisym : (x,y:Z) (Zle_bool x y)=true -> (Zle_bool y x)=true -> x=y.
Proof.
Intros. Apply Zle_antisym. Apply Zle_bool_imp_le. Assumption.
Apply Zle_bool_imp_le. Assumption.
Qed.
Lemma Zle_bool_trans : (x,y,z:Z) (Zle_bool x y)=true -> (Zle_bool y z)=true -> (Zle_bool x z)=true.
Proof.
Intros x y z; Intros. Apply Zle_imp_le_bool. Apply Zle_trans with m:=y. Apply Zle_bool_imp_le. Assumption.
Apply Zle_bool_imp_le. Assumption.
Qed.
Definition Zle_bool_total : (x,y:Z) {(Zle_bool x y)=true}+{(Zle_bool y x)=true}.
Proof.
Intros x y; Intros. Unfold Zle_bool. Cut (Zcompare x y)=SUPERIEUR<->(Zcompare y x)=INFERIEUR.
Case (Zcompare x y). Left . Reflexivity.
Left . Reflexivity.
Right . Rewrite (proj1 ? ? H (refl_equal ? ?)). Reflexivity.
Apply Zcompare_ANTISYM.
Defined.
Lemma Zle_bool_plus_mono : (x,y,z,t:Z) (Zle_bool x y)=true -> (Zle_bool z t)=true ->
(Zle_bool (Zplus x z) (Zplus y t))=true.
Proof.
Intros. Apply Zle_imp_le_bool. Apply Zle_plus_plus. Apply Zle_bool_imp_le. Assumption.
Apply Zle_bool_imp_le. Assumption.
Qed.
Lemma Zone_pos : (Zle_bool `1` `0`)=false.
Proof.
Reflexivity.
Qed.
Lemma Zone_min_pos : (x:Z) (Zle_bool x `0`)=false -> (Zle_bool `1` x)=true.
Proof.
Intros x; Intros. Apply Zle_imp_le_bool. Change (Zle (Zs ZERO) x). Apply Zgt_le_S. Generalize H.
Unfold Zle_bool Zgt. Case (Zcompare x ZERO). Intro H0. Discriminate H0.
Intro H0. Discriminate H0.
Reflexivity.
Qed.
Lemma Zle_is_le_bool : (x,y:Z) (Zle x y) <-> (Zle_bool x y)=true.
Proof.
Intros. Split. Intro. Apply Zle_imp_le_bool. Assumption.
Intro. Apply Zle_bool_imp_le. Assumption.
Qed.
Lemma Zge_is_le_bool : (x,y:Z) (Zge x y) <-> (Zle_bool y x)=true.
Proof.
Intros. Split. Intro. Apply Zle_imp_le_bool. Apply Zge_le. Assumption.
Intro. Apply Zle_ge. Apply Zle_bool_imp_le. Assumption.
Qed.
Lemma Zlt_is_le_bool : (x,y:Z) (Zlt x y) <-> (Zle_bool x `y-1`)=true.
Proof.
Intros x y. Split. Intro. Apply Zle_imp_le_bool. Apply Zlt_n_Sm_le. Rewrite (Zs_pred y) in H.
Assumption.
Intro. Rewrite (Zs_pred y). Apply Zle_lt_n_Sm. Apply Zle_bool_imp_le. Assumption.
Qed.
Lemma Zgt_is_le_bool : (x,y:Z) (Zgt x y) <-> (Zle_bool y `x-1`)=true.
Proof.
Intros x y. Apply iff_trans with `y < x`. Split. Exact (Zgt_lt x y).
Exact (Zlt_gt y x).
Exact (Zlt_is_le_bool y x).
Qed.
|
