Library abstraction_jfla_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_jfla_def.
Section Abstractionj_def.
Definition absj_equal (a1: abstractionj) (a2:abstractionj) :=
(absj_r a1 == absj_r a2) /\
(absj_b1 a1) == (absj_b1 a2) /\
(absj_b0 a1) == (absj_b0 a2).
Instance absj_equal_is_equiv : Equivalence _ absj_equal.
Proof.
constructor ; unfold absj_equal ; red ; intuition.
transitivity (absj_r y) ; auto.
transitivity (absj_b1 y) ; auto.
transitivity (absj_b0 y) ; auto.
Qed.
End Abstractionj_def.
Definition absj_equiv (a1: abstractionj) (a2:abstractionj) :=
absj_included a1 a2 /\ absj_included a2 a1.
Definition absj_equiv_test (a1: abstractionj) (a2:abstractionj) :=
absj_included_test a1 a2 /\ absj_included_test a2 a1.
Section abstraction_equivalence_properties.
Property absj_included_test_impl_absj_included:
forall a1 a2: abstractionj,
forall H_a1_in_test_a2: absj_included_test a1 a2,
absj_included a1 a2.
Proof.
intros.
unfold absj_included.
intros.
unfold in_abstractionj.
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
(Qlt_le_trans
(ones w (pred i))
(absj_r a1 * i + absj_b1 a1)
(absj_r a1 * i + absj_b1 a2)); auto.
apply Qplus_le_compat; auto.
apply Qle_refl.
intro H_w.
apply
(Qle_trans
(absj_r a1 * i + absj_b0 a2)
(absj_r a1 * i + absj_b0 a1)
(ones w (pred 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_abstractionj a1,
forall H_wf_a2: well_formed_abstractionj a2,
forall H_a1_in_a2: absj_included_test a1 a2,
forall H_w_in_a1: in_abstractionj w a1,
in_abstractionj w a2.
Proof.
intros.
unfold in_abstractionj.
intros i H_i_ge_1.
split.
intro H_w.
unfold in_abstractionj 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 (Qlt_le_trans
(ones w (pred i))
(absj_r a1 * i + absj_b1 a1)
(absj_r a1 * i + absj_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_abstractionj 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.
rewrite ones_pred_i_eq_ones_i in *; auto.
apply
(Qle_trans
(absj_r a1 * i + absj_b0 a2)
(absj_r a1 * i + absj_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 absj_weakening_aux:
forall a1 a2: abstractionj,
forall H_one: absj_b1 a1 <= absj_b1 a2,
forall H_absj_b0: absj_b0 a1 >= absj_b0 a2,
forall H_r: absj_r a1 == absj_r a2,
absj_included_test a1 a2.
Proof.
intros.
unfold absj_included_test.
repeat split; auto.
Qed.
Property absj_weakening_0:
forall a1 a2: abstractionj,
forall H_absj_b01: absj_b0 a1 > 0,
forall H_r: absj_r a1 == absj_r a2,
forall H_one: absj_b1 a1 == absj_b1 a2,
forall H_absj_b02: absj_b0 a2 == 0,
absj_included_test a1 a2.
Proof.
intros.
eapply absj_weakening_aux; auto.
rewrite H_one.
apply Qle_refl.
rewrite H_absj_b02.
eapply Qlt_le_weak.
assumption.
Qed.
Property absj_equal_sym:
forall a1 a2: abstractionj,
forall H_a1_eq_a2: absj_equal a1 a2,
absj_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 absj_equal_impl_absj_included_test:
forall a1 a2: abstractionj,
forall H_a1_eq_a2: absj_equal a1 a2,
absj_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 absj_equal_impl_absj_equiv_test:
forall a1 a2: abstractionj,
forall H_a1_eq_a2: absj_equal a1 a2,
absj_equiv_test a1 a2.
Proof.
intros.
split.
apply absj_equal_impl_absj_included_test; auto.
apply absj_equal_impl_absj_included_test; auto.
apply absj_equal_sym.
assumption.
Qed.
Property absj_equiv_test_impl_absj_equal:
forall a1 a2: abstractionj,
forall H_a1_eq_a2: absj_equiv_test a1 a2,
absj_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_absj_b11_le_absj_b12 H_absj_b02_le_absj_b01.
elim H_tmp2; clear H_tmp2.
intros H_r' H_tmp'.
elim H_tmp'; clear H_tmp' H_r'.
intros H_absj_b12_le_absj_b11 H_absj_b01_le_absj_b02.
repeat split.
trivial.
apply Qle_antisym; assumption.
apply Qle_antisym; assumption.
Qed.
Property absj_equal_correctness:
forall a1 a2: abstractionj,
forall H_wf1: well_formed_abstractionj a1,
forall H_wf2: well_formed_abstractionj a2,
forall w: ibw,
forall H_w_in_a1: in_abstractionj w a1,
forall H_eq: absj_equal a1 a2,
in_abstractionj w a2.
Proof.
intros.
apply absj_equal_impl_absj_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.
End abstraction_equivalence_properties.
Fixpoint ones_early_opt (a:abstractionj) (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 ones_i' (absj_r a * i + absj_b1 a) with
| Lt => Some (S ones_i')
| Gt | Eq =>
match Qcompare (absj_r a * i + absj_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| _ => None
end
end
end
end.
Fixpoint ones_late_opt (a:abstractionj) (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 (absj_r a * i + absj_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| Gt =>
match Qcompare ones_i' (absj_r a * i + absj_b1 a) with
| Lt => Some (S ones_i')
| Gt | Eq => None
end
end
end
end.
Definition non_empty_alt (a: abstractionj) :=
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 ones_early a i' ?= absj_r a * S i' + absj_b1 a with
| Eq => 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 absj_r a * (S i') + absj_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 ones_i' (absj_r a * S i' + absj_b1 a) with
| Lt => Some (S ones_i')
| Gt | Eq =>
match Qcompare (absj_r a * S i' + absj_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 (absj_r a * S i' + absj_b0 a) ones_i' with
| Lt | Eq => Some (ones_i')
| Gt =>
match Qcompare ones_i' (absj_r a * S i' + absj_b1 a) with
| Lt => Some (S ones_i')
| Gt | Eq => None
end
end
end)%nat.
Proof.
intros.
simpl.
reflexivity.
Qed.
Lemma ones_early_alt_remove_Zabs_nat:
forall a:abstractionj,
forall i,
((Z_of_nat (ones_early_alt a i))%Z =
Zmax O (Zmin i (cg (absj_r a * i + absj_b1 a))))%Z.
Proof.
intros.
unfold ones_early_alt.
rewrite inj_Zabs_nat.
elim (Zabs_spec (Zmax O (Zmin i (cg (absj_r a * i + absj_b1 a))))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
elim (Zmax_spec O (Zmin i (cg (absj_r a * i + absj_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:abstractionj,
forall i,
((Z_of_nat (ones_late_alt a i))%Z =
Zmax O (Zmin i (cg (absj_r a * i + absj_b0 a))))%Z.
Proof.
intros.
unfold ones_late_alt.
rewrite inj_Zabs_nat.
elim (Zabs_spec (Zmax O (Zmin i (cg (absj_r a * i + absj_b0 a))))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
elim (Zmax_spec O (Zmin i (cg (absj_r a * i + absj_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: abstractionj,
well_formed_ones (ones_early a).
Proof.
intros.
split.
simpl.
reflexivity.
intro.
simpl.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
intro H_cmp.
right.
reflexivity.
intro H_cmp.
left.
reflexivity.
intro H_cmp.
right.
reflexivity.
Qed.
Property ones_late_well_formed:
forall a: abstractionj,
well_formed_ones (ones_late a).
Proof.
intros.
split.
simpl.
reflexivity.
intro.
simpl.
case_eq (absj_r a * S i + absj_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: abstractionj,
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 (0%nat ?= absj_r a * 1%nat + absj_b1 a);
intros;
simpl;
reflexivity.
assert (H_aux:
(ones_early a (S (S i'))
=
match ones_early a (S i') ?= absj_r a * (S (S i')) + absj_b1 a with
| Eq => 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 ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
| Eq => 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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a).
intro.
assert (H_aux:
beq_nat ((ones_early a (S i'))) (ones_early a (S i')) = true).
rewrite (beq_nat_refl (ones_early a (S i'))).
reflexivity.
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_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: abstractionj,
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 (absj_r a * 1%nat + absj_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 absj_r a * S (S i') + absj_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 (absj_r a * S (S i') + absj_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: abstractionj,
forall H_wf: well_formed_abstractionj 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 (cg (absj_r a * O%nat + absj_b1 a)))).
intro H_tmp; destruct H_tmp.
rewrite H0.
reflexivity.
intro H_tmp; destruct H_tmp.
rewrite H0.
elim (Zmin_spec 0%nat (cg (absj_r a * 0%nat + absj_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) (cg (absj_r a * S i + absj_b1 a)))).
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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
(cg (absj_r a * S i + absj_b1 a))
(cg (absj_r a * i + absj_b1 a))); auto.
apply Zle_ge.
apply cg_monotone_linear.
assert (H_aux:
absj_r a * i + absj_b1 a ==
absj_r a * i + absj_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b1 a ==
absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
(cg (absj_r a * i + absj_b1 a))); auto.
apply cg_monotone_linear.
assert (H_aux:
absj_r a * i + absj_b1 a ==
absj_r a * i + absj_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b1 a ==
absj_r a * i + absj_b1 a + absj_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: ones_early a i >= absj_r a * S i + absj_b1 a).
clear H0; clear H2.
rewrite H_cc_aux1.
apply (Qle_trans
(absj_r a * S i + absj_b1 a)
(cg(absj_r a * S i + absj_b1 a))
0).
destruct (cg_def_linear (absj_r a * S i + absj_b1 a)); assumption.
apply Zle_impl_Qle.
apply Zge_le.
assumption.
rewrite red_ones_early.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a);
try solve [ intro H_cmp; apply inj_eq; assumption].
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
absurd (ones_early a i < absj_r a * S i + absj_b1 a); auto.
apply Qle_not_lt.
assumption.
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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)
(cg (absj_r a * i + absj_b1 a) + 1)).
apply inj_lt.
auto with arith.
rewrite <- cg_plus_int_rewrite.
apply (Zle_trans
(S i)
(cg (absj_r a * S i + absj_b1 a))
(cg (absj_r a * i + absj_b1 a + 1))); auto.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b1 a ==
absj_r a * i + absj_b1 a + absj_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: ones_early a i < absj_r a * S i + absj_b1 a).
rewrite H_cc_aux1.
apply (Qle_lt_trans
i
(cg (absj_r a * S i + absj_b1 a) - 1)%Z
(absj_r a * S i + absj_b1 a));
try solve [ elim (cg_def_linear (absj_r a * S i + absj_b1 a));
intros; assumption ].
assert (H_aux:
(cg (absj_r a * S i + absj_b1 a) - 1%nat) ==
(cg (absj_r a * S i + absj_b1 a) - 1%nat)%Z).
unfold Qeq; simpl; omega.
rewrite <- H_aux; clear H_aux.
unfold Qminus.
rewrite -> Qle_minus_iff.
assert (H_aux:
cg (absj_r a * S i + absj_b1 a) + - (1) + - i ==
cg (absj_r a * S i + absj_b1 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_early.
rewrite Qlt_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_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: ones_early a i < absj_r a * S i + absj_b1 a).
rewrite Qlt_alt.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a); auto;
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_le_trans
(ones_early_alt a i)
(absj_r a * S i + absj_b1 a)
(cg (absj_r a * S i + absj_b1 a))); auto.
elim (cg_def_linear (absj_r a * S i + absj_b1 a)); auto.
rewrite ones_early_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:
absj_r a * (i + 1) + absj_b1 a ==
absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
(cg (absj_r a * i + absj_b1 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b1 a ==
absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
(cg (absj_r a * i + absj_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 cg_monotone_linear.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite Qmult_comm.
assert (H_aux: absj_r a * S i == S i * absj_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: ones_early a i >= absj_r a * S i + absj_b1 a).
rewrite Qge_alt.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
intro H_cmp.
intro.
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.
intro.
congruence.
rewrite IHi in H_cmp.
apply Zle_antisym.
rewrite ones_early_alt_remove_Zabs_nat.
rewrite Zmin_right; auto.
rewrite Zmax_right.
apply cg_monotone_linear.
assert (H_aux:
absj_r a * i + absj_b1 a ==
absj_r a * i + absj_b1 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b1 a ==
absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
(cg (absj_r a * i + absj_b1 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b1 a ==
absj_r a * i + absj_b1 a + absj_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 (absj_r a * S i + absj_b1 a))
(cg (absj_r a * i + absj_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 cg_monotone_linear.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
rewrite Qmult_comm.
assert (H_aux: absj_r a * S i == S i * absj_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.
Property ones_late_eq_ones_late_alt:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj 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 (absj_r a * O%nat + absj_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 (absj_r a * 0%nat + absj_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 (absj_r a * S i + absj_b0 a)))).
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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 (absj_r a * S i + absj_b0 a))
(cg (absj_r a * i + absj_b0 a))); auto.
apply Zle_ge.
apply cg_monotone_linear.
assert (H_aux:
absj_r a * i + absj_b0 a ==
absj_r a * i + absj_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
(cg (absj_r a * i + absj_b0 a))); auto.
apply cg_monotone_linear.
assert (H_aux:
absj_r a * i + absj_b0 a ==
absj_r a * i + absj_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_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: absj_r a * S i + absj_b0 a <= ones_late a i).
clear H0; clear H2.
rewrite H_cc_aux1.
apply (Qle_trans
(absj_r a * S i + absj_b0 a)
(cg(absj_r a * S i + absj_b0 a))
0).
destruct (cg_def_linear (absj_r a * S i + absj_b0 a)); assumption.
apply Zle_impl_Qle.
apply Zge_le.
assumption.
rewrite red_ones_late.
case_eq (absj_r a * S i + absj_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 < absj_r a * S i + absj_b0 a); auto.
apply Qle_not_lt.
assumption.
intro H_tmp; destruct H_tmp.
elim (Zmin_spec (S i) (cg (absj_r a * (S i) + absj_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 (absj_r a * i + absj_b0 a) + 1)).
apply inj_lt.
auto with arith.
rewrite <- cg_plus_int_rewrite.
apply (Zle_trans
(S i)
(cg (absj_r a * S i + absj_b0 a))
(cg (absj_r a * i + absj_b0 a + 1))); auto.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_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: absj_r a * S i + absj_b0 a > ones_late a i).
rewrite H_cc_aux1.
apply (Qle_lt_trans
i
(cg (absj_r a * S i + absj_b0 a) - 1)%Z
(absj_r a * S i + absj_b0 a));
try solve [ elim (cg_def_linear (absj_r a * S i + absj_b0 a));
intros; assumption ].
assert (H_aux:
(cg (absj_r a * S i + absj_b0 a) - 1%nat) ==
(cg (absj_r a * S i + absj_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 (absj_r a * S i + absj_b0 a) + - (1) + - i ==
cg (absj_r a * S i + absj_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: absj_r a * S i + absj_b0 a > ones_late a i).
rewrite Qlt_alt.
case_eq (absj_r a * S i + absj_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)
(absj_r a * S i + absj_b0 a)
(cg (absj_r a * S i + absj_b0 a))); auto.
elim (cg_def_linear (absj_r a * S i + absj_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:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
(cg (absj_r a * i + absj_b0 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
(cg (absj_r a * i + absj_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: absj_r a * S i == S i * absj_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: absj_r a * S i + absj_b0 a <= ones_late a i).
rewrite Qge_alt.
case_eq (absj_r a * S i + absj_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 < absj_r a * S i + absj_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:
absj_r a * i + absj_b0 a ==
absj_r a * i + absj_b0 a + 0).
ring.
rewrite H_aux; clear H_aux.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
(cg (absj_r a * i + absj_b0 a) + 1%nat)); auto.
rewrite <- cg_plus_int_rewrite.
apply cg_monotone_linear.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_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 (absj_r a * S i + absj_b0 a))
(cg (absj_r a * i + absj_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: absj_r a * S i == S i * absj_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_i_lt_a:
forall a i,
forall H_w: w_early a (S i) = true,
ones (w_early a) i < (absj_r a * S i + absj_b1 a).
Proof.
intros.
simpl in H_w.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
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 <- Qlt_alt in H_cmp.
rewrite ones_early_eq_ones_w_early in H_cmp.
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_ge_a:
forall a i,
forall H_w: w_early a (S i) = false,
ones (w_early a) i >= (absj_r a * S i + absj_b1 a).
Proof.
intros.
simpl in H_w.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
intro H_cmp.
rewrite <- Qeq_alt in H_cmp.
rewrite ones_early_eq_ones_w_early in H_cmp.
rewrite H_cmp.
apply Qle_refl.
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 <- Qgt_alt in H_cmp.
rewrite ones_early_eq_ones_w_early in H_cmp.
apply Qlt_le_weak.
assumption.
Qed.
Property ones_w_le_ones_early:
forall w: ibw,
forall a: abstractionj,
forall H_wf_a: well_formed_abstractionj a,
forall H_w_in_a: in_abstractionj 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 (0%nat ?= absj_r a * 1%nat + absj_b1 a);
try solve [ intros; apply le_refl ].
intros H_cmp.
rewrite <- Qeq_alt in H_cmp.
absurd (0 == absj_r a * 1 + absj_b1 a); auto.
apply Qlt_not_eq.
assumption.
intros H_cmp.
rewrite <- Qgt_alt in H_cmp.
absurd (absj_r a * 1 + absj_b1 a < 0); auto.
apply Qle_not_lt.
apply Qlt_le_weak.
assumption.
intro H_w.
simpl.
rewrite H_w.
simpl.
case_eq (0%nat ?= absj_r a * 1%nat + absj_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 ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
| Eq => (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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_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.
change (pred (S (S i'))) with (S i') in H_ones_le_a.
rewrite H_cmp in H_ones_le_a.
assert (H_aux:
(ones_early a (S (S i'))
=
match ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
| Eq => 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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a);
try omega.
intro H_cmp'.
rewrite <- Qeq_alt in H_cmp'.
rewrite <- H_cmp' in H_ones_le_a.
absurd (ones_early a (S i') < ones_early a (S i')); auto.
apply Qle_not_lt.
apply Qle_refl.
intro H_cmp'.
rewrite <- Qgt_alt in H_cmp'.
absurd (absj_r a * S (S i') + absj_b1 a < ones_early a (S i')); auto.
apply Qle_not_lt.
apply Qlt_le_weak.
assumption.
intro H_w.
rewrite ones_S_i_eq_ones_i; auto.
assert (H_aux:
(ones_early a (S (S i'))
=
match ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a with
| Eq => 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 (ones_early a (S i') ?= absj_r a * S (S i') + absj_b1 a);
omega.
Qed.
Property ones_late_le_ones_w:
forall w: ibw,
forall a: abstractionj,
forall H_wf_a: well_formed_abstractionj a,
forall H_w_in_a: in_abstractionj 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 (absj_r a * 1%nat + absj_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 (absj_r a * 1%nat + absj_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 < absj_r a * 1 + absj_b0 a); auto.
apply Qle_not_lt.
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 (absj_r a * S (S i') + absj_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 (absj_r a * S (S i') + absj_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'))
(absj_r a * S (S i') + absj_b0 a)
(ones w (S i')));
try solve [ exact H_cmp ].
unfold in_abstractionj in H_w_in_a.
replace (ones w (S i')) with (ones w (pred (S (S i')))); auto.
apply (H_w_in_a (S (S i'))); auto with arith.
Qed.
Lemma ones_early_opt_impl_ones_early:
forall a: abstractionj,
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 (ones_early a i ?= absj_r a * S i + absj_b1 a);
try reflexivity.
intro H_cmp.
case_eq (absj_r a * S i + absj_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.
intro H_cmp.
case_eq (absj_r a * S i + absj_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: abstractionj,
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 (absj_r a * S i + absj_b0 a ?= ones_late a i);
try reflexivity.
intro H_cmp.
case_eq (ones_late a i ?= absj_r a * S i + absj_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.
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: abstractionj,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
forall H_absj_b1_lt_absj_b0: absj_b1 a < absj_b0 a,
forall i,
ones_late a i = ones_early a i.
Proof.
induction i.
simpl.
reflexivity.
simpl.
case_eq (absj_r a * S i + absj_b0 a ?= ones_late a i).
intros H_cmp_zero.
rewrite IHi.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
intros H_cmp_one.
rewrite <- Qeq_alt in *.
rewrite IHi in H_cmp_zero.
rewrite H_cmp_one in H_cmp_zero.
apply Qeq_sym in H_cmp_zero.
absurd (absj_r a * S i + absj_b1 a == absj_r a * S i + absj_b0 a);
auto.
apply Qlt_not_eq.
apply Qplus_lt_compat_l.
assumption.
intros H_cmp_one.
rewrite <- Qeq_alt in *.
rewrite <- Qlt_alt in *.
absurd (ones_early a i < absj_r a * S i + absj_b1 a);
auto.
rewrite IHi in H_cmp_zero.
rewrite <- H_cmp_zero.
apply Qle_not_lt.
apply Qplus_le_compat; try solve [apply Qle_refl; auto].
apply Qlt_le_weak.
assumption.
reflexivity.
intros H_cmp_zero.
rewrite IHi.
case_eq (ones_early a i ?= absj_r a * S i + absj_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.
rewrite H_cmp_one in H_cmp_zero.
absurd (absj_r a * S i + absj_b0 a < absj_r a * S i + absj_b1 a);
auto.
apply Qle_not_lt.
apply Qplus_le_compat; try solve [apply Qle_refl; auto].
apply Qlt_le_weak.
assumption.
intros H_cmp_one.
rewrite <- Qlt_alt in *.
absurd (absj_r a * S i + absj_b0 a < absj_r a * S i + absj_b1 a).
apply Qle_not_lt.
apply Qplus_le_compat; try solve [apply Qle_refl; auto].
apply Qlt_le_weak.
assumption.
rewrite IHi in H_cmp_zero.
apply
(Qlt_trans
(absj_r a * S i + absj_b0 a)
(ones_early a i)
(absj_r a * S i + absj_b1 a)); auto.
reflexivity.
intros H_cmp_zero.
rewrite IHi.
case_eq (ones_early a i ?= absj_r a * S i + absj_b1 a).
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.
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: abstractionj,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
in_abstractionj (w_early a) a.
Proof.
intros.
unfold in_abstractionj.
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_i_lt_a.
exact H_w_early_S_i'.
intro H_w_early_S_i'.
assert (H_cmp: (absj_r a * S i' + absj_b1 a) <= (ones_early a i')).
rewrite ones_early_eq_ones_w_early.
apply w_early_S_i_eq_false_impl_ones_early_i_ge_a; auto.
rewrite Qge_alt in H_cmp.
pose (H_non_empty_i:=H_non_empty (S i')).
assert (H_aux: (ones_early a (S i') = ones_early a i')%nat).
simpl.
case_eq (ones_early a i' ?= absj_r a * S i' + absj_b1 a);
try reflexivity.
intros.
congruence.
rewrite H_aux in H_non_empty_i.
simpl in H_non_empty_i.
case_eq (absj_r a * S i' + absj_b0 a ?= ones_late a i').
intro H_cmp'.
rewrite H_cmp' in *.
rewrite <- Qeq_alt in H_cmp'.
rewrite H_cmp'.
apply le_impl_Qle.
simpl.
rewrite <- ones_early_eq_ones_w_early.
exact H_non_empty_i.
intro H_cmp'.
rewrite <- Qlt_alt in H_cmp'.
simpl.
rewrite <- ones_early_eq_ones_w_early.
apply
(Qle_trans
(absj_r a * S i' + absj_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 (absj_b1 a) (absj_b0 a)).
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.
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
(absj_r a * S (S i'') + absj_b0 a)
(absj_r a * S (S i'') + absj_b1 a)
(ones_early a (S i'')));
try solve [
apply Qplus_le_compat; auto;
apply Qle_refl].
rewrite <- Qge_alt in H_cmp.
assumption.
Qed.
Property ones_late_le_ones_early_impl_late_in_a:
forall a: abstractionj,
forall H_non_empty: (forall i, (ones_late a i <= ones_early a i)%nat),
in_abstractionj (w_late a) a.
Proof.
intros.
unfold in_abstractionj.
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 (absj_r a * S i' + absj_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 (ones_early a i' ?= absj_r a * S i' + absj_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 lt_impl_Qlt.
apply le_lt_n_Sm in H_non_empty_i.
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.
apply (Qle_lt_trans
(ones_late a i')
(ones_early a i')
(absj_r a * S i' + absj_b1 a)); 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 (absj_b1 a) (absj_b0 a)).
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.
apply (Qlt_le_trans
(ones_late a i')
(absj_r a * S i' + absj_b0 a)
(absj_r a * S i' + absj_b1 a)); auto.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
assumption.
intro H_w.
simpl.
simpl in H_w.
rewrite <- ones_late_eq_ones_w_late.
case_eq (absj_r a * S i' + absj_b0 a ?= ones_late a i').
intro H_cmp.
rewrite <- Qeq_alt in H_cmp.
rewrite H_cmp.
apply Qle_refl.
intro H_cmp.
rewrite <- Qlt_alt in H_cmp.
apply Qlt_le_weak.
assumption.
intro H_cmp.
rewrite H_cmp in H_w.
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: abstractionj,
forall H_wf: well_formed_abstractionj 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: abstractionj,
forall H_wf: well_formed_abstractionj a,
forall H_non_empty: non_empty a,
in_abstractionj (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: abstractionj,
forall H_wf: well_formed_abstractionj a,
forall H_non_empty: non_empty a,
in_abstractionj (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.
End early_and_late_properties.
Lemma ones_late_le_ones_early_impl_non_empty:
forall a,
forall H_wf: well_formed_abstractionj 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:
forall a,
forall H_wf: well_formed_abstractionj a,
forall H_non_empty: non_empty_test a,
forall i,
(ones_late a i <= ones_early a i)%nat.
Proof.
intros.
unfold non_empty_test in 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.
apply cg_monotone_linear.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
assumption.
Qed.
End non_empty_test_properties.
Section std_properties.
Lemma absj_std_red:
forall a: abstractionj,
absj_std a =
absjmake
(absj_b1 a * (QDen (absj_r a) # Qden (absj_r a)))
(absj_b0 a)
(absj_r a * (QDen (absj_b1 a) # Qden (absj_b1 a))).
Proof.
intros.
reflexivity.
Qed.
Property absj_std_correctness:
forall a: abstractionj,
absj_equal a (absj_std a).
Proof.
intros a.
rewrite absj_std_red.
repeat split.
simpl.
assert (H_aux: (' Qden (absj_b1 a) # Qden (absj_b1 a)) == 1).
unfold Qeq.
simpl.
rewrite Pmult_1_r.
reflexivity.
rewrite H_aux; clear H_aux.
rewrite Qmult_1_r.
reflexivity.
simpl.
assert (H_aux: (' Qden (absj_r a) # Qden (absj_r a)) == 1).
unfold Qeq.
simpl.
rewrite Pmult_1_r.
reflexivity.
rewrite H_aux; clear H_aux.
rewrite Qmult_1_r.
reflexivity.
Qed.
Property absj_std_well_formed_abstractionj_compat:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj a,
well_formed_abstractionj (absj_std a).
Proof.
intros.
unfold well_formed_abstractionj in *.
rewrite absj_std_red.
simpl.
assert (H_aux: (' Qden (absj_b1 a) # Qden (absj_b1 a)) == 1).
unfold Qeq.
simpl.
rewrite Pmult_1_r.
reflexivity.
rewrite H_aux; clear H_aux.
rewrite Qmult_1_r.
assumption.
Qed.
Property absj_std_in_abstractionj_compat:
forall w: ibw,
forall a: abstractionj,
forall H_w_in_a: in_abstractionj w a,
in_abstractionj w (absj_std a).
Proof.
intros.
rewrite absj_std_red.
unfold in_abstractionj.
simpl.
intros.
assert (H_aux: (' Qden (absj_b1 a) # Qden (absj_b1 a)) == 1).
unfold Qeq.
simpl.
rewrite Pmult_1_r.
reflexivity.
rewrite H_aux; clear H_aux.
assert (H_aux: (' Qden (absj_r a) # Qden (absj_r a)) == 1).
unfold Qeq.
simpl.
rewrite Pmult_1_r.
reflexivity.
rewrite H_aux; clear H_aux.
repeat rewrite Qmult_1_r.
pose (H_cc := H_w_in_a i H_i_ge_1).
assumption.
Qed.
End std_properties.
Section on_properties.
Lemma on_w1_w2_lt_on_a1_a2:
forall (w1:ibw) (w2:ibw),
forall (a1:abstractionj) (a2:abstractionj),
forall H_wf_a1: well_formed_abstractionj a1,
forall H_wf_a2: well_formed_abstractionj a2,
forall (H_a1_eq_absj_w1: in_abstractionj w1 a1),
forall (H_a2_eq_absj_w2: in_abstractionj w2 a2),
forall H_wf_b1_1: Qden (absj_b1 a1) = Qden (absj_r a1),
forall H_wf_b1_2: Qden (absj_b1 a2) = Qden (absj_r a2),
forall epsilon: Q,
forall H_epsilon: epsilon == (1 - (1 # Qden (absj_r a1) )) * ((absj_r a2) - (1 # Qden (absj_r a2))),
forall i,
forall H_i_ge_1: (i >= 1)%nat,
forall (H_on: on w1 w2 i = true),
ones (on w1 w2) (pred i) <
(absj_r a1 * absj_r a2) * i + ((absj_b1 a1 * absj_r a2 + absj_b1 a2) + epsilon).
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 (pred i) < absj_r a1 * i + absj_b1 a1).
unfold in_abstractionj in H_a1_eq_absj_w1.
generalize (H_a1_eq_absj_w1 i H_i_ge_1).
clear H_a1_eq_absj_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 (pred (ones w1 i)) < (absj_r a2 * ones w1 i + absj_b1 a2)).
unfold in_abstractionj in H_a2_eq_absj_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_absj_w2 (ones w1 i) H_ones_w1_ge_1).
clear H_a2_eq_absj_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.
assert (H_aux: ones w1 (pred i) = pred (ones w1 i)).
apply ones_pred_i_eq_pred_ones_i; assumption.
rewrite H_aux; rewrite H_aux in H_w1_le_a1; clear H_aux.
assert (H_aux: pred (ones w1 i) == ones w1 i - 1).
case_eq (ones w1 i).
intro H_ones_w1.
absurd (O = ones w1 i); auto.
apply lt_O_neq.
apply w_i_eq_true_impl_ones_pos; auto.
intros.
rewrite <- n_plus_1_eq_S_n.
simpl.
assert (H_aux: n + 1 - 1 == n).
ring.
rewrite H_aux; clear H_aux.
apply Qeq_refl.
rewrite H_aux in H_w1_le_a1; clear H_aux.
assert (H_aux: ones w1 i - 1 == - (1) + ones w1 i).
ring.
rewrite H_aux in H_w1_le_a1; clear H_aux.
assert (H_aux:
absj_r a1 * i + absj_b1 a1 ==
- (1) + (absj_r a1 * i + absj_b1 a1 + 1)).
ring.
rewrite H_aux in H_w1_le_a1; clear H_aux.
rewrite Qlt_plus in H_w1_le_a1.
assert (H_tmp:
absj_r a1 * i + absj_b1 a1 + 1 ==
absj_r a1 * i + (Qnum (absj_b1 a1) + QDen (absj_b1 a1)) / (QDen (absj_b1 a1))).
rewrite <- Qplus_assoc.
apply Qplus_eq_compat; try solve [ apply Qeq_refl ].
unfold Qplus, Qeq, Q_of_nat, Qdiv; simpl; ring_simplify; simpl.
rewrite Pmult_1_r. reflexivity.
rewrite H_tmp in H_w1_le_a1.
assert (H_den:
1 # Qden (absj_r a1) <= 1 # Qden (Qred (absj_r a1 * i + ((Qnum (absj_b1 a1) + QDen (absj_b1 a1)) / (QDen (absj_b1 a1)))))).
apply den_r_le_den_r_i_p_b.
assumption.
apply
(Qlt_impl_Qle_red (ones w1 i) (absj_r a1 * i + (((Qnum (absj_b1 a1) + QDen (absj_b1 a1)) / (QDen (absj_b1 a1)))))
(1 # Qden (absj_r a1)) H_den) in H_w1_le_a1.
clear H_den.
rewrite <- H_tmp in H_w1_le_a1.
assert (H_den:
1 # Qden (absj_r a2) <= 1 # Qden (Qred (absj_r a2 * ones w1 i + absj_b1 a2))).
apply den_r_le_den_r_i_p_b.
assumption.
apply
(Qlt_impl_Qle_red (ones w2 (pred (ones w1 i))) (absj_r a2 * ones w1 i + absj_b1 a2)
(1 # Qden (absj_r a2)) H_den) in H_w2_le_a2.
clear H_den.
apply
(Qle_lt_trans
(ones w2 (pred (ones w1 i)))
(Qred (absj_r a2 * ones w1 i + absj_b1 a2) - (1 # Qden (absj_r a2)))
(absj_r a1 * absj_r a2 * i + (absj_b1 a1 * absj_r a2 + absj_b1 a2 + epsilon)));
auto.
apply (Qle_lt_trans
(Qred (absj_r a2 * ones w1 i + absj_b1 a2) - (1 # Qden (absj_r a2)))
(Qred (absj_r a2 * (Qred (absj_r a1 * i + absj_b1 a1 + 1) - (1 # Qden (absj_r a1))) + absj_b1 a2) - (1 # Qden (absj_r a2)))
(absj_r a1 * absj_r a2 * i + (absj_b1 a1 * absj_r a2 + absj_b1 a2 + epsilon))).
apply Qplus_le_compat; try solve [ apply Qle_refl ].
repeat rewrite Qred_correct.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
repeat rewrite (Qmult_comm (absj_r a2)).
apply Qmult_le_compat_r.
2: (destruct H_wf_a2; auto).
rewrite Qred_correct in H_w1_le_a1.
assumption.
repeat rewrite Qred_correct.
assert (H_aux:
absj_r a2 * (absj_r a1 * i + absj_b1 a1 + 1 - (1 # Qden (absj_r a1))) +
absj_b1 a2 - (1 # Qden (absj_r a2))
==
(absj_r a1 * absj_r a2 * i + absj_b1 a1 * absj_r a2 + absj_b1 a2)
+ (absj_r a2 * (1 - (1 # Qden (absj_r a1))) - (1 # Qden (absj_r a2)))).
ring.
rewrite H_aux; clear H_aux.
assert (H_aux:
absj_r a1 * absj_r a2 * i + (absj_b1 a1 * absj_r a2 + absj_b1 a2 + epsilon) ==
(absj_r a1 * absj_r a2 * i + absj_b1 a1 * absj_r a2 + absj_b1 a2) + epsilon).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_lt_compat_l.
rewrite H_epsilon.
assert (H_aux:
(1 - (1 # Qden (absj_r a1))) * (absj_r a2 - (1 # Qden (absj_r a2))) ==
absj_r a2 * (1 - (1 # Qden (absj_r a1))) - (1 # Qden (absj_r a2)) * (1 - (1 # Qden (absj_r a1)))).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_lt_compat_l.
apply Qround.Qopp_lt_compat.
rewrite <- (Qmult_1_r (1 # Qden (absj_r a2))) at 2.
repeat rewrite (Qmult_comm (1 # Qden (absj_r a2))).
apply Qmult_lt_compat_r.
unfold Qlt; simpl; ring_simplify; simpl; auto with zarith.
apply <- Qlt_minus_iff.
assert (H_aux:
1 + - (1 - (1 # Qden (absj_r a1))) ==
1 # Qden (absj_r a1)).
ring.
rewrite H_aux; clear H_aux.
unfold Qlt; simpl; ring_simplify; simpl; auto with zarith.
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 absj_b0_neg_impl_ones_ge_a:
forall (w:ibw) (a:abstractionj),
forall H_wf_a: well_formed_abstractionj a,
forall H_flo: absj_b0 a <= 0,
forall H_a_eq_absj_w: in_abstractionj w a,
forall i:nat,
ones w i >= absj_r a * i + absj_b0 a.
Proof.
induction i.
assert (H_aux: absj_r a * 0 == 0).
ring.
rewrite H_aux; clear H_aux.
assert (H_aux: 0 + absj_b0 a == absj_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:
absj_r a * (i + 1) + absj_b0 a ==
absj_r a * i + absj_b0 a + absj_r a).
ring.
rewrite H_aux; clear H_aux.
apply Qplus_le_compat; try solve [ elim H_wf_a; auto ].
intro H_w.
unfold in_abstractionj in H_a_eq_absj_w.
assert (H_S_i_ge_1:(S i >= 1)%nat).
auto with arith.
generalize (H_a_eq_absj_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.
replace (pred (S i)) with i; auto.
rewrite ones_S_i_eq_ones_i; auto.
Qed.
Lemma on_w1_w2_ge_on_a1_a2:
forall (w1:ibw) (w2:ibw),
forall (a1:abstractionj) (a2:abstractionj),
forall H_wf_a1: well_formed_abstractionj a1,
forall H_flo_a1: absj_b0 a1 <= 0,
forall H_wf_a2: well_formed_abstractionj a2,
forall H_flo_a2: absj_b0 a2 <= 0,
forall (H_a1_eq_absj_w1: in_abstractionj w1 a1),
forall (H_a2_eq_absj_w2: in_abstractionj w2 a2),
forall i,
forall (H_on: on w1 w2 i = false),
absj_r a1 * absj_r a2 * i + (absj_b0 a1 * absj_r a2 + absj_b0 a2)
<= ones (on w1 w2) i.
Proof.
intros.
rewrite ones_on_def.
generalize (absj_b0_neg_impl_ones_ge_a H_wf_a1 H_flo_a1 H_a1_eq_absj_w1 i).
intro H_w1_ge_a1.
generalize (absj_b0_neg_impl_ones_ge_a H_wf_a2 H_flo_a2 H_a2_eq_absj_w2 (ones w1 i)).
intro H_w2_ge_a2.
apply
(Qle_trans
(absj_r a1 * absj_r a2 * i + (absj_b0 a1 * absj_r a2 + absj_b0 a2))
(absj_r a2 * ones w1 i + absj_b0 a2)
(ones w2 (ones w1 i))); auto.
rewrite Qplus_assoc.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
assert (H_r2_pos: 0 <= absj_r a2);
destruct H_wf_a2; auto.
generalize
(Qmult_le_compat_r
(absj_r a1 * i + absj_b0 a1)
(ones w1 i)
(absj_r a2)
H_w1_ge_a1
H_r2_pos).
intro H_cc.
rewrite Qmult_plus_distr_l in H_cc.
assert (H_aux: absj_r a1 * i * absj_r a2 == absj_r a1 * absj_r a2 * i).
ring.
rewrite H_aux in H_cc; clear H_aux.
assert (H_aux: ones w1 i * absj_r a2 == absj_r a2 * ones w1 i).
ring.
rewrite H_aux in H_cc; clear H_aux.
exact H_cc.
Qed.
Property on_absj_alt_correctness_aux:
forall (w1:ibw) (w2:ibw),
forall (a1:abstractionj) (a2:abstractionj),
forall H_wf_a1: well_formed_abstractionj a1,
forall H_wf_a2: well_formed_abstractionj a2,
forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
forall H_wf_b1_1: Qden (absj_b1 a1) = Qden (absj_r a1),
forall H_wf_b1_2: Qden (absj_b1 a2) = Qden (absj_r a2),
in_abstractionj (on w1 w2) (on_absj_alt a1 a2).
Proof.
intros.
assert (H_aux:
exists a1_0,
(absj_b1 a1_0 == absj_b1 a1) /\
(absj_b0 a1_0 == 0) /\
(absj_r a1_0 == absj_r a1)).
exists (absjmake (absj_b1 a1) 0 (absj_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_abstractionj a1_0).
unfold well_formed_abstractionj.
destruct H_a1_0.
destruct H0.
rewrite H1.
assumption.
assert (H_absj_b01_0: absj_b0 a1_0 <= 0).
destruct H_a1_0.
destruct H0.
rewrite H0.
eapply Qle_refl.
assert (H_aux:
exists a2_0,
(absj_b1 a2_0 == absj_b1 a2) /\
(absj_b0 a2_0 == 0) /\
(absj_r a2_0 == absj_r a2)).
exists (absjmake (absj_b1 a2) 0 (absj_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_abstractionj a2_0).
unfold well_formed_abstractionj.
destruct H_a2_0.
destruct H0.
rewrite H1.
assumption.
assert (H_absj_b02_0: absj_b0 a2_0 <= 0).
destruct H_a2_0.
destruct H0.
rewrite H0.
eapply Qle_refl.
unfold in_abstractionj.
intros.
split.
intro H_on.
simpl.
pose (epsilon :=
(1 - (1 # Qden (absj_r a1))) * (absj_r a2 - (1 # Qden (absj_r a2)))).
assert (H_epsilon:
epsilon == (1 - (1 # Qden (absj_r a1))) * (absj_r a2 - (1 # Qden (absj_r a2)))).
apply Qeq_refl.
rewrite <- H_epsilon.
eapply on_w1_w2_lt_on_a1_a2; assumption.
intro H_on.
elim (Q_dec (absj_b0 a1) 0);
elim (Q_dec (absj_b0 a2) 0).
intros H_aux1 H_aux2.
elim H_aux1;
elim H_aux2.
clear H_aux1 H_aux2.
intros H_absj_b01 H_absj_b02.
elim (Qlt_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qlt_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
rewrite ones_pred_i_eq_ones_i; auto.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (absj_b0 a1) 0 H_absj_b01)
H_wf_a2 (Qlt_le_weak (absj_b0 a2) 0 H_absj_b02)
H_a1_eq_absj_w1 H_a2_eq_absj_w2);
auto.
clear H_aux1 H_aux2.
intros H_absj_b01 H_absj_b02.
elim (Qgt_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qlt_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
assert (H_a1_0_eq_absj_w1: in_abstractionj w1 a1_0).
assert (H_a1_in_a1_0: absj_included_test a1 a1_0).
apply absj_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_absj_w1).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_absj_b01_0
H_wf_a2 (Qlt_le_weak (absj_b0 a2) 0 H_absj_b02)
H_a1_0_eq_absj_w1 H_a2_eq_absj_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
rewrite ones_pred_i_eq_ones_i; auto.
clear H_aux1 H_aux2.
intros H_absj_b01 H_absj_b02.
elim (Qlt_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qgt_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
assert (H_a2_0_eq_absj_w2: in_abstractionj w2 a2_0).
assert (H_a2_in_a2_0: absj_included_test a2 a2_0).
apply absj_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_absj_w2).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (absj_b0 a1) 0 H_absj_b01)
H_wf_a2_0 H_absj_b02_0
H_a1_eq_absj_w1 H_a2_0_eq_absj_w2
i H_on).
decompose [and] H_a2_0.
rewrite H2, H1.
rewrite ones_pred_i_eq_ones_i; auto.
clear H_aux1 H_aux2.
intros H_absj_b01 H_absj_b02.
elim (Qgt_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qgt_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
assert (H_a1_0_eq_absj_w1: in_abstractionj w1 a1_0).
assert (H_a1_in_a1_0: absj_included_test a1 a1_0).
apply absj_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_absj_w1).
assert (H_a2_0_eq_absj_w2: in_abstractionj w2 a2_0).
assert (H_a2_in_a2_0: absj_included_test a2 a2_0).
apply absj_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_absj_w2).
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_absj_b01_0
H_wf_a2_0 H_absj_b02_0
H_a1_0_eq_absj_w1 H_a2_0_eq_absj_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
decompose [and] H_a2_0.
rewrite H5, H4.
rewrite ones_pred_i_eq_ones_i; auto.
intros H_absj_b02 H_aux.
elim H_aux.
clear H_aux.
intro H_absj_b01.
elim (Qlt_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qeq_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
assert (H_absj_b02_le_0: absj_b0 a2 <= 0).
rewrite H_absj_b02.
apply Qle_refl.
rewrite ones_pred_i_eq_ones_i; auto.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 (Qlt_le_weak (absj_b0 a1) 0 H_absj_b01)
H_wf_a2 H_absj_b02_le_0
H_a1_eq_absj_w1 H_a2_eq_absj_w2);
auto.
clear H_aux.
intro H_absj_b01.
elim (Qgt_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qeq_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
assert (H_a1_0_eq_absj_w1: in_abstractionj w1 a1_0).
assert (H_a1_in_a1_0: absj_included_test a1 a1_0).
apply absj_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_absj_w1).
assert (H_absj_b02_le_0: absj_b0 a2 <= 0).
rewrite H_absj_b02.
apply Qle_refl.
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1_0 H_absj_b01_0
H_wf_a2 H_absj_b02_le_0
H_a1_0_eq_absj_w1 H_a2_eq_absj_w2
i H_on).
decompose [and] H_a1_0.
rewrite H2, H1.
rewrite ones_pred_i_eq_ones_i; auto.
intros H_aux H_absj_b01.
elim H_aux.
clear H_aux.
intro H_absj_b02.
elim (Qeq_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qlt_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
assert (H_absj_b01_le_0: absj_b0 a1 <= 0).
rewrite H_absj_b01.
apply Qle_refl.
rewrite ones_pred_i_eq_ones_i; auto.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_absj_b01_le_0
H_wf_a2 (Qlt_le_weak (absj_b0 a2) 0 H_absj_b02)
H_a1_eq_absj_w1 H_a2_eq_absj_w2);
auto.
clear H_aux.
intro H_absj_b02.
elim (Qeq_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qgt_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp.
rewrite H_absj_b02_eq_cmp.
assert (H_a2_0_eq_absj_w2: in_abstractionj w2 a2_0).
assert (H_a2_in_a2_0: absj_included_test a2 a2_0).
apply absj_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_absj_w2).
assert (H_absj_b01_le_0: absj_b0 a1 <= 0).
rewrite H_absj_b01.
apply Qle_refl.
generalize
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_absj_b01_le_0
H_wf_a2_0 H_absj_b02_0
H_a1_eq_absj_w1 H_a2_0_eq_absj_w2
i H_on).
decompose [and] H_a2_0.
rewrite H2, H1.
rewrite ones_pred_i_eq_ones_i; auto.
intros H_absj_b02 H_absj_b01.
elim (Qeq_alt (absj_b0 a1) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b01).
clear H_aux1 H_aux2.
intro H_absj_b01_eq_cmp.
elim (Qeq_alt (absj_b0 a2) 0).
intros H_aux1 H_aux2.
generalize (H_aux1 H_absj_b02).
clear H_aux1 H_aux2.
intro H_absj_b02_eq_cmp.
simpl.
rewrite H_absj_b01_eq_cmp, H_absj_b02_eq_cmp.
assert (H_absj_b01_le_0: absj_b0 a1 <= 0).
rewrite H_absj_b01.
apply Qle_refl.
assert (H_absj_b02_le_0: absj_b0 a2 <= 0).
rewrite H_absj_b02.
apply Qle_refl.
rewrite ones_pred_i_eq_ones_i; auto.
apply
(on_w1_w2_ge_on_a1_a2
H_wf_a1 H_absj_b01_le_0
H_wf_a2 H_absj_b02_le_0
H_a1_eq_absj_w1 H_a2_eq_absj_w2
i H_on).
Qed.
Property on_absj_correctness_aux:
forall (w1:ibw) (w2:ibw),
forall (a1:abstractionj) (a2:abstractionj),
forall H_wf_a1: well_formed_abstractionj a1,
forall H_wf_a2: well_formed_abstractionj a2,
forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
in_abstractionj (on w1 w2) (on_absj a1 a2).
Proof.
intros.
unfold on_absj.
apply on_absj_alt_correctness_aux; auto;
try solve [
apply absj_std_well_formed_abstractionj_compat; auto];
try solve [
apply absj_std_in_abstractionj_compat; auto].
rewrite absj_std_red.
simpl.
rewrite Pmult_comm.
reflexivity.
rewrite absj_std_red.
simpl.
rewrite Pmult_comm.
reflexivity.
Qed.
Property on_absj_alt_well_formed_abstractionj_compat:
forall a1 a2: abstractionj,
forall H_wf1: well_formed_abstractionj a1,
forall H_wf2: well_formed_abstractionj a2,
well_formed_abstractionj (on_absj_alt a1 a2).
Proof.
intros.
unfold well_formed_abstractionj.
simpl.
destruct H_wf1 as [Ha1_0 Ha1_1].
destruct H_wf2 as [Ha2_0 Ha2_1].
split.
apply Qmult_le_0_compat; assumption.
apply (Qle_trans
(absj_r a1 * absj_r a2)
(1 * absj_r a2)
1); try solve [ ring_simplify; auto ].
apply Qmult_le_compat_r; auto.
Qed.
End on_properties.
Section not_properties.
Property not_absj_correctness_aux:
forall w: ibw,
forall a:abstractionj,
forall H_wf_a: well_formed_abstractionj a,
forall H_a_eq_absj_w: in_abstractionj w a,
forall H_wf_b1: Qden (absj_b1 a) = Qden (absj_r a),
in_abstractionj (not w) (not_absj a).
Proof.
intros.
unfold in_abstractionj.
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.
rewrite ones_not_def.
assert (H_aux: (i' - ones w i')%nat == i' - ones w i').
apply minus_impl_Qminus.
apply ones_i_le_i.
rewrite H_aux; clear H_aux.
pose (H_tmp:= H_a_eq_absj_w (S i') H_i_ge_1).
elim H_tmp; clear H_tmp.
intros H_true H_false.
simpl in H_true, H_false.
split.
intro H_not_w.
simpl.
assert (H_w: w (S i') = false).
case_eq (w (S i')); auto.
intro H_w.
simpl in H_not_w.
rewrite H_w in H_not_w.
simpl in H_not_w; congruence.
pose (H_cc:= H_false H_w).
apply <- Qlt_minus_iff.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
(1 - absj_r a) * (i' + 1) + (- absj_b0 a - (1 - (1 # Qden (absj_r a)))) + - (i' - ones w i') ==
ones w i' + (1 # Qden (absj_r a)) + - (absj_r a * (i' + 1) + absj_b0 a)).
ring.
rewrite H_aux; clear H_aux.
apply -> Qlt_minus_iff.
rewrite n_plus_1_eq_S_n.
apply Qle_impl_Qlt; try solve [ exact H_cc ].
compute; reflexivity.
intro H_not_w.
simpl.
assert (H_w: w (S i') = true).
case_eq (w (S i')); auto.
intro H_w.
simpl in H_not_w.
rewrite H_w in H_not_w.
simpl in H_not_w; congruence.
pose (H_cc:= H_true H_w).
apply <- Qle_minus_iff.
rewrite <- n_plus_1_eq_S_n.
assert (H_aux:
i' - ones w i' +
- ((1 - absj_r a) * (i' + 1) + (- absj_b1 a - (1 - (1 # Qden (absj_r a)))))
==
absj_r a * (i' + 1) + absj_b1 a - (1 # Qden (absj_r a)) - ones w i').
ring.
rewrite H_aux; clear H_aux.
apply -> Qle_minus_iff.
rewrite n_plus_1_eq_S_n.
rewrite <- (Qred_correct (absj_r a * S i' + absj_b1 a)).
apply Qlt_impl_Qle_red; auto.
apply den_r_le_den_r_i_p_b; auto.
Qed.
Lemma absj_included_test_not_not_absj:
forall a: abstractionj,
absj_included_test a (not_absj (not_absj a)).
Proof.
intros.
unfold absj_included_test.
repeat split.
simpl.
ring.
simpl.
ring_simplify.
apply Qle_refl.
simpl.
ring_simplify.
apply Qle_refl.
Qed.
Lemma not_not_absj_included_test_absj:
forall a: abstractionj,
absj_included_test (not_absj (not_absj a)) a.
Proof.
intros.
unfold absj_included_test.
repeat split.
simpl.
ring.
simpl.
ring_simplify.
apply Qle_refl.
simpl.
ring_simplify.
apply Qle_refl.
Qed.
Property not_not_absj_equal_absj:
forall a: abstractionj,
absj_equal (not_absj (not_absj a)) a.
Proof.
intros.
apply absj_equiv_test_impl_absj_equal.
split.
apply not_not_absj_included_test_absj.
apply absj_included_test_not_not_absj.
Qed.
Property not_std_correctness:
forall w: ibw,
forall a:abstractionj,
forall H_wf_a: well_formed_abstractionj a,
forall H_a_eq_absj_w: in_abstractionj w a,
in_abstractionj (not w) (not_absj (absj_std a)).
Proof.
intros.
assert (H_wf_std_a: well_formed_abstractionj (absj_std a)).
unfold well_formed_abstractionj.
rewrite absj_std_red.
simpl.
assert (H_aux: (QDen (absj_b1 a) # Qden (absj_b1 a)) == 1).
unfold Qeq.
simpl.
rewrite Pmult_1_r.
reflexivity.
rewrite H_aux; clear H_aux.
rewrite Qmult_1_r.
assumption.
apply not_absj_correctness_aux; auto.
apply (absj_equal_correctness H_wf_a H_wf_std_a); auto.
apply absj_std_correctness.
simpl.
apply Pmult_comm.
Qed.
Property not_absj_well_formed_abstractionj_compat:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj a,
well_formed_abstractionj (not_absj a).
Proof.
intros.
unfold well_formed_abstractionj.
simpl.
destruct H_wf as [H0 H1].
split.
apply -> Qle_minus_iff.
assumption.
apply <- Qle_minus_iff.
ring_simplify.
assumption.
Qed.
Property pre_not_absj_std_well_formed_abstractionj_compat:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj a,
well_formed_abstractionj (absj_std a).
Proof.
intros.
unfold well_formed_abstractionj.
rewrite absj_std_red.
simpl.
assert (H_aux: (QDen (absj_b1 a) # Qden (absj_b1 a)) == 1).
unfold Qeq.
simpl.
rewrite Pmult_1_r.
reflexivity.
rewrite H_aux; clear H_aux.
rewrite Qmult_1_r.
assumption.
Qed.
End not_properties.
Section prec_absj_properties.
Property w_early_prec_a:
forall a: abstractionj,
forall H_wf: well_formed_abstractionj a,
forall w: ibw,
forall H_w_in_a: in_abstractionj 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: abstractionj,
forall H_wf: well_formed_abstractionj a,
forall w: ibw,
forall H_w_in_a: in_abstractionj 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_absj_alt_correctness:
forall a1 a2: abstractionj,
forall H_wf1: well_formed_abstractionj a1,
forall H_wf2: well_formed_abstractionj a2,
forall H_prec_test: prec_absj_alt a1 a2,
prec_absj a1 a2.
Proof.
intros.
unfold prec_absj.
intros.
pose (H_early2_prec_w2:= w_early_prec_a H_wf2 H_w2_in_a2).
unfold prec_absj_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_absj_alt_complet:
forall a1 a2: abstractionj,
forall H_wf1: well_formed_abstractionj a1,
forall H_non_empty1: non_empty a1,
forall H_wf2: well_formed_abstractionj a2,
forall H_non_empty2: non_empty a2,
forall H_prec: prec_absj a1 a2,
prec_absj_alt a1 a2.
Proof.
intros.
unfold prec_absj_alt.
unfold prec_absj in H_prec.
apply H_prec.
apply late_in_abs; auto.
apply early_in_abs; auto.
Qed.
Property prec_absj_test_correctness_aux:
forall a1 a2: abstractionj,
forall H_wf1: well_formed_abstractionj a1,
forall H_wf2: well_formed_abstractionj a2,
forall H_prec_test: prec_absj_test a1 a2,
forall H_sync: absj_r a1 == absj_r a2,
prec_absj a1 a2.
Proof.
intros.
apply prec_absj_alt_correctness; auto.
unfold prec_absj_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 cg_monotone_linear.
unfold prec_absj_test in H_prec_test.
rewrite H_sync.
apply Qplus_le_compat; try solve [ apply Qle_refl ].
assumption.
Qed.
End prec_absj_properties.