Library abstraction_phd_aux
Set Implicit Arguments.
Require Import Setoid.
Require Import floor.
Require Import Bool.
Require Import Omega.
Require Import ZArith.
Require Import Znumtheory.
Require Import Z_misc.
Require Import QArith.
Require Import Q_misc.
Require Import comparison.
Require Import misc.
Require Import ibw_def.
Require Import ibw_aux.
Require Import ibw_prop.
Require Import abstraction_phd_def.
Section Abstraction_phd_def.
Definition abs_equal (a1: abstraction_phd) (a2:abstraction_phd) :=
(abs_r a1 == abs_r a2) /\
(abs_b1 a1) == (abs_b1 a2) /\
(abs_b0 a1) == (abs_b0 a2).
Instance abs_equal_is_equiv : Equivalence abs_equal.
Proof.
constructor ; unfold abs_equal ; red ; intuition.
transitivity (abs_r y) ; auto.
transitivity (abs_b1 y) ; auto.
transitivity (abs_b0 y) ; auto.
Qed.
End Abstraction_phd_def.
Definition abs_equiv (a1: abstraction_phd) (a2:abstraction_phd) :=
abs_included a1 a2 /\ abs_included a2 a1.
Definition abs_equiv_test (a1: abstraction_phd) (a2:abstraction_phd) :=
abs_included_test a1 a2 /\ abs_included_test a2 a1.
Section abstraction_equivalence_properties.
Property abs_included_test_impl_abs_included:
forall a1 a2: abstraction_phd,
forall H_a1_in_test_a2: abs_included_test a1 a2,
abs_included a1 a2.
Proof.
intros.
unfold abs_included.
intros.
unfold in_abstraction_phd.
intros.
case_eq i.
intros H_i.
rewrite H_i in H_i_ge_1.
absurd ((0 >= 1)%nat); auto.
apply gt_not_le.
auto.
intros i' H_i.
rewrite <- H_i.
elim (H_w_in_a1 i H_i_ge_1).
intros H_le H_ge.
elim H_a1_in_test_a2.
intros H_r H_tmp.
elim H_tmp; clear H_tmp.
intros H_one H_zero.
rewrite <- H_r.
split.
intro H_w.
apply
(Qle_trans
(ones w i)
(abs_r a1 * i + abs_b1 a1)
(abs_r a1 * i + abs_b1 a2)); auto.
apply Qplus_le_compat; auto.
apply Qle_refl.
intro H_w.
apply
(Qle_trans
(abs_r a1 * i + abs_b0 a2)
(abs_r a1 * i + abs_b0 a1)
(ones w i)); auto.
apply Qplus_le_compat; auto.
apply Qle_refl.
Qed.
Property w_in_a1_and_a1_in_a2_impl_w_in_a2:
forall w a1 a2,
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_wf_a2: well_formed_abstraction_phd a2,
forall H_a1_in_a2: abs_included_test a1 a2,
forall H_w_in_a1: in_abstraction_phd w a1,
in_abstraction_phd w a2.
Proof.
intros.
unfold in_abstraction_phd.
intros i H_i_ge_1.
split.
intro H_w.
unfold in_abstraction_phd in H_w_in_a1.
generalize (H_w_in_a1 i H_i_ge_1).
intro H_w_in_a1_i.
elim H_w_in_a1_i.
intros H_w_in_a1_true H_w_in_a1_false.
generalize (H_w_in_a1_true H_w).
clear H_w_in_a1_i H_w_in_a1_true H_w_in_a1_false.
intro H_w_le_a1.
elim H_a1_in_a2.
intros H_r1_eq_r2 H_aux.
elim H_aux. clear H_aux.
intros H_d2_le_d1 H_D1_le_D2.
rewrite <- H_r1_eq_r2.
apply (Qle_trans
(ones w i)
(abs_r a1 * i + abs_b1 a1)
(abs_r a1 * i + abs_b1 a2)
H_w_le_a1).
apply Qplus_le_compat; auto.
apply Qmult_le_compat_r; try solve [apply Qle_refl].
unfold Q_of_nat, Qle; simpl; auto with zarith.
intro H_w.
unfold in_abstraction_phd in H_w_in_a1.
generalize (H_w_in_a1 i H_i_ge_1).
intro H_w_in_a1_i.
elim H_w_in_a1_i.
intros H_w_in_a1_true H_w_in_a1_false.
generalize (H_w_in_a1_false H_w).
clear H_w_in_a1_i H_w_in_a1_true H_w_in_a1_false.
intro H_a1_le_w.
elim H_a1_in_a2.
intros H_r1_eq_r2 H_aux.
elim H_aux. clear H_aux.
intros H_d2_le_d1 H_D1_le_D2.
rewrite <- H_r1_eq_r2.
apply
(Qle_trans
(abs_r a1 * i + abs_b0 a2)
(abs_r a1 * i + abs_b0 a1)
(ones w i));
auto.
apply Qplus_le_compat; auto.
apply Qmult_le_compat_r; try solve [apply Qle_refl].
apply (Qle_trans 0 1 i).
unfold Q_of_nat, Qle; simpl; auto with zarith.
apply (le_impl_Qle H_i_ge_1).
Qed.
Property abs_weakening_aux:
forall a1 a2: abstraction_phd,
forall H_one: abs_b1 a1 <= abs_b1 a2,
forall H_abs_b0: abs_b0 a1 >= abs_b0 a2,
forall H_r: abs_r a1 == abs_r a2,
abs_included_test a1 a2.
Proof.
intros.
unfold abs_included_test.
repeat split; auto.
Qed.
Property abs_weakening_0:
forall a1 a2: abstraction_phd,
forall H_abs_b01: abs_b0 a1 > 0,
forall H_r: abs_r a1 == abs_r a2,
forall H_one: abs_b1 a1 == abs_b1 a2,
forall H_abs_b02: abs_b0 a2 == 0,
abs_included_test a1 a2.
Proof.
intros.
eapply abs_weakening_aux; auto.
rewrite H_one.
apply Qle_refl.
rewrite H_abs_b02.
eapply Qlt_le_weak.
assumption.
Qed.
Property abs_equal_sym:
forall a1 a2: abstraction_phd,
forall H_a1_eq_a2: abs_equal a1 a2,
abs_equal a2 a1.
Proof.
intros.
elim H_a1_eq_a2.
intros H_r H_tmp.
elim H_tmp; clear H_tmp.
intros H_one H_zero.
repeat split;
symmetry;
assumption.
Qed.
Property abs_equal_impl_abs_included_test:
forall a1 a2: abstraction_phd,
forall H_a1_eq_a2: abs_equal a1 a2,
abs_included_test a1 a2.
Proof.
intros.
elim H_a1_eq_a2.
intros H_r H_tmp.
elim H_tmp; clear H_tmp.
intros H_one H_zero.
repeat split.
trivial.
rewrite H_one.
apply Qle_refl.
rewrite H_zero.
apply Qle_refl.
Qed.
Property abs_equal_impl_abs_equiv_test:
forall a1 a2: abstraction_phd,
forall H_a1_eq_a2: abs_equal a1 a2,
abs_equiv_test a1 a2.
Proof.
intros.
split.
apply abs_equal_impl_abs_included_test; auto.
apply abs_equal_impl_abs_included_test; auto.
apply abs_equal_sym.
assumption.
Qed.
Property abs_equiv_test_impl_abs_equal:
forall a1 a2: abstraction_phd,
forall H_a1_eq_a2: abs_equiv_test a1 a2,
abs_equal a1 a2.
Proof.
intros.
elim H_a1_eq_a2.
intros H_tmp1 H_tmp2.
elim H_tmp1; clear H_tmp1.
intros H_r H_tmp'.
elim H_tmp'; clear H_tmp'.
intros H_abs_b11_le_abs_b12 H_abs_b02_le_abs_b01.
elim H_tmp2; clear H_tmp2.
intros H_r' H_tmp'.
elim H_tmp'; clear H_tmp' H_r'.
intros H_abs_b12_le_abs_b11 H_abs_b01_le_abs_b02.
repeat split.
trivial.
apply Qle_antisym; assumption.
apply Qle_antisym; assumption.
Qed.
Property abs_equal_correctness:
forall a1 a2: abstraction_phd,
forall H_wf1: well_formed_abstraction_phd a1,
forall H_wf2: well_formed_abstraction_phd a2,
forall w: ibw,
forall H_w_in_a1: in_abstraction_phd w a1,
forall H_eq: abs_equal a1 a2,
in_abstraction_phd w a2.
Proof.
intros.
apply abs_equal_impl_abs_included_test in H_eq.
exact (w_in_a1_and_a1_in_a2_impl_w_in_a2 H_wf1 H_wf2 H_eq H_w_in_a1).
Qed.
Property well_formed_abstraction_phd_abs_equal_compat:
forall a1 a2: abstraction_phd,
forall H_eq: abs_equal a1 a2,
forall H_wf1: well_formed_abstraction_phd a1,
well_formed_abstraction_phd a2.
Proof.
intros.
destruct H_eq as [H_r [H_b1 H_b0]].
unfold well_formed_abstraction_phd in *.
rewrite <- H_r.
assumption.
Qed.
End abstraction_equivalence_properties.
Fixpoint ones_early_opt (a:abstraction_phd) (i:nat) { struct i } :=
match i with
| O => Some O
| S i' =>
let ones_i'_opt := ones_early_opt a i' in
match ones_i'_opt with
| None => None
| Some ones_i' =>
match Qcompare (S ones_i') (abs_r a * i + abs_b1 a) with
| Lt | Eq => Some (S ones_i')
| Gt =>
match Qcompare (abs_r a * i + abs_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| _ => None
end
end
end
end.
Fixpoint ones_late_opt (a:abstraction_phd) (i:nat) { struct i } :=
match i with
| O => Some O
| S i' =>
let ones_i'_opt := ones_late_opt a i' in
match ones_i'_opt with
| None => None
| Some ones_i' =>
match Qcompare (abs_r a * i + abs_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| Gt =>
match Qcompare (S ones_i') (abs_r a * i + abs_b1 a) with
| Lt | Eq => Some (S ones_i')
| Gt => None
end
end
end
end.
Definition non_empty_alt (a: abstraction_phd) :=
forall i, (ones_late a i <= ones_early a i)%nat.
Section early_and_late_properties.
Lemma red_ones_early:
forall a i',
(ones_early a (S i') =
match S (ones_early a i') ?= abs_r a * S i' + abs_b1 a with
| Eq => S (ones_early a i')
| Lt => S (ones_early a i')
| Gt => ones_early a i'
end)%nat.
Proof.
intros.
simpl.
reflexivity.
Qed.
Lemma red_ones_late:
forall a i',
(ones_late a (S i') =
match abs_r a * (S i') + abs_b0 a ?= ones_late a i' with
| Lt | Eq => ones_late a i'
| Gt => S (ones_late a i')
end)%nat.
Proof.
intros.
simpl.
reflexivity.
Qed.
Lemma red_ones_early_opt:
forall a i',
(ones_early_opt a (S i') =
match ones_early_opt a i' with
| None => None
| Some ones_i' =>
match Qcompare (S ones_i') (abs_r a * S i' + abs_b1 a) with
| Lt | Eq => Some (S ones_i')
| Gt =>
match Qcompare (abs_r a * S i' + abs_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| _ => None
end
end
end)%nat.
Proof.
intros.
simpl.
reflexivity.
Qed.
Lemma red_ones_late_opt:
forall a i',
(ones_late_opt a (S i') =
match ones_late_opt a i' with
| None => None
| Some ones_i' =>
match Qcompare (abs_r a * S i' + abs_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| Gt =>
match Qcompare (S ones_i') (abs_r a * S i' + abs_b1 a) with
| Lt | Eq => Some (S ones_i')
| Gt => None
end
end
end)%nat.
Proof.
intros.
simpl.
reflexivity.
Qed.
Lemma ones_early_alt_remove_Zabs_nat:
forall a:abstraction_phd,
forall i,
((Z_of_nat (ones_early_alt a i))%Z =
Zmax O (Zmin i (fl (abs_r a * i + abs_b1 a))))%Z.
Proof.
intros.
unfold ones_early_alt.
rewrite inj_Zabs_nat.
elim (Zabs_spec (Zmax O (Zmin i (fl (abs_r a * i + abs_b1 a))))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
elim (Zmax_spec O (Zmin i (fl (abs_r a * i + abs_b1 a)))).
intro H_tmp; destruct H_tmp.
rewrite H2.
auto.
intro H_tmp; destruct H_tmp.
rewrite H2 in H.
assert (H_aux: Z_of_nat 0%nat = 0%Z); omega.
Qed.
Lemma ones_late_alt_remove_Zabs_nat:
forall a:abstraction_phd,
forall i,
((Z_of_nat (ones_late_alt a i))%Z =
Zmax O (Zmin i (cg (abs_r a * i + abs_b0 a))))%Z.
Proof.
intros.
unfold ones_late_alt.
rewrite inj_Zabs_nat.
elim (Zabs_spec (Zmax O (Zmin i (cg (abs_r a * i + abs_b0 a))))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
elim (Zmax_spec O (Zmin i (cg (abs_r a * i + abs_b0 a)))).
intro H_tmp; destruct H_tmp.
rewrite H2.
auto.
intro H_tmp; destruct H_tmp.
rewrite H2 in H.
assert (H_aux: Z_of_nat 0%nat = 0%Z); omega.
Qed.
Property ones_early_well_formed:
forall a: abstraction_phd,
well_formed_ones (ones_early a).
Proof.
intros.
split.
simpl.
reflexivity.
intro.
simpl.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
intro H_cmp.
left.
reflexivity.
intro H_cmp.
left.
reflexivity.
intro H_cmp.
right.
reflexivity.
Qed.
Property ones_late_well_formed:
forall a: abstraction_phd,
well_formed_ones (ones_late a).
Proof.
intros.
split.
simpl.
reflexivity.
intro.
simpl.
case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
omega.
Qed.
Property w_early_well_formed:
forall a,
well_formed_ibw (w_early a).
Proof.
intros.
unfold well_formed_ibw.
simpl.
reflexivity.
Qed.
Property w_late_well_formed:
forall a,
well_formed_ibw (w_late a).
Proof.
intros.
unfold well_formed_ibw.
simpl.
reflexivity.
Qed.
Property ones_early_eq_ones_w_early:
forall a: abstraction_phd,
forall i,
(ones_early a i = ones (w_early a) i)%nat.
Proof.
intros.
case i.
simpl.
reflexivity.
clear i.
intro i'.
induction i'.
simpl.
case_eq (1%nat ?= abs_r a * 1%nat + abs_b1 a);
intros;
simpl;
reflexivity.
assert (H_aux:
(ones_early a (S (S i'))
=
match S (ones_early a (S i')) ?= abs_r a * (S (S i')) + abs_b1 a with
| Eq => S (ones_early a (S i'))
| Lt => S (ones_early a (S i'))
| Gt => ones_early a (S i')
end)%nat).
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
assert (H_aux:
(ones (w_early a) (S (S i'))
=
((if negb
(beq_nat
match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
| Eq => S (ones_early a (S i'))
| Lt => S (ones_early a (S i'))
| Gt => ones_early a (S i')
end (ones_early a (S i')))
then 1
else 0) + ones (w_early a) (S i'))%nat)%nat).
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a).
intro.
assert (H_aux:
beq_nat (S (ones_early a (S i'))) (ones_early a (S i')) = false).
apply S_n_nbeq_n.
rewrite H_aux; clear H_aux.
assert (H_aux: ((if negb false then 1 else 0) = 1)%nat).
auto.
rewrite H_aux; clear H_aux.
unfold plus.
rewrite IHi'.
reflexivity.
intro.
assert (H_aux:
beq_nat (S (ones_early a (S i'))) (ones_early a (S i')) = false).
apply S_n_nbeq_n.
rewrite H_aux; clear H_aux.
assert (H_aux: ((if negb false then 1 else 0) = 1)%nat).
auto.
rewrite H_aux; clear H_aux.
unfold plus.
rewrite IHi'.
reflexivity.
intro.
assert (H_aux:
beq_nat ((ones_early a (S i'))) (ones_early a (S i')) = true).
rewrite <- beq_nat_refl.
trivial.
rewrite H_aux; clear H_aux.
assert (H_aux: ((if negb true then 1 else 0) = 0)%nat).
auto.
rewrite H_aux; clear H_aux.
unfold plus.
rewrite IHi'.
reflexivity.
Qed.
Property ones_late_eq_ones_w_late:
forall a: abstraction_phd,
forall i,
(ones_late a i = ones (w_late a) i)%nat.
Proof.
intros.
case i.
simpl.
reflexivity.
clear i.
intro i'.
induction i'.
simpl.
case_eq (abs_r a * 1%nat + abs_b0 a ?= 0%nat);
intros;
simpl;
reflexivity.
rewrite red_ones_late.
assert (H_aux:
(ones (w_late a) (S (S i'))
=
((if negb
(beq_nat
match abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i') with
| Eq | Lt => ones_late a (S i')
| Gt => S (ones_late a (S i'))
end (ones_late a (S i')))
then 1
else 0) + ones (w_late a) (S i'))%nat)%nat).
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
case_eq (abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i')).
intro.
assert (H_aux:
beq_nat ((ones_late a (S i'))) (ones_late a (S i')) = true).
rewrite <- beq_nat_refl.
trivial.
rewrite H_aux; clear H_aux.
assert (H_aux: ((if negb true then 1 else 0) = 0)%nat).
auto.
rewrite H_aux; clear H_aux.
unfold plus.
rewrite IHi'.
reflexivity.
intro.
assert (H_aux:
beq_nat ((ones_late a (S i'))) (ones_late a (S i')) = true).
rewrite <- beq_nat_refl.
trivial.
rewrite H_aux; clear H_aux.
assert (H_aux: ((if negb true then 1 else 0) = 0)%nat).
auto.
rewrite H_aux; clear H_aux.
unfold plus.
rewrite IHi'.
reflexivity.
intro.
assert (H_aux:
beq_nat (S (ones_late a (S i'))) (ones_late a (S i')) = false).
apply S_n_nbeq_n.
rewrite H_aux; clear H_aux.
assert (H_aux: ((if negb false then 1 else 0) = 1)%nat).
auto.
rewrite H_aux; clear H_aux.
unfold plus.
rewrite IHi'.
reflexivity.
Qed.
Property ones_early_eq_ones_early_alt:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall i,
ones_early a i = ones_early_alt a i.
Proof.
induction i.
simpl.
apply Zeq_impl_nat_eq.
rewrite ones_early_alt_remove_Zabs_nat.
elim (Zmax_spec O (Zmin O%nat (fl (abs_r a * O%nat + abs_b1 a)))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
rewrite H0.
elim (Zmin_spec 0%nat (fl (abs_r a * 0%nat + abs_b1 a))).
intro H_tmp; destruct H_tmp.
rewrite H2.
reflexivity.
intro H_tmp; destruct H_tmp.
rewrite H2 in H.
congruence.
apply Zeq_impl_nat_eq.
rewrite ones_early_alt_remove_Zabs_nat.
elim (Zmax_spec O (Zmin (S i) (fl (abs_r a * S i + abs_b1 a)))).
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (fl (abs_r a * (S i) + abs_b1 a))).
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
absurd (0%nat >= S i)%Z; auto.
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
assert (H_cc_aux1: ones_early a i = 0%nat).
rewrite IHi.
apply Zeq_impl_nat_eq.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite Zmax_left; auto.
rewrite Zmin_right.
apply
(Zge_trans
0%nat
(fl (abs_r a * S i + abs_b1 a))
(fl (abs_r a * i + abs_b1 a))); auto.
apply Zle_ge.
apply fl_monotone_linear.
assert (H_aux:
abs_r a * i + abs_b1 a ==
abs_r a * i + abs_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
abs_r a * i + abs_b1 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
destruct H_wf; assumption.
apply Zgt_impl_Zge.
assert (H_aux: (i + 1%nat)%Z = S i).
assert (H_aux: (Z_of_nat (i + 1%nat)%nat = (i + 1%nat)%Z)%Z).
apply inj_plus.
rewrite <- H_aux; clear H_aux.
rewrite plus_comm.
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
apply (Zgt_le_trans
(S i)
(fl (abs_r a * S i + abs_b1 a))
(fl (abs_r a * i + abs_b1 a))); auto.
apply fl_monotone_linear.
assert (H_aux:
abs_r a * i + abs_b1 a ==
abs_r a * i + abs_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
abs_r a * i + abs_b1 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
destruct H_wf; assumption.
assert (H_cc_aux2: S (ones_early a i) > abs_r a * S i + abs_b1 a).
clear H0; clear H2.
rewrite H_cc_aux1.
apply (Qlt_le_trans
(abs_r a * S i + abs_b1 a)
(fl (abs_r a * S i + abs_b1 a) + 1)
1).
destruct (fl_def (abs_r a * S i + abs_b1 a)); assumption.
assert (H_aux: forall x, fl x + 1 == (fl x + 1)%Z).
intro; unfold Qeq, Qplus, Q_of_nat; simpl; ring_simplify; auto.
rewrite H_aux; clear H_aux.
apply Zle_impl_Qle.
assert (H_aux: (1 = 0 + 1)%Z).
auto with zarith.
rewrite H_aux; clear H_aux.
apply Zplus_le_compat_r.
apply Zge_le.
assumption.
rewrite red_ones_early.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
try solve [ intro H_cmp; apply inj_eq; assumption].
intro H_cmp.
rewrite <- Qeq_alt in H_cmp.
absurd (S (ones_early a i) > abs_r a * S i + abs_b1 a); auto.
apply Qle_not_lt.
rewrite H_cmp.
apply Qle_refl.
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
absurd (S (ones_early a i) < abs_r a * S i + abs_b1 a); auto.
apply Qle_not_lt.
apply Qlt_le_weak.
assumption.
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (fl (abs_r a * (S i) + abs_b1 a))).
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
assert (H_cc_aux1: ones_early a i = i).
rewrite IHi.
apply Zeq_impl_nat_eq.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite Zmin_left.
rewrite Zmax_right.
trivial.
apply inj_le.
auto with arith.
apply Zlt_impl_Zle.
apply (Zlt_le_trans
i
(S i)
(fl (abs_r a * i + abs_b1 a) + 1%nat)).
apply inj_lt.
auto with arith.
rewrite <- fl_plus_int_rewrite.
apply (Zle_trans
(S i)
(fl (abs_r a * S i + abs_b1 a))
(fl (abs_r a * i + abs_b1 a + 1))); auto.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
abs_r a * i + abs_b1 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
destruct H_wf; assumption.
assert (H_cc_aux2: S (ones_early a i) <= abs_r a * S i + abs_b1 a).
rewrite H_cc_aux1.
apply (Qle_trans
(S i)
(fl (abs_r a * S i + abs_b1 a))
(abs_r a * S i + abs_b1 a));
try solve [ elim (fl_def (abs_r a * S i + abs_b1 a)); auto ].
apply Zle_impl_Qle.
assumption.
rewrite red_ones_early.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a); auto.
intro H_cmp.
rewrite Qle_alt in H_cc_aux2.
rewrite H_cmp in H_cc_aux2.
congruence.
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
clear H2 H0.
rewrite ones_early_eq_ones_w_early.
case_eq (w_early a (S i)).
intro H_w_early.
rewrite ones_S_i_eq_S_ones_i; auto.
rewrite <- ones_early_eq_ones_w_early.
rewrite IHi.
assert (H_aux: (Z_of_nat (1 + ones_early_alt a i)) = (1 + ones_early_alt a i)%Z).
apply inj_plus.
rewrite H_aux; clear H_aux.
assert (H_cmp: S (ones_early a i) <= abs_r a * S i + abs_b1 a).
rewrite Qle_alt.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
try solve [congruence].
intro H_cmp;
simpl in H_w_early;
rewrite H_cmp in H_w_early;
rewrite <- beq_nat_refl in H_w_early;
simpl in H_w_early;
congruence.
rewrite IHi in H_cmp.
apply Zle_antisym.
assert (TH_aux: forall (x: nat) (y: Z), (x < y)%Z -> (1%nat + x <= y)%Z).
intros x y H_lt.
replace (1%nat + x)%Z with (- ( -(1) + - x))%Z by ring.
apply Zle_0_minus_le.
unfold Zminus.
rewrite Zopp_involutive.
rewrite Zplus_assoc.
apply Zlt_left.
assumption.
apply TH_aux; auto.
apply Qlt_impl_Zlt.
apply -> (Qlt_plus 1%nat).
assert (H_aux: (1%nat + ones_early_alt a i) == S (ones_early_alt a i)).
rewrite Qplus_comm.
rewrite n_plus_1_eq_S_n.
apply Qeq_refl.
rewrite H_aux; clear H_aux.
rewrite Qplus_comm.
apply
(Qle_lt_trans
(S (ones_early_alt a i))
(abs_r a * S i + abs_b1 a)
(fl (abs_r a * S i + abs_b1 a) + 1)); auto.
elim (fl_def (abs_r a * S i + abs_b1 a)); auto.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite Zmin_right; auto.
rewrite Zmax_right.
rewrite Zplus_comm.
rewrite <- fl_plus_int_rewrite.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
abs_r a * i + abs_b1 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
replace 1%Z with (Z_of_nat 1); auto.
destruct H_wf; auto.
apply Zlt_impl_Zle.
apply
(Zlt_le_trans
0%nat
(fl (abs_r a * S i + abs_b1 a))
(fl (abs_r a * i + abs_b1 a) + 1%nat)); auto.
rewrite <- fl_plus_int_rewrite.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
abs_r a * i + abs_b1 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
destruct H_wf; auto.
apply
(Zge_trans
i
(fl (abs_r a * S i + abs_b1 a))
(fl (abs_r a * i + abs_b1 a))).
assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
intros x y H_gt.
apply Zgt_impl_Zge.
assert (H_aux: (x + 1%nat)%Z = S x).
assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
apply inj_plus.
rewrite <- H_aux; clear H_aux.
rewrite plus_comm.
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
assumption.
apply TH_aux; auto.
apply Zle_ge.
apply fl_monotone_linear.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite Qmult_comm.
assert (H_aux: abs_r a * S i == S i * abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
destruct H_wf; auto.
intro H_w_early.
rewrite ones_S_i_eq_ones_i; auto.
rewrite <- ones_early_eq_ones_w_early.
rewrite IHi.
assert (H_cmp: S (ones_early a i) > abs_r a * S i + abs_b1 a).
rewrite Qgt_alt.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
intro H_cmp.
simpl in H_w_early.
rewrite H_cmp in H_w_early.
rewrite S_n_nbeq_n in H_w_early.
simpl in H_w_early;
congruence.
intro H_cmp.
simpl in H_w_early.
rewrite H_cmp in H_w_early.
rewrite S_n_nbeq_n in H_w_early.
simpl in H_w_early;
congruence.
intro H_cmp.
auto.
rewrite IHi in H_cmp.
apply Zle_antisym.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite Zmin_right; auto.
rewrite Zmax_right.
apply fl_monotone_linear.
assert (H_aux:
abs_r a * i + abs_b1 a ==
abs_r a * i + abs_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
abs_r a * i + abs_b1 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
destruct H_wf; assumption.
apply Zlt_impl_Zle.
apply (Zlt_le_trans
0%nat
(fl (abs_r a * S i + abs_b1 a))
(fl (abs_r a * i + abs_b1 a) + 1%nat)); auto.
rewrite <- fl_plus_int_rewrite.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
abs_r a * i + abs_b1 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
destruct H_wf; auto.
apply
(Zge_trans
i
(fl (abs_r a * S i + abs_b1 a))
(fl (abs_r a * i + abs_b1 a))).
assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
intros x y H_gt.
apply Zgt_impl_Zge.
assert (H_aux: (x + 1%nat)%Z = S x).
assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
apply inj_plus.
rewrite <- H_aux; clear H_aux.
rewrite plus_comm.
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
assumption.
apply TH_aux.
auto.
apply Zle_ge.
apply fl_monotone_linear.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite Qmult_comm.
assert (H_aux: abs_r a * S i == S i * abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
destruct H_wf; auto.
apply Zlt_impl_Zle.
apply Qlt_impl_Zlt.
apply
(Qle_lt_trans
(fl (abs_r a * S i + abs_b1 a))
(abs_r a * S i + abs_b1 a)
(ones_early_alt a i + 1%nat)%Z); auto.
elim (fl_def (abs_r a * S i + abs_b1 a)); auto.
rewrite <- inj_plus.
assert (H_aux: (ones_early_alt a i + 1%nat)%nat = S (ones_early_alt a i)).
rewrite plus_comm.
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
assumption.
Qed.
Property ones_late_eq_ones_late_alt:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall i,
ones_late a i = ones_late_alt a i.
Proof.
induction i.
simpl.
apply Zeq_impl_nat_eq.
rewrite ones_late_alt_remove_Zabs_nat.
elim (Zmax_spec O (Zmin O%nat (cg (abs_r a * O%nat + abs_b0 a)))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
rewrite H0.
elim (Zmin_spec 0%nat (cg (abs_r a * 0%nat + abs_b0 a))).
intro H_tmp; destruct H_tmp.
rewrite H2.
reflexivity.
intro H_tmp; destruct H_tmp.
rewrite H2 in H.
congruence.
apply Zeq_impl_nat_eq.
rewrite ones_late_alt_remove_Zabs_nat.
elim (Zmax_spec O (Zmin (S i) (cg (abs_r a * S i + abs_b0 a)))).
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (abs_r a * (S i) + abs_b0 a))).
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
absurd (0%nat >= S i)%Z; auto.
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
assert (H_cc_aux1: ones_late a i = 0%nat).
rewrite IHi.
apply Zeq_impl_nat_eq.
rewrite ones_late_alt_remove_Zabs_nat.
rewrite Zmax_left; auto.
rewrite Zmin_right.
apply
(Zge_trans
0%nat
(cg (abs_r a * S i + abs_b0 a))
(cg (abs_r a * i + abs_b0 a))); auto.
apply Zle_ge.
apply cg_monotone_linear.
assert (H_aux:
abs_r a * i + abs_b0 a ==
abs_r a * i + abs_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
destruct H_wf; assumption.
apply Zgt_impl_Zge.
assert (H_aux: (i + 1%nat)%Z = S i).
assert (H_aux: (Z_of_nat (i + 1%nat)%nat = (i + 1%nat)%Z)%Z).
apply inj_plus.
rewrite <- H_aux; clear H_aux.
rewrite plus_comm.
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
apply (Zgt_le_trans
(S i)
(cg (abs_r a * S i + abs_b0 a))
(cg (abs_r a * i + abs_b0 a))); auto.
apply cg_monotone_linear.
assert (H_aux:
abs_r a * i + abs_b0 a ==
abs_r a * i + abs_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
destruct H_wf; assumption.
assert (H_cc_aux2: abs_r a * S i + abs_b0 a <= ones_late a i).
clear H0; clear H2.
rewrite H_cc_aux1.
apply (Qle_trans
(abs_r a * S i + abs_b0 a)
(cg(abs_r a * S i + abs_b0 a))
0).
destruct (cg_def_linear (abs_r a * S i + abs_b0 a)); assumption.
apply Zle_impl_Qle.
apply Zge_le.
assumption.
rewrite red_ones_late.
case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
try solve [ intro H_cmp; apply inj_eq; assumption].
intro H_cmp.
rewrite <- Qgt_alt in H_cmp.
absurd (ones_late a i < abs_r a * S i + abs_b0 a); auto.
apply Qle_not_lt.
assumption.
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (abs_r a * (S i) + abs_b0 a))).
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
assert (H_cc_aux1: ones_late a i = i).
rewrite IHi.
apply Zeq_impl_nat_eq.
rewrite ones_late_alt_remove_Zabs_nat.
rewrite Zmin_left.
rewrite Zmax_right.
trivial.
apply inj_le.
auto with arith.
apply Zlt_impl_Zle.
apply (Zlt_le_trans
i
(S i)
(cg (abs_r a * i + abs_b0 a) + 1)).
apply inj_lt.
auto with arith.
rewrite <- cg_plus_int_rewrite.
apply (Zle_trans
(S i)
(cg (abs_r a * S i + abs_b0 a))
(cg (abs_r a * i + abs_b0 a + 1))); auto.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
destruct H_wf; assumption.
assert (H_cc_aux2: abs_r a * S i + abs_b0 a > ones_late a i).
rewrite H_cc_aux1.
apply (Qle_lt_trans
i
(cg (abs_r a * S i + abs_b0 a) - 1)%Z
(abs_r a * S i + abs_b0 a));
try solve [ elim (cg_def_linear (abs_r a * S i + abs_b0 a));
intros; assumption ].
assert (H_aux:
(cg (abs_r a * S i + abs_b0 a) - 1%nat) ==
(cg (abs_r a * S i + abs_b0 a) - 1%nat)%Z).
unfold Qeq; simpl; omega.
rewrite <- H_aux; clear H_aux.
unfold Qminus.
rewrite -> Qle_minus_iff.
assert (H_aux:
cg (abs_r a * S i + abs_b0 a) + - (1) + - i ==
cg (abs_r a * S i + abs_b0 a) + - (i + 1)).
ring.
rewrite H_aux; clear H_aux.
rewrite n_plus_1_eq_S_n.
rewrite <- Qle_minus_iff.
apply Zle_impl_Qle.
assumption.
rewrite red_ones_late.
simpl in H_cc_aux2.
rewrite Qgt_alt in H_cc_aux2.
rewrite H_cc_aux2.
rewrite H_cc_aux1.
reflexivity.
intro H_tmp; destruct H_tmp.
rewrite H0 in *.
rewrite H2 in *.
clear H2 H0.
rewrite ones_late_eq_ones_w_late.
case_eq (w_late a (S i)).
intro H_w_late.
rewrite ones_S_i_eq_S_ones_i; auto.
rewrite <- ones_late_eq_ones_w_late.
rewrite IHi.
assert (H_aux: (Z_of_nat (1 + ones_late_alt a i)) = (1 + ones_late_alt a i)%Z).
apply inj_plus.
rewrite H_aux; clear H_aux.
assert (H_cmp: abs_r a * S i + abs_b0 a > ones_late a i).
rewrite Qlt_alt.
case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
try solve [
intro H_cmp;
simpl in H_w_late;
rewrite H_cmp in H_w_late;
rewrite <- beq_nat_refl in H_w_late;
simpl in H_w_late;
congruence].
rewrite <- Qlt_alt.
rewrite <- Qgt_alt.
trivial.
rewrite IHi in H_cmp.
apply Zle_antisym.
assert (TH_aux: forall (x: nat) (y: Z), (x < y)%Z -> (1%nat + x <= y)%Z).
intros x y H_lt.
replace (1%nat + x)%Z with (- ( -(1) + - x))%Z by ring.
apply Zle_0_minus_le.
unfold Zminus.
rewrite Zopp_involutive.
rewrite Zplus_assoc.
apply Zlt_left.
assumption.
apply TH_aux; auto.
apply Qlt_impl_Zlt.
apply
(Qlt_le_trans
(ones_late_alt a i)
(abs_r a * S i + abs_b0 a)
(cg (abs_r a * S i + abs_b0 a))); auto.
elim (cg_def_linear (abs_r a * S i + abs_b0 a)); auto.
rewrite ones_late_alt_remove_Zabs_nat.
rewrite Zmin_right; auto.
rewrite Zmax_right.
rewrite Zplus_comm.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
replace 1%Z with (Z_of_nat 1); auto.
destruct H_wf; auto.
apply Zlt_impl_Zle.
apply
(Zlt_le_trans
0%nat
(cg (abs_r a * S i + abs_b0 a))
(cg (abs_r a * i + abs_b0 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
destruct H_wf; auto.
apply
(Zge_trans
i
(cg (abs_r a * S i + abs_b0 a))
(cg (abs_r a * i + abs_b0 a))).
assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
intros x y H_gt.
apply Zgt_impl_Zge.
assert (H_aux: (x + 1%nat)%Z = S x).
assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
apply inj_plus.
rewrite <- H_aux; clear H_aux.
rewrite plus_comm.
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
assumption.
apply TH_aux; auto.
apply Zle_ge.
apply cg_monotone_linear.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite Qmult_comm.
assert (H_aux: abs_r a * S i == S i * abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
destruct H_wf; auto.
intro H_w_late.
rewrite ones_S_i_eq_ones_i; auto.
rewrite <- ones_late_eq_ones_w_late.
rewrite IHi.
assert (H_cmp: abs_r a * S i + abs_b0 a <= ones_late a i).
rewrite Qge_alt.
case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i).
intro H_cmp.
rewrite <- Qeq_alt in H_cmp.
intro H_cmp'.
rewrite <- Qlt_alt in H_cmp'.
rewrite H_cmp in H_cmp'.
absurd (ones_late a i < ones_late a i); auto.
apply Qle_not_lt.
apply Qle_refl.
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
intro H_cmp'.
rewrite <- Qlt_alt in H_cmp'.
absurd (ones_late a i < abs_r a * S i + abs_b0 a); auto.
apply Qle_not_lt.
apply Qlt_le_weak.
assumption.
intro H_cmp.
simpl in H_w_late.
rewrite H_cmp in H_w_late.
rewrite S_n_nbeq_n in H_w_late.
simpl in H_w_late.
congruence.
rewrite IHi in H_cmp.
apply Zle_antisym.
rewrite ones_late_alt_remove_Zabs_nat.
rewrite Zmin_right; auto.
rewrite Zmax_right.
apply cg_monotone_linear.
assert (H_aux:
abs_r a * i + abs_b0 a ==
abs_r a * i + abs_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
destruct H_wf; assumption.
apply Zlt_impl_Zle.
apply
(Zlt_le_trans
0%nat
(cg (abs_r a * S i + abs_b0 a))
(cg (abs_r a * i + abs_b0 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [apply Qle_refl].
destruct H_wf; auto.
apply
(Zge_trans
i
(cg (abs_r a * S i + abs_b0 a))
(cg (abs_r a * i + abs_b0 a))).
assert (TH_aux: forall (x: nat) (y: Z), (S x > y)%Z -> (x >= y)%Z).
intros x y H_gt.
apply Zgt_impl_Zge.
assert (H_aux: (x + 1%nat)%Z = S x).
assert (H_aux: (Z_of_nat (x + 1%nat)%nat = (x + 1%nat)%Z)%Z).
apply inj_plus.
rewrite <- H_aux; clear H_aux.
rewrite plus_comm.
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
assumption.
apply TH_aux; auto.
apply Zle_ge.
apply cg_monotone_linear.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite Qmult_comm.
assert (H_aux: abs_r a * S i == S i * abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qmult_le_compat_r; try solve [ apply le_impl_Qle; auto].
destruct H_wf; auto.
rewrite <- Zge_iff_le.
apply n_ge_cg_linear.
assumption.
Qed.
Lemma w_early_S_i_eq_true_impl_ones_early_S_i_le_a:
forall a i,
forall H_w: w_early a (S i) = true,
ones (w_early a) (S i) <= (abs_r a * S i + abs_b1 a).
Proof.
intros.
assert (H_w_i: (ones (w_early a) (S i) = S (ones (w_early a) i))%nat).
apply ones_S_i_eq_S_ones_i; auto.
simpl in H_w.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
intro H_cmp.
rewrite <- Qeq_alt in H_cmp.
rewrite ones_early_eq_ones_w_early in H_cmp.
rewrite <- H_cmp.
rewrite H_w_i.
apply Qle_refl.
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
rewrite ones_early_eq_ones_w_early in H_cmp.
apply Qlt_le_weak.
rewrite H_w_i.
assumption.
intro H_cmp.
rewrite H_cmp in H_w.
rewrite <- beq_nat_refl in H_w.
simpl in H_w.
congruence.
Qed.
Lemma w_early_S_i_eq_false_impl_ones_early_i_gt_a:
forall a i,
forall H_w: w_early a (S i) = false,
S (ones (w_early a) i) > (abs_r a * S i + abs_b1 a).
Proof.
intros.
simpl in H_w.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
intro H_cmp.
rewrite H_cmp in H_w.
rewrite S_n_nbeq_n in H_w.
simpl in H_w.
congruence.
intro H_cmp.
rewrite H_cmp in H_w.
rewrite S_n_nbeq_n in H_w.
simpl in H_w.
congruence.
intro H_cmp.
clear H_w.
rewrite <- Qgt_alt in H_cmp.
rewrite ones_early_eq_ones_w_early in H_cmp.
assumption.
Qed.
Property ones_w_le_ones_early:
forall w: ibw,
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall H_w_in_a: in_abstraction_phd w a,
forall i: nat,
(ones w i <= ones_early a i)%nat.
Proof.
intros.
case_eq i.
intro H_i.
simpl.
apply le_refl.
intros i' H_i.
clear H_i i.
induction i'.
case_eq (w 1%nat).
intro H_w.
assert (H_1_ge_1: (1 >= 1)%nat);
auto.
pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
elim H_w_in_a_1. intros H_aux_true H_aux_false.
generalize (H_aux_true H_w).
clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
intro H_ones_le_a.
simpl in H_ones_le_a.
simpl.
rewrite H_w.
simpl.
case_eq (1%nat ?= abs_r a * 1%nat + abs_b1 a);
try solve [ intros; apply le_refl ].
intros H_cmp.
rewrite <- Qgt_alt in H_cmp.
absurd (abs_r a * 1 + abs_b1 a < 1); auto.
apply Qle_not_lt.
rewrite H_w in H_ones_le_a.
assumption.
intro H_w.
assert (H_1_ge_1: (1 >= 1)%nat);
auto.
pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
elim H_w_in_a_1. intros H_aux_true H_aux_false.
generalize (H_aux_false H_w).
clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
intro H_ones_ge_a.
simpl in H_ones_ge_a.
simpl in H_ones_ge_a.
simpl.
rewrite H_w.
simpl.
case_eq (1%nat ?= abs_r a * 1%nat + abs_b1 a);
try solve [ intros; unfold Q_of_nat, Qle; simpl; auto with zarith ].
case_eq (w (S (S i'))).
intro H_w.
rewrite ones_S_i_eq_S_ones_i; auto.
change ((1 + ones w (S i'))%nat) with (S (ones w (S i'))).
elim (le_lt_eq_dec (ones w (S i')) (ones_early a (S i'))); try omega.
intro H_cmp.
apply
(le_trans
(S (ones w (S i')))
(ones_early a (S i'))
(ones_early a (S (S i')))); try omega.
assert (H_aux:
(ones_early a (S (S i'))
=
match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
| Eq => S (ones_early a (S i'))
| Lt => S (ones_early a (S i'))
| Gt => ones_early a (S i')
end)%nat).
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a);
try omega.
intro H_cmp.
rewrite H_cmp.
assert (H_S_S_i'_ge_1: (S (S i') >= 1)%nat);
auto with arith.
pose (H_tmp:= H_w_in_a (S (S i')) H_S_S_i'_ge_1).
destruct H_tmp.
generalize (H H_w).
clear H_S_S_i'_ge_1 H H0 IHi'.
intro H_ones_le_a.
assert (H_aux:
(ones_early a (S (S i'))
=
match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
| Eq => S (ones_early a (S i'))
| Lt => S (ones_early a (S i'))
| Gt => ones_early a (S i')
end)%nat).
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a);
try omega.
intro H_cmp'.
rewrite <- Qgt_alt in H_cmp'.
absurd (abs_r a * S (S i') + abs_b1 a < S (ones_early a (S i'))); auto.
apply Qle_not_lt.
rewrite ones_S_i_eq_S_ones_i in H_ones_le_a; auto.
rewrite H_cmp in H_ones_le_a.
assumption.
intro H_w.
rewrite ones_S_i_eq_ones_i; auto.
assert (H_aux:
(ones_early a (S (S i'))
=
match S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a with
| Eq => S (ones_early a (S i'))
| Lt => S (ones_early a (S i'))
| Gt => ones_early a (S i')
end)%nat).
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
case_eq (S (ones_early a (S i')) ?= abs_r a * S (S i') + abs_b1 a);
omega.
Qed.
Property ones_late_le_ones_w:
forall w: ibw,
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall H_w_in_a: in_abstraction_phd w a,
forall i: nat,
(ones_late a i <= ones w i)%nat.
Proof.
intros.
case_eq i.
intro H_i.
simpl.
apply le_refl.
intros i' H_i.
clear H_i i.
induction i'.
case_eq (w 1%nat).
intro H_w.
assert (H_1_ge_1: (1 >= 1)%nat);
auto.
pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
elim H_w_in_a_1. intros H_aux_true H_aux_false.
generalize (H_aux_true H_w).
clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
intro H_ones_le_a.
simpl in H_ones_le_a.
simpl.
rewrite H_w.
simpl.
case_eq (abs_r a * 1%nat + abs_b0 a ?= 0%nat);
try solve [ auto; intros; apply le_refl ].
intro H_w.
assert (H_1_ge_1: (1 >= 1)%nat);
auto.
pose (H_w_in_a_1:= H_w_in_a 1%nat H_1_ge_1).
elim H_w_in_a_1. intros H_aux_true H_aux_false.
generalize (H_aux_false H_w).
clear H_1_ge_1 H_w_in_a_1 H_aux_true H_aux_false.
intro H_ones_ge_a.
simpl in H_ones_ge_a.
simpl.
rewrite H_w.
simpl.
case_eq (abs_r a * 1%nat + abs_b0 a ?= 0%nat);
try solve [ auto; intros; unfold Q_of_nat, Qle; simpl; auto with zarith ].
intros H_cmp.
rewrite <- Qgt_alt in H_cmp.
absurd (0 < abs_r a * 1 + abs_b0 a); auto.
apply Qle_not_lt.
rewrite H_w in H_ones_ge_a.
assumption.
case_eq (w (S (S i'))).
intro H_w.
rewrite ones_S_i_eq_S_ones_i; auto.
change ((1 + ones w (S i'))%nat) with (S (ones w (S i'))).
rewrite red_ones_late.
case_eq (abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i')); omega.
intro H_w.
rewrite ones_S_i_eq_ones_i; auto.
rewrite red_ones_late.
case_eq (abs_r a * S (S i') + abs_b0 a ?= ones_late a (S i'));
try omega.
rewrite <- Qgt_alt.
intro H_cmp.
apply lt_le_S.
apply Qlt_impl_lt.
apply
(Qlt_le_trans
(ones_late a (S i'))
(abs_r a * S (S i') + abs_b0 a)
(ones w (S i')));
try solve [ exact H_cmp ].
unfold in_abstraction_phd in H_w_in_a.
rewrite <- ones_S_i_eq_ones_i; auto.
apply (H_w_in_a (S (S i'))); auto with arith.
Qed.
Lemma ones_early_opt_impl_ones_early:
forall a: abstraction_phd,
forall i,
forall (H_ones_early_opt:
exists v,
ones_early_opt a i = Some v),
ones_early_opt a i = Some (ones_early a i).
Proof.
intros.
induction i.
simpl.
reflexivity.
simpl.
assert (IH_pre: exists v : nat, ones_early_opt a i = Some v).
elim H_ones_early_opt.
intros v_S_i H_ones_S_i.
simpl in H_ones_S_i.
case_eq (ones_early_opt a i).
intros v_i H_ones_i.
exists v_i.
reflexivity.
intros H_ones_i.
rewrite H_ones_i in H_ones_S_i.
congruence.
rewrite IHi; auto.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
try reflexivity.
intro H_cmp.
case_eq (abs_r a * S i + abs_b0 a ?= ones_early a i);
try reflexivity.
intro H_cmp'.
absurd (exists v : nat, ones_early_opt a (S i) = Some v);
auto.
unfold Logic.not.
intro H_tmp.
elim H_tmp; clear H_tmp.
intro v.
simpl.
rewrite IHi; auto.
rewrite H_cmp.
rewrite H_cmp'.
congruence.
Qed.
Lemma ones_late_opt_impl_ones_late:
forall a: abstraction_phd,
forall i,
forall (H_ones_late_opt:
exists v,
ones_late_opt a i = Some v),
ones_late_opt a i = Some (ones_late a i).
Proof.
intros.
induction i.
simpl.
reflexivity.
simpl.
assert (IH_pre: exists v : nat, ones_late_opt a i = Some v).
elim H_ones_late_opt.
intros v_S_i H_ones_S_i.
simpl in H_ones_S_i.
case_eq (ones_late_opt a i).
intros v_i H_ones_i.
exists v_i.
reflexivity.
intros H_ones_i.
rewrite H_ones_i in H_ones_S_i.
congruence.
rewrite IHi; auto.
case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i);
try reflexivity.
intro H_cmp.
case_eq (S (ones_late a i) ?= abs_r a * S i + abs_b1 a);
try reflexivity.
intro H_cmp'.
absurd (exists v : nat, ones_late_opt a (S i) = Some v);
auto.
unfold Logic.not.
intro H_tmp.
elim H_tmp; clear H_tmp.
intro v.
simpl.
rewrite IHi; auto.
rewrite H_cmp.
rewrite H_cmp'.
congruence.
Qed.
Property ones_late_eq_ones_early:
forall a: abstraction_phd,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
forall H_abs_b1_lt_abs_b0: abs_b1 a - abs_b0 a < 1,
forall i,
ones_late a i = ones_early a i.
Proof.
induction i.
simpl.
reflexivity.
simpl.
case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i).
intros H_cmp_zero.
rewrite IHi.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
intros H_cmp_one.
rewrite <- Qeq_alt in *.
rewrite IHi in H_cmp_zero.
rewrite <- n_plus_1_eq_S_n in H_cmp_one.
rewrite <- H_cmp_zero in H_cmp_one.
absurd (abs_r a * S i + abs_b1 a == abs_r a * S i + abs_b0 a + 1);
try solve [rewrite H_cmp_one; apply Qeq_refl].
apply Qlt_not_eq.
rewrite <- Qplus_assoc.
apply Qplus_lt_compat_l.
apply <- Qlt_minus_iff.
assert (H_aux:
abs_b0 a + 1 + - abs_b1 a == 1 + - (abs_b1 a - abs_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
intros H_cmp_one.
rewrite <- Qeq_alt in *.
rewrite <- Qlt_alt in *.
absurd (S (ones_early a i) < abs_r a * S i + abs_b1 a);
auto.
rewrite IHi in H_cmp_zero.
apply Qle_not_lt.
rewrite <- (n_plus_1_eq_S_n (ones_early a i)).
rewrite <- H_cmp_zero.
rewrite <- Qplus_assoc.
apply Qplus_le_compat; try solve [apply Qle_refl; auto].
apply Qlt_le_weak.
apply <- Qlt_minus_iff.
assert (H_aux:
abs_b0 a + 1 + - abs_b1 a == 1 + - (abs_b1 a - abs_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
reflexivity.
intros H_cmp_zero.
rewrite IHi.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
intros H_cmp_one.
rewrite <- Qeq_alt in H_cmp_one.
rewrite <- Qlt_alt in H_cmp_zero.
rewrite IHi in H_cmp_zero.
assert (H_aux:
ones_early a i == abs_r a * S i + abs_b1 a - 1).
rewrite <- H_cmp_one.
rewrite <- n_plus_1_eq_S_n.
ring.
rewrite H_aux in H_cmp_zero; clear H_aux.
absurd (abs_r a * S i + abs_b0 a < abs_r a * S i + abs_b1 a - 1);
auto.
apply Qle_not_lt.
unfold Qminus.
rewrite <- Qplus_assoc.
apply Qplus_le_compat; try solve [apply Qle_refl; auto].
apply Qlt_le_weak.
apply <- Qlt_minus_iff.
assert (H_aux:
abs_b0 a + - (abs_b1 a + - (1)) == 1 + - (abs_b1 a - abs_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
intros H_cmp_one.
rewrite <- Qlt_alt in *.
absurd (abs_r a * S i + abs_b0 a < abs_r a * S i + abs_b1 a - 1).
apply Qle_not_lt.
unfold Qminus.
rewrite <- Qplus_assoc.
apply Qplus_le_compat; try solve [apply Qle_refl; auto].
apply Qlt_le_weak.
apply <- Qlt_minus_iff.
assert (H_aux:
abs_b0 a + - (abs_b1 a + - (1)) == 1 + - (abs_b1 a - abs_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
rewrite IHi in H_cmp_zero.
apply
(Qlt_trans
(abs_r a * S i + abs_b0 a)
(ones_early a i)
(abs_r a * S i + abs_b1 a - 1)); auto.
apply -> (Qlt_plus 1%nat).
rewrite Qplus_comm.
rewrite n_plus_1_eq_S_n.
assert (H_aux:
1 + (abs_r a * S i + abs_b1 a - 1) == abs_r a * S i + abs_b1 a).
ring.
rewrite H_aux; clear H_aux.
assumption.
reflexivity.
intros H_cmp_zero.
rewrite IHi.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a).
intros H_cmp_one.
reflexivity.
intros H_cmp_one.
reflexivity.
intros H_cmp_one.
pose (H_non_empty_S_i:= H_non_empty (S i)).
simpl in H_non_empty_S_i.
rewrite H_cmp_one in H_non_empty_S_i.
rewrite H_cmp_zero in H_non_empty_S_i.
rewrite IHi in H_non_empty_S_i.
absurd ((S (ones_early a i) <= ones_early a i)%nat); auto.
apply lt_not_le.
auto with arith.
Qed.
Property ones_late_le_ones_early_impl_early_in_a:
forall a: abstraction_phd,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
in_abstraction_phd (w_early a) a.
Proof.
intros.
unfold in_abstraction_phd.
intros.
case_eq i.
intros H_i.
rewrite H_i in H_i_ge_1.
absurd ((0 >= 1)%nat); auto.
unfold ge.
auto with arith.
intros i' H_i.
rewrite H_i in H_i_ge_1.
clear H_i i.
split.
intro H_w_early_S_i'.
apply w_early_S_i_eq_true_impl_ones_early_S_i_le_a.
exact H_w_early_S_i'.
intro H_w_early_S_i'.
assert (H_cmp: (abs_r a * S i' + abs_b1 a) < S (ones_early a i')).
rewrite ones_early_eq_ones_w_early.
apply w_early_S_i_eq_false_impl_ones_early_i_gt_a; auto.
pose (H_non_empty_i:=H_non_empty (S i')).
simpl in H_non_empty_i.
rewrite Qgt_alt in H_cmp.
rewrite H_cmp in H_non_empty_i.
case_eq (abs_r a * S i' + abs_b0 a ?= ones_late a i').
intro H_cmp'.
rewrite <- Qeq_alt in H_cmp'.
rewrite H_cmp'.
apply le_impl_Qle.
simpl.
rewrite H_cmp.
rewrite <- beq_nat_refl.
simpl.
rewrite <- ones_early_eq_ones_w_early.
apply H_non_empty.
intro H_cmp'.
rewrite <- Qlt_alt in H_cmp'.
simpl.
rewrite <- ones_early_eq_ones_w_early.
rewrite H_cmp.
rewrite <- beq_nat_refl.
simpl.
apply
(Qle_trans
(abs_r a * S i' + abs_b0 a)
(ones_late a i')
(ones_early a i')).
apply Qlt_le_weak; assumption.
apply le_impl_Qle.
apply H_non_empty.
intro H_cmp'.
rewrite H_cmp' in H_non_empty_i.
assert (H_w_late: w_late a (S i') = true).
simpl.
rewrite H_cmp'.
rewrite S_n_nbeq_n.
trivial.
case_eq i'.
intro H_i'.
rewrite H_i' in *.
simpl in *.
absurd (1 <= 0)%nat; auto with arith.
intros i'' H_i'.
rewrite H_i' in *.
elim (Qlt_le_dec (abs_b1 a - abs_b0 a) 1).
intro H_one_lt_zero.
generalize (ones_late_eq_ones_early a H_non_empty H_one_lt_zero).
intro H_late_eq_early.
assert (H_late_eq_early':
forall i : nat, ones (w_late a) i = ones (w_early a) i).
intros.
rewrite <- ones_late_eq_ones_w_late.
rewrite <- ones_early_eq_ones_w_early.
apply H_late_eq_early.
assert (H_wf_early: well_formed_ibw (w_early a)).
apply w_early_well_formed.
assert (H_wf_late: well_formed_ibw (w_late a)).
apply w_late_well_formed.
generalize (ones_eq_impl_w_eq _ _ H_late_eq_early').
intro H_w.
absurd (w_late a (S (S i'')) = w_early a (S (S i''))); auto.
rewrite H_w_late, H_w_early_S_i'.
discriminate.
intro H_zero_lt_one.
rewrite <- Qgt_alt in *.
replace (pred (S (S i''))) with (S i''); auto.
rewrite <- ones_early_eq_ones_w_early.
apply
(Qle_trans
(abs_r a * S (S i'') + abs_b0 a)
(abs_r a * S (S i'') + (abs_b1 a - 1))
(ones_early a (S (S i'')))).
apply Qplus_le_compat; try solve [apply Qle_refl].
rewrite Qle_minus_iff.
assert (H_aux:
abs_b1 a - 1 + - abs_b0 a == abs_b1 a - abs_b0 a + - (1)).
ring.
rewrite H_aux; clear H_aux.
rewrite <- Qle_minus_iff.
assumption.
rewrite ones_early_eq_ones_w_early.
rewrite ones_S_i_eq_ones_i; auto.
rewrite <- ones_early_eq_ones_w_early.
apply Qlt_le_weak.
rewrite Qlt_minus_iff.
assert (H_aux:
ones_early a (S i'') + - (abs_r a * S (S i'') + (abs_b1 a - 1)) ==
ones_early a (S i'') + 1 + - (abs_r a * S (S i'') + abs_b1 a)).
ring.
rewrite H_aux; clear H_aux.
rewrite <- Qlt_minus_iff.
rewrite n_plus_1_eq_S_n.
assumption.
Qed.
Property ones_late_le_ones_early_impl_late_in_a:
forall a: abstraction_phd,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
in_abstraction_phd (w_late a) a.
Proof.
intros.
unfold in_abstraction_phd.
intros.
case_eq i.
intros H_i.
rewrite H_i in H_i_ge_1.
absurd ((0 >= 1)%nat); auto.
unfold ge.
auto with arith.
intros i' H_i.
rewrite H_i in H_i_ge_1.
clear H_i i.
split.
intro H_w.
simpl in H_w.
case_eq (abs_r a * S i' + abs_b0 a ?= ones_late a i').
intro H_cmp.
rewrite H_cmp in H_w.
rewrite <- beq_nat_refl in H_w.
simpl in H_w.
congruence.
intro H_cmp.
rewrite H_cmp in H_w.
rewrite <- beq_nat_refl in H_w.
simpl in H_w.
congruence.
intro H_cmp.
rewrite H_cmp in H_w.
simpl.
pose (H_non_empty_i:=H_non_empty (S i')).
simpl in H_non_empty_i.
rewrite H_cmp in H_non_empty_i.
case_eq (S (ones_early a i') ?= abs_r a * S i' + abs_b1 a).
intro H_cmp'.
rewrite H_cmp' in *.
rewrite <- Qeq_alt in H_cmp'.
rewrite <- H_cmp'.
rewrite <- ones_late_eq_ones_w_late.
apply le_impl_Qle.
apply le_lt_n_Sm in H_non_empty_i.
rewrite H_cmp.
rewrite S_n_nbeq_n.
simpl.
auto with arith.
intro H_cmp'.
rewrite H_cmp' in H_non_empty_i.
rewrite <- Qlt_alt in H_cmp'.
simpl.
rewrite <- ones_late_eq_ones_w_late.
rewrite H_cmp.
rewrite S_n_nbeq_n.
simpl.
apply (Qle_trans
(S (ones_late a i'))
(S (ones_early a i'))
(abs_r a * S i' + abs_b1 a));
try solve [apply Qlt_le_weak; auto].
apply le_impl_Qle.
auto with arith.
intro H_cmp'.
rewrite H_cmp' in H_non_empty_i.
rewrite <- Qgt_alt in *.
rewrite <- ones_late_eq_ones_w_late.
elim (Qlt_le_dec (abs_b1 a - abs_b0 a) 1).
intro H_b1_lt_b0.
generalize (ones_late_eq_ones_early a H_non_empty H_b1_lt_b0 i').
intro H_late_eq_early.
rewrite H_late_eq_early in H_non_empty_i.
absurd ((S (ones_early a i') <= ones_early a i')%nat); auto.
apply lt_not_le.
auto.
intro H_b0_le_b1.
rewrite Qgt_alt in H_cmp.
rewrite H_cmp.
rewrite <- Qgt_alt in H_cmp.
rewrite S_n_nbeq_n.
simpl.
apply (Qle_trans
(S (ones_late a i'))
(abs_r a * S i' + abs_b0 a + 1)
(abs_r a * S i' + abs_b1 a)).
rewrite <- n_plus_1_eq_S_n.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply Qlt_le_weak.
assumption.
rewrite <- Qplus_assoc.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply <- Qle_minus_iff.
assert (H_aux:
abs_b1 a + - (abs_b0 a + 1) == abs_b1 a - abs_b0 a + - (1)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
assumption.
intro H_w.
simpl.
simpl in H_w.
rewrite <- ones_late_eq_ones_w_late.
case_eq (abs_r a * S i' + abs_b0 a ?= ones_late a i').
intro H_cmp.
rewrite <- Qeq_alt in H_cmp.
rewrite H_cmp.
rewrite <- beq_nat_refl.
simpl.
apply Qle_refl.
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
apply Qlt_le_weak.
rewrite <- beq_nat_refl.
simpl.
assumption.
intro H_cmp.
rewrite H_cmp in H_w.
rewrite S_n_nbeq_n in H_w.
simpl in H_w.
congruence.
Qed.
Property non_empty_impl_ones_late_le_ones_early:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall H_non_empty: non_empty a,
forall i,
(ones_late a i <= ones_early a i)%nat.
Proof.
intros.
elim H_non_empty.
intros w H_w_in_a.
apply
(le_trans
(ones_late a i)
(ones w i)
(ones_early a i)).
apply ones_late_le_ones_w; auto.
apply ones_w_le_ones_early; auto.
Qed.
Property early_in_abs:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall H_non_empty: non_empty a,
in_abstraction_phd (w_early a) a.
Proof.
intros.
apply ones_late_le_ones_early_impl_early_in_a.
intros.
apply non_empty_impl_ones_late_le_ones_early; auto.
Qed.
Property late_in_abs:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall H_non_empty: non_empty a,
in_abstraction_phd (w_late a) a.
Proof.
intros.
apply ones_late_le_ones_early_impl_late_in_a.
intros.
apply non_empty_impl_ones_late_le_ones_early; auto.
Qed.
Property ones_early_rewrite:
forall a1 a2,
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_wf_a2: well_formed_abstraction_phd a2,
abs_equal a1 a2 ->
forall i, (ones_early a1 i = ones_early a2 i).
Proof.
intros a1 a2 H_wf_a1 H_wf_a2 H_a1_eq_a2 i.
destruct H_a1_eq_a2 as [H_r [H_b1 H_b0]].
repeat rewrite ones_early_eq_ones_early_alt; auto.
repeat unfold ones_early_alt.
rewrite H_r.
rewrite H_b1.
reflexivity.
Qed.
Property ones_late_rewrite:
forall a1 a2,
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_wf_a2: well_formed_abstraction_phd a2,
abs_equal a1 a2 ->
forall i, (ones_late a1 i = ones_late a2 i).
Proof.
intros a1 a2 H_wf_a1 H_wf_a2 H_a1_eq_a2 i.
destruct H_a1_eq_a2 as [H_r [H_b1 H_b0]].
repeat rewrite ones_late_eq_ones_late_alt; auto.
repeat unfold ones_late_alt.
rewrite H_r.
rewrite H_b0.
reflexivity.
Qed.
Property exists_i_st_ones_early_eq_r_i_plus_b:
forall a: abstraction_phd,
forall H_swf_a: strong_well_formed_abstraction_phd a,
exists i: nat,
(fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z.
Proof.
intros.
elim (Qlt_le_dec (abs_b1 a) 0).
intro H_b1.
elim (Qeq_dec (abs_r a) (0)).
intro H_r_eq_0.
destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
absurd (abs_b1 a < 0); auto.
apply Qle_not_lt.
apply (Qle_trans _ (abs_b0 a) _); auto.
intro H_r_diff_0.
pose (i := Zabs_nat (cg (- abs_b1 a / abs_r a))).
assert (zi: Z_of_nat i = cg (- abs_b1 a / abs_r a)).
unfold i.
rewrite inj_Zabs_nat.
apply Zabs_eq.
apply Qle_impl_Zle.
apply (Qle_trans _ (- abs_b1 a / abs_r a) _);
try solve [ eapply cg_def_linear ].
apply Qle_shift_div_l.
elim (Q_dec (abs_r a) 0); auto.
intro H; elim H; auto; clear H; intro H_absurd.
absurd (abs_r a < 0); auto.
apply Qle_not_lt.
eapply H_swf_a.
intro H_absurd.
absurd (abs_r a == 0); auto.
assert (H_aux: Z0 * abs_r a == - 0).
ring.
rewrite H_aux; clear H_aux.
apply Qopp_le_compat.
apply Qlt_le_weak.
exact H_b1.
exists i.
rewrite ones_early_eq_ones_early_alt; try solve [ eapply H_swf_a ].
rewrite ones_early_alt_remove_Zabs_nat.
elim (Zmin_spec i (fl (abs_r a * i + abs_b1 a))).
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
elim (Z_le_lt_eq_dec i (fl (abs_r a * i + abs_b1 a))); auto.
intro H_i.
absurd ((i < fl (abs_r a * i + abs_b1 a))%Z); auto.
clear H_i H_min.
apply Zle_not_lt.
apply Qle_impl_Zle.
apply (Qle_trans _
(abs_r a * i + abs_b1 a) _);
try solve [elim (fl_def (abs_r a * i + abs_b1 a)); auto].
apply <- Qle_minus_iff.
assert (H_aux:
i + - (abs_r a * i + abs_b1 a) == (1 - abs_r a) * i + - abs_b1 a).
ring.
rewrite H_aux; clear H_aux.
apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
try solve [ ring_simplify; apply Qle_refl ].
apply Qplus_le_compat; auto.
apply Qmult_le_0_compat.
apply -> Qle_minus_iff.
eapply H_swf_a.
apply Zle_impl_Qle.
omega.
rewrite <- (Qopp_involutive Z0).
apply Qopp_le_compat.
apply Qlt_le_weak.
exact H_b1.
intro H_i.
rewrite H_i.
assert (H_aux:
Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply n_le_fl_linear.
rewrite <- (Qopp_involutive (abs_b1 a)).
apply -> Qle_minus_iff.
unfold Q_of_nat.
rewrite zi.
apply (Qle_trans _
(abs_r a * (- abs_b1 a / abs_r a)) _).
rewrite Qmult_div_r; auto.
apply Qle_refl.
apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
eapply cg_def_linear.
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
assert (H_aux:
Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply n_le_fl_linear.
rewrite <- (Qopp_involutive (abs_b1 a)).
apply -> Qle_minus_iff.
unfold Q_of_nat.
rewrite zi.
apply (Qle_trans _
(abs_r a * (- abs_b1 a / abs_r a)) _).
rewrite Qmult_div_r; auto.
apply Qle_refl.
apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
eapply cg_def_linear.
intro H_b1.
elim (Qeq_dec (abs_r a) (1)).
intro H_r_eq_1.
elim (Qle_lt_or_eq 0 (abs_b1 a)); auto.
intro H_b1'.
destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
absurd (0 < abs_b1 a); auto.
apply Qle_not_lt.
auto.
clear H_b1; intro H_b1.
exists 1%nat.
rewrite ones_early_eq_ones_early_alt; try solve [ eapply H_swf_a ].
rewrite ones_early_alt_remove_Zabs_nat.
repeat rewrite <- H_b1 in *.
repeat rewrite H_r_eq_1.
compute.
reflexivity.
intro H_r_diff_1.
pose (i := Zabs_nat (cg (abs_b1 a / (1 - abs_r a)))).
assert (zi: Z_of_nat i = cg (abs_b1 a / (1 - abs_r a))).
unfold i.
rewrite inj_Zabs_nat.
apply Zabs_eq.
apply Qle_impl_Zle.
apply (Qle_trans _ (abs_b1 a / (1 - abs_r a)) _);
try solve [ eapply cg_def_linear ].
apply Qle_shift_div_l.
apply -> Qlt_minus_iff.
elim (Q_dec (abs_r a) 1); auto.
intro H; elim H; auto; clear H; intro H_absurd.
absurd (1 < abs_r a); auto.
apply Qle_not_lt.
eapply H_swf_a.
intro H_absurd.
absurd (abs_r a == 1); auto.
ring_simplify.
eapply H_b1.
exists i.
rewrite ones_early_eq_ones_early_alt; try solve [ eapply H_swf_a ].
rewrite ones_early_alt_remove_Zabs_nat.
elim (Zmin_spec i (fl (abs_r a * i + abs_b1 a))).
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
elim (Z_le_lt_eq_dec i (fl (abs_r a * i + abs_b1 a))); auto.
intro H_i.
absurd ((i < fl (abs_r a * i + abs_b1 a))%Z); auto.
clear H_i H_min.
apply Zle_not_lt.
apply Qle_impl_Zle.
apply (Qle_trans _
(abs_r a * i + abs_b1 a) _);
try solve [elim (fl_def (abs_r a * i + abs_b1 a)); auto].
unfold Q_of_nat.
repeat rewrite zi.
apply <- Qle_minus_iff.
assert (H_aux:
cg (abs_b1 a / (1 - abs_r a)) +
- (abs_r a * cg (abs_b1 a / (1 - abs_r a)) + abs_b1 a) ==
(1 - abs_r a) * cg (abs_b1 a / (1 - abs_r a)) + - abs_b1 a).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
apply (Qle_trans _
((1 - abs_r a) * (abs_b1 a / (1 - abs_r a))) _).
rewrite Qmult_div_r; try solve [ apply Qle_refl ].
intro H_absurd.
absurd (abs_r a == 1); auto.
apply (Qplus_comp (abs_r a) (abs_r a)) in H_absurd;
try reflexivity.
ring_simplify in H_absurd.
rewrite H_absurd.
reflexivity.
rewrite Qmult_comm.
assert (H_aux:
(1 - abs_r a) * cg (abs_b1 a / (1 - abs_r a)) ==
cg (abs_b1 a / (1 - abs_r a)) * (1 - abs_r a)).
rewrite Qmult_comm.
reflexivity.
rewrite H_aux; clear H_aux.
apply Qmult_le_compat_r; try solve [ eapply cg_def_linear ].
unfold Qminus.
apply -> Qle_minus_iff.
eapply H_swf_a.
intro H_i.
rewrite H_i.
assert (H_aux:
Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply n_le_fl_linear.
rewrite inj_0.
apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
try solve [ ring_simplify; apply Qle_refl ].
apply Qplus_le_compat; auto.
apply Qmult_le_0_compat.
eapply H_swf_a.
apply Zle_impl_Qle.
unfold i; auto with zarith.
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
assert (H_aux:
Zmax O (fl (abs_r a * i + abs_b1 a)) = fl (abs_r a * i + abs_b1 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply n_le_fl_linear.
rewrite inj_0.
apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
try solve [ ring_simplify; apply Qle_refl ].
apply Qplus_le_compat; auto.
apply Qmult_le_0_compat.
eapply H_swf_a.
apply Zle_impl_Qle.
unfold i; auto with zarith.
Qed.
Property exists_i_st_ones_late_eq_r_i_plus_b:
forall a: abstraction_phd,
forall H_swf_a: strong_well_formed_abstraction_phd a,
exists i: nat,
(cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z.
Proof.
intros.
elim (Qlt_le_dec (abs_b0 a) 0).
intro H_b0.
elim (Qeq_dec (abs_r a) (0)).
intro H_r_eq_0.
destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
absurd (abs_b0 a < 0); auto.
apply Qle_not_lt.
auto.
intro H_r_diff_0.
pose (i := Zabs_nat (cg (- abs_b0 a / abs_r a))).
assert (zi: Z_of_nat i = cg (- abs_b0 a / abs_r a)).
unfold i.
rewrite inj_Zabs_nat.
apply Zabs_eq.
apply Qle_impl_Zle.
apply (Qle_trans _ (- abs_b0 a / abs_r a) _);
try solve [ eapply cg_def_linear ].
apply Qle_shift_div_l.
elim (Q_dec (abs_r a) 0); auto.
intro H; elim H; auto; clear H; intro H_absurd.
absurd (abs_r a < 0); auto.
apply Qle_not_lt.
eapply H_swf_a.
intro H_absurd.
absurd (abs_r a == 0); auto.
assert (H_aux: Z0 * abs_r a == - 0).
ring.
rewrite H_aux; clear H_aux.
apply Qopp_le_compat.
apply Qlt_le_weak.
exact H_b0.
exists i.
rewrite ones_late_eq_ones_late_alt; try solve [ eapply H_swf_a ].
rewrite ones_late_alt_remove_Zabs_nat.
elim (Zmin_spec i (cg (abs_r a * i + abs_b0 a))).
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
elim (Z_le_lt_eq_dec i (cg (abs_r a * i + abs_b0 a))); auto.
intro H_i.
absurd ((i < cg (abs_r a * i + abs_b0 a))%Z); auto.
clear H_i H_min.
apply Zle_not_lt.
pose (H_aux := (n_ge_cg_linear (abs_r a * i + abs_b0 a) i)).
apply Zge_le in H_aux; auto; clear H_aux.
assert (H_aux: i == i + 0); try ring.
rewrite H_aux at 2; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qlt_le_weak; eapply H_b0 ].
assert (H_aux: i == 1 * i); try ring.
rewrite H_aux at 2; clear H_aux.
apply Qmult_le_compat_r.
eapply H_swf_a.
apply Zle_impl_Qle.
unfold i; auto with zarith.
intro H_i.
rewrite H_i.
assert (H_aux:
Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply Qle_impl_Zle.
apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
try solve [ eapply cg_def_linear ].
rewrite <- (Qopp_involutive (abs_b0 a)).
apply -> Qle_minus_iff.
unfold Q_of_nat.
rewrite zi.
apply (Qle_trans _
(abs_r a * (- abs_b0 a / abs_r a)) _).
rewrite Qmult_div_r; auto.
apply Qle_refl.
apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
eapply cg_def_linear.
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
assert (H_aux:
Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply Qle_impl_Zle.
apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
try solve [ eapply cg_def_linear ].
rewrite <- (Qopp_involutive (abs_b0 a)).
apply -> Qle_minus_iff.
unfold Q_of_nat.
rewrite zi.
apply (Qle_trans _
(abs_r a * (- abs_b0 a / abs_r a)) _).
rewrite Qmult_div_r; auto.
apply Qle_refl.
apply Qmult_le_compat_l; try solve [ eapply H_swf_a ].
eapply cg_def_linear.
intro H_b0.
elim (Qeq_dec (abs_r a) (1)).
intro H_r_eq_1.
elim (Qle_lt_or_eq 0 (abs_b0 a)); auto.
intro H_b0'.
destruct H_swf_a as [ H_wf_a [ H_b0_b1 [ H_r_impl_b1 H_r_impl_b0 ] ] ].
absurd (0 < abs_b0 a); auto.
apply Qle_not_lt.
apply (Qle_trans _ (abs_b1 a) _); eauto.
clear H_b0; intro H_b0.
exists 1%nat.
rewrite ones_late_eq_ones_late_alt; try solve [ eapply H_swf_a ].
rewrite ones_late_alt_remove_Zabs_nat.
repeat rewrite <- H_b0 in *.
repeat rewrite H_r_eq_1.
compute.
reflexivity.
intro H_r_diff_1.
pose (i := Zabs_nat (cg ((abs_b1 a) / (1 - abs_r a)))).
assert (zi: Z_of_nat i = cg ((abs_b1 a) / (1 - abs_r a))).
unfold i.
rewrite inj_Zabs_nat.
apply Zabs_eq.
apply Qle_impl_Zle.
apply (Qle_trans _ ((abs_b1 a) / (1 - abs_r a)) _);
try solve [ eapply cg_def_linear ].
apply Qle_shift_div_l.
apply -> Qlt_minus_iff.
elim (Q_dec (abs_r a) 1); auto.
intro H; elim H; auto; clear H; intro H_absurd.
absurd (1 < abs_r a); auto.
apply Qle_not_lt.
eapply H_swf_a.
intro H_absurd.
absurd (abs_r a == 1); auto.
ring_simplify.
apply (Qle_trans _ (abs_b0 a) _); try solve [ eapply H_swf_a ]; auto.
exists i.
rewrite ones_late_eq_ones_late_alt; try solve [ eapply H_swf_a ].
rewrite ones_late_alt_remove_Zabs_nat.
elim (Zmin_spec i (cg (abs_r a * i + abs_b0 a))).
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
elim (Z_le_lt_eq_dec i (cg (abs_r a * i + abs_b0 a))); auto.
intro H_i.
absurd ((i < cg (abs_r a * i + abs_b0 a))%Z); auto.
clear H_i H_min.
apply Zle_not_lt.
apply Qle_impl_Zle.
apply Zle_impl_Qle.
pose (H_aux := (n_ge_cg_linear (abs_r a * i + abs_b0 a) i)).
apply Zge_le in H_aux; auto; clear H_aux.
apply <- Qle_minus_iff.
assert (H_aux:
i + - (abs_r a * i + abs_b0 a) ==
i * (1 - abs_r a) + - abs_b0 a); try ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
unfold Q_of_nat.
rewrite zi.
apply (Qle_trans _
(((abs_b1 a) / (1 - abs_r a)) * (1 - abs_r a)) _).
assert (H_aux:
(abs_b1 a / (1 - abs_r a)) * (1 - abs_r a) == abs_b1 a).
assert (H_aux:
(abs_b1 a / (1 - abs_r a)) * (1 - abs_r a) ==
(abs_b1 a * (1 - abs_r a) / (1 - abs_r a))).
unfold Qdiv.
ring.
rewrite H_aux; clear H_aux.
rewrite Qdiv_mult_l; try reflexivity.
intro H_absurd.
absurd (abs_r a == 1); auto.
apply (Qplus_comp (abs_r a) (abs_r a)) in H_absurd;
try reflexivity.
ring_simplify in H_absurd.
rewrite H_absurd.
reflexivity.
rewrite H_aux; clear H_aux.
eapply H_swf_a.
apply Qmult_le_compat_r; try solve [eapply cg_def_linear].
apply -> Qle_minus_iff.
eapply H_swf_a.
intro H_i.
rewrite H_i.
assert (H_aux:
Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply Qle_impl_Zle.
apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
try solve [ eapply cg_def_linear ].
rewrite inj_0.
apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
try solve [ ring_simplify; apply Qle_refl ].
apply Qplus_le_compat; auto.
apply Qmult_le_0_compat.
eapply H_swf_a.
apply Zle_impl_Qle.
unfold i; auto with zarith.
intros [H_min H_aux].
rewrite H_aux in *; clear H_aux.
assert (H_aux:
Zmax O (cg (abs_r a * i + abs_b0 a)) = cg (abs_r a * i + abs_b0 a));
try solve [ rewrite H_aux; reflexivity ].
apply Zmax_right.
apply Qle_impl_Zle.
apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
try solve [ eapply cg_def_linear ].
rewrite inj_0.
apply (Qle_trans _ (inject_Z 0 + inject_Z 0) _);
try solve [ ring_simplify; apply Qle_refl ].
apply Qplus_le_compat; auto.
apply Qmult_le_0_compat.
eapply H_swf_a.
apply Zle_impl_Qle.
unfold i; auto with zarith.
Qed.
Lemma ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_S_i_plus_b:
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall i: nat,
forall H_early_eq_r_i_plus_b: (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z,
(fl (abs_r a * S i + abs_b1 a) = (ones_early a (S i))%Z)%Z.
Proof.
intros.
elim (Qeq_dec (abs_r a) 1).
intro H_r.
rewrite H_r in *.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
1 * (i + 1) + abs_b1 a ==
1 * i + abs_b1 a + 1); try ring.
rewrite H_aux; clear H_aux.
assert (H_aux: (fl (1 * i + abs_b1 a + 1) = fl (1 * i + abs_b1 a) + 1)%Z).
apply fl_plus_int_rewrite.
rewrite H_aux; clear H_aux.
rewrite H_early_eq_r_i_plus_b.
assert (H_aux: 1%Z = 1%nat); auto.
rewrite H_aux; clear H_aux.
rewrite <- inj_plus.
assert (H_aux: forall n: nat, (n + 1)%nat = S n).
intro.
rewrite plus_comm.
compute.
reflexivity.
rewrite H_aux; clear H_aux.
rewrite red_ones_early.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
try reflexivity.
intro H_S_early.
rewrite <- Qgt_alt in H_S_early.
absurd (abs_r a * S i + abs_b1 a < S (ones_early a i)); auto.
apply Qle_not_lt.
rewrite <- n_plus_1_eq_S_n.
rewrite H_r.
unfold Q_of_nat.
rewrite <- H_early_eq_r_i_plus_b.
apply (Qle_trans _ ((1 * i + abs_b1 a) + 1) _);
[apply Qplus_le_compat;
[ eapply fl_def; apply Qle_refl| apply Qle_refl ] |].
ring_simplify.
assert (H_aux: i + abs_b1 a + 1 == abs_b1 a + (i + 1));
[ring|].
rewrite H_aux; clear H_aux.
rewrite n_plus_1_eq_S_n.
apply Qle_refl.
intro H_r.
assert (H_max: (0 <= fl (abs_r a * S i + abs_b1 a))%Z).
apply (Zle_trans _ (fl (abs_r a * i + abs_b1 a)) _).
rewrite H_early_eq_r_i_plus_b.
rewrite <- inj_0.
apply inj_le.
auto with arith.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b1 a ==
(abs_r a * i + abs_b1 a) + abs_r a).
ring.
rewrite H_aux; clear H_aux.
rewrite <- (Qplus_0_r (abs_r a * i + abs_b1 a)) at 1.
apply Qplus_le_compat; [ apply Qle_refl | apply H_wf_a ].
assert (H_min: (fl (abs_r a * S i + abs_b1 a) <= S i)%Z).
assert (H_aux: (fl (abs_r a + S i) = S i)%Z).
unfold Q_of_nat.
rewrite fl_plus_int_rewrite.
rewrite <- Zplus_0_l.
apply Zplus_eq_compat; try reflexivity.
apply fl_eq_0; try solve [ eapply H_wf_a ].
elim (Q_dec (abs_r a) 1); auto.
intro H_aux; elim H_aux; auto.
intro H_absurd.
absurd (1 < abs_r a); auto.
apply Qle_not_lt.
eapply H_wf_a.
intro H_absurd.
absurd (abs_r a == 1); auto.
unfold Q_of_nat; rewrite <- H_aux at 2; clear H_aux.
apply fl_monotone_linear.
apply <- Qle_minus_iff.
assert (H_aux:
abs_r a + S i + - (abs_r a * S i + abs_b1 a) ==
S i + - (abs_r a * (S i - 1) + abs_b1 a)); try ring.
rewrite H_aux; clear H_aux.
repeat rewrite <- n_plus_1_eq_S_n.
assert (H_aux: i + 1 - 1 == i); try ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
apply (Qle_trans _ (fl (abs_r a * i + abs_b1 a) + 1) _);
try solve [ apply Qlt_le_weak; eapply fl_def ].
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite H_early_eq_r_i_plus_b.
rewrite ones_early_eq_ones_w_early.
apply Zle_impl_Qle.
apply inj_le.
apply ones_i_le_i.
rewrite ones_early_eq_ones_early_alt; auto.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite Zmin_right;
try solve [ apply Zle_ge; assumption ].
rewrite Zmax_right; auto.
Qed.
Lemma ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_S_i_plus_b:
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall i: nat,
forall H_late_eq_r_i_plus_b: (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z,
(cg (abs_r a * S i + abs_b0 a) = (ones_late a (S i))%Z)%Z.
Proof.
intros.
assert (H_max: (0 <= cg (abs_r a * S i + abs_b0 a))%Z).
apply (Zle_trans _ (cg (abs_r a * i + abs_b0 a)) _).
rewrite H_late_eq_r_i_plus_b.
rewrite <- inj_0.
apply inj_le.
auto with arith.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
(abs_r a * i + abs_b0 a) + abs_r a).
ring.
rewrite H_aux; clear H_aux.
rewrite <- (Qplus_0_r (abs_r a * i + abs_b0 a)) at 1.
apply Qplus_le_compat; [ apply Qle_refl | apply H_wf_a ].
assert (H_min: (cg (abs_r a * S i + abs_b0 a) <= S i)%Z).
pose (H_aux := (n_ge_cg_linear (abs_r a * S i + abs_b0 a) (S i))).
apply Zge_le in H_aux; auto; clear H_aux.
assert (H_aux: inject_Z (Z_of_nat (S i)) = Q_of_nat (S i));
[ unfold Q_of_nat; reflexivity |].
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a); [ring |].
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; [| eapply H_wf_a ].
apply (Qle_trans _ (cg (abs_r a * i + abs_b0 a)) _);
[ eapply cg_def_linear |].
rewrite H_late_eq_r_i_plus_b.
rewrite ones_late_eq_ones_w_late.
apply Zle_impl_Qle.
apply inj_le.
apply ones_i_le_i.
rewrite ones_late_eq_ones_late_alt; auto.
rewrite ones_late_alt_remove_Zabs_nat.
rewrite Zmin_right;
try solve [ apply Zle_ge; assumption ].
rewrite Zmax_right; auto.
Qed.
Lemma ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i_plus_x_plus_b:
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall i: nat,
forall H_early_eq_r_i_plus_b: (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z,
forall x: nat,
(fl (abs_r a * (x + i)%nat + abs_b1 a) = (ones_early a (x + i)%nat)%Z)%Z.
Proof.
intros.
induction x.
rewrite plus_0_l.
assumption.
assert (H_aux: ((S x + i)%nat = S (x + i))%nat); auto with arith.
rewrite H_aux; clear H_aux.
apply ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_S_i_plus_b; auto.
Qed.
Lemma ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i_plus_x_plus_b:
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall i: nat,
forall H_late_eq_r_i_plus_b: (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z,
forall x: nat,
(cg (abs_r a * (x + i)%nat + abs_b0 a) = (ones_late a (x + i)%nat)%Z)%Z.
Proof.
intros.
induction x.
rewrite plus_0_l.
assumption.
assert (H_aux: ((S x + i)%nat = S (x + i))%nat); auto with arith.
rewrite H_aux; clear H_aux.
apply ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_S_i_plus_b; auto.
Qed.
Property ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b:
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall i: nat,
forall H_early_eq_r_i_plus_b: (fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z,
forall i': nat,
forall H_i_le_i': (i <= i')%nat,
(fl (abs_r a * i' + abs_b1 a) = (ones_early a i')%Z)%Z.
Proof.
intros.
case_eq i'.
intro H_i'.
case_eq i.
intro H_i.
rewrite H_i in H_early_eq_r_i_plus_b.
rewrite H_early_eq_r_i_plus_b.
reflexivity.
intros i0 H_i.
rewrite H_i' in H_i_le_i'.
rewrite H_i in H_i_le_i'.
absurd (S i0 <= O)%nat; auto with arith.
intros i0' H_i'.
rewrite H_i' in *.
assert (H_aux: exists x:nat, (i' = (x + i)%nat)%nat).
exists (S i0' - i)%nat.
omega.
elim H_aux; clear H_aux.
intros x H_x.
rewrite <- H_i'.
rewrite H_x.
apply ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i_plus_x_plus_b;
auto.
Qed.
Property ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b:
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall i: nat,
forall H_late_eq_r_i_plus_b: (cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z,
forall i': nat,
forall H_i_le_i': (i <= i')%nat,
(cg (abs_r a * i' + abs_b0 a) = (ones_late a i')%Z)%Z.
Proof.
intros.
case_eq i'.
intro H_i'.
case_eq i.
intro H_i.
rewrite H_i in H_late_eq_r_i_plus_b.
rewrite H_late_eq_r_i_plus_b.
reflexivity.
intros i0 H_i.
rewrite H_i' in H_i_le_i'.
rewrite H_i in H_i_le_i'.
absurd (S i0 <= O)%nat; auto with arith.
intros i0' H_i'.
rewrite H_i' in *.
assert (H_aux: exists x:nat, (i' = (x + i)%nat)%nat).
exists (S i0' - i)%nat.
omega.
elim H_aux; clear H_aux.
intros x H_x.
rewrite <- H_i'.
rewrite H_x.
apply ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i_plus_x_plus_b;
auto.
Qed.
Lemma exists_i_st_ones_early_and_ones_late_eq_r_i_plus_b:
forall a: abstraction_phd,
forall H_swf_a: strong_well_formed_abstraction_phd a,
exists i: nat,
(fl (abs_r a * i + abs_b1 a) = (ones_early a i)%Z)%Z
/\
(cg (abs_r a * i + abs_b0 a) = (ones_late a i)%Z)%Z.
Proof.
intros.
elim (exists_i_st_ones_early_eq_r_i_plus_b H_swf_a).
intros i1 H_early.
elim (exists_i_st_ones_late_eq_r_i_plus_b H_swf_a).
intros i2 H_late.
pose (i := Max.max i1 i2).
exists i.
split.
destruct H_swf_a as [ H_wf_a H_wf_a_aux ].
apply (ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b H_wf_a H_early).
apply Max.le_max_l.
destruct H_swf_a as [ H_wf_a H_wf_a_aux ].
apply (ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b H_wf_a H_late).
apply Max.le_max_r.
Qed.
Lemma exists_i_st_ones_early1_and_ones_late2_eq_r_i_plus_b:
forall a1 a2: abstraction_phd,
forall H_swf_a1: strong_well_formed_abstraction_phd a1,
forall H_swf_a2: strong_well_formed_abstraction_phd a2,
exists i: nat,
(fl (abs_r a1 * i + abs_b1 a1) = (ones_early a1 i)%Z)%Z
/\
(cg (abs_r a2 * i + abs_b0 a2) = (ones_late a2 i)%Z)%Z.
Proof.
intros.
elim (exists_i_st_ones_early_eq_r_i_plus_b H_swf_a1).
intros i1 H_early1.
elim (exists_i_st_ones_late_eq_r_i_plus_b H_swf_a2).
intros i2 H_late2.
pose (i := Max.max i1 i2).
exists i.
split.
destruct H_swf_a1 as [ H_wf_a1 H_wf_a1_aux ].
apply (ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b H_wf_a1 H_early1).
apply Max.le_max_l.
destruct H_swf_a2 as [ H_wf_a2 H_wf_a2_aux ].
apply (ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b H_wf_a2 H_late2).
apply Max.le_max_r.
Qed.
End early_and_late_properties.
Lemma ones_late_le_ones_early_impl_non_empty:
forall a,
forall H_wf: well_formed_abstraction_phd a,
forall H_early_prec_late: (forall i, ones_late a i <= ones_early a i)%nat,
non_empty a.
Proof.
intros.
unfold non_empty.
exists (w_early a).
apply ones_late_le_ones_early_impl_early_in_a; assumption.
Qed.
Section non_empty_test_properties.
Property non_empty_test_impl_ones_late_le_ones_early_aux:
forall a,
forall H_wf: well_formed_abstraction_phd a,
forall H_non_empty_alt: non_empty_test_alt a,
forall i,
(ones_late a i <= ones_early a i)%nat.
Proof.
intros.
destruct H_non_empty_alt as [H_den_b1 H_non_empty].
rewrite ones_early_eq_ones_early_alt; auto.
rewrite ones_late_eq_ones_late_alt; auto.
apply inj_le_rev.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite ones_late_alt_remove_Zabs_nat.
apply Zmax_le_compat_l.
apply Zmin_le_compat_l.
assert (H_aux:
(fl (abs_r a * i + abs_b1 a) =
fl (Qred (abs_r a * i + abs_b1 a)))%Z).
apply fl_rewrite.
rewrite Qred_correct.
apply Qeq_refl.
rewrite H_aux; clear H_aux.
rewrite fl_eq_cg.
apply cg_monotone_linear.
apply
(Qle_trans
(abs_r a * i + abs_b0 a)
(abs_r a * i + (abs_b1 a - (1 - (1 # Qden (Qred (abs_r a * i + abs_b1 a))))))
(Qred (abs_r a * i + abs_b1 a) - (1 - (1 # Qden (Qred (abs_r a * i + abs_b1 a)))))).
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply
(Qle_trans
(abs_b0 a)
(abs_b1 a - (1 - (1 # Qden (abs_r a))))
(abs_b1 a - (1 - (1 # Qden (Qred (abs_r a * i + abs_b1 a)))))).
apply <- Qle_minus_iff.
assert (H_aux:
abs_b1 a - (1 - (1 # Qden (abs_r a))) + - abs_b0 a ==
abs_b1 a - abs_b0 a + - (1 - (1 # Qden (abs_r a)))).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
assumption.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply Qopp_le_compat.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply Qopp_le_compat.
apply den_r_le_den_r_i_p_b; auto.
unfold Qminus.
rewrite Qplus_assoc.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite Qred_correct.
apply Qle_refl.
Qed.
Lemma simpl_std:
forall x y: Q,
((Qnum x * QDen y)%Z # (Qden x * Qden y)) == x.
Proof.
intros.
unfold Qeq, Qmult, Qdiv; simpl.
rewrite Zpos_mult_morphism.
ring.
Qed.
Property non_empty_test_equal_compat:
forall a1 a2: abstraction_phd,
forall H_a1_eq_a2: abs_equal a1 a2,
forall H_non_empty1: non_empty_test a1,
forall H_den:
1 # Qden (abs_b1 a1) * Qden (abs_r a1) <=
1 # Qden (abs_b1 a2) * Qden (abs_r a2),
non_empty_test a2.
Proof.
intros.
unfold non_empty_test in *.
destruct H_a1_eq_a2 as [H_r [H_b1 H_b0]].
simpl in *.
rewrite simpl_std in *.
rewrite <- H_b0.
apply
(Qle_trans
(1 - (1 # Qden (abs_b1 a2) * Qden (abs_r a2)))
(1 - (1 # Qden (abs_b1 a1) * Qden (abs_r a1)))
(abs_b1 a2 - abs_b0 a1)); auto.
apply Qplus_le_compat; try solve [apply Qle_refl].
apply Qopp_le_compat.
assumption.
rewrite <- H_b1.
assumption.
Qed.
Property abs_equal_abs_std_non_empty:
forall a: abstraction_phd,
abs_equal a (abs_std a).
Proof.
intros.
repeat split; auto;
unfold Qeq; simpl;
rewrite Zpos_mult_morphism;
ring.
Qed.
Property non_empty_test_impl_ones_late_le_ones_early:
forall a,
forall H_wf: well_formed_abstraction_phd a,
forall H_non_empty: non_empty_test a,
forall i,
(ones_late a i <= ones_early a i)%nat.
Proof.
intros.
pose (a_std := abs_std a).
assert (H_a_eq_a_std: abs_equal a a_std).
apply abs_equal_abs_std_non_empty.
assert (H_wf_std: well_formed_abstraction_phd a_std).
apply (well_formed_abstraction_phd_abs_equal_compat H_a_eq_a_std).
assumption.
rewrite (ones_early_rewrite H_wf H_wf_std); auto.
rewrite (ones_late_rewrite H_wf H_wf_std); auto.
apply non_empty_test_impl_ones_late_le_ones_early_aux; auto.
split; auto.
Qed.
End non_empty_test_properties.
Section on_properties.
Property on_abs_well_formed_abstraction_phd_compat:
forall (a1:abstraction_phd) (a2:abstraction_phd),
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_wf_a2: well_formed_abstraction_phd a2,
well_formed_abstraction_phd (on_abs a1 a2).
Proof.
intros.
unfold well_formed_abstraction_phd.
simpl.
destruct H_wf_a1 as [ H_r1_pos H_r1_le_1 ].
destruct H_wf_a2 as [ H_r2_pos H_r1_le_2 ].
split.
apply Qmult_le_0_compat; assumption.
apply (Qle_trans _ (abs_r a2) _); auto.
assert (H_aux: abs_r a2 == 1 * abs_r a2); [ring|].
rewrite H_aux at 2; clear H_aux.
apply Qmult_le_compat_r; auto.
Qed.
Lemma on_w1_w2_le_on_a1_a2:
forall (w1:ibw) (w2:ibw),
forall (a1:abstraction_phd) (a2:abstraction_phd),
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_wf_a2: well_formed_abstraction_phd a2,
forall (H_a1_eq_abs_w1: in_abstraction_phd w1 a1),
forall (H_a2_eq_abs_w2: in_abstraction_phd w2 a2),
forall i,
forall H_i_ge_1: (i >= 1)%nat,
forall (H_on: on w1 w2 i = true),
ones (on w1 w2) i <=
(abs_r a1 * abs_r a2) * i + (abs_b1 a1 * abs_r a2 + abs_b1 a2).
Proof.
intros.
generalize (on_eq_1_impl_w1_eq_1 w1 w2 i H_on).
intro H_w1.
generalize (on_eq_1_impl_w2_eq_1 w1 w2 i H_on).
intro H_w2.
assert (H_w1_le_a1 : ones w1 i <= abs_r a1 * i + abs_b1 a1).
unfold in_abstraction_phd in H_a1_eq_abs_w1.
generalize (H_a1_eq_abs_w1 i H_i_ge_1).
clear H_a1_eq_abs_w1.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_false.
generalize (H_aux_true H_w1). clear H_aux_true.
trivial.
rewrite ones_on_def.
assert (H_w2_le_a2:
ones w2 (ones w1 i) <= (abs_r a2 * ones w1 i + abs_b1 a2)).
unfold in_abstraction_phd in H_a2_eq_abs_w2.
assert (H_ones_w1_ge_1: (ones w1 i >= 1)%nat).
case_eq i.
intro H_i.
rewrite H_i in H_i_ge_1.
absurd ((0 >= 1)%nat); auto.
unfold ge.
apply le_Sn_O.
intros.
simpl.
rewrite <- H.
rewrite H_w1.
auto with arith.
generalize (H_a2_eq_abs_w2 (ones w1 i) H_ones_w1_ge_1).
clear H_a2_eq_abs_w2.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_false.
generalize (H_aux_true H_w2). clear H_aux_true.
trivial.
apply
(Qle_trans
(ones w2 (ones w1 i))
(abs_r a2 * ones w1 i + abs_b1 a2)
(abs_r a1 * abs_r a2 * i + (abs_b1 a1 * abs_r a2 + abs_b1 a2))
H_w2_le_a2).
assert (H_aux:
abs_r a1 * abs_r a2 * i + (abs_b1 a1 * abs_r a2 + abs_b1 a2) ==
(abs_r a1 * abs_r a2 * i + abs_b1 a1 * abs_r a2) + abs_b1 a2).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
assert (H_aux:
abs_r a1 * abs_r a2 * i + abs_b1 a1 * abs_r a2 ==
(abs_r a1 * i + abs_b1 a1) * abs_r a2).
ring.
rewrite H_aux; clear H_aux.
rewrite Qmult_comm.
apply Qmult_le_compat_r; try solve [ apply H_wf_a2 ].
assumption.
Qed.
Lemma on_ge_0:
forall (w1:ibw) (w2:ibw) i,
forall (H_on: on w1 w2 i = false),
(ones (on w1 w2) i >= 0).
Proof.
intros.
assert ((0 <= ones (on w1 w2) i)%nat).
auto with arith.
simpl.
apply (le_impl_Qle H).
Qed.
Lemma abs_b0_neg_impl_ones_ge_a:
forall (w:ibw) (a:abstraction_phd),
forall H_wf_a: well_formed_abstraction_phd a,
forall H_flo: abs_b0 a <= 0,
forall H_a_eq_abs_w: in_abstraction_phd w a,
forall i:nat,
ones w i >= abs_r a * i + abs_b0 a.
Proof.
induction i.
assert (H_aux: abs_r a * 0 == 0).
ring.
rewrite H_aux; clear H_aux.
assert (H_aux: 0 + abs_b0 a == abs_b0 a).
apply Qplus_0_l.
rewrite H_aux; clear H_aux.
simpl.
exact H_flo.
case_eq (w (S i)).
intro H_w.
rewrite ones_S_i_eq_S_ones_i; auto.
simpl.
repeat rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
abs_r a * (i + 1) + abs_b0 a ==
abs_r a * i + abs_b0 a + abs_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply H_wf_a ].
exact IHi.
intro H_w.
unfold in_abstraction_phd in H_a_eq_abs_w.
assert (H_S_i_ge_1:(S i >= 1)%nat).
auto with arith.
generalize (H_a_eq_abs_w (S i) H_S_i_ge_1).
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_true.
generalize (H_aux_false H_w). clear H_aux_false.
intro H_cc.
simpl in H_cc.
rewrite H_w in H_cc.
simpl in H_cc.
apply
(Qle_trans
(abs_r a * S i + abs_b0 a)
(ones w i)
(ones w (S i))); auto.
apply le_impl_Qle.
apply ones_increasing; auto.
Qed.
Lemma on_w1_w2_ge_on_a1_a2:
forall (w1:ibw) (w2:ibw),
forall (a1:abstraction_phd) (a2:abstraction_phd),
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_flo_a1: abs_b0 a1 <= 0,
forall H_wf_a2: well_formed_abstraction_phd a2,
forall H_flo_a2: abs_b0 a2 <= 0,
forall (H_a1_eq_abs_w1: in_abstraction_phd w1 a1),
forall (H_a2_eq_abs_w2: in_abstraction_phd w2 a2),
forall i,
forall (H_on: on w1 w2 i = false),
abs_r a1 * abs_r a2 * i + (abs_b0 a1 * abs_r a2 + abs_b0 a2)
<= ones (on w1 w2) i.
Proof.
intros.
rewrite ones_on_def.
generalize (abs_b0_neg_impl_ones_ge_a H_wf_a1 H_flo_a1 H_a1_eq_abs_w1 i).
intro H_w1_ge_a1.
generalize (abs_b0_neg_impl_ones_ge_a H_wf_a2 H_flo_a2 H_a2_eq_abs_w2 (ones w1 i)).
intro H_w2_ge_a2.
apply
(Qle_trans
(abs_r a1 * abs_r a2 * i + (abs_b0 a1 * abs_r a2 + abs_b0 a2))
(abs_r a2 * ones w1 i + abs_b0 a2)
(ones w2 (ones w1 i))); auto.
rewrite Qplus_assoc.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
assert (H_r_pos_2: (0 <= abs_r a2)).
apply H_wf_a2.
generalize
(Qmult_le_compat_r
(abs_r a1 * i + abs_b0 a1)
(ones w1 i)
(abs_r a2)
H_w1_ge_a1
(H_r_pos_2)).
intro H_cc.
rewrite Qmult_plus_distr_l in H_cc.
assert (H_aux: abs_r a1 * i * abs_r a2 == abs_r a1 * abs_r a2 * i).
ring.
rewrite H_aux in H_cc; clear H_aux.
assert (H_aux: ones w1 i * abs_r a2 == abs_r a2 * ones w1 i).
ring.
rewrite H_aux in H_cc; clear H_aux.
exact H_cc.
Qed.
Property on_abs_correctness_aux:
forall (w1:ibw) (w2:ibw),
forall (a1:abstraction_phd) (a2:abstraction_phd),
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_wf_a2: well_formed_abstraction_phd a2,
forall (H_a1_eq_abs_w1: in_abstraction_phd w1 a1),
forall (H_a2_eq_abs_w2: in_abstraction_phd w2 a2),
in_abstraction_phd (on w1 w2) (on_abs a1 a2).
Proof.
intros.
assert (H_aux:
exists a1_0,
(abs_b1 a1_0 == abs_b1 a1) /\
(abs_b0 a1_0 == 0) /\
(abs_r a1_0 == abs_r a1)).
exists (absmake (abs_b1 a1) 0 (abs_r a1)).
simpl.
repeat split; eapply Qeq_refl.
elim H_aux.
clear H_aux.
intros a1_0 H_a1_0.
assert (H_wf_a1_0: well_formed_abstraction_phd a1_0).
unfold well_formed_abstraction_phd.
destruct H_a1_0.
destruct H0.
rewrite H1.
assumption.
assert (H_abs_b01_0: abs_b0 a1_0 <= 0).
destruct H_a1_0.
destruct H0.
rewrite H0.
eapply Qle_refl.
assert (H_aux:
exists a2_0,
(abs_b1 a2_0 == abs_b1 a2) /\
(abs_b0 a2_0 == 0) /\
(abs_r a2_0 == abs_r a2)).
exists (absmake (abs_b1 a2) 0 (abs_r a2)).
simpl.
repeat split; eapply Qeq_refl.
elim H_aux.
clear H_aux.
intros a2_0 H_a2_0.
assert (H_wf_a2_0: well_formed_abstraction_phd a2_0).
unfold well_formed_abstraction_phd.
destruct H_a2_0.
destruct H0.
rewrite H1.
assumption.
assert (H_abs_b02_0: abs_b0 a2_0 <= 0).
destruct H_a2_0.
destruct H0.
rewrite H0.
eapply Qle_refl.
unfold in_abstraction_phd.
intros.
split.
intro H_on.
simpl.
eapply on_w1_w2_le_on_a1_a2; assumption.
intro H_on.
elim (Q_dec (abs_b0 a1) 0);
elim (Q_dec (abs_b0 a2) 0).
intros H_aux1 H_aux2.
elim H_aux1;
elim H_aux2.
clear H_aux1 H_aux2.
intros H_abs_b01 H_abs_b02.
elim (Qlt_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qlt_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (abs_b0 a1) 0 H_abs_b01)
H_wf_a2 (Qlt_le_weak (abs_b0 a2) 0 H_abs_b02)
H_a1_eq_abs_w1 H_a2_eq_abs_w2);
auto.
clear H_aux1 H_aux2.
intros H_abs_b01 H_abs_b02.
elim (Qgt_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qlt_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
assert (H_a1_0_eq_abs_w1: in_abstraction_phd w1 a1_0).
assert (H_a1_in_a1_0: abs_included_test a1 a1_0).
apply abs_weakening_0;
decompose [and] H_a1_0;
auto.
rewrite H2; reflexivity.
rewrite H; reflexivity.
apply
(w_in_a1_and_a1_in_a2_impl_w_in_a2
H_wf_a1 H_wf_a1_0
H_a1_in_a1_0 H_a1_eq_abs_w1).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_abs_b01_0
H_wf_a2 (Qlt_le_weak (abs_b0 a2) 0 H_abs_b02)
H_a1_0_eq_abs_w1 H_a2_eq_abs_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
trivial.
clear H_aux1 H_aux2.
intros H_abs_b01 H_abs_b02.
elim (Qlt_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qgt_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
assert (H_a2_0_eq_abs_w2: in_abstraction_phd w2 a2_0).
assert (H_a2_in_a2_0: abs_included_test a2 a2_0).
apply abs_weakening_0;
decompose [and] H_a2_0;
auto.
rewrite H2; reflexivity.
rewrite H; reflexivity.
apply
(w_in_a1_and_a1_in_a2_impl_w_in_a2
H_wf_a2 H_wf_a2_0
H_a2_in_a2_0 H_a2_eq_abs_w2).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (abs_b0 a1) 0 H_abs_b01)
H_wf_a2_0 H_abs_b02_0
H_a1_eq_abs_w1 H_a2_0_eq_abs_w2
i H_on).
decompose [and] H_a2_0.
rewrite H2, H1.
trivial.
clear H_aux1 H_aux2.
intros H_abs_b01 H_abs_b02.
elim (Qgt_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qgt_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
assert (H_a1_0_eq_abs_w1: in_abstraction_phd w1 a1_0).
assert (H_a1_in_a1_0: abs_included_test a1 a1_0).
apply abs_weakening_0;
decompose [and] H_a1_0;
auto.
rewrite H2; reflexivity.
rewrite H; reflexivity.
apply
(w_in_a1_and_a1_in_a2_impl_w_in_a2
H_wf_a1 H_wf_a1_0
H_a1_in_a1_0 H_a1_eq_abs_w1).
assert (H_a2_0_eq_abs_w2: in_abstraction_phd w2 a2_0).
assert (H_a2_in_a2_0: abs_included_test a2 a2_0).
apply abs_weakening_0;
decompose [and] H_a2_0;
auto.
rewrite H2; reflexivity.
rewrite H; reflexivity.
apply
(w_in_a1_and_a1_in_a2_impl_w_in_a2
H_wf_a2 H_wf_a2_0
H_a2_in_a2_0 H_a2_eq_abs_w2).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_abs_b01_0
H_wf_a2_0 H_abs_b02_0
H_a1_0_eq_abs_w1 H_a2_0_eq_abs_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
decompose [and] H_a2_0.
rewrite H5, H4.
trivial.
intros H_abs_b02 H_aux.
elim H_aux.
clear H_aux.
intro H_abs_b01.
elim (Qlt_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qeq_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
assert (H_abs_b02_le_0: abs_b0 a2 <= 0).
rewrite H_abs_b02.
apply Qle_refl.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (abs_b0 a1) 0 H_abs_b01)
H_wf_a2 H_abs_b02_le_0
H_a1_eq_abs_w1 H_a2_eq_abs_w2);
auto.
clear H_aux.
intro H_abs_b01.
elim (Qgt_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qeq_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
assert (H_a1_0_eq_abs_w1: in_abstraction_phd w1 a1_0).
assert (H_a1_in_a1_0: abs_included_test a1 a1_0).
apply abs_weakening_0;
decompose [and] H_a1_0;
auto.
rewrite H2; reflexivity.
rewrite H; reflexivity.
apply
(w_in_a1_and_a1_in_a2_impl_w_in_a2
H_wf_a1 H_wf_a1_0
H_a1_in_a1_0 H_a1_eq_abs_w1).
assert (H_abs_b02_le_0: abs_b0 a2 <= 0).
rewrite H_abs_b02.
apply Qle_refl.
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_abs_b01_0
H_wf_a2 H_abs_b02_le_0
H_a1_0_eq_abs_w1 H_a2_eq_abs_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
trivial.
intros H_aux H_abs_b01.
elim H_aux.
clear H_aux.
intro H_abs_b02.
elim (Qeq_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qlt_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
assert (H_abs_b01_le_0: abs_b0 a1 <= 0).
rewrite H_abs_b01.
apply Qle_refl.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_abs_b01_le_0
H_wf_a2 (Qlt_le_weak (abs_b0 a2) 0 H_abs_b02)
H_a1_eq_abs_w1 H_a2_eq_abs_w2);
auto.
clear H_aux.
intro H_abs_b02.
elim (Qeq_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qgt_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp.
rewrite H_abs_b02_eq_cmp.
assert (H_a2_0_eq_abs_w2: in_abstraction_phd w2 a2_0).
assert (H_a2_in_a2_0: abs_included_test a2 a2_0).
apply abs_weakening_0;
decompose [and] H_a2_0;
auto.
rewrite H2; reflexivity.
rewrite H; reflexivity.
apply
(w_in_a1_and_a1_in_a2_impl_w_in_a2
H_wf_a2 H_wf_a2_0
H_a2_in_a2_0 H_a2_eq_abs_w2).
assert (H_abs_b01_le_0: abs_b0 a1 <= 0).
rewrite H_abs_b01.
apply Qle_refl.
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_abs_b01_le_0
H_wf_a2_0 H_abs_b02_0
H_a1_eq_abs_w1 H_a2_0_eq_abs_w2
i H_on).
decompose [and] H_a2_0.
rewrite H2, H1.
trivial.
intros H_abs_b02 H_abs_b01.
elim (Qeq_alt (abs_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b01).
clear H_aux1 H_aux2.
intro H_abs_b01_eq_cmp.
elim (Qeq_alt (abs_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_abs_b02).
clear H_aux1 H_aux2.
intro H_abs_b02_eq_cmp.
simpl.
rewrite H_abs_b01_eq_cmp, H_abs_b02_eq_cmp.
assert (H_abs_b01_le_0: abs_b0 a1 <= 0).
rewrite H_abs_b01.
apply Qle_refl.
assert (H_abs_b02_le_0: abs_b0 a2 <= 0).
rewrite H_abs_b02.
apply Qle_refl.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_abs_b01_le_0
H_wf_a2 H_abs_b02_le_0
H_a1_eq_abs_w1 H_a2_eq_abs_w2
i H_on).
Qed.
End on_properties.
Section not_properties.
Property not_abs_correctness_aux:
forall w: ibw,
forall a:abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
forall H_a_eq_abs_w: in_abstraction_phd w a,
in_abstraction_phd (not w) (not_abs a).
Proof.
intros.
unfold in_abstraction_phd.
intros.
case_eq i.
intros H_i.
rewrite H_i in H_i_ge_1.
absurd ((0 >= 1)%nat); auto.
unfold ge.
auto with arith.
intros i' H_i.
rewrite H_i in H_i_ge_1.
clear H_i i.
induction i'.
split.
intro H_not.
assert (H_w: w 1%nat = false).
unfold not in H_not.
assert (H_false_eq_not_true: false = negb true); auto.
rewrite H_false_eq_not_true; clear H_false_eq_not_true.
apply negb_sym.
auto.
simpl.
rewrite H_w.
simpl.
pose (H_w_1_in_a:= H_a_eq_abs_w 1%nat H_i_ge_1).
destruct H_w_1_in_a.
pose (H_cc:= H0 H_w).
simpl in H_cc.
rewrite H_w in H_cc.
simpl in H_cc.
apply <- Qle_minus_iff.
assert (H_aux:
(1 - abs_r a) * 1 + - abs_b0 a + - (1) ==
0 + - (abs_r a * 1 + abs_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
assumption.
intro H_not.
assert (H_w: w 1%nat = true).
unfold not in H_not.
assert (H_false_eq_not_true: true = negb false); auto.
rewrite H_false_eq_not_true; clear H_false_eq_not_true.
apply negb_sym.
auto.
simpl.
generalize (H_a_eq_abs_w 1%nat H_i_ge_1).
clear H_a_eq_abs_w.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_false.
generalize (H_aux_true H_w). clear H_aux_true.
simpl.
intro H_abs_b1.
rewrite H_w in *.
simpl.
simpl in H_abs_b1.
apply <- Qle_minus_iff.
assert (H_aux:
0 + - ((1 - abs_r a) * 1 + - abs_b1 a) ==
abs_r a * 1 + abs_b1 a + - (1)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
assumption.
split.
intro H_not_S_S_i'.
assert (H_w_S_S_i': w (S (S i')) = false).
unfold not in H_not_S_S_i'.
assert (H_false_eq_not_true: false = negb true); auto.
rewrite H_false_eq_not_true; clear H_false_eq_not_true.
apply negb_sym.
auto.
case_eq (w (S i')).
intros H_w_S_i'.
assert (H_not_S_i': not w (S i') = false).
unfold not.
rewrite H_w_S_i'.
simpl.
trivial.
rewrite ones_S_i_eq_S_ones_i; auto.
simpl.
rewrite H_w_S_i'.
simpl.
rewrite ones_not_def.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
eapply minus_impl_Qminus.
eapply ones_i_le_i.
rewrite H_aux; clear H_aux.
assert (H_ones_w_ge_a: abs_r a * S (S i') + abs_b0 a <= ones w (S (S i'))).
unfold in_abstraction_phd in H_a_eq_abs_w.
generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
clear H_a_eq_abs_w.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_true.
generalize (H_aux_false H_w_S_S_i'). clear H_aux_false.
trivial.
rewrite ones_S_i_eq_ones_i in H_ones_w_ge_a; auto.
rewrite ones_S_i_eq_S_ones_i in H_ones_w_ge_a; auto.
simpl in H_ones_w_ge_a.
rewrite <- (n_plus_1_eq_S_n (S i')) in H_ones_w_ge_a.
rewrite <- (n_plus_1_eq_S_n (ones w i')) in H_ones_w_ge_a.
rewrite <- n_plus_1_eq_S_n.
rewrite -> Qle_minus_iff.
assert (H_aux:
(1 - abs_r a) * (S i' + 1) + - abs_b0 a + - (i' - ones w i' + 1) ==
ones w i' + (S i' - i') + - (abs_r a * (S i' + 1) + abs_b0 a)).
ring.
rewrite H_aux; clear H_aux.
rewrite <- Qle_minus_iff.
assert (H_aux: S i' - i' == 1).
rewrite <- n_plus_1_eq_S_n.
ring.
rewrite H_aux; clear H_aux.
assumption.
intros H_w_S_i'.
assert (H_not_w_S_i': not w (S i') = true).
unfold not.
rewrite H_w_S_i'.
simpl.
trivial.
simpl.
rewrite H_w_S_S_i'.
rewrite H_w_S_i'.
simpl.
assert (H_ones_w_ge_a: abs_r a * S (S i') + abs_b0 a <= ones w (S (S i'))).
unfold in_abstraction_phd in H_a_eq_abs_w.
generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
clear H_a_eq_abs_w.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_true.
generalize (H_aux_false H_w_S_S_i'). clear H_aux_false.
intro H_cc.
trivial.
rewrite ones_S_i_eq_ones_i in H_ones_w_ge_a; auto.
rewrite ones_S_i_eq_ones_i in H_ones_w_ge_a; auto.
rewrite ones_not_def.
rewrite <- n_plus_1_eq_S_n.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
eapply minus_impl_Qminus.
eapply ones_i_le_i.
rewrite H_aux; clear H_aux.
apply <- Qle_minus_iff.
assert (H_aux:
(1 - abs_r a) * S (S i') + - abs_b0 a + - (i' - ones w i' + 1 + 1) ==
ones w i' + (S (S i') - i' - 1 - 1) + - (abs_r a * S (S i') + abs_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
assert (H_aux: ones w i' + (S (S i') - i' - 1 - 1) == ones w i').
repeat rewrite <- n_plus_1_eq_S_n.
ring.
rewrite H_aux; clear H_aux.
assumption.
intro H_not_S_S_i'.
assert (H_w_S_S_i': w (S (S i')) = true).
unfold not in H_not_S_S_i'.
assert (H_false_eq_not_true: true = negb false); auto.
rewrite H_false_eq_not_true; clear H_false_eq_not_true.
apply negb_sym.
auto.
case_eq (w (S i')).
intros H_w_S_i'.
assert (H_not_w_S_i': not w (S i') = false).
unfold not.
rewrite H_w_S_i'.
simpl.
trivial.
case_eq (w i').
intros H_w_i'.
rewrite ones_S_i_eq_ones_i; auto.
simpl.
rewrite H_w_S_i'.
simpl.
rewrite ones_not_def.
assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
eapply minus_impl_Qminus.
eapply ones_i_le_i.
rewrite H_aux; clear H_aux.
assert (H_ones_w_le_a: ones w (S (S i')) <= abs_r a * (S (S i')) + abs_b1 a).
unfold in_abstraction_phd in H_a_eq_abs_w.
generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
clear H_a_eq_abs_w.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_false.
generalize (H_aux_true H_w_S_S_i'). clear H_aux_true.
trivial.
rewrite ones_S_i_eq_S_ones_i in H_ones_w_le_a; auto.
simpl in H_ones_w_le_a.
rewrite H_w_S_i' in H_ones_w_le_a.
simpl in H_ones_w_le_a.
rewrite <- (n_plus_1_eq_S_n (S (ones w i'))) in H_ones_w_le_a.
rewrite <- (n_plus_1_eq_S_n (ones w i')) in H_ones_w_le_a.
apply <- Qle_minus_iff.
assert (H_aux:
i' - ones w i' + - ((1 - abs_r a) * S (S i') + - abs_b1 a) ==
abs_r a * S (S i') + abs_b1 a + - (ones w i' + S (S i') + - i')).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
rewrite <- n_plus_1_eq_S_n at 1.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
ones w i' + (i' + 1 + 1) + - i' == ones w i' + 1 + 1).
ring.
rewrite H_aux; clear H_aux.
assumption.
intros H_w_i'.
case_eq i'.
intro H_i'.
rewrite H_i' in *.
simpl.
rewrite H_w_S_S_i'.
rewrite H_w_S_i'.
simpl.
simpl in IHi'.
rewrite H_w_S_i' in IHi'.
simpl in IHi'.
pose (H_w_2_in_a:= H_a_eq_abs_w 2).
simpl in H_w_2_in_a.
rewrite H_w_S_S_i' in H_w_2_in_a.
rewrite H_w_S_i' in H_w_2_in_a.
simpl in H_w_2_in_a.
assert (H_2_ge_1: (2 >= 1)%nat);
auto with arith.
pose (H_tmp:= H_w_2_in_a H_2_ge_1).
destruct H_tmp as [H_true H_false].
apply <- Qle_minus_iff.
assert (H_aux:
0 + - ((1 - abs_r a) * 2 + - abs_b1 a) ==
abs_r a * 2 + abs_b1 a + - (2)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
auto.
intros i'' H_i''.
rewrite <- H_i''.
assert (H_not_w_i: not w i' = true).
unfold not.
rewrite H_i''.
rewrite <- H_i''.
rewrite H_w_i'.
simpl.
trivial.
rewrite ones_S_i_eq_ones_i; auto.
simpl.
rewrite H_w_S_i'.
simpl.
rewrite ones_not_def.
assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
eapply minus_impl_Qminus.
eapply ones_i_le_i.
rewrite H_aux; clear H_aux.
assert (H_ones_w_le_a:
ones w (S (S i')) <= abs_r a * S (S i') + abs_b1 a).
unfold in_abstraction_phd in H_a_eq_abs_w.
generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
clear H_a_eq_abs_w.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_false.
generalize (H_aux_true H_w_S_S_i'). clear H_aux_true.
trivial.
rewrite ones_S_i_eq_S_ones_i in H_ones_w_le_a; auto.
rewrite ones_S_i_eq_S_ones_i in H_ones_w_le_a; auto.
simpl in H_ones_w_le_a.
rewrite <- n_plus_1_eq_S_n in H_ones_w_le_a.
rewrite <- n_plus_1_eq_S_n in H_ones_w_le_a.
apply <- Qle_minus_iff.
assert (H_aux:
i' - ones w i' + - ((1 - abs_r a) * S (S i') + - abs_b1 a) ==
abs_r a * S (S i') + abs_b1 a + - (ones w i' + S (S i') + - i')).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
rewrite <- n_plus_1_eq_S_n at 1.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
ones w i' + (i' + 1 + 1) + - i' == ones w i' + 1 + 1).
ring.
rewrite H_aux; clear H_aux.
assumption.
intros H_w_S_i'.
assert (H_not_w_S_i': not w (S i') = true).
unfold not.
rewrite H_w_S_i'.
simpl.
trivial.
rewrite ones_S_i_eq_ones_i; auto.
simpl.
rewrite H_w_S_i'.
simpl.
rewrite <- (n_plus_1_eq_S_n (ones (not w) i')).
rewrite ones_not_def.
assert (H_aux: (i' - ones w i')%nat == (i' - ones w i')%Q).
eapply minus_impl_Qminus.
eapply ones_i_le_i.
rewrite H_aux; clear H_aux.
assert (H_ones_w_le_a: ones w (S (S i')) <= abs_r a * S (S i') + abs_b1 a).
unfold in_abstraction_phd in H_a_eq_abs_w.
generalize (H_a_eq_abs_w (S (S i')) H_i_ge_1).
clear H_a_eq_abs_w.
intro H_aux. elim H_aux. clear H_aux.
intros H_aux_true H_aux_false. clear H_aux_false.
generalize (H_aux_true H_w_S_S_i'). clear H_aux_true.
trivial.
rewrite ones_S_i_eq_S_ones_i in H_ones_w_le_a; auto.
rewrite ones_S_i_eq_ones_i in H_ones_w_le_a; auto.
simpl in H_ones_w_le_a.
rewrite <- n_plus_1_eq_S_n in H_ones_w_le_a.
apply <- Qle_minus_iff.
assert (H_aux:
i' - ones w i' + 1 + - ((1 - abs_r a) * S (S i') + - abs_b1 a) ==
abs_r a * S (S i') + abs_b1 a + - (ones w i' + S (S i') - i' - 1)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
rewrite <- n_plus_1_eq_S_n at 1.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
ones w i' + (i' + 1 + 1) + - i' - 1 == ones w i' + 1).
ring.
rewrite H_aux; clear H_aux.
assumption.
Qed.
Lemma abs_included_test_not_not_abs:
forall a: abstraction_phd,
abs_included_test a (not_abs (not_abs a)).
Proof.
intros.
unfold abs_included_test.
repeat split.
simpl.
ring.
simpl.
ring_simplify.
apply Qle_refl.
simpl.
ring_simplify.
apply Qle_refl.
Qed.
Lemma not_not_abs_included_test_abs:
forall a: abstraction_phd,
abs_included_test (not_abs (not_abs a)) a.
Proof.
intros.
unfold abs_included_test.
repeat split.
simpl.
ring.
simpl.
ring_simplify.
apply Qle_refl.
simpl.
ring_simplify.
apply Qle_refl.
Qed.
Property not_not_abs_equal_abs:
forall a: abstraction_phd,
abs_equal (not_abs (not_abs a)) a.
Proof.
intros.
apply abs_equiv_test_impl_abs_equal.
split.
apply not_not_abs_included_test_abs.
apply abs_included_test_not_not_abs.
Qed.
Property not_abs_well_formed_abstraction_phd_compat:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
well_formed_abstraction_phd (not_abs a).
Proof.
intros.
unfold well_formed_abstraction_phd.
simpl.
destruct H_wf as [H0 H1].
split.
apply -> Qle_minus_iff.
assumption.
apply <- Qle_minus_iff.
ring_simplify.
assumption.
Qed.
Property not_abs_eq_compat:
forall a1 a2: abstraction_phd,
forall H_eq: abs_equal a1 a2,
abs_equal (not_abs a1) (not_abs a2).
Proof.
intros.
unfold abs_equal.
destruct H_eq as [ H_r [ H_b1 H_b0 ] ].
repeat split.
simpl.
rewrite H_r.
apply Qeq_refl.
simpl.
rewrite H_b0.
apply Qeq_refl.
simpl.
rewrite H_b1.
apply Qeq_refl.
Qed.
End not_properties.
Section prec_abs_properties.
Property w_early_prec_a:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall w: ibw,
forall H_w_in_a: in_abstraction_phd w a,
prec (w_early a) w.
Proof.
intros.
unfold prec.
unfold ge.
intros.
rewrite <- ones_early_eq_ones_w_early.
apply ones_w_le_ones_early; assumption.
Qed.
Property a_prec_w_late:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall w: ibw,
forall H_w_in_a: in_abstraction_phd w a,
prec w (w_late a).
Proof.
intros.
unfold prec.
unfold ge.
intros.
rewrite <- ones_late_eq_ones_w_late.
apply ones_late_le_ones_w; assumption.
Qed.
Property prec_abs_alt_correctness:
forall a1 a2: abstraction_phd,
forall H_wf1: well_formed_abstraction_phd a1,
forall H_wf2: well_formed_abstraction_phd a2,
forall H_prec_test: prec_abs_alt a1 a2,
prec_abs a1 a2.
Proof.
intros.
unfold prec_abs.
intros.
pose (H_early2_prec_w2:= w_early_prec_a H_wf2 H_w2_in_a2).
unfold prec_abs_alt in H_prec_test.
pose (H_w1_prec_late1:= a_prec_w_late H_wf1 H_w1_in_a1).
assert (H_w1_prec_w_early2: prec w1 (w_early a2)).
apply (prec_trans H_w1_prec_late1 H_prec_test).
apply (prec_trans H_w1_prec_w_early2 H_early2_prec_w2).
Qed.
Property prec_abs_alt_complet:
forall a1 a2: abstraction_phd,
forall H_wf1: well_formed_abstraction_phd a1,
forall H_non_empty1: non_empty a1,
forall H_wf2: well_formed_abstraction_phd a2,
forall H_non_empty2: non_empty a2,
forall H_prec: prec_abs a1 a2,
prec_abs_alt a1 a2.
Proof.
intros.
unfold prec_abs_alt.
unfold prec_abs in H_prec.
apply H_prec.
apply late_in_abs; auto.
apply early_in_abs; auto.
Qed.
Property prec_abs_test_correctness_aux:
forall a1 a2: abstraction_phd,
forall H_wf1: well_formed_abstraction_phd a1,
forall H_wf2: well_formed_abstraction_phd a2,
forall H_prec_test: prec_abs_test a1 a2,
forall H_sync: abs_r a1 == abs_r a2,
prec_abs a1 a2.
Proof.
intros.
apply prec_abs_alt_correctness; auto.
unfold prec_abs_alt.
unfold prec.
intro i.
rewrite <- ones_early_eq_ones_w_early.
rewrite <- ones_late_eq_ones_w_late.
unfold ge.
apply inj_le_rev.
rewrite ones_early_eq_ones_early_alt; auto.
rewrite ones_late_eq_ones_late_alt; auto.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite ones_late_alt_remove_Zabs_nat.
apply Zmax_le_compat_l.
apply Zmin_le_compat_l.
apply Zlt_impl_Zle.
rewrite <- cg_plus_int_rewrite.
apply x_lt_y_impl_fl_x_lt_cg_y; auto.
rewrite H_sync.
rewrite <- Qplus_assoc.
apply Qplus_lt_compat_l.
unfold prec_abs_test in H_prec_test.
apply <- Qlt_minus_iff.
assert (H_aux:
abs_b0 a1 + 1 + - abs_b1 a2 == 1 + - (abs_b1 a2 - abs_b0 a1)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
Qed.
End prec_abs_properties.
Section sync_properties.
Property sync_early_late:
forall a: abstraction_phd,
forall H_swf: strong_well_formed_abstraction_phd a,
forall H_non_empty: non_empty a,
sync (w_late a) (w_early a).
Proof.
intros.
assert (H_wf: well_formed_abstraction_phd a); [ eapply H_swf |].
unfold sync.
elim (exists_i_st_ones_early_and_ones_late_eq_r_i_plus_b H_swf).
intros i_lim [ H_early H_late ].
pose (b1_pref := (- i_lim)%Z).
pose (b2_pref := (i_lim)%Z).
pose (b1_suff := fl (abs_b0 a - abs_b1 a)).
pose (b2_suff := cg (abs_b0 a - abs_b1 a + 1 + 1)).
exists (Zmin b1_pref b1_suff).
exists (Zmax b2_pref b2_suff).
intro i.
elim (le_lt_dec i_lim i).
intro H_i.
rewrite <- ones_early_eq_ones_w_early.
rewrite <- ones_late_eq_ones_w_late.
rewrite <-
(ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b
H_wf H_early); auto.
rewrite <-
(ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b
H_wf H_late); auto.
split.
apply (Zle_trans _ b1_suff _); [ apply Zle_min_r |].
apply Zle_left_rev.
assert (H_aux:
(cg (abs_r a * i + abs_b0 a) - fl (abs_r a * i + abs_b1 a) + - b1_suff =
cg (abs_r a * i + abs_b0 a) + - (fl (abs_r a * i + abs_b1 a) + b1_suff))%Z);
[ ring |].
rewrite H_aux; clear H_aux.
apply Zle_left.
apply Qle_impl_Zle.
apply (Qle_trans _ (abs_r a * i + abs_b0 a) _);
[| eapply cg_def_linear ].
rewrite Zplus_eq_Qplus.
apply (Qle_trans _ ((abs_r a * i + abs_b1 a) + b1_suff) _);
[ apply Qplus_le_compat; [ eapply fl_def | apply Qle_refl ] |].
rewrite <- Qplus_assoc.
apply Qplus_le_compat; [ apply Qle_refl |].
unfold b1_suff.
apply (Qle_trans _ (abs_b1 a + (abs_b0 a - abs_b1 a)) _);
[ apply Qplus_le_compat; [ apply Qle_refl | eapply fl_def ] |].
ring_simplify.
apply Qle_refl.
apply (Zle_trans _ (b2_suff) _); [| apply Zle_max_r ].
apply Zle_left_rev.
assert (H_aux:
(b2_suff + - (cg (abs_r a * i + abs_b0 a) - fl (abs_r a * i + abs_b1 a)) =
b2_suff + fl (abs_r a * i + abs_b1 a) + - (cg (abs_r a * i + abs_b0 a)))%Z);
[ ring | rewrite H_aux; clear H_aux ].
apply Zle_left.
apply Qle_impl_Zle.
apply (Qle_trans _ ((abs_r a * i + abs_b0 a) + 1) _).
apply <- Qle_minus_iff.
assert (H_aux:
abs_r a * i + abs_b0 a + 1 + - cg (abs_r a * i + abs_b0 a) ==
abs_r a * i + abs_b0 a + - (cg (abs_r a * i + abs_b0 a) - 1));
[ ring | rewrite H_aux; clear H_aux ].
apply -> Qle_minus_iff.
apply Qlt_le_weak.
assert (H_aux:
cg (abs_r a * i + abs_b0 a) - 1 ==
(cg (abs_r a * i + abs_b0 a) - 1%Z)%Z).
unfold Zminus.
unfold Qminus.
rewrite Zplus_eq_Qplus.
apply Qplus_eq_compat; [| compute ]; reflexivity.
rewrite H_aux; clear H_aux.
eapply cg_def_linear.
rewrite Zplus_eq_Qplus.
apply (Qle_trans _ (b2_suff + (abs_r a * i + abs_b1 a) - 1) _).
apply <- Qle_minus_iff.
assert (H_aux:
b2_suff + (abs_r a * i + abs_b1 a) - 1 + - (abs_r a * i + abs_b0 a + 1) ==
b2_suff + - ((abs_b0 a - abs_b1 a) + 1 + 1));
[ ring | rewrite H_aux; clear H_aux ].
apply -> Qle_minus_iff.
unfold b2_suff.
apply (Qle_trans _ (abs_b0 a - abs_b1 a + 1 + 1) _);
[ apply Qle_refl | eapply cg_def_linear ].
unfold Qminus.
rewrite <- Qplus_assoc.
apply Qplus_le_compat; [ apply Qle_refl |].
apply <- Qle_minus_iff.
assert (H_aux:
fl (abs_r a * i + abs_b1 a) + - (abs_r a * i + abs_b1 a + - (1)) ==
fl (abs_r a * i + abs_b1 a) + 1 + - (abs_r a * i + abs_b1 a));
[ ring | rewrite H_aux; clear H_aux ].
apply -> Qle_minus_iff.
apply Qlt_le_weak.
eapply fl_def.
intro H_i.
split.
apply (Zle_trans _ b1_pref _); [ apply Zle_min_l |].
apply Zle_left_rev.
assert (H_aux:
(ones (w_late a) i - ones (w_early a) i + - b1_pref =
ones (w_late a) i + - (ones (w_early a) i + b1_pref))%Z);
[ ring | rewrite H_aux; clear H_aux ].
apply Zle_left.
apply (Zle_trans _ (0) _);
[| rewrite <- inj_0;
apply le_impl_Zle;
auto with arith ].
apply Zle_left_rev.
assert (H_aux:
(0 + - (ones (w_early a) i + b1_pref) =
- b1_pref + - (ones (w_early a) i))%Z);
[ ring | rewrite H_aux; clear H_aux ].
apply Zle_left.
apply (Zle_trans _ (i) _); [ apply inj_le; apply ones_i_le_i |].
unfold b1_pref.
rewrite Zopp_involutive.
apply inj_le.
apply lt_le_weak.
exact H_i.
apply (Zle_trans _ b2_pref _); [| apply Zle_max_l ].
apply Zle_left_rev.
assert (H_aux:
(b2_pref + - (ones (w_late a) i - ones (w_early a) i) =
(ones (w_early a) i + - (ones (w_late a) i - b2_pref)))%Z);
[ ring | rewrite H_aux; clear H_aux ].
apply Zle_left.
apply (Zle_trans _ (0) _);
[| rewrite <- inj_0;
apply le_impl_Zle;
auto with arith ].
apply Zle_left_rev.
assert (H_aux:
(0 + - (ones (w_late a) i - b2_pref) =
b2_pref + - (ones (w_late a) i))%Z);
[ ring | rewrite H_aux; clear H_aux ].
apply Zle_left.
apply (Zle_trans _ (i) _); [ apply inj_le; apply ones_i_le_i |].
unfold b2_pref.
apply inj_le.
apply lt_le_weak.
exact H_i.
Qed.
Property sync_abs_refl:
forall a: abstraction_phd,
forall H_swf: strong_well_formed_abstraction_phd a,
forall H_non_empty: non_empty a,
sync_abs a a.
Proof.
intros.
assert (H_wf: well_formed_abstraction_phd a); [ eapply H_swf |].
unfold sync_abs.
intros.
apply sync_sym.
elim (sync_early_late H_swf); auto.
intros b1 H_tmp.
elim H_tmp; clear H_tmp.
intros b2 H_late_early.
unfold sync.
exists b1.
exists (- b1)%Z.
intros.
split.
apply Zle_left_rev.
assert (H_aux:
(ones w2 i - ones w1 i + - b1)%Z = (ones w2 i + - (b1 + ones w1 i))%Z).
ring.
rewrite H_aux; clear H_aux.
apply Zle_left.
apply (Zle_trans
(b1 + ones w1 i)
(ones_late a i)
(ones w2 i)).
2: (apply inj_le; apply ones_late_le_ones_w; auto).
apply Zle_left_rev.
assert (H_aux:
(ones_late a i + - (b1 + ones w1 i))%Z =
(ones_late a i + - b1 + - ones w1 i)%Z).
ring.
rewrite H_aux; clear H_aux.
apply Zle_left.
apply (Zle_trans
(ones w1 i)
(ones_early a i)
(ones_late a i + - b1)).
apply inj_le; apply ones_w_le_ones_early; auto.
apply Zle_left_rev.
assert (H_aux:
(ones_late a i + - b1 + - ones_early a i)%Z =
(ones_late a i - ones_early a i + - b1)%Z).
ring.
rewrite H_aux; clear H_aux.
apply Zle_left.
rewrite ones_early_eq_ones_w_early.
rewrite ones_late_eq_ones_w_late.
destruct (H_late_early i); auto.
apply Zle_left_rev.
assert (H_aux:
(- b1 + - (ones w2 i - ones w1 i))%Z =
(- b1 + ones w1 i + - ones w2 i)%Z).
ring.
rewrite H_aux; clear H_aux.
apply Zle_left.
apply (Zle_trans
(ones w2 i)
(ones_early a i)
(- b1 + ones w1 i)).
apply inj_le; apply ones_w_le_ones_early; auto.
apply Zle_left_rev.
assert (H_aux:
(- b1 + ones w1 i + - ones_early a i)%Z =
(ones w1 i + - (ones_early a i + b1))%Z).
ring.
rewrite H_aux; clear H_aux.
apply Zle_left.
apply (Zle_trans
(ones_early a i + b1)
(ones_late a i)
(ones w1 i)).
2: (apply inj_le; apply ones_late_le_ones_w; auto).
apply Zle_left_rev.
assert (H_aux:
(ones_late a i + - (ones_early a i + b1))%Z =
(ones_late a i - ones_early a i + - b1)%Z).
ring.
rewrite H_aux; clear H_aux.
apply Zle_left.
rewrite ones_early_eq_ones_w_early.
rewrite ones_late_eq_ones_w_late.
destruct (H_late_early i); auto.
Qed.
Property sync_abs_test_correctness:
forall a1 a2: abstraction_phd,
forall H_swf_a1: strong_well_formed_abstraction_phd a1,
forall H_swf_a2: strong_well_formed_abstraction_phd a2,
forall H_sync: sync_abs_test a1 a2,
forall H_non_empty_1: non_empty a1,
forall H_non_empty_2: non_empty a2,
sync_abs a1 a2.
Proof.
intros.
assert (H_wf_a1: well_formed_abstraction_phd a1); [ eapply H_swf_a1 |].
assert (H_wf_a2: well_formed_abstraction_phd a2); [ eapply H_swf_a2 |].
unfold sync_abs_test in H_sync.
unfold sync_abs.
intros.
pose (a :=
absmake
(Qmax (abs_b1 a1) (abs_b1 a2))
(Qmin (abs_b0 a1) (abs_b0 a2))
(abs_r a1)).
assert (H_wf_a: well_formed_abstraction_phd a).
unfold well_formed_abstraction_phd.
simpl.
assumption.
assert (H_swf_a: strong_well_formed_abstraction_phd a).
unfold strong_well_formed_abstraction_phd.
split; [ assumption |].
repeat split.
simpl.
apply (Qle_trans _ (abs_b0 a1) _); [ apply Qle_min_l |].
apply (Qle_trans _ (abs_b1 a1) _); [| apply Qle_max_l ].
eapply H_swf_a1.
simpl.
elim (Qmax_dec (abs_b1 a1) (abs_b1 a2)).
intro H_max.
rewrite H_max.
eapply H_swf_a1.
intro H_max.
rewrite H_max.
rewrite H_sync.
eapply H_swf_a2.
simpl.
elim (Qmin_dec (abs_b0 a1) (abs_b0 a2)).
intro H_min.
rewrite H_min.
eapply H_swf_a1.
intro H_min.
rewrite H_min.
rewrite H_sync.
eapply H_swf_a2.
assert (H_a1_in_a: abs_included_test a1 a).
unfold abs_included_test.
simpl.
repeat split.
unfold Qmax.
case_eq (abs_b1 a1 ?= abs_b1 a2); try solve [intros; apply Qle_refl].
rewrite <- Qlt_alt.
apply Qlt_le_weak.
unfold Qmin.
case_eq (abs_b0 a1 ?= abs_b0 a2); try solve [intros; apply Qle_refl].
rewrite <- Qgt_alt.
apply Qlt_le_weak.
assert (H_a2_in_a: abs_included_test a2 a).
unfold abs_included_test.
simpl.
repeat split.
rewrite H_sync; apply Qeq_refl.
unfold Qmax.
case_eq (abs_b1 a1 ?= abs_b1 a2); try solve [intros; apply Qle_refl].
rewrite <- Qeq_alt.
intro H_cmp; rewrite H_cmp; apply Qle_refl.
rewrite <- Qgt_alt.
apply Qlt_le_weak.
unfold Qmin.
case_eq (abs_b0 a1 ?= abs_b0 a2); try solve [intros; apply Qle_refl].
rewrite <- Qeq_alt.
intro H_cmp; rewrite H_cmp; apply Qle_refl.
rewrite <- Qlt_alt.
apply Qlt_le_weak.
assert (H_w1_in_a: in_abstraction_phd w1 a).
apply (w_in_a1_and_a1_in_a2_impl_w_in_a2 H_wf_a1 H_wf_a H_a1_in_a H_w1_in_a1).
assert (H_w2_in_a: in_abstraction_phd w2 a).
apply (w_in_a1_and_a1_in_a2_impl_w_in_a2 H_wf_a2 H_wf_a H_a2_in_a H_w2_in_a2).
assert (H_non_empty: non_empty a).
unfold non_empty.
exists (w_late a).
apply ones_late_le_ones_early_impl_late_in_a.
intro.
apply (le_trans
(ones_late a i)
(ones_early a1 i)
(ones_early a i)).
apply (le_trans
(ones_late a i)
(ones_late a1 i)
(ones_early a1 i));
try solve [apply non_empty_impl_ones_late_le_ones_early; auto].
induction i.
simpl; auto.
apply le_lt_or_eq in IHi.
destruct IHi.
apply (le_trans
(ones_late a (S i))
(ones_late a1 i)
(ones_late a1 (S i)));
try solve
[ rewrite ones_late_eq_ones_w_late;
rewrite ones_late_eq_ones_w_late;
apply ones_increasing;
auto ].
simpl.
case_eq (abs_r a1 * S i + Qmin (abs_b0 a1) (abs_b0 a2) ?= ones_late a i);
try solve [intro; auto with arith].
simpl.
rewrite H.
destruct (Qmin_dec (abs_b0 a1) (abs_b0 a2));
try solve [rewrite e; apply le_refl].
rewrite e.
case_eq (abs_r a1 * S i + abs_b0 a2 ?= ones_late a1 i);
case_eq (abs_r a1 * S i + abs_b0 a1 ?= ones_late a1 i);
auto with arith.
intros H_cmp1 H_cmp2.
rewrite <- Qeq_alt in H_cmp1.
rewrite <- Qgt_alt in H_cmp2.
rewrite <- H_cmp1 in H_cmp2.
absurd (abs_r a1 * S i + abs_b0 a1 < abs_r a1 * S i + abs_b0 a2); auto.
apply Qle_not_lt.
apply Qplus_le_compat; try solve [apply Qle_refl].
rewrite <- e.
apply Qle_min_l.
intros H_cmp1 H_cmp2.
rewrite <- Qlt_alt in H_cmp1.
rewrite <- Qgt_alt in H_cmp2.
absurd (abs_r a1 * S i + abs_b0 a1 < abs_r a1 * S i + abs_b0 a2);
try solve [
apply (Qlt_trans
(abs_r a1 * S i + abs_b0 a1)
(ones_late a1 i)
(abs_r a1 * S i + abs_b0 a2)); auto ].
apply Qle_not_lt.
apply Qplus_le_compat; try solve [apply Qle_refl].
rewrite <- e.
apply Qle_min_l.
induction i.
simpl; auto.
apply le_lt_or_eq in IHi.
destruct IHi.
apply (le_trans
(ones_early a1 (S i))
(ones_early a i)
(ones_early a (S i)));
try solve
[ rewrite ones_early_eq_ones_w_early;
rewrite ones_early_eq_ones_w_early;
apply ones_increasing;
auto ].
simpl.
case_eq (S (ones_early a1 i) ?= abs_r a1 * S i + abs_b1 a1);
try solve [intro; auto with arith].
simpl.
rewrite H.
destruct (Qmax_dec (abs_b1 a1) (abs_b1 a2));
try solve [rewrite e; apply le_refl].
rewrite e.
case_eq (S (ones_early a i) ?= abs_r a1 * S i + abs_b1 a1);
case_eq (S (ones_early a i) ?= abs_r a1 * S i + abs_b1 a2);
auto with arith.
intros H_cmp1 H_cmp2.
rewrite <- Qgt_alt in H_cmp1.
rewrite <- Qeq_alt in H_cmp2.
absurd (abs_r a1 * S i + abs_b1 a2 < abs_r a1 * S i + abs_b1 a1);
try solve [rewrite <- H_cmp2; assumption].
apply Qle_not_lt.
apply Qplus_le_compat; try solve [apply Qle_refl].
rewrite <- e.
apply Qle_max_l.
intros H_cmp1 H_cmp2.
rewrite <- Qgt_alt in H_cmp1.
rewrite <- Qlt_alt in H_cmp2.
absurd (abs_r a1 * S i + abs_b1 a2 < abs_r a1 * S i + abs_b1 a1);
try solve [
apply (Qlt_trans
(abs_r a1 * S i + abs_b1 a2)
(S (ones_early a i))
(abs_r a1 * S i + abs_b1 a1)); auto ].
apply Qle_not_lt.
apply Qplus_le_compat; try solve [apply Qle_refl].
rewrite <- e.
apply Qle_max_l.
apply (sync_abs_refl H_swf_a H_non_empty H_w1_in_a H_w2_in_a).
Qed.
Require Coq.Logic.Classical.
Property sync_abs_test_completeness:
forall a1 a2: abstraction_phd,
forall H_swf_a1: strong_well_formed_abstraction_phd a1,
forall H_swf_a2: strong_well_formed_abstraction_phd a2,
forall H_non_empty_1: non_empty a1,
forall H_non_empty_2: non_empty a2,
forall H_sync: sync_abs a1 a2,
sync_abs_test a1 a2.
Proof.
intros.
assert (H_wf_a1: well_formed_abstraction_phd a1); [ eapply H_swf_a1 |].
assert (H_wf_a2: well_formed_abstraction_phd a2); [ eapply H_swf_a2 |].
unfold sync_abs_test.
assert (H_early_late: sync (w_early a1) (w_late a2)).
apply H_sync.
apply early_in_abs; assumption.
apply late_in_abs; assumption.
elim H_early_late.
intros k1 H_aux.
elim H_aux; clear H_aux.
intros k2 H_ones_early_late.
elim (exists_i_st_ones_early1_and_ones_late2_eq_r_i_plus_b H_swf_a1 H_swf_a2).
intros i_lim [ H_early H_late ].
elim (Q_dec (abs_r a1) (abs_r a2)); auto.
intro H_aux; elim H_aux; clear H_aux.
intro H_r.
absurd (forall i : nat, (k1 <= ones (w_early a1) i - ones (w_late a2) i <= k2)%Z);
auto.
apply Classical_Pred_Type.ex_not_not_all.
pose (i := (i_lim + Zabs_nat (cg ((k1 + abs_b0 a2 - abs_b1 a1 - 1) / (abs_r a1 - abs_r a2))))%nat).
exists i.
apply Classical_Prop.or_not_and.
left.
apply Zlt_not_le.
rewrite <- ones_early_eq_ones_w_early.
rewrite <- ones_late_eq_ones_w_late.
rewrite <-
(ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b
H_wf_a1 H_early);
[| unfold i; omega ].
rewrite <-
(ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b
H_wf_a2 H_late);
[| unfold i; omega ].
apply Zlt_left_rev.
assert (H_aux:
(k1 + - (fl (abs_r a1 * i + abs_b1 a1) - cg (abs_r a2 * i + abs_b0 a2)) =
k1 + cg (abs_r a2 * i + abs_b0 a2) + - (fl (abs_r a1 * i + abs_b1 a1)))%Z);
[ ring | rewrite H_aux; clear H_aux ].
apply Zlt_left_lt.
apply Qlt_impl_Zlt.
apply (Qle_lt_trans _ (abs_r a1 * i + abs_b1 a1) _);
[ eapply fl_def |].
rewrite Zplus_eq_Qplus.
apply (Qlt_le_trans _ (k1 + (abs_r a2 * i + abs_b0 a2)) _);
[| apply Qplus_le_compat; [ apply Qle_refl | eapply cg_def_linear ] ].
apply <- Qlt_minus_iff.
assert (H_aux:
k1 + (abs_r a2 * i + abs_b0 a2) + - (abs_r a1 * i + abs_b1 a1) ==
((abs_r a2 - abs_r a1) * i + - -(k1 + abs_b0 a2 - abs_b1 a1)));
[ ring | rewrite H_aux; clear H_aux ].
apply -> Qlt_minus_iff.
unfold i.
pose (x := (cg ((k1 + abs_b0 a2 - abs_b1 a1 - 1) / (abs_r a1 - abs_r a2)))%Z).
fold x.
fold x in i.
unfold Q_of_nat.
rewrite inj_plus.
rewrite Zplus_eq_Qplus.
assert (H_aux:
(abs_r a2 - abs_r a1) *
(i_lim + Zabs_nat x)
==
(abs_r a2 - abs_r a1) * i_lim +
((abs_r a2 - abs_r a1) * Zabs_nat x));
[ ring | rewrite H_aux; clear H_aux ].
apply
(Qlt_le_trans _
((abs_r a2 - abs_r a1) * Zabs_nat x)
_).
apply
(Qlt_le_trans _
((abs_r a2 - abs_r a1) * x)
_).
unfold x.
apply
(Qlt_le_trans _
((abs_r a2 - abs_r a1) * ((k1 + abs_b0 a2 - abs_b1 a1 - 1) / (abs_r a1 - abs_r a2)))
_).
assert (H_aux:
(abs_r a2 - abs_r a1) * ((k1 + abs_b0 a2 - abs_b1 a1 - 1) / (abs_r a1 - abs_r a2)) ==
- ((abs_r a1 - abs_r a2) * ((k1 + abs_b0 a2 - abs_b1 a1 - 1) / (abs_r a1 - abs_r a2))));
[ ring | rewrite H_aux; clear H_aux ].
rewrite Qmult_div_r.
apply <- Qlt_minus_iff.
assert (H_aux:
- (k1 + abs_b0 a2 - abs_b1 a1 - 1) + - - (k1 + abs_b0 a2 - abs_b1 a1) ==
(1));
[ ring | rewrite H_aux; clear H_aux ].
apply Zlt_impl_Qlt.
auto with arith zarith.
apply Qlt_not_eq.
apply <- Qlt_minus_iff.
assert (H_aux:
0 + - (abs_r a1 - abs_r a2) ==
abs_r a2 + - abs_r a1);
[ ring | rewrite H_aux; clear H_aux ].
apply -> Qlt_minus_iff.
assumption.
apply Qmult_le_compat_l.
eapply cg_def_linear.
unfold Qminus.
apply -> Qle_minus_iff.
apply Qlt_le_weak.
assumption.
apply Qmult_le_compat_l.
unfold Q_of_nat.
rewrite inj_Zabs_nat.
elim (Zabs_dec x).
intro H_x.
rewrite H_x.
rewrite Zabs_involutive.
apply Qle_refl.
intro H_x.
rewrite H_x.
rewrite Zabs_Zopp.
rewrite Zabs_involutive.
apply Zle_impl_Qle.
apply (Zle_trans _ 0 _).
apply Zle_left_rev.
ring_simplify.
apply Zabs_pos.
apply Zabs_pos.
unfold Qminus.
apply -> Qle_minus_iff.
apply Qlt_le_weak.
assumption.
rewrite <- (Qplus_0_l ((abs_r a2 - abs_r a1) * Zabs_nat x)) at 1.
apply Qplus_le_compat; [| apply Qle_refl].
apply Qmult_le_0_compat.
unfold Qminus.
apply -> Qle_minus_iff.
apply Qlt_le_weak.
assumption.
apply Zle_impl_Qle.
rewrite <- inj_0.
apply inj_le.
auto with arith.
intro H_r.
absurd (forall i : nat, (k1 <= ones (w_early a1) i - ones (w_late a2) i <= k2)%Z);
auto.
apply Classical_Pred_Type.ex_not_not_all.
pose (x := fl ((abs_b0 a2 - abs_b1 a1 + k2 + 1 + 1) / (abs_r a1 - abs_r a2) + 1)).
pose (i := (i_lim + Zabs_nat x)%nat).
exists i.
apply Classical_Prop.or_not_and.
right.
apply Zlt_not_le.
rewrite <- ones_early_eq_ones_w_early.
rewrite <- ones_late_eq_ones_w_late.
rewrite <-
(ones_early_eq_r_i_plus_b_impl_ones_early_eq_r_i'_plus_b
H_wf_a1 H_early);
[| unfold i; omega ].
rewrite <-
(ones_late_eq_r_i_plus_b_impl_ones_late_eq_r_i'_plus_b
H_wf_a2 H_late);
[| unfold i; omega ].
apply Zlt_left_rev.
assert (H_aux:
(fl (abs_r a1 * i + abs_b1 a1) - cg (abs_r a2 * i + abs_b0 a2) + - k2 =
fl (abs_r a1 * i + abs_b1 a1) + - (cg (abs_r a2 * i + abs_b0 a2) + k2))%Z);
[ ring | rewrite H_aux; clear H_aux ].
apply Zlt_left_lt.
apply Qlt_impl_Zlt.
apply (Qle_lt_trans _ (abs_r a1 * i + abs_b1 a1 - 1) _).
2: apply <- Qlt_minus_iff.
2: assert (H_aux:
fl (abs_r a1 * i + abs_b1 a1) + - (abs_r a1 * i + abs_b1 a1 - 1) ==
fl (abs_r a1 * i + abs_b1 a1) + 1 + - (abs_r a1 * i + abs_b1 a1));
[ ring | rewrite H_aux; clear H_aux ].
2: apply -> Qlt_minus_iff.
2: eapply fl_def.
rewrite Zplus_eq_Qplus.
apply (Qle_trans _ ((abs_r a2 * i + abs_b0 a2) + k2 + 1) _).
1: apply <- Qle_minus_iff.
1: assert (H_aux:
abs_r a2 * i + abs_b0 a2 + k2 + 1 + - (cg (abs_r a2 * i + abs_b0 a2) + k2) ==
abs_r a2 * i + abs_b0 a2 + k2 + - (cg (abs_r a2 * i + abs_b0 a2) + k2 - 1));
[ ring | rewrite H_aux; clear H_aux ].
1: apply -> Qle_minus_iff.
1: unfold Qminus.
1: rewrite <- (Zplus_eq_Qplus (cg (abs_r a2 * i + abs_b0 a2)) k2).
1: rewrite <- (Zplus_eq_Qplus (cg (abs_r a2 * i + abs_b0 a2) + k2)%Z (- (1))).
1: unfold Q_of_nat.
1: rewrite <- cg_plus_int_rewrite.
1: apply Qlt_le_weak.
1: eapply cg_def_linear.
apply <- Qle_minus_iff.
assert (H_aux:
abs_r a1 * i + abs_b1 a1 - 1 + - (abs_r a2 * i + abs_b0 a2 + k2 + 1) ==
(abs_r a1 - abs_r a2) * i + - (abs_b0 a2 - abs_b1 a1 + k2 + 1 + 1));
[ ring | rewrite H_aux; clear H_aux ].
apply -> Qle_minus_iff.
unfold i.
unfold Q_of_nat.
rewrite inj_plus.
rewrite Zplus_eq_Qplus.
assert (H_aux:
(abs_r a1 - abs_r a2) * (i_lim + Zabs_nat x)
==
(abs_r a1 - abs_r a2) * i_lim + ((abs_r a1 - abs_r a2) * Zabs_nat x));
[ ring | rewrite H_aux; clear H_aux ].
apply
(Qle_trans _
((abs_r a1 - abs_r a2) * Zabs_nat x)
_).
apply
(Qle_trans _
((abs_r a1 - abs_r a2) * x)
_).
unfold x.
pose (x' := ((abs_b0 a2 - abs_b1 a1 + k2 + 1 + 1) / (abs_r a1 - abs_r a2) + 1)).
fold x'.
apply
(Qle_trans _
((abs_r a1 - abs_r a2) * (x' - 1))
_).
unfold x'.
assert (H_aux:
(abs_r a1 - abs_r a2) * ((abs_b0 a2 - abs_b1 a1 + k2 + 1 + 1) / (abs_r a1 - abs_r a2) + 1 - 1) ==
(abs_r a1 - abs_r a2) * ((abs_b0 a2 - abs_b1 a1 + k2 + 1 + 1) / (abs_r a1 - abs_r a2)));
[ ring | rewrite H_aux; clear H_aux ].
rewrite Qmult_div_r.
apply Qle_refl.
apply Qnot_eq_sym.
apply Qlt_not_eq.
unfold Qminus.
apply -> Qlt_minus_iff.
assumption.
apply Qmult_le_compat_l.
apply <- Qle_minus_iff.
assert (H_aux: fl x' + - (x' - 1) == fl x' + 1 + - x');
[ ring | rewrite H_aux; clear H_aux ].
apply -> Qle_minus_iff.
apply Qlt_le_weak.
eapply fl_def.
unfold Qminus.
apply -> Qle_minus_iff.
apply Qlt_le_weak.
assumption.
apply Qmult_le_compat_l.
unfold Q_of_nat.
rewrite inj_Zabs_nat.
elim (Zabs_dec x).
intro H_x.
rewrite H_x.
rewrite Zabs_involutive.
apply Qle_refl.
intro H_x.
rewrite H_x.
rewrite Zabs_Zopp.
rewrite Zabs_involutive.
apply Zle_impl_Qle.
apply (Zle_trans _ 0 _).
apply Zle_left_rev.
ring_simplify.
apply Zabs_pos.
apply Zabs_pos.
unfold Qminus.
apply -> Qle_minus_iff.
apply Qlt_le_weak.
assumption.
rewrite <- (Qplus_0_l ((abs_r a1 - abs_r a2) * Zabs_nat x)) at 1.
apply Qplus_le_compat; [| apply Qle_refl].
apply Qmult_le_0_compat.
unfold Qminus.
apply -> Qle_minus_iff.
apply Qlt_le_weak.
assumption.
apply Zle_impl_Qle.
rewrite <- inj_0.
apply inj_le.
auto with arith.
Qed.
Property sync_abs_sym:
forall a1 a2: abstraction_phd,
sync_abs a1 a2 -> sync_abs a2 a1.
Proof.
intros a1 a2 H_sync.
unfold sync_abs.
intros w2 w1 H_w2_in_a2 H_w1_in_a1.
apply sync_sym.
apply H_sync; auto.
Qed.
Property sync_abs_trans:
forall a1 a2 a3: abstraction_phd,
forall H_swf_a1: strong_well_formed_abstraction_phd a1,
forall H_swf_a2: strong_well_formed_abstraction_phd a2,
forall H_swf_a3: strong_well_formed_abstraction_phd a3,
forall H_non_empty_1: non_empty a1,
forall H_non_empty_2: non_empty a2,
forall H_non_empty_3: non_empty a3,
forall H_sync12: sync_abs a1 a2,
forall H_sync23: sync_abs a2 a3,
sync_abs a1 a3.
Proof.
intros.
apply sync_abs_test_correctness; auto.
unfold sync_abs_test.
generalize (sync_abs_test_completeness H_swf_a2 H_swf_a3 H_non_empty_2 H_non_empty_3 H_sync23).
generalize (sync_abs_test_completeness H_swf_a1 H_swf_a2 H_non_empty_1 H_non_empty_2 H_sync12).
apply (Qeq_trans (abs_r a1) (abs_r a2) (abs_r a3)); auto.
Qed.
End sync_properties.
Section adaptability_properties.
Property adaptability_abs_impl_adaptability_abs_alt:
forall a1 a2: abstraction_phd,
forall H_sub: adaptability_abs a1 a2,
adaptability_abs_alt a1 a2.
Proof.
intros.
unfold adaptability_abs_alt.
unfold adaptability_abs in H_sub.
split.
unfold prec_abs.
intros.
unfold adaptability in H_sub.
destruct (H_sub w1 w2 H_w1_in_a1 H_w2_in_a2).
assumption.
unfold sync_abs.
intros.
unfold adaptability in H_sub.
destruct (H_sub w1 w2 H_w1_in_a1 H_w2_in_a2).
assumption.
Qed.
Property adaptability_abs_alt_impl_adaptability_abs:
forall a1 a2: abstraction_phd,
forall H_sub: adaptability_abs_alt a1 a2,
adaptability_abs a1 a2.
Proof.
intros.
unfold adaptability_abs.
unfold adaptability_abs_alt in H_sub.
elim H_sub; intros H_prec H_sync.
intros.
split.
apply H_prec; auto.
apply H_sync; auto.
Qed.
End adaptability_properties.
Section size_properties.
Lemma subtype_impl_a2_b0_le_a1_b1:
forall a1 a2: abstraction_phd,
forall H_swf_a1: strong_well_formed_abstraction_phd a1,
forall H_swf_a2: strong_well_formed_abstraction_phd a2,
forall H_non_empty_1: non_empty a1,
forall H_non_empty_2: non_empty a2,
forall H_sub: prec_abs a1 a2 /\ abs_r a1 == abs_r a2,
0 <= abs_b1 a1 - abs_b0 a2.
Proof.
intros.
destruct H_sub as [ H_prec H_sync ].
elim (exists_i_st_ones_early1_and_ones_late2_eq_r_i_plus_b H_swf_a1 H_swf_a2).
intros i [H_early1 H_late2].
rewrite <- H_sync in H_late2.
apply (Qle_trans _ (ones_early a1 i - ones_late a2 i)%Z _).
apply Zle_impl_Qle.
rewrite ones_early_eq_ones_w_early.
rewrite ones_late_eq_ones_w_late.
apply Zle_left.
unfold prec_abs in H_prec.
unfold prec in H_prec.
unfold ge in H_prec.
apply inj_le.
apply H_prec.
destruct H_swf_a1 as [ H_wf_a1 _ ].
apply early_in_abs; auto.
destruct H_swf_a2 as [ H_wf_a2 _ ].
apply late_in_abs; auto.
rewrite <- H_early1.
rewrite <- H_late2.
apply
(Qle_trans _ (fl ((abs_r a1 * i + abs_b1 a1) - (abs_r a1 * i + abs_b0 a2)))%Z _);
try solve [ apply Zle_impl_Qle; apply fl_minus_cg_le_fl ].
apply (Qle_trans _ (abs_r a1 * i + abs_b1 a1 - (abs_r a1 * i + abs_b0 a2)) _);
try solve [ eapply fl_def ].
assert (H_aux:
(abs_r a1 * i + abs_b1 a1 - (abs_r a1 * i + abs_b0 a2)) ==
(abs_b1 a1 - abs_b0 a2)); try ring.
rewrite H_aux; clear H_aux.
apply Qle_refl.
Qed.
Lemma size_early1_late2_le_size_abs_aux:
forall a1 a2: abstraction_phd,
forall H_wf_a1: well_formed_abstraction_phd a1,
forall H_wf_a2: well_formed_abstraction_phd a2,
forall H_sub: prec_abs a1 a2 /\ abs_r a1 == abs_r a2,
forall i: nat,
((fl (abs_r a1 * i + abs_b1 a1)) -
(cg (abs_r a2 * i + abs_b0 a2)) <= size_abs a1 a2)%Z.
Proof.
intros.
unfold size_abs.
apply
(Zle_trans _
(fl ((abs_r a1 * i + abs_b1 a1) - (abs_r a2 * i + abs_b0 a2)))
_).
apply fl_minus_cg_le_fl.
apply fl_monotone_linear.
destruct H_sub as [ H_prec H_sync ].
rewrite <- H_sync.
assert (H_aux:
abs_r a1 * i + abs_b1 a1 - (abs_r a1 * i + abs_b0 a2) ==
abs_b1 a1 - abs_b0 a2); try ring.
rewrite H_aux; clear H_aux.
apply Qle_refl.
Qed.
Lemma size_early1_late2_le_size_abs:
forall a1 a2: abstraction_phd,
forall H_swf_a1: strong_well_formed_abstraction_phd a1,
forall H_swf_a2: strong_well_formed_abstraction_phd a2,
forall H_non_empty_1: non_empty a1,
forall H_non_empty_2: non_empty a2,
forall H_sub: prec_abs a1 a2 /\ abs_r a1 == abs_r a2,
forall i: nat,
(sizei (w_early a1) (w_late a2) i <= size_abs a1 a2)%Z.
Proof.
intros.
destruct H_sub as [ H_prec H_sync ].
assert (H_wf_a1: well_formed_abstraction_phd a1);
try solve [ eapply H_swf_a1 ].
assert (H_wf_a2: well_formed_abstraction_phd a2);
try solve [ eapply H_swf_a2 ].
assert (H_early1_prec_late2: prec (w_early a1) (w_late a2)).
apply H_prec.
apply early_in_abs; auto.
apply late_in_abs; auto.
unfold prec in H_early1_prec_late2.
assert (H_early1_prec_late2_i: (ones (w_early a1) i >= ones (w_late a2) i)%nat).
apply H_early1_prec_late2.
clear H_early1_prec_late2.
apply inj_le in H_early1_prec_late2_i.
unfold sizei, size_abs.
rewrite <- ones_early_eq_ones_w_early in *.
rewrite <- ones_late_eq_ones_w_late in *.
rewrite ones_early_eq_ones_early_alt in *; eauto.
rewrite ones_late_eq_ones_late_alt in *; auto.
rewrite ones_early_alt_remove_Zabs_nat in *.
rewrite ones_late_alt_remove_Zabs_nat in *.
elim (Zmax_spec 0%nat (Zmin i (fl (abs_r a1 * i + abs_b1 a1)))).
intros [H_early_1 H_aux].
rewrite H_aux in *; clear H_aux.
elim (Zmax_spec 0%nat (Zmin i ((cg (abs_r a2 * i + abs_b0 a2))))).
intros [H_late_1 H_aux].
rewrite H_aux in *; clear H_aux.
apply
(Zle_trans
(O - O)%Z
(fl 0)
(fl (abs_b1 a1 - abs_b0 a2)));
try solve [ compute; congruence ].
apply fl_monotone_linear.
apply subtype_impl_a2_b0_le_a1_b1; auto.
intros [H_late_1 H_aux].
rewrite H_aux in *; clear H_aux.
apply
(Zle_trans
(O - Zmin i (cg (abs_r a2 * i + abs_b0 a2)))%Z
(0)
(fl (abs_b1 a1 - abs_b0 a2))).
apply Zle_left_rev.
replace (0 + - (O - Zmin i (cg (abs_r a2 * i + abs_b0 a2))))%Z
with (Zmin i (cg (abs_r a2 * i + abs_b0 a2)))%Z by ring.
apply Zlt_le_weak.
exact H_late_1.
replace 0%Z with (fl 0); try solve [ compute; reflexivity ].
apply fl_monotone_linear.
apply subtype_impl_a2_b0_le_a1_b1; auto.
intros [H_early_1 H_aux].
rewrite H_aux in *; clear H_aux.
elim (Zmax_spec 0%nat (Zmin i ((cg (abs_r a2 * i + abs_b0 a2))))).
intros [H_late_1 H_aux].
rewrite H_aux in *; clear H_aux.
apply
(Zle_trans
(Zmin i (fl (abs_r a1 * i + abs_b1 a1)) - O)%Z
((fl (abs_r a1 * i + abs_b1 a1)) - (cg (abs_r a2 * i + abs_b0 a2)))
(fl (abs_b1 a1 - abs_b0 a2)));
try solve
[ apply size_early1_late2_le_size_abs_aux; auto;
split; auto ].
elim (Zmin_spec i (fl (abs_r a1 * i + abs_b1 a1))).
intros [H_early_1' H_aux].
rewrite H_aux in *; clear H_aux.
apply
(Zle_trans _
(fl (abs_r a1 * i + abs_b1 a1))
_);
try solve
[ replace (Zminus (Z_of_nat i) (Z_of_nat O))
with (Z_of_nat i) by ring;
assumption ].
apply Zle_left_rev.
replace (fl (abs_r a1 * i + abs_b1 a1) - cg (abs_r a2 * i + abs_b0 a2) +
- fl (abs_r a1 * i + abs_b1 a1))%Z
with (- cg (abs_r a2 * i + abs_b0 a2))%Z by ring.
elim (Zmin_spec i (cg (abs_r a2 * i + abs_b0 a2))).
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
contradiction H_late_1.
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
replace (- cg (abs_r a2 * i + abs_b0 a2))%Z
with (0 + - cg (abs_r a2 * i + abs_b0 a2))%Z by ring.
apply Zle_left.
apply Zge_le.
assumption.
intros [H_early_1' H_aux].
rewrite H_aux in *; clear H_aux.
apply Zle_left_rev.
replace (fl (abs_r a1 * i + abs_b1 a1) - cg (abs_r a2 * i + abs_b0 a2) +
- (fl (abs_r a1 * i + abs_b1 a1) - O))%Z
with (0 + - cg (abs_r a2 * i + abs_b0 a2))%Z by ring.
apply Zle_left.
elim (Zmin_spec i (cg (abs_r a2 * i + abs_b0 a2))).
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
omega.
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
replace (- cg (abs_r a2 * i + abs_b0 a2))%Z
with (0 + - cg (abs_r a2 * i + abs_b0 a2))%Z by ring.
apply Zge_le.
assumption.
intros [H_late_1 H_aux].
rewrite H_aux in *; clear H_aux.
elim (Zmin_spec i (fl (abs_r a1 * i + abs_b1 a1))).
intros [H_early_1' H_aux].
rewrite H_aux in *; clear H_aux.
elim (Zmin_spec i (cg (abs_r a2 * i + abs_b0 a2))).
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
ring_simplify.
replace 0%Z with (fl 0); try solve [ compute; reflexivity ].
apply fl_monotone_linear.
apply subtype_impl_a2_b0_le_a1_b1; auto.
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
apply
(Zle_trans _
((fl (abs_r a1 * i + abs_b1 a1)) - (cg (abs_r a2 * i + abs_b0 a2)))
_);
try solve
[ apply size_early1_late2_le_size_abs_aux; auto;
split; auto ].
omega.
intros [H_early_1' H_aux].
rewrite H_aux in *; clear H_aux.
elim (Zmin_spec i (cg (abs_r a2 * i + abs_b0 a2))).
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
omega.
intros [H_late_1' H_aux].
rewrite H_aux in *; clear H_aux.
apply
(Zle_trans _
((fl (abs_r a1 * i + abs_b1 a1)) - (cg (abs_r a2 * i + abs_b0 a2)))
_);
try solve
[ apply size_early1_late2_le_size_abs_aux; auto;
split; auto ].
omega.
Qed.
Property size_abs_correctness_aux:
forall (w1:ibw) (w2:ibw),
forall a1 a2: abstraction_phd,
forall H_swf_a1: strong_well_formed_abstraction_phd a1,
forall H_swf_a2: strong_well_formed_abstraction_phd a2,
forall H_non_empty_1: non_empty a1,
forall H_non_empty_2: non_empty a2,
forall (H_a1_eq_abs_w1: in_abstraction_phd w1 a1),
forall (H_a2_eq_abs_w2: in_abstraction_phd w2 a2),
forall H_sub: prec_abs a1 a2 /\ abs_r a1 == abs_r a2,
forall s,
forall H_size: size w1 w2 s,
(s <= size_abs a1 a2)%Z.
Proof.
intros.
assert (H_wf_a1: well_formed_abstraction_phd a1);
try solve [ eapply H_swf_a1 ].
assert (H_wf_a2: well_formed_abstraction_phd a2);
try solve [ eapply H_swf_a2 ].
unfold size in H_size.
destruct H_size as [ H_size_le_s H_size_eq_s ].
elim H_size_eq_s.
intros i H_sizei.
rewrite <- H_sizei.
apply
(Zle_trans
(sizei w1 w2 i)
(sizei (w_early a1) (w_late a2) i)
(size_abs a1 a2));
try solve [ apply size_early1_late2_le_size_abs; auto ].
unfold sizei.
apply Zle_left_rev.
replace (ones (w_early a1) i - ones (w_late a2) i + - (ones w1 i - ones w2 i))%Z
with (ones (w_early a1) i - ones w1 i + - (ones (w_late a2) i - ones w2 i))%Z by ring.
apply Zle_left.
apply
(Zle_trans
(ones (w_late a2) i - ones w2 i)
0
(ones (w_early a1) i - ones w1 i)).
apply Zle_left_rev.
replace (0 + - (ones (w_late a2) i - ones w2 i))%Z
with (ones w2 i - ones (w_late a2) i)%Z by ring.
apply Zle_left.
apply inj_le.
rewrite <- ones_late_eq_ones_w_late.
apply ones_late_le_ones_w; auto.
apply Zle_left.
rewrite <- ones_early_eq_ones_w_early.
apply inj_le.
apply ones_w_le_ones_early; auto.
Qed.
End size_properties.