Library abstraction_jfla_prop



Set Implicit Arguments.

Require Import Setoid.
Require Import floor.
Require Import Bool.
Require Import Omega.
Require Import ZArith.
Require Import Znumtheory.
Require Import Z_misc.
Require Import QArith.
Require Import Q_misc.
Require Import comparison.
Require Import misc.
Require Import ibw_def.
Require Import ibw_aux.
Require Import ibw_prop.
Require Import abstraction_jfla_def.
Require Import abstraction_jfla_aux.

Remark absj_weakening:
  forall a1 a2: abstractionj,
  forall H_one: absj_b1 a1 <= absj_b1 a2,
  forall H_absj_b0: absj_b0 a1 >= absj_b0 a2,
  forall H_r: absj_r a1 == absj_r a2,
  absj_included_test a1 a2.
Proof.
  apply absj_weakening_aux.
Qed.

Property early_def:
  forall a:abstractionj,
  forall H_wf: well_formed_abstractionj a,
  (forall w: ibw,
    (forall i, w i = true -> ones w (pred i) < absj_r a * i + absj_b1 a) ->
    prec (w_early a) w)
  /\
  (forall w_min:ibw,
    (forall w: ibw,
      (forall i, w i = true -> ones w (pred i) < absj_r a * i + absj_b1 a) ->
      prec w_min w )->
    prec w_min (w_early a)).
Proof.
  intros a H_wf.
  split.
    intros w H_ones_w.
    unfold prec.
    induction i.
      simpl; auto.
      case_eq (w (S i)).
        intro H_w.
        rewrite (ones_S_i_eq_S_ones_i w); auto.
        case_eq (w_early a (S i)).
          intro H_w_early.
          rewrite ones_S_i_eq_S_ones_i; auto.
          apply plus_le_compat_l.
          assumption.
          intro H_w_early.
          rewrite ones_S_i_eq_ones_i; auto.
          simpl.
          apply lt_le_S.

          apply (le_lt_eq_dec) in IHi.
          elim IHi; clear IHi; auto.
          intro H_absurd.
          rewrite H_absurd in *.
          assert (w_early a (S i) = true).
            pose (H:= H_ones_w (S i) H_w).
            simpl in H.
            rewrite H_absurd in H.
            rewrite <- ones_early_eq_ones_w_early in H.
            simpl.
            rewrite Qlt_alt in H.
            rewrite H.
            rewrite S_n_nbeq_n.
            auto.
          congruence.

        intro H_w.
        rewrite (ones_S_i_eq_ones_i w); auto.
        case_eq (w_early a (S i)).
          intro H_w_early.
          rewrite ones_S_i_eq_S_ones_i; simpl; auto.
          intro H_w_early.
          rewrite ones_S_i_eq_ones_i; auto.

    intros w_min H_w_min.
    apply (H_w_min (w_early a)).
    intros i H_w_early.
    rewrite <- ones_early_eq_ones_w_early.
    case_eq i.
      intro H_i;
      rewrite H_i in *.
      simpl in *.
      congruence.
      intros i' H_i; rewrite H_i in *.
      simpl.
      simpl in H_w_early.
      case_eq (ones_early a i' ?= absj_r a * S i' + absj_b1 a);
        try solve [
          intro H_cmp; rewrite H_cmp in H_w_early;
          rewrite <- beq_nat_refl in H_w_early; simpl in H_w_early; congruence ].
      intro H_cmp.
      rewrite <- Qlt_alt in H_cmp.
      assumption.
Qed.

Property late_def:
  forall a:abstractionj,
  forall H_wf: well_formed_abstractionj a,
  (forall w: ibw,
    (forall i, (i > 0)%nat ->
      w i = false -> ones w (pred i) >= absj_r a * i + absj_b0 a) ->
    prec w (w_late a))
  /\
  (forall w_maj:ibw,
    (forall w: ibw,
      (forall i, (i > 0)%nat ->
        w i = false -> ones w (pred i) >= absj_r a * i + absj_b0 a) ->
      prec w w_maj)->
    prec (w_late a) w_maj).
Proof.
  intros a H_wf.
  split.
    intros w H_ones_w.
    unfold prec.
    induction i.
      simpl; auto.
      case_eq (w (S i)).
        intro H_w.
        rewrite (ones_S_i_eq_S_ones_i w); auto.
        case_eq (w_late a (S i)).
          intro H_w_late.
          rewrite ones_S_i_eq_S_ones_i; auto.
          apply plus_le_compat_l.
          assumption.
          intro H_w_late.
          rewrite ones_S_i_eq_ones_i; auto.
          simpl.
          change (ones (w_late a) i <= S (ones w i))%nat.
          apply (le_trans
            (ones (w_late a) i)
            (ones w i)
            (S (ones w i))); auto.

        intro H_w.
        rewrite (ones_S_i_eq_ones_i w); auto.
        case_eq (w_late a (S i)).
          intro H_w_late.
          rewrite ones_S_i_eq_S_ones_i; simpl; auto.

          apply (le_lt_eq_dec) in IHi.
          elim IHi; clear IHi; auto.
          intro H_absurd.
          rewrite H_absurd in *.
          assert (w_late a (S i) = false).
            assert (H_S_i_ge_0: (S i > 0)%nat); auto with arith.
            pose (H:= H_ones_w (S i) H_S_i_ge_0 H_w).
            simpl in H.
            rewrite <- H_absurd in H.
            rewrite <- ones_late_eq_ones_w_late in H.
            simpl.
            rewrite Qle_alt in H.
            case_eq (absj_r a * S i + absj_b0 a ?= ones_late a i); try congruence;
              intro H_cmp; rewrite <- beq_nat_refl; auto.
          congruence.

          intro H_w_late.
          rewrite ones_S_i_eq_ones_i; auto.

    intros w_maj H_w_maj.
    apply (H_w_maj (w_late a)).
    intros i H_i_ge_0 H_w_late.
    rewrite <- ones_late_eq_ones_w_late.
    case_eq i.
      intro H_i;
      rewrite H_i in *.
      absurd ((0 > 0)%nat); auto with arith.
      intros i' H_i; rewrite H_i in *.
      simpl.
      simpl in H_w_late.
      case_eq (absj_r a * S i' + absj_b0 a ?= ones_late a i').
        intro H_cmp.
        rewrite <- Qeq_alt in H_cmp.
        rewrite H_cmp.
        apply Qle_refl.

        intro H_cmp.
        rewrite <- Qlt_alt in H_cmp.
        apply Qlt_le_weak.
        assumption.

        intro H_cmp; rewrite H_cmp in H_w_late.
        rewrite S_n_nbeq_n in H_w_late; simpl in H_w_late; congruence.
Qed.

Property early_prec_w:
  forall w: ibw,
  forall a: abstractionj,
  forall H_wf_a: well_formed_abstractionj a,
  in_abstractionj w a -> prec (w_early a) w.
Proof.
  intros w a H_wf_a H_w_in_a.
  unfold prec.
  intros i.
  rewrite <- ones_early_eq_ones_w_early.
  apply ones_w_le_ones_early; auto.
Qed.

Property w_prec_late:
  forall w: ibw,
  forall a: abstractionj,
  forall H_wf_a: well_formed_abstractionj a,
  in_abstractionj w a -> prec w (w_late a).
Proof.
  intros w a H_wf_a H_w_in_a.
  unfold prec.
  intros i.
  rewrite <- ones_late_eq_ones_w_late.
  apply ones_late_le_ones_w; auto.
Qed.

Property non_empty_impl_early_prec_late:
  forall a: abstractionj,
  forall H_wf: well_formed_abstractionj a,
  non_empty a -> prec (w_early a) (w_late a).
Proof.
  intros a H_wf H_non_empty.
  unfold prec.
  intros i.
  rewrite <- ones_early_eq_ones_w_early.
  rewrite <- ones_late_eq_ones_w_late.
  apply non_empty_impl_ones_late_le_ones_early; auto.
Qed.

Lemma early_prec_late_impl_early_in_a:
  forall a: abstractionj,
  prec (w_early a) (w_late a) -> in_abstractionj (w_early a) a.
Proof.
  intros a H_prec.
  unfold prec in H_prec.
  apply ones_late_le_ones_early_impl_early_in_a.
  intros.
  rewrite ones_early_eq_ones_w_early.
  rewrite ones_late_eq_ones_w_late.
  exact (H_prec i).
Qed.

Lemma early_prec_late_impl_late_in_a:
  forall a: abstractionj,
  prec (w_early a) (w_late a) -> in_abstractionj (w_late a) a.
Proof.
  intros a H_prec.
  unfold prec in H_prec.
  apply ones_late_le_ones_early_impl_late_in_a.
  intros.
  rewrite ones_early_eq_ones_w_early.
  rewrite ones_late_eq_ones_w_late.
  exact (H_prec i).
Qed.

Lemma early_prec_late_impl_early_late_in_a:
  forall a: abstractionj,
  prec (w_early a) (w_late a) ->
  (in_abstractionj (w_early a) a /\ in_abstractionj (w_late a) a).
Proof.
  intros.
  split.
  apply early_prec_late_impl_early_in_a; auto.
  apply early_prec_late_impl_late_in_a; auto.
Qed.

Property early_prec_late_impl_non_empty:
  forall a: abstractionj,
  forall H_wf: well_formed_abstractionj a,
  prec (w_early a) (w_late a) -> non_empty a.
Proof.
  intros a H_wf H_prec.
  unfold prec in H_prec.
  apply ones_late_le_ones_early_impl_non_empty; auto.
  intro i.
  rewrite ones_early_eq_ones_w_early.
  rewrite ones_late_eq_ones_w_late.
  exact (H_prec i).
Qed.

Lemma early_is_infimum:
  forall a: abstractionj,
  forall H_wf: well_formed_abstractionj a,
  prec (w_early a) (w_late a) ->
  (forall w:ibw, in_abstractionj w a -> prec (w_early a) w)
  /\
  (forall w_min: ibw, (forall w, in_abstractionj w a -> prec w_min w) -> prec w_min (w_early a)).
Proof.
  intros a H_wf H_prec.
  split; intros H.
  apply early_prec_w; auto.
  assert (H_early_in_a: in_abstractionj (w_early a) a).
    apply early_prec_late_impl_early_in_a; auto.
  intros H1.
  exact (H1 (w_early a) H_early_in_a).
Qed.

Lemma late_is_supremum:
  forall a: abstractionj,
  forall H_wf: well_formed_abstractionj a,
  prec (w_early a) (w_late a) ->
  (forall w:ibw, in_abstractionj w a -> prec w (w_late a))
  /\
  (forall w_maj: ibw, (forall w:ibw, in_abstractionj w a -> prec w w_maj) -> prec (w_late a) w_maj).
Proof.
  intros a H_wf H_prec.
  split; intros H.
  apply w_prec_late; auto.
  assert (H_late_in_a: in_abstractionj (w_late a) a).
    apply early_prec_late_impl_late_in_a; auto.
  intros H1.
  exact (H1 (w_late a) H_late_in_a).
Qed.

Property early_prec_late_impl_non_empty_and_early_is_infimum_and_late_is_supremum:
  forall a: abstractionj,
  forall H_wf: well_formed_abstractionj a,
  prec (w_early a) (w_late a) ->
  (non_empty a)
  /\
  ((forall w:ibw, in_abstractionj w a -> prec (w_early a) w)
   /\
   (forall w_min: ibw, (forall w, in_abstractionj w a -> prec w_min w) -> prec w_min (w_early a)))
  /\
  ((forall w:ibw, in_abstractionj w a -> prec w (w_late a))
   /\
   (forall w_maj: ibw, (forall w:ibw, in_abstractionj w a -> prec w w_maj) -> prec (w_late a) w_maj)).
Proof.
  intros.
  split.
  apply early_prec_late_impl_non_empty; auto.
  split.
  apply early_is_infimum; auto.
  apply late_is_supremum; auto.
Qed.

Property non_empty_equiv_early_prec_late:
  forall a: abstractionj,
  forall H_wf: well_formed_abstractionj a,
  non_empty a <-> prec (w_early a) (w_late a).
Proof.
  intros.
  split.
  apply non_empty_impl_early_prec_late; auto.
  apply early_prec_late_impl_non_empty; auto.
Qed.

Property ones_early_alt_correctness:
  forall a: abstractionj,
  forall H_wf: well_formed_abstractionj a,
  forall i,
  ones_early a i = ones_early_alt a i.
Proof.
  apply ones_early_eq_ones_early_alt.
Qed.

Property non_empty_test_correctness:
  forall a,
  forall H_wf: well_formed_abstractionj a,
  forall H_non_empty: non_empty_test a,
  non_empty a.
Proof.
  intros.
  apply ones_late_le_ones_early_impl_non_empty; auto.
  intros.
  apply non_empty_test_impl_ones_late_le_ones_early; auto.
Qed.

Property absj_included_test_correctness:
  forall a1 a2: abstractionj,
  absj_included_test a1 a2 -> absj_included a1 a2.
Proof.
  apply absj_included_test_impl_absj_included.
Qed.


Property on_absj_alt_correctness:
  forall (w1:ibw) (w2:ibw),
  forall (a1:abstractionj) (a2:abstractionj),
  forall H_wf_a1: well_formed_abstractionj a1,
  forall H_wf_a2: well_formed_abstractionj a2,
  forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
  forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
  forall H_wf_b1_1: Qden (absj_b1 a1) = Qden (absj_r a1),
  forall H_wf_b1_2: Qden (absj_b1 a2) = Qden (absj_r a2),
  in_abstractionj (on w1 w2) (on_absj_alt a1 a2).
Proof.
  apply on_absj_alt_correctness_aux.
Qed.

Property on_absj_correctness:
  forall w1 w2:ibw,
  forall a1 a2:abstractionj,
  forall H_wf_a1: well_formed_abstractionj a1,
  forall H_wf_a2: well_formed_abstractionj a2,
  forall H_a1_eq_absj_w1: in_abstractionj w1 a1,
  forall H_a2_eq_absj_w2: in_abstractionj w2 a2,
  in_abstractionj (on w1 w2) (on_absj a1 a2).
Proof.
  apply on_absj_correctness_aux.
Qed.


Property not_absj_correctness:
  forall w: ibw,

  forall a:abstractionj,
  forall H_wf_a: well_formed_abstractionj a,
  forall H_a_eq_absj_w: in_abstractionj w a,
  forall H_wf_b1: Qden (absj_b1 a) = Qden (absj_r a),
  in_abstractionj (not w) (not_absj a).
Proof.
  apply not_absj_correctness_aux.
Qed.


Property prec_absj_equiv_prec_absj_alt:
  forall a1 a2: abstractionj,
  forall H_wf1: well_formed_abstractionj a1,
  forall H_wf2: well_formed_abstractionj a2,
  forall H_non_empty1: non_empty a1,
  forall H_non_empty2: non_empty a2,
   prec_absj a1 a2 <-> prec_absj_alt a1 a2.
Proof.
  intros.
  split; intros.
  apply prec_absj_alt_complet; auto.
  apply prec_absj_alt_correctness; auto.
Qed.

Property prec_absj_test_correctness:
  forall a1 a2: abstractionj,
  forall H_wf1: well_formed_abstractionj a1,
  forall H_wf2: well_formed_abstractionj a2,
  sync_absj_test a1 a2 -> prec_absj_test a1 a2 -> prec_absj a1 a2.
Proof.
  intros.
  apply prec_absj_test_correctness_aux; auto.
Qed.