Library mcertikos.layerlib.ListLemma2

Require Import Arith.
Require Import Omega.
Require Export List.
Require Import ZArith.
Require Import ListLemma.
Require Import GlobalOracle.
Require Import Coqlib.

Lemma list_prefix_nil:
  ∀ {A:Type} (i: A) q q0 q1,
    ¬ In i q →
    q ++ i :: q0 = i :: q1 →
    q = nil.
Proof.
  intros.
  destruct q.
  + auto.
  + simpl in ×.
    injection H0;intros.
    contradict H. auto.
Qed.

Lemma list_In_middle:
  ∀ {A: Type} (i: A) q q0,
    In i (q ++ i :: q0).
Proof.
  induction q; simpl; intros; auto.
Qed.

Lemma list_valid_In_append:
  ∀ a curid l,
    (∀ i0 e, In (TEVENT i0 e) (a :: l) → i0 ≠ curid) →
    (∀ i0 e, In (TEVENT i0 e) l → i0 ≠ curid).
Proof.
  intros.
  apply (H i0 e).
  right.
  auto.
Qed.

Lemma list_valid_In_append´:
  ∀ a l P,
    (∀ i0 e, In (TEVENT i0 e) (a :: l) → P i0 e) →
    (∀ i0 e, In (TEVENT i0 e) l → P i0 e).
Proof.
  intros; eauto. eapply X.
  right. trivial.
Qed.

Lemma list_append_trans:
  ∀ {A: Type} (i: A) l0 l,
    i :: (l0 ++ l) = (i::l0) ++ l.
Proof.
  reflexivity.
Qed.

Lemma list_append_neq0:
  ∀ {A: Type} l (a: A),
    l = a :: l → False.
Proof.
  induction l; intros.
  - inv H.
  - inversion H. eauto.
Qed.

Lemma list_append_neq:
  ∀ {A: Type} l l´ (a: A),
    l = l´ ++ a :: l → False.
Proof.
  induction l; intros.
  - destruct l´; inv H.
  - destruct l´; inversion H.
    + eapply list_append_neq0 in H2; eauto.
    + specialize (IHl (l´ ++ a0 :: nil) a1). eapply IHl.
      rewrite <- app_assoc.
      rewrite <- app_comm_cons.
      rewrite app_nil_l. assumption.
Qed.

Lemma list_append_neq´:
  ∀ {A: Type} (l l´: list A),
    l = l´ ++ l → l´ = nil.
Proof.
  destruct l; intros.
  - rewrite app_nil_r in H. congruence.
  - destruct l´; trivial.
    inversion H. clear H.
    eapply list_append_neq in H2. inv H2.
Qed.

Lemma list_append_e_eq:
  ∀ {A : Type} l0 l (e e0: A),
    l0 ++ e :: l = e0 :: l →
    l0 = nil ∧ e = e0.
Proof.
  induction l0; intros.
  - inv H. eauto.
  - inversion H.
    symmetry in H2.
    apply list_append_neq in H2. inv H2.
Qed.

Lemma list_not_e_nil:
  ∀ {A:Type} (e: A) l l´,
    l ++ e :: l´ ≠ nil.
Proof.
  destruct l.
  - intros l´ HF. inv HF.
  - intros l´ HF. inv HF.
Qed.

Lemma list_same_tail:
  ∀ {A : Type} l0 l1 (i j: A),
    l0 ++ i :: nil = l1 ++ j :: nil →
    l0 = l1 ∧ i = j.
Proof.
  induction l0; simpl; intros.
  - destruct l1.
    + inv H. auto.
    + inv H. symmetry in H2.
      eapply list_not_e_nil in H2. inv H2.
  - destruct l1.
    + inv H. eapply list_not_e_nil in H2. inv H2.
    + inv H. exploit IHl0; eauto.
      intros (? & ?); subst.
      auto.
Qed.

Lemma list_append_rewrite:
  ∀ {A: Type} l (a b: A),
    a :: b :: l = (a:: nil) ++ (b :: l).
Proof.
  intros.
  rewrite <- app_comm_cons. trivial.
Qed.

Lemma list_tail_one_element:
  ∀ {A : Type} l2 l0 l1 (i j: A)
         (Heq: l0 ++ i :: nil = l1 ++ j :: l2),
    (i = j ∧ l2 = nil) ∨
    (∃ l2´, l0 = l1 ++ j :: l2´).
Proof.
  induction l2; simpl; intros.
  - eapply list_same_tail in Heq.
    destruct Heq as (? & ?); subst.
    left; auto.
  - right. rewrite list_append_rewrite in Heq.
    rewrite app_assoc in Heq.
    exploit IHl2; eauto.
    intros HF.
    destruct HF as [(? & ?) | HF´]; subst.
    + eapply list_same_tail in Heq.
      destruct Heq as (? & _); subst.
      eauto.
    + destruct HF´ as (l2´ & HF´).
      rewrite <- app_assoc in HF´.
      rewrite <- app_comm_cons in HF´.
      eauto.
Qed.

Lemma list_unique_element:
  ∀ {A: Type} q q´ q0 q1 (z: A)
         (Heq: q ++ z :: q0 = q´ ++ z :: q1)
         (Hnin: ¬ In z q)
         (Hnin0: ¬ In z q0),
    q = q´ ∧ q0 = q1.
Proof.
  induction q; simpl; intros.
  - destruct q´.
    + inv Heq. auto.
    + inv Heq. elim Hnin0.
      eapply list_In_middle; eauto.
  - destruct q´.
    + inv Heq. elim Hnin. left; trivial.
    + inv Heq. exploit IHq; eauto.
      intros (? & ?); subst. auto.
Qed.

Lemma list_not_in_append_re:
  ∀ {A: Type} (i: A) i0 l,
    ¬ In i (i0 :: l) →
    ¬ In i l.
Proof.
  intros.
  simpl in H.
  tauto.
Qed.

Lemma list_not_in_append:
  ∀ {A: Type} (i: A) i0 l,
    ¬ In i l →
    i0 ≠ i →
    ¬ In i (i0 :: l).
Proof.
  intros.
  simpl.
  tauto.
Qed.


  Lemma NoDup_app : ∀ A (xs ys : list A),
    NoDup (xs++ys)
     ↔ (NoDup xs ∧ NoDup ys
          ∧ (∀ x, ¬ (In x xs ∧ In x ys))).
  Proof.
    induction xs.
    + simpl.
      intros.
      intuition.
      constructor.
    + simpl.
      intros.
      intuition.
      - inversion H; subst.
        constructor.
        rewrite in_app in H2.
        auto.
        specialize IHxs with ys.
        tauto.
      - inversion H; subst.
        specialize IHxs with ys.
        tauto.
      - subst.
        inversion H.
        subst.
        contradict H3.
        rewrite in_app.
        auto.
      - inversion H; subst.
        specialize IHxs with ys.
        firstorder.
      - specialize IHxs with ys.
        inversion H0; subst.
        constructor.
        × rewrite in_app.
          specialize H2 with a.
          tauto.
        × rewrite IHxs.
          intuition.
          firstorder.

  Qed.

  Lemma NoDup_app_commute : ∀ A (xs ys : list A),
    NoDup (xs ++ ys) → NoDup (ys ++ xs).
  Proof.
    intros A xs ys.
    repeat rewrite NoDup_app.
    firstorder.
  Qed.

  Lemma prepend_inj : ∀ A (xs ys ys´ : list A),
    (xs ++ ys) = (xs ++ ys´) → ys=ys´.
  Proof.
    induction xs; simpl; intros.
      auto.
      injection H; auto.
  Qed.

  Lemma NoDup_singleton : ∀ A (x:A),
      NoDup (x :: nil).
  Proof.
    intros; constructor; simpl; auto; constructor.
  Qed.

  Lemma In_map : ∀ A B (f : A → B) x xs,
                   In x xs → In (f x) (map f xs).
  Proof.
    induction xs.
    + simpl; tauto.
    + simpl.
      destruct 1.
      - left; congruence.
      - right; auto.
  Qed.

  Lemma split_lists : ∀ A (xs xs´ ys ys´ : list A),
      xs ++ xs´ = ys ++ ys´ →
      (∃ xs1, xs ++ xs1 = ys) ∨ (∃ ys1, xs = ys ++ ys1).
  Proof.
    induction xs.
    + simpl. intros.
      eauto.
    + destruct ys; simpl; intros.
    - right.
      eauto.
    - injection H.
      intros.
      assert (IH := IHxs xs´ ys ys´ H0).
      clear IHxs.
      subst.
      destruct IH as [[xs1 ?] | [ys1 ?]]; subst; eauto.
  Qed.

  Lemma prepend_injectivity : ∀ A xs (x:A) l xs´ l´,
      xs ++ x :: l = xs´ ++ x :: l´ →
      ¬In x xs →
      ¬In x xs´ →
      xs = xs´.
  Proof.
    induction xs as [|a xs].
    + simpl.
      destruct xs´ as [|b xs´].
    - simpl.
      auto.
    - simpl.
      intros l´ H.
      inversion H.
      intuition.
      + destruct xs´ as [|b xs´].
    - simpl.
      intros l´ H.
      inversion H.
      intuition.
    - simpl.
      intros l´ H.
      intros.
      inversion H.
      f_equal; apply (IHxs x l _ l´).
      auto.
      intuition.
      intuition.
  Qed.