Library mcertikos.layerlib.ListLemma

Require Import Arith.
Require Import Omega.
Require Export List.
Require Import ZArith.

Open Scope nat_scope.
Lemma x_s1_p1_0:
  ∀ x: nat,
    x ≥ 1 →
    x - 1 + 1 = x.
Proof.
  intros. rewrite <- NPeano.Nat.add_sub_swap. rewrite plus_comm. rewrite minus_plus. reflexivity.
  omega.
Qed.

Open Scope Z_scope.
Lemma Z_succ_pred:
  ∀ x, Z.succ x - 1 = x.
Proof.
  intros. omega.
Qed.

Lemma firstn_length_eq:
  ∀ {A} (l : list A),
    firstn (length l) l = l.
Proof.
  induction l. simpl. reflexivity.
  simpl. rewrite IHl. reflexivity.
Qed.

Lemma firstn_cons:
  ∀ {A} (l : list A) a,
    firstn (length (a :: l )) (a :: l) = a :: firstn (length l ) l.
Proof.
  intros. simpl. reflexivity.
Qed.

Lemma firstn_cons_n:
  ∀ {A} n (l : list A) a,
    firstn (S n) (a :: l) = a :: firstn n l.
Proof.
  intros. simpl. reflexivity.
Qed.

Lemma length_cons:
  ∀ {A} (l : list A) a,
    S (length l ) = length ( a :: l ).
Proof.
  simpl. auto.
Qed.

Lemma firstn_overflow:
  ∀ {A} (l : list A),
    firstn (S (length l)) l = l.
Proof.
  intros. induction l. reflexivity.
  generalize (firstn_cons_n (length (a :: l)) l a); intros Hlc.
  rewrite Hlc.
  generalize (length_cons l a); intros Hlen. rewrite <- Hlen.
  rewrite IHl. reflexivity.
Qed.

Lemma firstn_overflow_cons:
  ∀ {A} n (l : list A),
    firstn (S (n + length l)) l = firstn (n + length l) l.
Proof.
  induction n.
  simpl. destruct l. reflexivity. rewrite <- length_cons. rewrite firstn_overflow.
  generalize (length_cons l a); intros Hlc. rewrite Hlc. rewrite firstn_length_eq. reflexivity.
  intros. induction l. reflexivity.
  rewrite firstn_cons_n. rewrite <- length_cons.
  replace (S n + S (length l))%nat with (S (S n + length l))%nat by omega.
  rewrite IHl. replace (S n + length l)%nat with (S (n + length l)%nat) by omega.
  rewrite (IHn l). rewrite firstn_cons_n. rewrite (IHn l). reflexivity.
Qed.

Lemma firstn_overflow_n:
  ∀ {A} n (l : list A),
    firstn (n + length l) l = l.
Proof.
  induction n. simpl. apply firstn_length_eq.
  intros. replace (S n + length l)%nat with (S (n + length l)%nat) by omega.
  rewrite (firstn_overflow_cons n l). rewrite (IHn l). reflexivity.
Qed.

Lemma firstn_nil:
  ∀ {A} n,
    firstn n nil = @nil A.
Proof.
  intros. destruct n; auto.
Qed.

Lemma skip_cons_n:
  ∀ {A} {n} (l : list A) (x: A),
    skipn n l = skipn (S n) (x :: l).
Proof.
  intros. simpl. reflexivity.
Qed.

Lemma skip_cons_1:
  ∀ {A} {n} {l : list A},
    skipn (S n) l = (skipn n (skipn 1 l)).
Proof.
  intros.
  destruct l.
  simpl. destruct n. simpl. reflexivity.
  simpl. reflexivity.
  simpl. reflexivity.
Qed.

Lemma skip1_simpl:
  ∀ {A} {a} {tl : list A},
    skipn 1 (a :: tl) = tl.
Proof.
  simpl. auto.
Qed.

Lemma skip0_eq:
  ∀ {A} {l : list A},
    skipn 0 l = l.
Proof.
  simpl. reflexivity.
Qed.

Lemma skip1_cons:
  ∀ {A} {n} {a} {l : list A},
    skipn n (skipn 1 l) = skipn (S n) (skipn 1 (a :: l )).
Proof.
  intros. rewrite skip1_simpl. rewrite <- skip_cons_1. reflexivity.
Qed.

Lemma skip_dist_1:
  ∀ {A} {n} {l : list A},
    skipn (S n) l = (skipn 1 (skipn n l)).
Proof.
  intros. generalize n; clear n.
  induction l; intros.
  simpl. destruct n. simpl. reflexivity.
  simpl. reflexivity.
  rewrite <- skip_cons_n. destruct n. reflexivity. rewrite IHl.
  rewrite <- skip_cons_n. reflexivity.
Qed.

Lemma skip1_comm:
  ∀ {A} {l : list A} {n},
    skipn n (skipn 1 l) = skipn 1 (skipn n l).
Proof.
  intros.
  rewrite <- skip_cons_1, <- skip_dist_1.
  trivial.
Qed.

Lemma skipn_cons:
  ∀ {A} {n} {l l´ : list A} {x: A},
    skipn n l = x :: l´ →
    skipn (S n) l = l´.
Proof.
  induction n.
  intros. simpl. simpl in H. rewrite H. reflexivity.
  induction l. inversion 1.
  intros. simpl in H. apply IHn in H.
  destruct l´ as [| v l´´].
  destruct l. simpl. reflexivity.
  simpl. simpl in H. assumption.
  rewrite <- skip_cons_n. assumption.
Qed.

Lemma firstn_skip1_cons:
  ∀ {A} {n} {l : list A} {a: A},
    firstn n l = skipn 1%nat (firstn (S n) (a::l)).
Proof.
  simpl. auto.
Qed.

Lemma firstn_dest:
  ∀ {A} {n} {l : list A} {a: A},
    firstn (S n) (a::l) = a :: firstn n l.
Proof.
  simpl. auto.
Qed.

Lemma list_eq_cons:
  ∀ {A} {l1 l2 : list A} {a : A},
    a :: l1 = a :: l2 →
    l1 = l2.
Proof.
  intros.
  inversion H. trivial.
Qed.

Lemma list_eq_dest:
  ∀ {A} {l1 l2 : list A} {a : A},
    l1 = l2 →
    a :: l1 = a :: l2.
Proof.
  intros. rewrite H. reflexivity.
Qed.

Lemma skipn_firstnp1:
  ∀ {A} n (l tl : list A) (x: A),
    skipn n l = x :: tl →
    firstn (S n) l = (firstn n l) ++ x :: nil.
Proof.
  induction n.
  - simpl. intros. rewrite H. reflexivity.
  - induction l. inversion 1.
    intros. rewrite firstn_dest. rewrite firstn_dest. rewrite <- app_comm_cons.
    apply list_eq_dest. simpl in H. apply IHn in H. assumption.
Qed.

Lemma non_nil_list: ∀ {A} {l : list A},
    l ≠ nil → ∃ h t, l = h :: t.
Proof.
  destruct l.
  intros H. contradiction H; trivial.
  intros H. repeat econstructor.
Qed.

Lemma list_non_nil: ∀ {A} {l : list A},
    (∃ h t, l = h :: t) → l ≠ nil.
Proof.
  destruct l.
  intros H. destruct H as (h & t & H). discriminate H.
  intros H. inversion 1.
Qed.

Lemma skipn_nil:
  ∀ {A} {n}, skipn n nil = @nil A.
Proof.
  intros. destruct n; simpl; reflexivity.
Qed.

Lemma length_firstn_skipn:
  ∀ {A} n (l : list A),
    (length (firstn n l) + length (skipn n l))%nat = length l.
Proof.
  intros.
  rewrite <- app_length with (l := firstn n l ) (l´ := skipn n l ).
  rewrite firstn_skipn. reflexivity.
Qed.

Lemma length_firstn_eq:
  ∀ {A} n (l : list A),
    (length l - length (firstn n l) = length l - n) % nat.
Proof.
  intros.
  rewrite firstn_length.
  assert (Hcase: (length l < n ∨ length l ≥ n)%nat) by omega.
  destruct Hcase as [Hx | Hx]; generalize Hx.
  - intros Hlt. rewrite min_r by omega.
    rewrite minus_diag. rewrite not_le_minus_0 by omega. reflexivity.
  - intros Hge. rewrite min_l by omega. reflexivity.
Qed.

Lemma length_skipn:
  ∀ {A} n (l : list A),
    length (skipn n l) = (length l - n)%nat.
Proof.
  intros.
  rewrite <- length_firstn_eq.
  generalize (length_firstn_skipn n l); intros Hlfs.
  rewrite <- Hlfs. omega.
Qed.

Lemma length_skipn_lt:
  ∀ {A} n (l : list A),
    (n < length l) % nat →
    (length (skipn n l) > 0) % nat.
Proof.
  intros.
  rewrite length_skipn.
  omega.
Qed.

Lemma length_not_nil:
  ∀ {A} (l : list A),
    (length l > 0) % nat →
    l ≠ nil.
Proof.
  intros.
  destruct l eqn: Hl. inversion H.
  discriminate.
Qed.

Lemma skipn_lt:
  ∀ {A} (l : list A) (n: nat),
    (n < length l)%nat →
    skipn n l ≠ nil.
Proof.
  intros.
  apply length_not_nil.
  apply length_skipn_lt.
  assumption.
Qed.

Lemma skipn_length:
  ∀ {A} (l : list A),
    skipn (length l) l = nil.
Proof.
  induction l; simpl; auto.
Qed.

Lemma skipn_S_length:
  ∀ {A} (l : list A),
    skipn (S (length l)) l = nil.
Proof.
  intros. rewrite skip_dist_1. rewrite skipn_length. reflexivity.
Qed.

Lemma skipn_overflow:
  ∀ {A} (l : list A) (n: nat),
    skipn (n + length l) l = nil.
Proof.
  intros. induction n. simpl. apply skipn_length.
  rewrite plus_Sn_m. rewrite skip_dist_1. rewrite IHn. reflexivity.
Qed.

Lemma skipn_ge:
  ∀ {A} (l : list A) (n: nat),
    (n ≥ length l)%nat →
    skipn n l = nil.
Proof.
  intros.
  pose (m := (n - length l)%nat).
  assert (n = (m + length l)%nat) by (unfold m; omega).
  rewrite H0. apply skipn_overflow.
Qed.

Lemma in_skipn:
  ∀ {A} (n: nat) (l : list A) a,
    In a (skipn n l) →
    In a l.
Proof.
  induction n. auto.
  induction l. auto.
  simpl. intros.
  right. apply IHn. assumption.
Qed.

Lemma last_tl:
  ∀ {A: Type} l (h: A) d,
    l ≠ nil →
    last (h :: l) d = last l d.
Proof.
  induction l.
  - simpl. intros. contradict H. reflexivity.
  - simpl. intros. reflexivity.
Qed.

Lemma forall_list:
  ∀ A P {l : list A} e,
    Forall P l →
    In e l →
    P e.
Proof.
  intros.
  destruct (Forall_forall P l).
  apply H1; assumption.
Qed.

Lemma forall_list_skipn:
  ∀ A P {l : list A} n e,
    Forall P l →
    In e (skipn n l) →
    P e.
Proof.
  intros.
  apply in_skipn in H0.
  apply forall_list with (l :=l); assumption.
Qed.

Definition isChar (x: Z) :=
  0 ≤ x ≤ 255.

Lemma forall_erange:
  ∀ {l } n e,
    Forall isChar l →
    In e (skipn n l) →
    isChar e.
Proof.
  intros.
  apply forall_list_skipn with (l :=l) (n:=n); assumption.
Qed.

Lemma forall_skipn_hd_erange:
  ∀ {l } n e tl,
    Forall isChar l →
    skipn n l = e :: tl →
    isChar e.
Proof.
  intros.
  assert (In e (skipn n l)).
  {
    rewrite H0.
    constructor. reflexivity.
  }
  apply (@forall_erange l n e); assumption.
Qed.

Lemma forall_hd:
  ∀ {A} {P} {e} {tl: list A},
    Forall P (e :: tl) →
    P e.
Proof.
  intros. inversion H. subst.
  assumption.
Qed.

Lemma forall_tl:
  ∀ {A} {P} {e} {tl : list A},
    Forall P (e :: tl) →
    Forall P tl.
Proof.
  intros.
  inversion H. assumption.
Qed.

Lemma forall_last:
  ∀ {A} {l: list A} {P} {d},
    Forall P l →
    P d →
    P (last l d).
Proof.
  induction l.
  - simpl. auto.
  - intros. destruct l.
    + simpl. apply forall_hd in H. assumption.
    + rewrite last_tl. apply forall_tl in H.
      generalize (IHl P d H H0). auto.
      firstorder.
Qed.

Lemma Zlength_lt:
  ∀ {A} i (l : list A),
    0 ≤ i < Zlength l →
    (Z.to_nat i < length l)%nat.
Proof.
  intros. rewrite Zlength_correct in H.
  destruct H. assert (Hl: 0 ≤ Z.of_nat (length l)) by omega.
  generalize (Z2Nat.inj_lt i (Z.of_nat (length l)) H Hl); intros.
  apply H1 in H0. rewrite Nat2Z.id in H0. assumption.
Qed.

Lemma Zlength_le:
  ∀ {A} i (l : list A),
    0 ≤ i ≤ Zlength l →
    (Z.to_nat i ≤ length l)%nat.
Proof.
  intros. rewrite Zlength_correct in H.
  destruct H. assert (Hl: 0 ≤ Z.of_nat (length l)) by omega.
  generalize (Z2Nat.inj_le i (Z.of_nat (length l)) H Hl); intros.
  apply H1 in H0. rewrite Nat2Z.id in H0. assumption.
Qed.

Lemma skip_1_tl:
  ∀ {A} n (ls tls: list A) h,
    skipn n ls = h :: tls →
    skipn (S n) ls = tls.
Proof.
  intros.
  rewrite skip_dist_1.
  simpl.
  rewrite H.
  trivial.
Qed.

Lemma skip_nth_eq:
  ∀ {A} n (l tl : list A) h default,
    skipn n l = h :: tl →
    nth n l default = h.
Proof.
  induction n. simpl. intros. rewrite H. simpl. reflexivity.
  induction l. simpl. inversion 1.
  rewrite <- skip_cons_n. intros. simpl.
  generalize (IHn l tl h default H). auto.
Qed.

Lemma skipn_skipn:
  ∀ {A} n m (l : list A),
    skipn n (skipn m l) = skipn (n + m) l.
Proof.
  induction n. simpl. trivial.
  destruct l. repeat rewrite skipn_nil. reflexivity.
  rewrite skip_dist_1. rewrite (IHn m (a :: l)).
  rewrite <- skip_dist_1. simpl. reflexivity.
Qed.

Lemma skipn_append:
  ∀ {A} n (l1 l2: list A),
    (n ≤ length l1)%nat →
    skipn n (l1 ++ l2) = skipn n l1 ++ l2.
Proof.
  induction n.
  - intros. simpl. reflexivity.
  - intros. destruct l1. simpl in H. inversion H.
    simpl. apply IHn. simpl in H. omega.
Qed.

Lemma skipn_less:
  ∀ {A} n l l´ (h: A) z,
    skipn n (h :: l) = z :: l´ →
    skipn n l = l´.
Proof.
  induction n.
  - intros. simpl in ×. inversion H. reflexivity.
  - intros. simpl in ×. destruct l. rewrite skipn_nil in H. inversion H.
    apply IHn in H. assumption.
Qed.

Lemma eq_imply_le:
  ∀ x y: Z, x = y → x ≥ y.
Proof. intros. omega. Qed.

Lemma skipn_length_tail:
  ∀ {A} (l tl : list A),
    skipn (length l) (l ++ tl) = tl.
Proof.
  intros. induction l. simpl. reflexivity.
  simpl. assumption.
Qed.

Lemma skipn_gt_tail:
  ∀ {A} n (l tl : list A),
    (n < length l )%nat →
    skipn n l ++ tl = skipn n (l ++ tl).
Proof.
  induction n. simpl. reflexivity.
  intros. simpl. destruct l. inversion H. simpl.
  apply IHn. simpl in H. omega.
Qed.

Lemma skipn_ge_tail:
  ∀ {A} n (l tl : list A),
    (n ≤ length l )%nat →
    skipn n l ++ tl = skipn n (l ++ tl).
Proof.
  intros.
  assert (Hcase: n = length l ∨ (n < length l)%nat) by omega.
  destruct Hcase as [Hcase1 | Hcase1]; generalize Hcase1.
  {
    intros. subst. rewrite skipn_length_tail. rewrite skipn_length. reflexivity.
  }
  {
    intros. apply skipn_gt_tail. assumption.
  }
Qed.

Lemma last_cons_eq:
  ∀ {A} (a z default: A) (tl : list A),
    nth (length (a :: tl)) (z :: a :: tl) default = nth (length tl) (a :: tl) default.
Proof.
  intros. simpl. reflexivity.
Qed.

Lemma last_nth_eq:
  ∀ {A} (tl : list A) (z default : A),
    nth (length tl) (z :: tl) default = last (z :: tl) default.
Proof.
  induction tl. simpl. reflexivity. intros.
  generalize (last_cons_eq a z default tl); intros Hlc.
  rewrite Hlc. generalize (IHtl a default); intros Hihtl.
  rewrite Hihtl. reflexivity.
Qed.

Lemma zlength_to_length:
  ∀ {A} (l : list A),
    (Z.to_nat (Zlength l )) = length l.
Proof.
  intros. rewrite Zlength_correct. rewrite Nat2Z.id. reflexivity.
Qed.

Lemma length_to_zlength:
  ∀ {A} (l : list A),
    (Z.of_nat (length l )) = Zlength l.
Proof.
  intros. rewrite <- Zlength_correct. reflexivity.
Qed.

Lemma Zlength_ge_0:
  ∀ {A} (l : list A),
    0 ≤ Zlength l.
Proof.
  intros. induction l. rewrite Zlength_nil. omega.
  rewrite Zlength_cons. omega.
Qed.

Lemma app_Zlength:
  ∀ {A} (l1 l2 : list A),
    Zlength (l1 ++ l2) = Zlength l1 + Zlength l2.
Proof.
  intros. rewrite Zlength_correct. rewrite app_length. rewrite Nat2Z.inj_add.
  repeat rewrite Zlength_correct. reflexivity.
Qed.

Lemma list_gt_0:
  ∀ {A: Type} (ls: list A), 0 ≤ Zlength ls.
Proof.
  intros; induction ls.
  - unfold Zlength; simpl; omega.
  - rewrite Zlength_cons. omega.
Qed.

Lemma length_ge_1:
  ∀ {T: Type} (c: T) (stl: list T),
    (1 ≤ length (c :: stl))%nat.
Proof.
  intros. simpl. induction stl.
  simpl. omega.
  simpl. omega.
Qed.

Lemma Zlength_ge_1:
  ∀ {T: Type} (c: T) (stl: list T),
    1 ≤ Zlength (c :: stl).
Proof.
  intros.
  rewrite <- (Z2Nat.id 1).
  rewrite <- (Z2Nat.id (Zlength (c :: stl))).
  apply inj_le.
  rewrite zlength_to_length.
  replace (Z.to_nat 1) with 1%nat.
  apply length_ge_1.
  vm_compute. reflexivity.
  apply (Zlength_ge_0 (c :: stl)).
  omega.
Qed.

Lemma list_hd_eq:
  ∀ {A: Type} (a b: A) (l1 l2: list A),
    a :: l1 = b :: l2 →
    a = b.
Proof.
  intros.
  inversion H. reflexivity.
Qed.

Lemma list_tl_eq:
  ∀ {A: Type} (a b: A) (l1 l2: list A),
    a :: l1 = b :: l2 →
    l1 = l2.
Proof.
  intros.
  inversion H. reflexivity.
Qed.

Lemma skipn_cons_not_nil:
  ∀ {A: Type} n (h: A) l,
    skipn n l ≠ nil →
    skipn n (h :: l) ≠ nil.
Proof.
  induction n.
  intros. simpl. contradict H. inversion H.
  intros. simpl. destruct l. contradict H. rewrite skipn_nil. reflexivity.
  generalize H. simpl. apply (IHn a l).
Qed.

Lemma skipn_cons_relation:
  ∀ {A: Type} n (h: A) x l´ l,
    skipn n l = x :: l´ →
    ∃ y, skipn n (h :: l) = y :: x :: l´.
Proof.
  induction n.
  intros. simpl. simpl in H. ∃ h. rewrite H. reflexivity.
  intros. simpl. destruct l.
  - simpl in H. inversion H.
  - simpl in H. apply (IHn a x l´ l H).
Qed.

Lemma skipn_last:
  ∀ {A: Type} l (h: A) d,
    skipn (length l) (h :: l) = last (h :: l) d :: nil.
Proof.
  induction l.
  - simpl. intros. reflexivity.
  - simpl. intros.
    rewrite (IHl a d). simpl. reflexivity.
Qed.

Lemma last_concat: ∀ (A : Type) (l1 l2: list A) (d: A),
                     l2 ≠ nil → last (l1 ++ l2) d = last l2 d.
Proof.
  intro.
  induction l1.
  simpl.
  intros.
  reflexivity.
  simpl.
  intros.
  case_eq (l1 ++ l2); intros.
  apply app_eq_nil in H0.
  destruct H0.
  contradiction.
  rewrite <- H0.
  eapply IHl1; eauto.
Qed.

Lemma skipn_remains:
  ∀ {A} (ls: list A) m,
    (0 < m)%nat →
    ls ≠ nil →
    ∃ h tl, skipn (length ls - m) ls = h :: tl.
Proof.
  induction ls.
  - simpl. intros. contradiction H0. reflexivity.
  - intros. simpl.
    destruct m.
    + omega.
    + assert (Hlm: (length ls ≤ m)%nat ∨ (length ls > m)%nat) by omega.
      destruct Hlm as [Hlm | Hlm].
      × replace (length ls - m)%nat with 0%nat by omega.
        simpl. ∃ a, ls. reflexivity.
      × replace (length ls - m)%nat with (S (length ls - S m))%nat by omega.
        simpl.
        destruct ls eqn: Hls.
        {
          simpl in Hlm. omega.
        }
        {
          apply (IHls (S m)). omega. intro Hx. inversion Hx.
        }
Qed.

Lemma skipn_cons_exists:
  ∀ {A} (ls: list A) n h tl a,
    skipn n ls = h :: tl →
    ∃ h0, skipn n (a :: ls) = h0 :: h :: tl.
Proof.
  induction ls.
  - intros. rewrite skipn_nil in H. inversion H.
  - intros. destruct n.
    + simpl in ×. ∃ a0. rewrite H. reflexivity.
    + simpl in ×. apply IHls. assumption.
Qed.

Lemma nth_error_valid_length:
  ∀ {T} l n (v: T),
    nth_error l n = value v →
    (length l > n)%nat.
Proof.
  induction l.
  - simpl. intros n v. destruct n; simpl; inversion 1.
  - simpl. induction n.
    + simpl. intros v H. omega.
    + intros v H. apply gt_n_S.
      simpl in H. apply (IHl n v H).
Qed.