Library abstraction_phd_prop
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.
Require Import abstraction_phd_aux.
Remark abs_weakening:
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.
apply abs_weakening_aux.
Qed.
Property early_def:
forall a:abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
(forall w: ibw,
(forall i, w i = true -> ones w i <= abs_r a * i + abs_b1 a) ->
prec (w_early a) w)
/\
(forall w_min:ibw,
(forall w: ibw,
(forall i, w i = true -> ones w i <= abs_r a * i + abs_b1 a) ->
prec w_min w) ->
prec w_min (w_early a)).
Proof.
intros a H_wf.
split.
intros w H_ones_w.
unfold prec.
induction i.
simpl; auto.
case_eq (w (S i)).
intro H_w.
rewrite (ones_S_i_eq_S_ones_i w); auto.
case_eq (w_early a (S i)).
intro H_w_early.
rewrite ones_S_i_eq_S_ones_i; auto.
apply plus_le_compat_l.
assumption.
intro H_w_early.
rewrite ones_S_i_eq_ones_i; auto.
simpl.
apply lt_le_S.
apply (le_lt_eq_dec) in IHi.
elim IHi; clear IHi; auto.
intro H_absurd.
rewrite H_absurd in *.
assert (w_early a (S i) = true).
pose (H:= H_ones_w (S i) H_w).
simpl in H.
rewrite H_w in H.
simpl in H.
rewrite H_absurd in H.
rewrite <- ones_early_eq_ones_w_early in H.
simpl.
rewrite Qle_alt in H.
case_eq (S (ones_early a i) ?= abs_r a * S i + abs_b1 a);
try solve [ intro H_cmp; rewrite S_n_nbeq_n; simpl; reflexivity ].
intro H_cmp.
rewrite H_cmp in H.
congruence.
congruence.
intro H_w.
rewrite (ones_S_i_eq_ones_i w); auto.
case_eq (w_early a (S i)).
intro H_w_early.
rewrite ones_S_i_eq_S_ones_i; simpl; auto.
intro H_w_early.
rewrite ones_S_i_eq_ones_i; auto.
intros w_min H_w_min.
apply (H_w_min (w_early a)).
intros i H_w_early.
rewrite <- ones_early_eq_ones_w_early.
case_eq i.
intro H_i;
rewrite H_i in *.
simpl in *.
congruence.
intros i' H_i; rewrite H_i in *.
simpl.
simpl in H_w_early.
case_eq (S (ones_early a i') ?= abs_r a * S i' + abs_b1 a);
try solve [
intro H_cmp; rewrite H_cmp in H_w_early;
rewrite <- beq_nat_refl in H_w_early; simpl in H_w_early; congruence ].
intro H_cmp.
rewrite <- Qeq_alt in H_cmp.
rewrite H_cmp; auto.
apply Qle_refl.
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
apply Qlt_le_weak.
assumption.
Qed.
Property late_def:
forall a:abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
(forall w: ibw,
(forall i, (i > 0)%nat ->
w i = false -> ones w i >= abs_r a * i + abs_b0 a) ->
prec w (w_late a))
/\
(forall w_mah:ibw,
(forall w: ibw,
(forall i, (i > 0)%nat ->
w i = false -> ones w (pred i) >= abs_r a * i + abs_b0 a) ->
prec w w_mah)->
prec (w_late a) w_mah).
Proof.
intros a H_wf.
split.
intros w H_ones_w.
unfold prec.
induction i.
simpl; auto.
case_eq (w (S i)).
intro H_w.
rewrite (ones_S_i_eq_S_ones_i w); auto.
case_eq (w_late a (S i)).
intro H_w_late.
rewrite ones_S_i_eq_S_ones_i; auto.
apply plus_le_compat_l.
assumption.
intro H_w_late.
rewrite ones_S_i_eq_ones_i; auto.
simpl.
change (ones (w_late a) i <= S (ones w i))%nat.
apply (le_trans
(ones (w_late a) i)
(ones w i)
(S (ones w i))); auto.
intro H_w.
rewrite (ones_S_i_eq_ones_i w); auto.
case_eq (w_late a (S i)).
intro H_w_late.
rewrite ones_S_i_eq_S_ones_i; simpl; auto.
apply (le_lt_eq_dec) in IHi.
elim IHi; clear IHi; auto.
intro H_absurd.
rewrite H_absurd in *.
assert (w_late a (S i) = false).
assert (H_S_i_ge_0: (S i > 0)%nat); auto with arith.
pose (H:= H_ones_w (S i) H_S_i_ge_0 H_w).
simpl in H.
rewrite H_w in H.
simpl in H.
rewrite <- H_absurd in H.
rewrite <- ones_late_eq_ones_w_late in H.
simpl.
rewrite Qle_alt in H.
case_eq (abs_r a * S i + abs_b0 a ?= ones_late a i); try congruence;
intro H_cmp; rewrite <- beq_nat_refl; auto.
congruence.
intro H_w_late.
rewrite ones_S_i_eq_ones_i; auto.
intros w_maj H_w_maj.
apply (H_w_maj (w_late a)).
intros i H_i_ge_0 H_w_late.
rewrite <- ones_late_eq_ones_w_late.
case_eq i.
intro H_i;
rewrite H_i in *.
absurd ((0 > 0)%nat); auto with arith.
intros i' H_i; rewrite H_i in *.
simpl.
simpl in H_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.
apply Qle_refl.
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
apply Qlt_le_weak.
assumption.
intro H_cmp; rewrite H_cmp in H_w_late.
rewrite S_n_nbeq_n in H_w_late; simpl in H_w_late; congruence.
Qed.
Property early_prec_w:
forall w: ibw,
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
in_abstraction_phd w a -> prec (w_early a) w.
Proof.
intros w a H_wf_a H_w_in_a.
unfold prec.
intros i.
rewrite <- ones_early_eq_ones_w_early.
apply ones_w_le_ones_early; auto.
Qed.
Property w_prec_late:
forall w: ibw,
forall a: abstraction_phd,
forall H_wf_a: well_formed_abstraction_phd a,
in_abstraction_phd w a -> prec w (w_late a).
Proof.
intros w a H_wf_a H_w_in_a.
unfold prec.
intros i.
rewrite <- ones_late_eq_ones_w_late.
apply ones_late_le_ones_w; auto.
Qed.
Property non_empty_impl_early_prec_late:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
non_empty a -> prec (w_early a) (w_late a).
Proof.
intros a H_wf H_non_empty.
unfold prec.
intros i.
rewrite <- ones_early_eq_ones_w_early.
rewrite <- ones_late_eq_ones_w_late.
apply non_empty_impl_ones_late_le_ones_early; auto.
Qed.
Lemma early_prec_late_impl_early_in_a:
forall a: abstraction_phd,
prec (w_early a) (w_late a) -> in_abstraction_phd (w_early a) a.
Proof.
intros a H_prec.
unfold prec in H_prec.
apply ones_late_le_ones_early_impl_early_in_a.
intros.
rewrite ones_early_eq_ones_w_early.
rewrite ones_late_eq_ones_w_late.
exact (H_prec i).
Qed.
Lemma early_prec_late_impl_late_in_a:
forall a: abstraction_phd,
prec (w_early a) (w_late a) -> in_abstraction_phd (w_late a) a.
Proof.
intros a H_prec.
unfold prec in H_prec.
apply ones_late_le_ones_early_impl_late_in_a.
intros.
rewrite ones_early_eq_ones_w_early.
rewrite ones_late_eq_ones_w_late.
exact (H_prec i).
Qed.
Lemma early_prec_late_impl_early_late_in_a:
forall a: abstraction_phd,
prec (w_early a) (w_late a) ->
(in_abstraction_phd (w_early a) a /\ in_abstraction_phd (w_late a) a).
Proof.
intros.
split.
apply early_prec_late_impl_early_in_a; auto.
apply early_prec_late_impl_late_in_a; auto.
Qed.
Property early_prec_late_impl_non_empty:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
prec (w_early a) (w_late a) -> non_empty a.
Proof.
intros a H_wf H_prec.
unfold prec in H_prec.
apply ones_late_le_ones_early_impl_non_empty; auto.
intro i.
rewrite ones_early_eq_ones_w_early.
rewrite ones_late_eq_ones_w_late.
exact (H_prec i).
Qed.
Property non_empty_equiv_early_prec_late:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
non_empty a <-> prec (w_early a) (w_late a).
Proof.
intros.
split.
apply non_empty_impl_early_prec_late; auto.
apply early_prec_late_impl_non_empty; auto.
Qed.
Lemma early_is_infimum:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
prec (w_early a) (w_late a) ->
(forall w:ibw, in_abstraction_phd w a -> prec (w_early a) w)
/\
(forall w_min: ibw, (forall w, in_abstraction_phd w a -> prec w_min w) -> prec w_min (w_early a)).
Proof.
intros a H_wf H_prec.
split; intros H.
apply early_prec_w; auto.
assert (H_early_in_a: in_abstraction_phd (w_early a) a).
apply early_prec_late_impl_early_in_a; auto.
intros H1.
exact (H1 (w_early a) H_early_in_a).
Qed.
Lemma late_is_supremum:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
prec (w_early a) (w_late a) ->
(forall w:ibw, in_abstraction_phd w a -> prec w (w_late a))
/\
(forall w_maj: ibw, (forall w:ibw, in_abstraction_phd w a -> prec w w_maj) -> prec (w_late a) w_maj).
Proof.
intros a H_wf H_prec.
split; intros H.
apply w_prec_late; auto.
assert (H_late_in_a: in_abstraction_phd (w_late a) a).
apply early_prec_late_impl_late_in_a; auto.
intros H1.
exact (H1 (w_late a) H_late_in_a).
Qed.
Lemma early_is_minimum:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
non_empty a ->
(forall w:ibw, in_abstraction_phd w a -> prec (w_early a) w)
/\
(in_abstraction_phd (w_early a) a).
Proof.
intros a H_wf H_non_empty.
split.
intros w H_w_in_a.
apply early_prec_w; auto.
apply early_in_abs; auto.
Qed.
Lemma late_is_maximum:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
non_empty a ->
(forall w:ibw, in_abstraction_phd w a -> prec w (w_late a))
/\
(in_abstraction_phd (w_late a) a).
Proof.
intros a H_wf H_non_empty.
split.
intros w H_w_in_a.
apply w_prec_late; auto.
apply late_in_abs; auto.
Qed.
Property ones_early_alt_correctness:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall i,
ones_early a i = ones_early_alt a i.
Proof.
apply ones_early_eq_ones_early_alt.
Qed.
Property ones_late_alt_correctness:
forall a: abstraction_phd,
forall H_wf: well_formed_abstraction_phd a,
forall i,
ones_late a i = ones_late_alt a i.
Proof.
apply ones_late_eq_ones_late_alt.
Qed.
Property non_empty_test_correctness:
forall a,
forall H_wf: well_formed_abstraction_phd a,
forall H_non_empty: non_empty_test a,
non_empty a.
Proof.
intros.
apply ones_late_le_ones_early_impl_non_empty; auto.
intros.
apply non_empty_test_impl_ones_late_le_ones_early; auto.
Qed.
Property abs_included_test_correctness:
forall a1 a2: abstraction_phd,
abs_included_test a1 a2 -> abs_included a1 a2.
Proof.
apply abs_included_test_impl_abs_included.
Qed.
Property on_abs_correctness:
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.
apply on_abs_correctness_aux.
Qed.
Property not_abs_correctness:
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.
apply not_abs_correctness_aux.
Qed.
Property prec_abs_equiv_prec_abs_alt:
forall a1 a2: abstraction_phd,
forall H_wf1: well_formed_abstraction_phd a1,
forall H_wf2: well_formed_abstraction_phd a2,
forall H_non_empty1: non_empty a1,
forall H_non_empty2: non_empty a2,
prec_abs a1 a2 <-> prec_abs_alt a1 a2.
Proof.
intros.
split; intros.
apply prec_abs_alt_complet; auto.
apply prec_abs_alt_correctness; auto.
Qed.
Property prec_abs_test_correctness:
forall a1 a2: abstraction_phd,
forall H_wf1: well_formed_abstraction_phd a1,
forall H_wf2: well_formed_abstraction_phd a2,
sync_abs_test a1 a2 -> prec_abs_test a1 a2 -> prec_abs a1 a2.
Proof.
intros.
apply prec_abs_test_correctness_aux; auto.
Qed.
Property sync_abs_equiv_sync_abs_test:
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,
sync_abs a1 a2 <-> sync_abs_test a1 a2.
Proof.
intros.
split; intros.
apply sync_abs_test_completeness; assumption.
apply sync_abs_test_correctness; assumption.
Qed.
Property adaptability_abs_equiv_adaptability_abs_alt:
forall a1 a2: abstraction_phd,
adaptability_abs_alt a1 a2 <-> adaptability_abs a1 a2.
Proof.
intros.
split; intros.
apply adaptability_abs_alt_impl_adaptability_abs; auto.
apply adaptability_abs_impl_adaptability_abs_alt; auto.
Qed.
Property adaptability_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_non_empty_1: non_empty a1,
forall H_non_empty_2: non_empty a2,
adaptability_abs_test a1 a2 -> adaptability_abs a1 a2.
Proof.
intros a1 a2 H_swf_a1 H_swf_a2 H_non_empty_1 H_non_empty_2 H_adap_test.
destruct H_adap_test as [ H_prec_test H_sync_test].
rewrite <- adaptability_abs_equiv_adaptability_abs_alt.
split.
apply prec_abs_test_correctness; auto; [ apply H_swf_a1 | apply H_swf_a2 ].
apply sync_abs_test_correctness; auto.
Qed.
Property size_abs_correctness:
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: adaptability_abs a1 a2,
forall s,
forall H_size: size w1 w2 s,
(s <= size_abs a1 a2)%Z.
Proof.
intros.
apply
(size_abs_correctness_aux
H_swf_a1 H_swf_a2
H_non_empty_1 H_non_empty_2
H_a1_eq_abs_w1 H_a2_eq_abs_w2);
auto.
apply adaptability_abs_impl_adaptability_abs_alt in H_sub.
destruct H_sub as [ H_prec H_sync ].
split; [assumption|].
apply sync_abs_test_completeness; assumption.
Qed.