NumOf.v 9.54 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.

Fixpoint numof_aux (f : Z -> bool) (a : Z) (n : nat) : Z :=
  match n with
    | S n => (numof_aux f a n + (if f (a + (Z.of_nat n)) then 1%Z else 0%Z))%Z
    | 0 => 0%Z
  end.

(* Why3 goal *)
26
Definition numof : (Z -> bool) -> Z -> Z -> Z.
27
Proof.
28 29 30 31
  exact (fun f a b => numof_aux f a (Z.to_nat (b - a))).
Defined.

(* Why3 goal *)
32 33 34 35 36 37 38 39 40
Lemma numof_def : forall (p:(Z -> bool)) (a:Z) (b:Z), ((b <= a)%Z ->
  ((numof p a b) = 0%Z)) /\ ((~ (b <= a)%Z) -> ((((p (b - 1%Z)%Z) = true) ->
  ((numof p a b) = (1%Z + (numof p a (b - 1%Z)%Z))%Z)) /\ ((~ ((p
  (b - 1%Z)%Z) = true)) -> ((numof p a b) = (numof p a (b - 1%Z)%Z))))).
Proof.
intros p a b.
unfold numof.
split ; intros h1.
- assert (Z.to_nat (b - a) = 0).
41 42
  revert h1.
  rewrite <-Z.le_sub_0.
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
  now destruct (b - a)%Z.
  now rewrite H.
- rewrite S_pred with (m := 0) (n := Z.to_nat (b - a)).
  2: apply (Z2Nat.inj_lt 0); omega.
  rewrite <- Z2Nat.inj_pred.
  simpl numof_aux.
  rewrite Z2Nat.id by omega.
  replace (a + Zpred (b - a))%Z with (b - 1)%Z by (unfold Zpred ; ring).
  replace (Zpred (b - a)) with (b - 1 - a)%Z by (unfold Zpred ; ring).
  split ; intros h2.
  rewrite h2.
  apply Zplus_comm.
  apply Bool.not_true_is_false in h2.
  rewrite h2.
  apply Zplus_0_r.
58 59
Qed.

60 61 62 63 64
Lemma Numof_empty :
  forall p a b, (b <= a)%Z -> numof p a b = 0%Z.
Proof.
  intros p a b h1.
  now apply numof_def.
65 66 67
Qed.

(* Why3 goal *)
68 69
Lemma Numof_bounds :
  forall (p:(Z -> bool)) (a:Z) (b:Z),
70
  (a < b)%Z -> (0%Z <= (numof p a b))%Z /\ ((numof p a b) <= (b - a)%Z)%Z.
71
Proof.
72 73 74 75 76 77 78 79 80 81 82 83
  intros p a b h1.
  unfold numof.
  set (x := Z.to_nat (b - a)).
  rewrite <-Z2Nat.id with (n := (b - a)%Z) by omega.
  change (0 <= numof_aux p a x <= Z.of_nat x)%Z.
  induction x.
  simpl; omega.
  rewrite Nat2Z.inj_succ; simpl numof_aux.
  case (p (a + Z.of_nat x)%Z); omega.
Qed.

(* Why3 goal *)
84 85 86 87
Lemma Numof_append :
  forall (p:(Z -> bool)) (a:Z) (b:Z) (c:Z),
  ((a <= b)%Z /\ (b <= c)%Z) ->
  ((numof p a c) = ((numof p a b) + (numof p b c))%Z).
88
Proof.
89 90 91 92 93 94 95
  intros p a b c (h1,h2).
  pattern c.
  apply Zlt_lower_bound_ind with (z := b); auto.
  intros.
  case (Z.eq_dec b x).
  intro e; rewrite e.
  rewrite Numof_empty with (a := x) (b := x); omega.
96 97 98 99 100 101 102 103 104 105
  intro H6.
  refine (_ (proj2 (numof_def p a x) _)).
  intros [H1 H2].
  refine (_ (proj2 (numof_def p b x) _)).
  intros [H3 H4].
  destruct (Bool.bool_dec (p (x - 1)%Z) true) as [H5|H5].
  rewrite H1, H3, H ; auto with zarith.
  rewrite H2, H4, H ; auto with zarith.
  clear -H0 H6 ; omega.
  clear -h1 H0 H6 ; omega.
106 107 108
Qed.

Lemma numof_succ: forall p a, numof p a (a + 1) = (if p a then 1%Z else 0%Z).
109
Proof.
110 111 112 113 114 115 116 117 118
  intros.
  unfold numof.
  replace (a + 1 - a)%Z with 1%Z by omega.
  simpl.
  rewrite <-Zplus_0_r_reverse.
  trivial.
Qed.

Lemma numof_pred: forall p a, numof p (a - 1) a = (if p (a - 1)%Z then 1%Z else 0%Z).
119
Proof.
120
  intros.
121
  replace (numof p (a - 1) a)%Z with (numof p (a - 1) ((a - 1) + 1))%Z.
122
  apply numof_succ.
123 124
  repeat apply f_equal.
  omega.
125 126 127
Qed.

(* Why3 goal *)
128 129 130
Lemma Numof_left_no_add :
  forall (p:(Z -> bool)) (a:Z) (b:Z),
  (a < b)%Z -> ~ ((p a) = true) -> ((numof p a b) = (numof p (a + 1%Z)%Z b)).
131
Proof.
132 133 134 135 136 137 138 139
  intros p a b h1 h2.
  rewrite Numof_append with (b := (a+1)%Z) by omega.
  rewrite (numof_succ p a).
  apply Bool.not_true_is_false in h2.
  rewrite h2; trivial.
Qed.

(* Why3 goal *)
140 141 142
Lemma Numof_left_add : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z -> (((p
  a) = true) -> ((numof p a b) = (1%Z + (numof p (a + 1%Z)%Z b))%Z)).
Proof.
143 144 145 146 147 148 149
  intros p a b h1 h2.
  rewrite Numof_append with (b := (a+1)%Z) by omega.
  rewrite (numof_succ p a).
  rewrite h2; trivial.
Qed.

(* Why3 goal *)
150 151 152 153
Lemma Empty :
  forall (p:(Z -> bool)) (a:Z) (b:Z),
  (forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ~ ((p n) = true)) ->
  ((numof p a b) = 0%Z).
154
Proof.
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171
  intros p a b.
  case (Z_lt_le_dec a b); intro; [|intro; apply Numof_empty]; auto.
  pattern b.
  apply Zlt_lower_bound_ind with (z := a); auto with zarith; intros.
  case (Z.eq_dec a x); intro e.
  rewrite e; apply Numof_empty; omega.
  rewrite Numof_append with (b := (x - 1)%Z) by omega.
  assert (numof p (x - 1) x = 0)%Z.
  rewrite numof_pred.
  assert (a <= (x - 1)%Z < x)%Z as H2 by omega.
  generalize (H1 (x - 1)%Z H2).
  intro H3; apply Bool.not_true_is_false in H3; rewrite H3; trivial.
  rewrite H2.
  rewrite H; auto with zarith.
Qed.

(* Why3 goal *)
172
Lemma Full : forall (p:(Z -> bool)) (a:Z) (b:Z), (a <= b)%Z ->
173 174
  (forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ((p n) = true)) ->
  ((numof p a b) = (b - a)%Z).
175
Proof.
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191
  intros p a b h1.
  pattern b.
  apply Zlt_lower_bound_ind with (z := a); auto with zarith; intros.
  case (Z.eq_dec a x); intro e.
  rewrite e; rewrite Zminus_diag; apply Numof_empty; omega.
  rewrite Numof_append with (b := (x - 1)%Z) by omega.
  assert (numof p (x - 1) x = 1)%Z.
  rewrite numof_pred.
  assert (a <= (x - 1)%Z < x)%Z as H2 by omega.
  generalize (H1 (x - 1)%Z H2).
  intro; rewrite H3; trivial.
  rewrite H2.
  rewrite H; auto with zarith.
Qed.

Lemma numof_nat: forall p a b, (0 <= numof p a b)%Z.
192
Proof.
193 194 195 196 197 198 199 200 201 202 203 204 205 206
  intros.
  case (Z_lt_le_dec a b); intro; [|rewrite Numof_empty; auto with zarith].
  pattern b.
  apply Zlt_lower_bound_ind with (z := a) (x := b); auto with zarith; intros.
  case (Z.eq_dec a x); intro e.
  rewrite e; rewrite Numof_empty; omega.
  rewrite Numof_append with (b := (x - 1)%Z) by omega.
  apply Z.add_nonneg_nonneg.
  apply H; omega.
  rewrite numof_pred.
  case (p (x - 1)%Z); easy.
Qed.

Lemma numof_pos: forall p a b k, (a <= k < b)%Z -> p k = true -> (0 < numof p a b)%Z.
207
Proof.
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
  intros p a b k h.
  generalize h; pattern b.
  apply Zlt_lower_bound_ind with (z := (a + 1)%Z) (x := b); auto with zarith; intros.
  rewrite Z.add_1_r in H0; apply Zle_succ_gt in H0.
  rewrite Numof_append with (b := (x - 1)%Z) by omega.
  case (Z.eq_dec k (x-1)); intro e.
  rewrite e in H1.
  apply Z.add_nonneg_pos.
  apply numof_nat.
  rewrite numof_pred, H1; easy.
  apply Z.add_pos_nonneg.
  apply H; auto with zarith.
  apply numof_nat.
Qed.

(* Why3 goal *)
224 225
Lemma numof_increasing :
  forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z),
226 227
  ((i <= j)%Z /\ (j <= k)%Z) -> ((numof p i j) <= (numof p i k))%Z.
Proof.
228 229 230 231 232 233 234
intros p i j k (h1,h2).
rewrite (Numof_append p i j k) by omega.
rewrite <-Z.le_sub_le_add_l, Zminus_diag.
apply numof_nat.
Qed.

(* Why3 goal *)
235 236 237
Lemma numof_strictly_increasing :
  forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z) (l:Z),
  ((i <= j)%Z /\ ((j <= k)%Z /\ (k < l)%Z)) ->
238
  ((p k) = true) -> ((numof p i j) < (numof p i l))%Z.
239
Proof.
240 241 242 243 244 245 246
intros p i j k l (h1,(h2,h3)) h4.
rewrite (Numof_append p i j l) by omega.
rewrite <-Z.lt_sub_lt_add_l, Zminus_diag.
apply numof_pos with (k := k); auto with zarith.
Qed.

(* Why3 goal *)
247 248 249 250 251
Lemma numof_change_any :
  forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z),
  (forall (j:Z),
   ((a <= j)%Z /\ (j < b)%Z) -> ((p1 j) = true) -> ((p2 j) = true)) ->
  ((numof p1 a b) <= (numof p2 a b))%Z.
252
Proof.
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
  intros p1 p2 a b.
  case (Z_lt_le_dec a b); intro; [|rewrite Numof_empty, Numof_empty; omega].
  pattern b.
  apply Zlt_lower_bound_ind with (z := a); auto with zarith; intros.
  case (Z.eq_dec a x); intro eq.
  rewrite eq; rewrite Numof_empty, Numof_empty; omega.
  rewrite Numof_append with (b := (x-1)%Z) by omega.
  rewrite Numof_append with (p := p2) (b := (x-1)%Z) by omega.
  apply Z.add_le_mono.
  apply H; auto with zarith.
  rewrite numof_pred, numof_pred.
  case (Bool.bool_dec (p1 (x - 1)%Z) true); intro e.
  rewrite e, H1; auto with zarith.
  apply Bool.not_true_is_false in e; rewrite e.
  case (p2 (x -1 )%Z); easy.
Qed.

(* Why3 goal *)
271 272 273 274 275 276
Lemma numof_change_some :
  forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z) (i:Z),
  ((a <= i)%Z /\ (i < b)%Z) ->
  (forall (j:Z),
   ((a <= j)%Z /\ (j < b)%Z) -> ((p1 j) = true) -> ((p2 j) = true)) ->
  ~ ((p1 i) = true) -> ((p2 i) = true) -> ((numof p1 a b) < (numof p2 a b))%Z.
277
Proof.
278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
  intros p1 p2 a b i (h1,h2) h3 h4 h5.
  generalize (Z_le_lt_eq_dec _ _ (numof_change_any p1 p2 a b h3)).
  intro H; destruct H; trivial.
  cut False; auto with zarith.
  rewrite Numof_append with (b := i) in e by omega.
  rewrite Numof_append with (p := p2) (b := i) in e by omega.
  rewrite (Numof_left_add _ _ _ h2 h5), (Numof_left_no_add _ _ _ h2 h4) in e.
  assert (forall j : int, (a <= j < i)%Z -> p1 j = true -> p2 j = true) by auto with zarith.
  generalize (numof_change_any p1 p2 _ _ H).
  assert (forall j : int, ((i + 1) <= j < b)%Z -> p1 j = true -> p2 j = true) by auto with zarith.
  generalize (numof_change_any p1 p2 _ _ H0).
  omega.
Qed.

Lemma le_ge_eq: forall a b, (a <= b)%Z /\ (b <= a)%Z -> (a = b)%Z.
293
Proof.
294 295 296 297
  auto with zarith.
Qed.

(* Why3 goal *)
298 299 300
Lemma numof_change_equiv :
  forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z) (b:Z),
  (forall (j:Z),
301
   ((a <= j)%Z /\ (j < b)%Z) -> ((p1 j) = true) <-> ((p2 j) = true)) ->
302
  ((numof p2 a b) = (numof p1 a b)).
303
Proof.
304 305 306 307
intros p1 p2 a b h1.
apply le_ge_eq.
split; apply numof_change_any; apply h1.
Qed.
MARCHE Claude's avatar
MARCHE Claude committed
308