Library abstraction_jfla_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_jfla_def.
Require Import abstraction_jfla_aux.
Remark absj_weakening:
forall a1 a2: abstractionj,
forall H_one: absj_b1 a1 <= absj_b1 a2,
forall H_absj_b0: absj_b0 a1 >= absj_b0 a2,
forall H_r: absj_r a1 == absj_r a2,
absj_included_test a1 a2.
Proof.
apply absj_weakening_aux.
Qed.
Property early_def:
forall a:abstractionj,
forall H_wf: well_formed_abstractionj a,
(forall w: ibw,
(forall i, w i = true -> ones w (pred i) < absj_r a * i + absj_b1 a) ->
prec (w_early a) w)
/\
(forall w_min:ibw,
(forall w: ibw,
(forall i, w i = true -> ones w (pred i) < absj_r a * i + absj_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_absurd in H.
rewrite <- ones_early_eq_ones_w_early in H.
simpl.
rewrite Qlt_alt in H.
rewrite H.
rewrite S_n_nbeq_n.
auto.
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 (ones_early a i' ?= absj_r a * S i' + absj_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 <- Qlt_alt in H_cmp.
assumption.
Qed.
Property late_def:
forall a:abstractionj,
forall H_wf: well_formed_abstractionj a,
(forall w: ibw,
(forall i, (i > 0)%nat ->
w i = false -> ones w (pred i) >= absj_r a * i + absj_b0 a) ->
prec w (w_late a))
/\
(forall w_maj:ibw,
(forall w: ibw,
(forall i, (i > 0)%nat ->
w i = false -> ones w (pred i) >= absj_r a * i + absj_b0 a) ->
prec w w_maj)->
prec (w_late a) w_maj).
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_absurd in H.
rewrite <- ones_late_eq_ones_w_late in H.
simpl.
rewrite Qle_alt in H.
case_eq (absj_r a * S i + absj_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 (absj_r a * S i' + absj_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: abstractionj,
forall H_wf_a: well_formed_abstractionj a,
in_abstractionj 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: abstractionj,
forall H_wf_a: well_formed_abstractionj a,
in_abstractionj 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: abstractionj,
forall H_wf: well_formed_abstractionj 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: abstractionj,
prec (w_early a) (w_late a) -> in_abstractionj (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: abstractionj,
prec (w_early a) (w_late a) -> in_abstractionj (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: abstractionj,
prec (w_early a) (w_late a) ->
(in_abstractionj (w_early a) a /\ in_abstractionj (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: abstractionj,
forall H_wf: well_formed_abstractionj 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.
Lemma early_is_infimum:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj a,
prec (w_early a) (w_late a) ->
(forall w:ibw, in_abstractionj w a -> prec (w_early a) w)
/\
(forall w_min: ibw, (forall w, in_abstractionj 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_abstractionj (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: abstractionj,
forall H_wf: well_formed_abstractionj a,
prec (w_early a) (w_late a) ->
(forall w:ibw, in_abstractionj w a -> prec w (w_late a))
/\
(forall w_maj: ibw, (forall w:ibw, in_abstractionj 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_abstractionj (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.
Property early_prec_late_impl_non_empty_and_early_is_infimum_and_late_is_supremum:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj a,
prec (w_early a) (w_late a) ->
(non_empty a)
/\
((forall w:ibw, in_abstractionj w a -> prec (w_early a) w)
/\
(forall w_min: ibw, (forall w, in_abstractionj w a -> prec w_min w) -> prec w_min (w_early a)))
/\
((forall w:ibw, in_abstractionj w a -> prec w (w_late a))
/\
(forall w_maj: ibw, (forall w:ibw, in_abstractionj w a -> prec w w_maj) -> prec (w_late a) w_maj)).
Proof.
intros.
split.
apply early_prec_late_impl_non_empty; auto.
split.
apply early_is_infimum; auto.
apply late_is_supremum; auto.
Qed.
Property non_empty_equiv_early_prec_late:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj 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.
Property ones_early_alt_correctness:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj a,
forall i,
ones_early a i = ones_early_alt a i.
Proof.
apply ones_early_eq_ones_early_alt.
Qed.
Property non_empty_test_correctness:
forall a,
forall H_wf: well_formed_abstractionj 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 absj_included_test_correctness:
forall a1 a2: abstractionj,
absj_included_test a1 a2 -> absj_included a1 a2.
Proof.
apply absj_included_test_impl_absj_included.
Qed.
Property on_absj_alt_correctness:
forall (w1:ibw) (w2:ibw),
forall (a1:abstractionj) (a2:abstractionj),
forall H_wf_a1: well_formed_abstractionj a1,
forall H_wf_a2: well_formed_abstractionj a2,
forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
forall H_wf_b1_1: Qden (absj_b1 a1) = Qden (absj_r a1),
forall H_wf_b1_2: Qden (absj_b1 a2) = Qden (absj_r a2),
in_abstractionj (on w1 w2) (on_absj_alt a1 a2).
Proof.
apply on_absj_alt_correctness_aux.
Qed.
Property on_absj_correctness:
forall w1 w2:ibw,
forall a1 a2:abstractionj,
forall H_wf_a1: well_formed_abstractionj a1,
forall H_wf_a2: well_formed_abstractionj a2,
forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
in_abstractionj (on w1 w2) (on_absj a1 a2).
Proof.
apply on_absj_correctness_aux.
Qed.
Property not_absj_correctness:
forall w: ibw,
forall a:abstractionj,
forall H_wf_a: well_formed_abstractionj a,
forall H_a_eq_absj_w: in_abstractionj w a,
forall H_wf_b1: Qden (absj_b1 a) = Qden (absj_r a),
in_abstractionj (not w) (not_absj a).
Proof.
apply not_absj_correctness_aux.
Qed.
Property prec_absj_equiv_prec_absj_alt:
forall a1 a2: abstractionj,
forall H_wf1: well_formed_abstractionj a1,
forall H_wf2: well_formed_abstractionj a2,
forall H_non_empty1: non_empty a1,
forall H_non_empty2: non_empty a2,
prec_absj a1 a2 <-> prec_absj_alt a1 a2.
Proof.
intros.
split; intros.
apply prec_absj_alt_complet; auto.
apply prec_absj_alt_correctness; auto.
Qed.
Property prec_absj_test_correctness:
forall a1 a2: abstractionj,
forall H_wf1: well_formed_abstractionj a1,
forall H_wf2: well_formed_abstractionj a2,
sync_absj_test a1 a2 -> prec_absj_test a1 a2 -> prec_absj a1 a2.
Proof.
intros.
apply prec_absj_test_correctness_aux; auto.
Qed.