Library abstraction_hfl_prim_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_hfl_prim_def.
Require Import abstraction_hfl_prim_aux.
Remark absh_weakening:
forall a1 a2: abstractionh,
forall H_one: absh_b1 a1 <= absh_b1 a2,
forall H_absh_b0: absh_b0 a1 >= absh_b0 a2,
forall H_r: absh_r a1 == absh_r a2,
absh_included_test a1 a2.
Proof.
apply absh_weakening_aux.
Qed.
Property early_def:
forall a:abstractionh,
forall H_wf: well_formed_abstractionh a,
(forall w: ibw,
(forall i, w i = true -> ones w i <= absh_r a * i + absh_b1 a) ->
prec (w_early a) w)
/\
(forall w_min:ibw,
(forall w: ibw,
(forall i, w i = true -> ones w i <= absh_r a * i + absh_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) ?= absh_r a * S i + absh_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') ?= absh_r a * S i' + absh_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:abstractionh,
forall H_wf: well_formed_abstractionh a,
(forall w: ibw,
(forall i, (i > 0)%nat ->
w i = false -> ones w i >= absh_r a * i + absh_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) >= absh_r a * i + absh_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 (absh_r a * S i + absh_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 (absh_r a * S i' + absh_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: abstractionh,
forall H_wf_a: well_formed_abstractionh a,
in_abstractionh 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: abstractionh,
forall H_wf_a: well_formed_abstractionh a,
in_abstractionh 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: abstractionh,
forall H_wf: well_formed_abstractionh 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: abstractionh,
prec (w_early a) (w_late a) -> in_abstractionh (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: abstractionh,
prec (w_early a) (w_late a) -> in_abstractionh (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: abstractionh,
prec (w_early a) (w_late a) ->
(in_abstractionh (w_early a) a /\ in_abstractionh (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: abstractionh,
forall H_wf: well_formed_abstractionh 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: abstractionh,
forall H_wf: well_formed_abstractionh a,
prec (w_early a) (w_late a) ->
(forall w:ibw, in_abstractionh w a -> prec (w_early a) w)
/\
(forall w_min: ibw, (forall w, in_abstractionh 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_abstractionh (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: abstractionh,
forall H_wf: well_formed_abstractionh a,
prec (w_early a) (w_late a) ->
(forall w:ibw, in_abstractionh w a -> prec w (w_late a))
/\
(forall w_maj: ibw, (forall w:ibw, in_abstractionh 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_abstractionh (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: abstractionh,
forall H_wf: well_formed_abstractionh a,
prec (w_early a) (w_late a) ->
(non_empty a)
/\
((forall w:ibw, in_abstractionh w a -> prec (w_early a) w)
/\
(forall w_min: ibw, (forall w, in_abstractionh w a -> prec w_min w) -> prec w_min (w_early a)))
/\
((forall w:ibw, in_abstractionh w a -> prec w (w_late a))
/\
(forall w_maj: ibw, (forall w:ibw, in_abstractionh 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: abstractionh,
forall H_wf: well_formed_abstractionh 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: abstractionh,
forall H_wf: well_formed_abstractionh 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_abstractionh 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 absh_included_test_correctness:
forall a1 a2: abstractionh,
absh_included_test a1 a2 -> absh_included a1 a2.
Proof.
apply absh_included_test_impl_absh_included.
Qed.
Property on_absh_correctness:
forall (w1:ibw) (w2:ibw),
forall (a1:abstractionh) (a2:abstractionh),
forall H_wf_a1: well_formed_abstractionh a1,
forall H_wf_a2: well_formed_abstractionh a2,
forall H_a1_eq_absh_w1: in_abstractionh w1 a1,
forall H_a2_eq_absh_w2: in_abstractionh w2 a2,
in_abstractionh (on w1 w2) (on_absh a1 a2).
Proof.
apply on_absh_correctness_aux.
Qed.
Property not_absh_correctness:
forall w: ibw,
forall a:abstractionh,
forall H_wf_a: well_formed_abstractionh a,
forall H_a_eq_absh_w: in_abstractionh w a,
in_abstractionh (not w) (not_absh a).
Proof.
apply not_absh_correctness_aux.
Qed.
Property prec_absh_equiv_prec_absh_alt:
forall a1 a2: abstractionh,
forall H_wf1: well_formed_abstractionh a1,
forall H_wf2: well_formed_abstractionh a2,
forall H_non_empty1: non_empty a1,
forall H_non_empty2: non_empty a2,
prec_absh a1 a2 <-> prec_absh_alt a1 a2.
Proof.
intros.
split; intros.
apply prec_absh_alt_complet; auto.
apply prec_absh_alt_correctness; auto.
Qed.
Property prec_absh_test_correctness:
forall a1 a2: abstractionh,
forall H_wf1: well_formed_abstractionh a1,
forall H_wf2: well_formed_abstractionh a2,
sync_absh_test a1 a2 -> prec_absh_test a1 a2 -> prec_absh a1 a2.
Proof.
intros.
apply prec_absh_test_correctness_aux; auto.
Qed.
Property subtyping_absh_equiv_subtyping_absh_alt:
forall a1 a2: abstractionh,
subtyping_absh_alt a1 a2 <-> subtyping_absh a1 a2.
Proof.
intros.
split; intros.
apply subtyping_absh_alt_impl_subtyping_absh; auto.
apply subtyping_absh_impl_subtyping_absh_alt; auto.
Qed.