Commit 721c0867 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Update some Coq realizations.

parent 8b809621
......@@ -24,60 +24,50 @@ Fixpoint numof_aux (f : Z -> bool) (a : Z) (n : nat) : Z :=
(* Why3 goal *)
Definition numof: (Z -> bool) -> Z -> Z -> Z.
Proof.
exact (fun f a b => numof_aux f a (Z.to_nat (b - a))).
Defined.
(* Why3 goal *)
Lemma Numof_empty : forall (p:(Z -> bool)) (a:Z) (b:Z), (b <= a)%Z ->
((numof p a b) = 0%Z).
intros p a b h1.
unfold numof.
assert (Z.to_nat (b - a) = 0).
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).
revert h1.
rewrite <-Z.le_sub_0.
destruct (b - a)%Z; intro.
easy.
assert (0 < Z.pos p0)%Z by (apply Pos2Z.is_pos).
assert False by omega; easy.
apply Z2Nat.inj_neg.
rewrite H; easy.
Qed.
(* Why3 goal *)
Lemma Numof_right_no_add : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z ->
((~ ((p (b - 1%Z)%Z) = true)) -> ((numof p a b) = (numof p a
(b - 1%Z)%Z))).
intros p a b h1 h2.
unfold numof, numof.
rewrite S_pred with (m := 0) (n := Z.to_nat (b - a)).
rewrite <-Z2Nat.inj_pred.
simpl.
rewrite Z2Nat.id by omega.
rewrite <-Z.sub_pred_l, Z.add_sub_assoc, Int.Comm with (x := a), <-Z.add_sub_assoc, <-Zminus_diag_reverse, <- Z.sub_1_r, <-Zplus_0_r_reverse.
apply Bool.not_true_is_false in h2.
rewrite h2; omega.
change (Z.to_nat 0 < Z.to_nat (b - a)).
rewrite <-Z2Nat.inj_lt; omega.
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.
Qed.
(* Why3 goal *)
Lemma Numof_right_add : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z -> (((p
(b - 1%Z)%Z) = true) -> ((numof p a b) = (1%Z + (numof p a
(b - 1%Z)%Z))%Z)).
intros p a b h1 h2.
unfold numof, numof.
rewrite S_pred with (m := 0) (n := Z.to_nat (b - a)), <-Z2Nat.inj_pred.
simpl numof_aux.
rewrite Z2Nat.id by omega.
rewrite <-Z.sub_pred_l, Z.add_sub_assoc, Int.Comm with (x := a), <-Z.add_sub_assoc, <-Zminus_diag_reverse, <- Z.sub_1_r, <-Zplus_0_r_reverse.
rewrite h2; omega.
change (Z.to_nat 0 < Z.to_nat (b - a)).
rewrite <-Z2Nat.inj_lt; omega.
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.
Qed.
(* Why3 goal *)
Lemma Numof_bounds : forall (p:(Z -> bool)) (a:Z) (b:Z), (a < b)%Z ->
((0%Z <= (numof p a b))%Z /\ ((numof p a b) <= (b - a)%Z)%Z).
Proof.
intros p a b h1.
unfold numof.
set (x := Z.to_nat (b - a)).
......@@ -92,6 +82,7 @@ Qed.
(* Why3 goal *)
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).
Proof.
intros p a b c (h1,h2).
pattern c.
apply Zlt_lower_bound_ind with (z := b); auto.
......@@ -99,15 +90,20 @@ Lemma Numof_append : forall (p:(Z -> bool)) (a:Z) (b:Z) (c:Z), ((a <= b)%Z /\
case (Z.eq_dec b x).
intro e; rewrite e.
rewrite Numof_empty with (a := x) (b := x); omega.
intro.
destruct (Bool.bool_dec (p (x - 1)%Z) true).
rewrite Numof_right_add, Numof_right_add with (a := b) (b := x); auto with zarith.
generalize (H (x - 1)%Z).
intuition.
rewrite Numof_right_no_add, Numof_right_no_add with (a := b) (b := x); auto with zarith.
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.
Qed.
Lemma numof_succ: forall p a, numof p a (a + 1) = (if p a then 1%Z else 0%Z).
Proof.
intros.
unfold numof.
replace (a + 1 - a)%Z with 1%Z by omega.
......@@ -117,6 +113,7 @@ Lemma numof_succ: forall p a, numof p a (a + 1) = (if p a then 1%Z else 0%Z).
Qed.
Lemma numof_pred: forall p a, numof p (a - 1) a = (if p (a - 1)%Z then 1%Z else 0%Z).
Proof.
intros.
replace (numof p (a - 1) a)%Z with (numof p (a - 1) ((a - 1) + 1))%Z.
apply numof_succ.
......@@ -127,6 +124,7 @@ Qed.
(* Why3 goal *)
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))).
Proof.
intros p a b h1 h2.
rewrite Numof_append with (b := (a+1)%Z) by omega.
rewrite (numof_succ p a).
......@@ -137,6 +135,7 @@ Qed.
(* Why3 goal *)
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.
intros p a b h1 h2.
rewrite Numof_append with (b := (a+1)%Z) by omega.
rewrite (numof_succ p a).
......@@ -146,6 +145,7 @@ Qed.
(* Why3 goal *)
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).
Proof.
intros p a b.
case (Z_lt_le_dec a b); intro; [|intro; apply Numof_empty]; auto.
pattern b.
......@@ -166,6 +166,7 @@ Qed.
Lemma Full : forall (p:(Z -> bool)) (a:Z) (b:Z), (a <= b)%Z ->
((forall (n:Z), ((a <= n)%Z /\ (n < b)%Z) -> ((p n) = true)) -> ((numof p a
b) = (b - a)%Z)).
Proof.
intros p a b h1.
pattern b.
apply Zlt_lower_bound_ind with (z := a); auto with zarith; intros.
......@@ -182,6 +183,7 @@ Lemma Full : forall (p:(Z -> bool)) (a:Z) (b:Z), (a <= b)%Z ->
Qed.
Lemma numof_nat: forall p a b, (0 <= numof p a b)%Z.
Proof.
intros.
case (Z_lt_le_dec a b); intro; [|rewrite Numof_empty; auto with zarith].
pattern b.
......@@ -196,6 +198,7 @@ Lemma numof_nat: forall p a b, (0 <= numof p a b)%Z.
Qed.
Lemma numof_pos: forall p a b k, (a <= k < b)%Z -> p k = true -> (0 < numof p a b)%Z.
Proof.
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.
......@@ -214,6 +217,7 @@ Qed.
(* Why3 goal *)
Lemma numof_increasing : forall (p:(Z -> bool)) (i:Z) (j:Z) (k:Z),
((i <= j)%Z /\ (j <= k)%Z) -> ((numof p i j) <= (numof p i k))%Z.
Proof.
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.
......@@ -224,6 +228,7 @@ Qed.
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)) -> (((p k) = true) ->
((numof p i j) < (numof p i l))%Z).
Proof.
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.
......@@ -234,6 +239,7 @@ Qed.
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.
Proof.
intros p1 p2 a b.
case (Z_lt_le_dec a b); intro; [|rewrite Numof_empty, Numof_empty; omega].
pattern b.
......@@ -256,6 +262,7 @@ 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))).
Proof.
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.
......@@ -271,6 +278,7 @@ Lemma numof_change_some : forall (p1:(Z -> bool)) (p2:(Z -> bool)) (a:Z)
Qed.
Lemma le_ge_eq: forall a b, (a <= b)%Z /\ (b <= a)%Z -> (a = b)%Z.
Proof.
auto with zarith.
Qed.
......@@ -278,7 +286,9 @@ Qed.
Lemma numof_change_equiv : 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 p2 a b) = (numof p1 a b)).
Proof.
intros p1 p2 a b h1.
apply le_ge_eq.
split; apply numof_change_any; apply h1.
Qed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment