Library abstraction_phd_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_phd_def.
Require Import abstraction_phd_aux.

Remark absh_weakening:
  forall a1 a2: abstractionh,
  forall H_one: absh_b1 a1 <= absh_b1 a2,
  forall H_absh_b0: absh_b0 a1 >= absh_b0 a2,
  forall H_r: absh_r a1 == absh_r a2,
  absh_included_test a1 a2.
Proof.
  apply absh_weakening_aux.
Qed.

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

          apply (le_lt_eq_dec) in IHi.
          elim IHi; clear IHi; auto.
          intro H_absurd.
          rewrite H_absurd in *.
          assert (w_early a (S i) = true).
            pose (H:= H_ones_w (S i) H_w).
            simpl in H.
            rewrite H_w in H.
            simpl in H.
            rewrite H_absurd in H.
            rewrite <- ones_early_eq_ones_w_early in H.
            simpl.
            rewrite Qle_alt in H.
            case_eq (S (ones_early a i) ?= absh_r a * S i + absh_b1 a);
              try solve [ intro H_cmp; rewrite S_n_nbeq_n; simpl; reflexivity ].
            intro H_cmp.
            rewrite H_cmp in H.
            congruence.
          congruence.

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

    intros w_min H_w_min.
    apply (H_w_min (w_early a)).
    intros i H_w_early.
    rewrite <- ones_early_eq_ones_w_early.
    case_eq i.
      intro H_i;
      rewrite H_i in *.
      simpl in *.
      congruence.
      intros i' H_i; rewrite H_i in *.
      simpl.
      simpl in H_w_early.
      case_eq (S (ones_early a i') ?= absh_r a * S i' + absh_b1 a);
        try solve [
          intro H_cmp; rewrite H_cmp in H_w_early;
          rewrite <- beq_nat_refl in H_w_early; simpl in H_w_early; congruence ].
        intro H_cmp.
        rewrite <- Qeq_alt in H_cmp.
        rewrite H_cmp; auto.
        apply Qle_refl.

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

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

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

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

          intro H_w_late.
          rewrite ones_S_i_eq_ones_i; auto.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Property ones_late_alt_correctness:
  forall a: abstractionh,
  forall H_wf: well_formed_abstractionh a,
  forall i,
  ones_late a i = ones_late_alt a i.
Proof.
  apply ones_late_eq_ones_late_alt.
Qed.

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

Property absh_included_test_correctness:
  forall a1 a2: abstractionh,
  absh_included_test a1 a2 -> absh_included a1 a2.
Proof.
  apply absh_included_test_impl_absh_included.
Qed.


Property on_absh_correctness:
  forall (w1:ibw) (w2:ibw),
  forall (a1:abstractionh) (a2:abstractionh),
  forall H_wf_a1: well_formed_abstractionh a1,
  forall H_wf_a2: well_formed_abstractionh a2,
  forall H_a1_eq_absh_w1: in_abstractionh w1 a1,
  forall H_a2_eq_absh_w2: in_abstractionh w2 a2,
  in_abstractionh (on w1 w2) (on_absh a1 a2).
Proof.
  apply on_absh_correctness_aux.
Qed.


Property not_absh_correctness:
  forall w: ibw,
  forall a:abstractionh,
  forall H_wf_a: well_formed_abstractionh a,
  forall H_a_eq_absh_w: in_abstractionh w a,
  in_abstractionh (not w) (not_absh a).
Proof.
  apply not_absh_correctness_aux.
Qed.


Property prec_absh_equiv_prec_absh_alt:
  forall a1 a2: abstractionh,
  forall H_wf1: well_formed_abstractionh a1,
  forall H_wf2: well_formed_abstractionh a2,
  forall H_non_empty1: non_empty a1,
  forall H_non_empty2: non_empty a2,
   prec_absh a1 a2 <-> prec_absh_alt a1 a2.
Proof.
  intros.
  split; intros.
  apply prec_absh_alt_complet; auto.
  apply prec_absh_alt_correctness; auto.
Qed.

Property prec_absh_test_correctness:
  forall a1 a2: abstractionh,
  forall H_wf1: well_formed_abstractionh a1,
  forall H_wf2: well_formed_abstractionh a2,
  sync_absh_test a1 a2 -> prec_absh_test a1 a2 -> prec_absh a1 a2.
Proof.
  intros.
  apply prec_absh_test_correctness_aux; auto.
Qed.


Property sync_absh_equiv_sync_absh_test:
  forall a1 a2: abstractionh,
  forall H_swf_a1: strong_well_formed_abstractionh a1,
  forall H_swf_a2: strong_well_formed_abstractionh a2,
  forall H_non_empty_1: non_empty a1,
  forall H_non_empty_2: non_empty a2,
  sync_absh a1 a2 <-> sync_absh_test a1 a2.
Proof.
  intros.
  split; intros.
    apply sync_absh_test_completeness; assumption.
    apply sync_absh_test_correctness; assumption.
Qed.


Property subtyping_absh_equiv_subtyping_absh_alt:
  forall a1 a2: abstractionh,
  subtyping_absh_alt a1 a2 <-> subtyping_absh a1 a2.
Proof.
  intros.
  split; intros.
  apply subtyping_absh_alt_impl_subtyping_absh; auto.
  apply subtyping_absh_impl_subtyping_absh_alt; auto.
Qed.


Property size_absh_correctness:
  forall (w1:ibw) (w2:ibw),
  forall a1 a2: abstractionh,
  forall H_swf_a1: strong_well_formed_abstractionh a1,
  forall H_swf_a2: strong_well_formed_abstractionh a2,
  forall H_non_empty_1: non_empty a1,
  forall H_non_empty_2: non_empty a2,
  forall (H_a1_eq_absh_w1: in_abstractionh w1 a1),
  forall (H_a2_eq_absh_w2: in_abstractionh w2 a2),
  forall H_sub: subtyping_absh a1 a2,
  forall s,
  forall H_size: size w1 w2 s,
  (s <= size_absh a1 a2)%Z.
Proof.
  intros.
  apply
    (size_absh_correctness_aux
      H_swf_a1 H_swf_a2
      H_non_empty_1 H_non_empty_2
      H_a1_eq_absh_w1 H_a2_eq_absh_w2);
    auto.
  apply subtyping_absh_impl_subtyping_absh_alt in H_sub.
  destruct H_sub as [ H_prec H_sync ].
  split; [assumption|].
  apply sync_absh_test_completeness; assumption.
Qed.