Library abstraction_hfl_prim_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_hfl_prim_def.
Section Abstractionh_def.
Definition absh_equal (a1: abstractionh) (a2:abstractionh) :=
(absh_r a1 == absh_r a2) /\
(absh_b1 a1) == (absh_b1 a2) /\
(absh_b0 a1) == (absh_b0 a2).
Instance absh_equal_is_equiv : Equivalence _ absh_equal.
Proof.
constructor ; unfold absh_equal ; red ; intuition.
transitivity (absh_r y) ; auto.
transitivity (absh_b1 y) ; auto.
transitivity (absh_b0 y) ; auto.
Qed.
End Abstractionh_def.
Definition absh_equiv (a1: abstractionh) (a2:abstractionh) :=
absh_included a1 a2 /\ absh_included a2 a1.
Definition absh_equiv_test (a1: abstractionh) (a2:abstractionh) :=
absh_included_test a1 a2 /\ absh_included_test a2 a1.
Section abstraction_equivalence_properties.
Property absh_included_test_impl_absh_included:
forall a1 a2: abstractionh,
forall H_a1_in_test_a2: absh_included_test a1 a2,
absh_included a1 a2.
Proof.
intros.
unfold absh_included.
intros.
unfold in_abstractionh.
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)
(absh_r a1 * i + absh_b1 a1)
(absh_r a1 * i + absh_b1 a2)); auto.
apply Qplus_le_compat; auto.
apply Qle_refl.
intro H_w.
apply
(Qle_trans
(absh_r a1 * i + absh_b0 a2)
(absh_r a1 * i + absh_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_abstractionh a1,
forall H_wf_a2: well_formed_abstractionh a2,
forall H_a1_in_a2: absh_included_test a1 a2,
forall H_w_in_a1: in_abstractionh w a1,
in_abstractionh w a2.
Proof.
intros.
unfold in_abstractionh.
intros i H_i_ge_1.
split.
intro H_w.
unfold in_abstractionh 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)
(absh_r a1 * i + absh_b1 a1)
(absh_r a1 * i + absh_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_abstractionh 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
(absh_r a1 * i + absh_b0 a2)
(absh_r a1 * i + absh_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 absh_weakening_aux:
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.
intros.
unfold absh_included_test.
repeat split; auto.
Qed.
Property absh_weakening_0:
forall a1 a2: abstractionh,
forall H_absh_b01: absh_b0 a1 > 0,
forall H_r: absh_r a1 == absh_r a2,
forall H_one: absh_b1 a1 == absh_b1 a2,
forall H_absh_b02: absh_b0 a2 == 0,
absh_included_test a1 a2.
Proof.
intros.
eapply absh_weakening_aux; auto.
rewrite H_one.
apply Qle_refl.
rewrite H_absh_b02.
eapply Qlt_le_weak.
assumption.
Qed.
Property absh_equal_sym:
forall a1 a2: abstractionh,
forall H_a1_eq_a2: absh_equal a1 a2,
absh_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 absh_equal_impl_absh_included_test:
forall a1 a2: abstractionh,
forall H_a1_eq_a2: absh_equal a1 a2,
absh_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 absh_equal_impl_absh_equiv_test:
forall a1 a2: abstractionh,
forall H_a1_eq_a2: absh_equal a1 a2,
absh_equiv_test a1 a2.
Proof.
intros.
split.
apply absh_equal_impl_absh_included_test; auto.
apply absh_equal_impl_absh_included_test; auto.
apply absh_equal_sym.
assumption.
Qed.
Property absh_equiv_test_impl_absh_equal:
forall a1 a2: abstractionh,
forall H_a1_eq_a2: absh_equiv_test a1 a2,
absh_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_absh_b11_le_absh_b12 H_absh_b02_le_absh_b01.
elim H_tmp2; clear H_tmp2.
intros H_r' H_tmp'.
elim H_tmp'; clear H_tmp' H_r'.
intros H_absh_b12_le_absh_b11 H_absh_b01_le_absh_b02.
repeat split.
trivial.
apply Qle_antisym; assumption.
apply Qle_antisym; assumption.
Qed.
Property absh_equal_correctness:
forall a1 a2: abstractionh,
forall H_wf1: well_formed_abstractionh a1,
forall H_wf2: well_formed_abstractionh a2,
forall w: ibw,
forall H_w_in_a1: in_abstractionh w a1,
forall H_eq: absh_equal a1 a2,
in_abstractionh w a2.
Proof.
intros.
apply absh_equal_impl_absh_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_abstractionh_absh_equal_compat:
forall a1 a2: abstractionh,
forall H_eq: absh_equal a1 a2,
forall H_wf1: well_formed_abstractionh a1,
well_formed_abstractionh a2.
Proof.
intros.
destruct H_eq as [H_r [H_b1 H_b0]].
unfold well_formed_abstractionh in *.
rewrite <- H_r.
assumption.
Qed.
End abstraction_equivalence_properties.
Fixpoint ones_early_opt (a:abstractionh) (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') (absh_r a * i + absh_b1 a) with
| Lt | Eq => Some (S ones_i')
| Gt =>
match Qcompare (absh_r a * i + absh_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| _ => None
end
end
end
end.
Fixpoint ones_late_opt (a:abstractionh) (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 (absh_r a * i + absh_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| Gt =>
match Qcompare (S ones_i') (absh_r a * i + absh_b1 a) with
| Lt | Eq => Some (S ones_i')
| Gt => None
end
end
end
end.
Definition non_empty_alt (a: abstractionh) :=
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') ?= absh_r a * S i' + absh_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 absh_r a * (S i') + absh_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') (absh_r a * S i' + absh_b1 a) with
| Lt | Eq => Some (S ones_i')
| Gt =>
match Qcompare (absh_r a * S i' + absh_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 (absh_r a * S i' + absh_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| Gt =>
match Qcompare (S ones_i') (absh_r a * S i' + absh_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:abstractionh,
forall i,
((Z_of_nat (ones_early_alt a i))%Z =
Zmax O (Zmin i (fl (absh_r a * i + absh_b1 a))))%Z.
Proof.
intros.
unfold ones_early_alt.
rewrite inj_Zabs_nat.
elim (Zabs_spec (Zmax O (Zmin i (fl (absh_r a * i + absh_b1 a))))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
elim (Zmax_spec O (Zmin i (fl (absh_r a * i + absh_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:abstractionh,
forall i,
((Z_of_nat (ones_late_alt a i))%Z =
Zmax O (Zmin i (cg (absh_r a * i + absh_b0 a))))%Z.
Proof.
intros.
unfold ones_late_alt.
rewrite inj_Zabs_nat.
elim (Zabs_spec (Zmax O (Zmin i (cg (absh_r a * i + absh_b0 a))))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
elim (Zmax_spec O (Zmin i (cg (absh_r a * i + absh_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: abstractionh,
well_formed_ones (ones_early a).
Proof.
intros.
split.
simpl.
reflexivity.
intro.
simpl.
case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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: abstractionh,
well_formed_ones (ones_late a).
Proof.
intros.
split.
simpl.
reflexivity.
intro.
simpl.
case_eq (absh_r a * S i + absh_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: abstractionh,
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 ?= absh_r a * 1%nat + absh_b1 a);
intros;
simpl;
reflexivity.
assert (H_aux:
(ones_early a (S (S i'))
=
match S (ones_early a (S i')) ?= absh_r a * (S (S i')) + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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: abstractionh,
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 (absh_r a * 1%nat + absh_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 absh_r a * S (S i') + absh_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 (absh_r a * S (S i') + absh_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: abstractionh,
forall H_wf: well_formed_abstractionh 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 (absh_r a * O%nat + absh_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 (absh_r a * 0%nat + absh_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 (absh_r a * S i + absh_b1 a)))).
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (fl (absh_r a * (S i) + absh_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 (absh_r a * S i + absh_b1 a))
(fl (absh_r a * i + absh_b1 a))); auto.
apply Zle_ge.
apply fl_monotone_linear.
assert (H_aux:
absh_r a * i + absh_b1 a ==
absh_r a * i + absh_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b1 a ==
absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
(fl (absh_r a * i + absh_b1 a))); auto.
apply fl_monotone_linear.
assert (H_aux:
absh_r a * i + absh_b1 a ==
absh_r a * i + absh_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b1 a ==
absh_r a * i + absh_b1 a + absh_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) > absh_r a * S i + absh_b1 a).
clear H0; clear H2.
rewrite H_cc_aux1.
apply (Qlt_le_trans
(absh_r a * S i + absh_b1 a)
(fl (absh_r a * S i + absh_b1 a) + 1)
1).
destruct (fl_def (absh_r a * S i + absh_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) ?= absh_r a * S i + absh_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) > absh_r a * S i + absh_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) < absh_r a * S i + absh_b1 a); auto.
apply Qle_not_lt.
apply Qlt_le_weak.
assumption.
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (fl (absh_r a * (S i) + absh_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 (absh_r a * i + absh_b1 a) + 1%nat)).
apply inj_lt.
auto with arith.
rewrite <- fl_plus_int_rewrite.
apply (Zle_trans
(S i)
(fl (absh_r a * S i + absh_b1 a))
(fl (absh_r a * i + absh_b1 a + 1))); auto.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b1 a ==
absh_r a * i + absh_b1 a + absh_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) <= absh_r a * S i + absh_b1 a).
rewrite H_cc_aux1.
apply (Qle_trans
(S i)
(fl (absh_r a * S i + absh_b1 a))
(absh_r a * S i + absh_b1 a));
try solve [ elim (fl_def (absh_r a * S i + absh_b1 a)); auto ].
apply Zle_impl_Qle.
assumption.
rewrite red_ones_early.
case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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) <= absh_r a * S i + absh_b1 a).
rewrite Qle_alt.
case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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))
(absh_r a * S i + absh_b1 a)
(fl (absh_r a * S i + absh_b1 a) + 1)); auto.
elim (fl_def (absh_r a * S i + absh_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:
absh_r a * (i + 1) + absh_b1 a ==
absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
(fl (absh_r a * i + absh_b1 a) + 1%nat)); auto.
rewrite <- fl_plus_int_rewrite.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b1 a ==
absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
(fl (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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) > absh_r a * S i + absh_b1 a).
rewrite Qgt_alt.
case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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:
absh_r a * i + absh_b1 a ==
absh_r a * i + absh_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b1 a ==
absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
(fl (absh_r a * i + absh_b1 a) + 1%nat)); auto.
rewrite <- fl_plus_int_rewrite.
apply fl_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b1 a ==
absh_r a * i + absh_b1 a + absh_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 (absh_r a * S i + absh_b1 a))
(fl (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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 (absh_r a * S i + absh_b1 a))
(absh_r a * S i + absh_b1 a)
(ones_early_alt a i + 1%nat)%Z); auto.
elim (fl_def (absh_r a * S i + absh_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: abstractionh,
forall H_wf: well_formed_abstractionh 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 (absh_r a * O%nat + absh_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 (absh_r a * 0%nat + absh_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 (absh_r a * S i + absh_b0 a)))).
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (absh_r a * (S i) + absh_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 (absh_r a * S i + absh_b0 a))
(cg (absh_r a * i + absh_b0 a))); auto.
apply Zle_ge.
apply cg_monotone_linear.
assert (H_aux:
absh_r a * i + absh_b0 a ==
absh_r a * i + absh_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
(cg (absh_r a * i + absh_b0 a))); auto.
apply cg_monotone_linear.
assert (H_aux:
absh_r a * i + absh_b0 a ==
absh_r a * i + absh_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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: absh_r a * S i + absh_b0 a <= ones_late a i).
clear H0; clear H2.
rewrite H_cc_aux1.
apply (Qle_trans
(absh_r a * S i + absh_b0 a)
(cg(absh_r a * S i + absh_b0 a))
0).
destruct (cg_def_linear (absh_r a * S i + absh_b0 a)); assumption.
apply Zle_impl_Qle.
apply Zge_le.
assumption.
rewrite red_ones_late.
case_eq (absh_r a * S i + absh_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 < absh_r a * S i + absh_b0 a); auto.
apply Qle_not_lt.
assumption.
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (absh_r a * (S i) + absh_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 (absh_r a * i + absh_b0 a) + 1)).
apply inj_lt.
auto with arith.
rewrite <- cg_plus_int_rewrite.
apply (Zle_trans
(S i)
(cg (absh_r a * S i + absh_b0 a))
(cg (absh_r a * i + absh_b0 a + 1))); auto.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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: absh_r a * S i + absh_b0 a > ones_late a i).
rewrite H_cc_aux1.
apply (Qle_lt_trans
i
(cg (absh_r a * S i + absh_b0 a) - 1)%Z
(absh_r a * S i + absh_b0 a));
try solve [ elim (cg_def_linear (absh_r a * S i + absh_b0 a));
intros; assumption ].
assert (H_aux:
(cg (absh_r a * S i + absh_b0 a) - 1%nat) ==
(cg (absh_r a * S i + absh_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 (absh_r a * S i + absh_b0 a) + - (1) + - i ==
cg (absh_r a * S i + absh_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: absh_r a * S i + absh_b0 a > ones_late a i).
rewrite Qlt_alt.
case_eq (absh_r a * S i + absh_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)
(absh_r a * S i + absh_b0 a)
(cg (absh_r a * S i + absh_b0 a))); auto.
elim (cg_def_linear (absh_r a * S i + absh_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:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
(cg (absh_r a * i + absh_b0 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
(cg (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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: absh_r a * S i + absh_b0 a <= ones_late a i).
rewrite Qge_alt.
case_eq (absh_r a * S i + absh_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 < absh_r a * S i + absh_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:
absh_r a * i + absh_b0 a ==
absh_r a * i + absh_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
(cg (absh_r a * i + absh_b0 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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 (absh_r a * S i + absh_b0 a))
(cg (absh_r a * i + absh_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: absh_r a * S i == S i * absh_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) <= (absh_r a * S i + absh_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) ?= absh_r a * S i + absh_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) > (absh_r a * S i + absh_b1 a).
Proof.
intros.
simpl in H_w.
case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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: abstractionh,
forall H_wf_a: well_formed_abstractionh a,
forall H_w_in_a: in_abstractionh 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 ?= absh_r a * 1%nat + absh_b1 a);
try solve [ intros; apply le_refl ].
intros H_cmp.
rewrite <- Qgt_alt in H_cmp.
absurd (absh_r a * 1 + absh_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 ?= absh_r a * 1%nat + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_b1 a);
try omega.
intro H_cmp'.
rewrite <- Qgt_alt in H_cmp'.
absurd (absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_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')) ?= absh_r a * S (S i') + absh_b1 a);
omega.
Qed.
Property ones_late_le_ones_w:
forall w: ibw,
forall a: abstractionh,
forall H_wf_a: well_formed_abstractionh a,
forall H_w_in_a: in_abstractionh 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 (absh_r a * 1%nat + absh_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 (absh_r a * 1%nat + absh_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 < absh_r a * 1 + absh_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 (absh_r a * S (S i') + absh_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 (absh_r a * S (S i') + absh_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'))
(absh_r a * S (S i') + absh_b0 a)
(ones w (S i')));
try solve [ exact H_cmp ].
unfold in_abstractionh 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: abstractionh,
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) ?= absh_r a * S i + absh_b1 a);
try reflexivity.
intro H_cmp.
case_eq (absh_r a * S i + absh_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: abstractionh,
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 (absh_r a * S i + absh_b0 a ?= ones_late a i);
try reflexivity.
intro H_cmp.
case_eq (S (ones_late a i) ?= absh_r a * S i + absh_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: abstractionh,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
forall H_absh_b1_lt_absh_b0: absh_b1 a - absh_b0 a < 1,
forall i,
ones_late a i = ones_early a i.
Proof.
induction i.
simpl.
reflexivity.
simpl.
case_eq (absh_r a * S i + absh_b0 a ?= ones_late a i).
intros H_cmp_zero.
rewrite IHi.
case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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 (absh_r a * S i + absh_b1 a == absh_r a * S i + absh_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:
absh_b0 a + 1 + - absh_b1 a == 1 + - (absh_b1 a - absh_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) < absh_r a * S i + absh_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:
absh_b0 a + 1 + - absh_b1 a == 1 + - (absh_b1 a - absh_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) ?= absh_r a * S i + absh_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 == absh_r a * S i + absh_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 (absh_r a * S i + absh_b0 a < absh_r a * S i + absh_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:
absh_b0 a + - (absh_b1 a + - (1)) == 1 + - (absh_b1 a - absh_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
intros H_cmp_one.
rewrite <- Qlt_alt in *.
absurd (absh_r a * S i + absh_b0 a < absh_r a * S i + absh_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:
absh_b0 a + - (absh_b1 a + - (1)) == 1 + - (absh_b1 a - absh_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
rewrite IHi in H_cmp_zero.
apply
(Qlt_trans
(absh_r a * S i + absh_b0 a)
(ones_early a i)
(absh_r a * S i + absh_b1 a - 1)); auto.
apply -> (Qlt_plus 1%nat).
rewrite Qplus_comm.
rewrite n_plus_1_eq_S_n.
assert (H_aux:
1 + (absh_r a * S i + absh_b1 a - 1) == absh_r a * S i + absh_b1 a).
ring.
rewrite H_aux; clear H_aux.
assumption.
reflexivity.
intros H_cmp_zero.
rewrite IHi.
case_eq (S (ones_early a i) ?= absh_r a * S i + absh_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: abstractionh,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
in_abstractionh (w_early a) a.
Proof.
intros.
unfold in_abstractionh.
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: (absh_r a * S i' + absh_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 (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 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
(absh_r a * S i' + absh_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 (absh_b1 a - absh_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
(absh_r a * S (S i'') + absh_b0 a)
(absh_r a * S (S i'') + (absh_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:
absh_b1 a - 1 + - absh_b0 a == absh_b1 a - absh_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'') + - (absh_r a * S (S i'') + (absh_b1 a - 1)) ==
ones_early a (S i'') + 1 + - (absh_r a * S (S i'') + absh_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: abstractionh,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
in_abstractionh (w_late a) a.
Proof.
intros.
unfold in_abstractionh.
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 (absh_r a * S i' + absh_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') ?= absh_r a * S i' + absh_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'))
(absh_r a * S i' + absh_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 (absh_b1 a - absh_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'))
(absh_r a * S i' + absh_b0 a + 1)
(absh_r a * S i' + absh_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:
absh_b1 a + - (absh_b0 a + 1) == absh_b1 a - absh_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 (absh_r a * S i' + absh_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: abstractionh,
forall H_wf: well_formed_abstractionh 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: abstractionh,
forall H_wf: well_formed_abstractionh a,
forall H_non_empty: non_empty a,
in_abstractionh (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: abstractionh,
forall H_wf: well_formed_abstractionh a,
forall H_non_empty: non_empty a,
in_abstractionh (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_abstractionh a1,
forall H_wf_a2: well_formed_abstractionh a2,
absh_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_abstractionh a1,
forall H_wf_a2: well_formed_abstractionh a2,
absh_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.
End early_and_late_properties.
Lemma ones_late_le_ones_early_impl_non_empty:
forall a,
forall H_wf: well_formed_abstractionh 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_abstractionh 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 (absh_r a * i + absh_b1 a) =
fl (Qred (absh_r a * i + absh_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
(absh_r a * i + absh_b0 a)
(absh_r a * i + (absh_b1 a - (1 - (1 # Qden (Qred (absh_r a * i + absh_b1 a))))))
(Qred (absh_r a * i + absh_b1 a) - (1 - (1 # Qden (Qred (absh_r a * i + absh_b1 a)))))).
apply Qplus_le_compat; try solve [ apply Qle_refl ].
apply
(Qle_trans
(absh_b0 a)
(absh_b1 a - (1 - (1 # Qden (absh_r a))))
(absh_b1 a - (1 - (1 # Qden (Qred (absh_r a * i + absh_b1 a)))))).
apply <- Qle_minus_iff.
assert (H_aux:
absh_b1 a - (1 - (1 # Qden (absh_r a))) + - absh_b0 a ==
absh_b1 a - absh_b0 a + - (1 - (1 # Qden (absh_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: abstractionh,
forall H_a1_eq_a2: absh_equal a1 a2,
forall H_non_empty1: non_empty_test a1,
forall H_den:
1 # Qden (absh_b1 a1) * Qden (absh_r a1) <=
1 # Qden (absh_b1 a2) * Qden (absh_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 (absh_b1 a2) * Qden (absh_r a2)))
(1 - (1 # Qden (absh_b1 a1) * Qden (absh_r a1)))
(absh_b1 a2 - absh_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: abstractionh,
absh_equal a (absh_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_abstractionh 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 := absh_std a).
assert (H_a_eq_a_std: absh_equal a a_std).
apply abs_equal_abs_std_non_empty.
assert (H_wf_std: well_formed_abstractionh a_std).
apply (well_formed_abstractionh_absh_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.
Lemma on_w1_w2_le_on_a1_a2:
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),
forall i,
forall H_i_ge_1: (i >= 1)%nat,
forall (H_on: on w1 w2 i = true),
ones (on w1 w2) i <=
(absh_r a1 * absh_r a2) * i + (absh_b1 a1 * absh_r a2 + absh_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 <= absh_r a1 * i + absh_b1 a1).
unfold in_abstractionh in H_a1_eq_absh_w1.
generalize (H_a1_eq_absh_w1 i H_i_ge_1).
clear H_a1_eq_absh_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) <= (absh_r a2 * ones w1 i + absh_b1 a2)).
unfold in_abstractionh in H_a2_eq_absh_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_absh_w2 (ones w1 i) H_ones_w1_ge_1).
clear H_a2_eq_absh_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))
(absh_r a2 * ones w1 i + absh_b1 a2)
(absh_r a1 * absh_r a2 * i + (absh_b1 a1 * absh_r a2 + absh_b1 a2))
H_w2_le_a2).
assert (H_aux:
absh_r a1 * absh_r a2 * i + (absh_b1 a1 * absh_r a2 + absh_b1 a2) ==
(absh_r a1 * absh_r a2 * i + absh_b1 a1 * absh_r a2) + absh_b1 a2).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
assert (H_aux:
absh_r a1 * absh_r a2 * i + absh_b1 a1 * absh_r a2 ==
(absh_r a1 * i + absh_b1 a1) * absh_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 absh_b0_neg_impl_ones_ge_a:
forall (w:ibw) (a:abstractionh),
forall H_wf_a: well_formed_abstractionh a,
forall H_flo: absh_b0 a <= 0,
forall H_a_eq_absh_w: in_abstractionh w a,
forall i:nat,
ones w i >= absh_r a * i + absh_b0 a.
Proof.
induction i.
assert (H_aux: absh_r a * 0 == 0).
ring.
rewrite H_aux; clear H_aux.
assert (H_aux: 0 + absh_b0 a == absh_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:
absh_r a * (i + 1) + absh_b0 a ==
absh_r a * i + absh_b0 a + absh_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_abstractionh in H_a_eq_absh_w.
assert (H_S_i_ge_1:(S i >= 1)%nat).
auto with arith.
generalize (H_a_eq_absh_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
(absh_r a * S i + absh_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:abstractionh) (a2:abstractionh),
forall H_wf_a1: well_formed_abstractionh a1,
forall H_flo_a1: absh_b0 a1 <= 0,
forall H_wf_a2: well_formed_abstractionh a2,
forall H_flo_a2: absh_b0 a2 <= 0,
forall (H_a1_eq_absh_w1: in_abstractionh w1 a1),
forall (H_a2_eq_absh_w2: in_abstractionh w2 a2),
forall i,
forall (H_on: on w1 w2 i = false),
absh_r a1 * absh_r a2 * i + (absh_b0 a1 * absh_r a2 + absh_b0 a2)
<= ones (on w1 w2) i.
Proof.
intros.
rewrite ones_on_def.
generalize (absh_b0_neg_impl_ones_ge_a H_wf_a1 H_flo_a1 H_a1_eq_absh_w1 i).
intro H_w1_ge_a1.
generalize (absh_b0_neg_impl_ones_ge_a H_wf_a2 H_flo_a2 H_a2_eq_absh_w2 (ones w1 i)).
intro H_w2_ge_a2.
apply
(Qle_trans
(absh_r a1 * absh_r a2 * i + (absh_b0 a1 * absh_r a2 + absh_b0 a2))
(absh_r a2 * ones w1 i + absh_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 <= absh_r a2)).
apply H_wf_a2.
generalize
(Qmult_le_compat_r
(absh_r a1 * i + absh_b0 a1)
(ones w1 i)
(absh_r a2)
H_w1_ge_a1
(H_r_pos_2)).
intro H_cc.
rewrite Qmult_plus_distr_l in H_cc.
assert (H_aux: absh_r a1 * i * absh_r a2 == absh_r a1 * absh_r a2 * i).
ring.
rewrite H_aux in H_cc; clear H_aux.
assert (H_aux: ones w1 i * absh_r a2 == absh_r a2 * ones w1 i).
ring.
rewrite H_aux in H_cc; clear H_aux.
exact H_cc.
Qed.
Property on_absh_correctness_aux:
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.
intros.
assert (H_aux:
exists a1_0,
(absh_b1 a1_0 == absh_b1 a1) /\
(absh_b0 a1_0 == 0) /\
(absh_r a1_0 == absh_r a1)).
exists (abshmake (absh_b1 a1) 0 (absh_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_abstractionh a1_0).
unfold well_formed_abstractionh.
destruct H_a1_0.
destruct H0.
rewrite H1.
assumption.
assert (H_absh_b01_0: absh_b0 a1_0 <= 0).
destruct H_a1_0.
destruct H0.
rewrite H0.
eapply Qle_refl.
assert (H_aux:
exists a2_0,
(absh_b1 a2_0 == absh_b1 a2) /\
(absh_b0 a2_0 == 0) /\
(absh_r a2_0 == absh_r a2)).
exists (abshmake (absh_b1 a2) 0 (absh_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_abstractionh a2_0).
unfold well_formed_abstractionh.
destruct H_a2_0.
destruct H0.
rewrite H1.
assumption.
assert (H_absh_b02_0: absh_b0 a2_0 <= 0).
destruct H_a2_0.
destruct H0.
rewrite H0.
eapply Qle_refl.
unfold in_abstractionh.
intros.
split.
intro H_on.
simpl.
eapply on_w1_w2_le_on_a1_a2; assumption.
intro H_on.
elim (Q_dec (absh_b0 a1) 0);
elim (Q_dec (absh_b0 a2) 0).
intros H_aux1 H_aux2.
elim H_aux1;
elim H_aux2.
clear H_aux1 H_aux2.
intros H_absh_b01 H_absh_b02.
elim (Qlt_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qlt_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (absh_b0 a1) 0 H_absh_b01)
H_wf_a2 (Qlt_le_weak (absh_b0 a2) 0 H_absh_b02)
H_a1_eq_absh_w1 H_a2_eq_absh_w2);
auto.
clear H_aux1 H_aux2.
intros H_absh_b01 H_absh_b02.
elim (Qgt_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qlt_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
assert (H_a1_0_eq_absh_w1: in_abstractionh w1 a1_0).
assert (H_a1_in_a1_0: absh_included_test a1 a1_0).
apply absh_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_absh_w1).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_absh_b01_0
H_wf_a2 (Qlt_le_weak (absh_b0 a2) 0 H_absh_b02)
H_a1_0_eq_absh_w1 H_a2_eq_absh_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
trivial.
clear H_aux1 H_aux2.
intros H_absh_b01 H_absh_b02.
elim (Qlt_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qgt_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
assert (H_a2_0_eq_absh_w2: in_abstractionh w2 a2_0).
assert (H_a2_in_a2_0: absh_included_test a2 a2_0).
apply absh_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_absh_w2).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (absh_b0 a1) 0 H_absh_b01)
H_wf_a2_0 H_absh_b02_0
H_a1_eq_absh_w1 H_a2_0_eq_absh_w2
i H_on).
decompose [and] H_a2_0.
rewrite H2, H1.
trivial.
clear H_aux1 H_aux2.
intros H_absh_b01 H_absh_b02.
elim (Qgt_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qgt_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
assert (H_a1_0_eq_absh_w1: in_abstractionh w1 a1_0).
assert (H_a1_in_a1_0: absh_included_test a1 a1_0).
apply absh_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_absh_w1).
assert (H_a2_0_eq_absh_w2: in_abstractionh w2 a2_0).
assert (H_a2_in_a2_0: absh_included_test a2 a2_0).
apply absh_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_absh_w2).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_absh_b01_0
H_wf_a2_0 H_absh_b02_0
H_a1_0_eq_absh_w1 H_a2_0_eq_absh_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
decompose [and] H_a2_0.
rewrite H5, H4.
trivial.
intros H_absh_b02 H_aux.
elim H_aux.
clear H_aux.
intro H_absh_b01.
elim (Qlt_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qeq_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
assert (H_absh_b02_le_0: absh_b0 a2 <= 0).
rewrite H_absh_b02.
apply Qle_refl.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (absh_b0 a1) 0 H_absh_b01)
H_wf_a2 H_absh_b02_le_0
H_a1_eq_absh_w1 H_a2_eq_absh_w2);
auto.
clear H_aux.
intro H_absh_b01.
elim (Qgt_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qeq_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
assert (H_a1_0_eq_absh_w1: in_abstractionh w1 a1_0).
assert (H_a1_in_a1_0: absh_included_test a1 a1_0).
apply absh_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_absh_w1).
assert (H_absh_b02_le_0: absh_b0 a2 <= 0).
rewrite H_absh_b02.
apply Qle_refl.
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_absh_b01_0
H_wf_a2 H_absh_b02_le_0
H_a1_0_eq_absh_w1 H_a2_eq_absh_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
trivial.
intros H_aux H_absh_b01.
elim H_aux.
clear H_aux.
intro H_absh_b02.
elim (Qeq_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qlt_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
assert (H_absh_b01_le_0: absh_b0 a1 <= 0).
rewrite H_absh_b01.
apply Qle_refl.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_absh_b01_le_0
H_wf_a2 (Qlt_le_weak (absh_b0 a2) 0 H_absh_b02)
H_a1_eq_absh_w1 H_a2_eq_absh_w2);
auto.
clear H_aux.
intro H_absh_b02.
elim (Qeq_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qgt_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp.
rewrite H_absh_b02_eq_cmp.
assert (H_a2_0_eq_absh_w2: in_abstractionh w2 a2_0).
assert (H_a2_in_a2_0: absh_included_test a2 a2_0).
apply absh_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_absh_w2).
assert (H_absh_b01_le_0: absh_b0 a1 <= 0).
rewrite H_absh_b01.
apply Qle_refl.
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_absh_b01_le_0
H_wf_a2_0 H_absh_b02_0
H_a1_eq_absh_w1 H_a2_0_eq_absh_w2
i H_on).
decompose [and] H_a2_0.
rewrite H2, H1.
trivial.
intros H_absh_b02 H_absh_b01.
elim (Qeq_alt (absh_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b01).
clear H_aux1 H_aux2.
intro H_absh_b01_eq_cmp.
elim (Qeq_alt (absh_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absh_b02).
clear H_aux1 H_aux2.
intro H_absh_b02_eq_cmp.
simpl.
rewrite H_absh_b01_eq_cmp, H_absh_b02_eq_cmp.
assert (H_absh_b01_le_0: absh_b0 a1 <= 0).
rewrite H_absh_b01.
apply Qle_refl.
assert (H_absh_b02_le_0: absh_b0 a2 <= 0).
rewrite H_absh_b02.
apply Qle_refl.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_absh_b01_le_0
H_wf_a2 H_absh_b02_le_0
H_a1_eq_absh_w1 H_a2_eq_absh_w2
i H_on).
Qed.
End on_properties.
Section not_properties.
Property not_absh_correctness_aux:
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.
intros.
unfold in_abstractionh.
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_absh_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 - absh_r a) * 1 + - absh_b0 a + - (1) ==
0 + - (absh_r a * 1 + absh_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_absh_w 1%nat H_i_ge_1).
clear H_a_eq_absh_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_absh_b1.
rewrite H_w in *.
simpl.
simpl in H_absh_b1.
apply <- Qle_minus_iff.
assert (H_aux:
0 + - ((1 - absh_r a) * 1 + - absh_b1 a) ==
absh_r a * 1 + absh_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: absh_r a * S (S i') + absh_b0 a <= ones w (S (S i'))).
unfold in_abstractionh in H_a_eq_absh_w.
generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
clear H_a_eq_absh_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 - absh_r a) * (S i' + 1) + - absh_b0 a + - (i' - ones w i' + 1) ==
ones w i' + (S i' - i') + - (absh_r a * (S i' + 1) + absh_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: absh_r a * S (S i') + absh_b0 a <= ones w (S (S i'))).
unfold in_abstractionh in H_a_eq_absh_w.
generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
clear H_a_eq_absh_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 - absh_r a) * S (S i') + - absh_b0 a + - (i' - ones w i' + 1 + 1) ==
ones w i' + (S (S i') - i' - 1 - 1) + - (absh_r a * S (S i') + absh_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')) <= absh_r a * (S (S i')) + absh_b1 a).
unfold in_abstractionh in H_a_eq_absh_w.
generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
clear H_a_eq_absh_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 - absh_r a) * S (S i') + - absh_b1 a) ==
absh_r a * S (S i') + absh_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_absh_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 - absh_r a) * 2 + - absh_b1 a) ==
absh_r a * 2 + absh_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')) <= absh_r a * S (S i') + absh_b1 a).
unfold in_abstractionh in H_a_eq_absh_w.
generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
clear H_a_eq_absh_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 - absh_r a) * S (S i') + - absh_b1 a) ==
absh_r a * S (S i') + absh_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')) <= absh_r a * S (S i') + absh_b1 a).
unfold in_abstractionh in H_a_eq_absh_w.
generalize (H_a_eq_absh_w (S (S i')) H_i_ge_1).
clear H_a_eq_absh_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 - absh_r a) * S (S i') + - absh_b1 a) ==
absh_r a * S (S i') + absh_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 absh_included_test_not_not_absh:
forall a: abstractionh,
absh_included_test a (not_absh (not_absh a)).
Proof.
intros.
unfold absh_included_test.
repeat split.
simpl.
ring.
simpl.
ring_simplify.
apply Qle_refl.
simpl.
ring_simplify.
apply Qle_refl.
Qed.
Lemma not_not_absh_included_test_absh:
forall a: abstractionh,
absh_included_test (not_absh (not_absh a)) a.
Proof.
intros.
unfold absh_included_test.
repeat split.
simpl.
ring.
simpl.
ring_simplify.
apply Qle_refl.
simpl.
ring_simplify.
apply Qle_refl.
Qed.
Property not_not_absh_equal_absh:
forall a: abstractionh,
absh_equal (not_absh (not_absh a)) a.
Proof.
intros.
apply absh_equiv_test_impl_absh_equal.
split.
apply not_not_absh_included_test_absh.
apply absh_included_test_not_not_absh.
Qed.
Property not_absh_well_formed_abstractionh_compat:
forall a: abstractionh,
forall H_wf: well_formed_abstractionh a,
well_formed_abstractionh (not_absh a).
Proof.
intros.
unfold well_formed_abstractionh.
simpl.
destruct H_wf as [H0 H1].
split.
apply -> Qle_minus_iff.
assumption.
apply <- Qle_minus_iff.
ring_simplify.
assumption.
Qed.
End not_properties.
Section prec_absh_properties.
Property w_early_prec_a:
forall a: abstractionh,
forall H_wf: well_formed_abstractionh a,
forall w: ibw,
forall H_w_in_a: in_abstractionh 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: abstractionh,
forall H_wf: well_formed_abstractionh a,
forall w: ibw,
forall H_w_in_a: in_abstractionh 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_absh_alt_correctness:
forall a1 a2: abstractionh,
forall H_wf1: well_formed_abstractionh a1,
forall H_wf2: well_formed_abstractionh a2,
forall H_prec_test: prec_absh_alt a1 a2,
prec_absh a1 a2.
Proof.
intros.
unfold prec_absh.
intros.
pose (H_early2_prec_w2:= w_early_prec_a H_wf2 H_w2_in_a2).
unfold prec_absh_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_absh_alt_complet:
forall a1 a2: abstractionh,
forall H_wf1: well_formed_abstractionh a1,
forall H_non_empty1: non_empty a1,
forall H_wf2: well_formed_abstractionh a2,
forall H_non_empty2: non_empty a2,
forall H_prec: prec_absh a1 a2,
prec_absh_alt a1 a2.
Proof.
intros.
unfold prec_absh_alt.
unfold prec_absh in H_prec.
apply H_prec.
apply late_in_abs; auto.
apply early_in_abs; auto.
Qed.
Property prec_absh_test_correctness_aux:
forall a1 a2: abstractionh,
forall H_wf1: well_formed_abstractionh a1,
forall H_wf2: well_formed_abstractionh a2,
forall H_prec_test: prec_absh_test a1 a2,
forall H_sync: absh_r a1 == absh_r a2,
prec_absh a1 a2.
Proof.
intros.
apply prec_absh_alt_correctness; auto.
unfold prec_absh_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_absh_test in H_prec_test.
apply <- Qlt_minus_iff.
assert (H_aux:
absh_b0 a1 + 1 + - absh_b1 a2 == 1 + - (absh_b1 a2 - absh_b0 a1)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
assumption.
Qed.
End prec_absh_properties.
Section subtyping_properties.
Property subtyping_absh_impl_subtyping_absh_alt:
forall a1 a2: abstractionh,
forall H_sub: subtyping_absh a1 a2,
subtyping_absh_alt a1 a2.
Proof.
intros.
unfold subtyping_absh_alt.
unfold subtyping_absh in H_sub.
split.
unfold prec_absh.
intros.
unfold subtyping in H_sub.
destruct (H_sub w1 w2 H_w1_in_a1 H_w2_in_a2).
assumption.
unfold sync_absh.
intros.
unfold subtyping in H_sub.
destruct (H_sub w1 w2 H_w1_in_a1 H_w2_in_a2).
assumption.
Qed.
Property subtyping_absh_alt_impl_subtyping_absh:
forall a1 a2: abstractionh,
forall H_sub: subtyping_absh_alt a1 a2,
subtyping_absh a1 a2.
Proof.
intros.
unfold subtyping_absh.
unfold subtyping_absh_alt in H_sub.
elim H_sub; intros H_prec H_sync.
intros.
split.
apply H_prec; auto.
apply H_sync; auto.
Qed.
End subtyping_properties.