Library mcertikos.layerlib.AuxFunctions

Require Import Coqlib.

Definition zle_le:
  ∀ x y z : Z, { x ≤ y ≤ z } + { x > y ∨ y > z}.
Proof.
  intros. destruct (zle x y).
  - destruct (zle y z).
    + left. auto.
    + right. auto.
  - right. auto.
Defined.

Definition zle_lt:
  ∀ x y z : Z, { x ≤ y < z } + { x > y ∨ y ≥ z}.
Proof.
  intros. destruct (zle x y).
  - destruct (zlt y z).
    + left. auto.
    + right. auto.
  - right. auto.
Defined.

Definition zlt_lt:
  ∀ x y z : Z, { x < y < z } + { x ≥ y ∨ y ≥ z}.
Proof.
  intros. destruct (zlt x y).
  - destruct (zlt y z).
    + left. auto.
    + right. auto.
  - right. auto.
Defined.

Definition zlt_le:
  ∀ x y z : Z, { x < y ≤ z } + { x ≥ y ∨ y > z}.
Proof.
  intros. destruct (zlt x y).
  - destruct (zle y z).
    + left. auto.
    + right. auto.
  - right. auto.
Defined.

Function new_list {A} (n: nat) (d: A) :=
  match n with
  | O ⇒ nil
  | S n´ ⇒ d :: new_list n´ d
  end.

Lemma zle_lt_true:
  ∀ (A: Type) (x y z: Z) (a b : A),
    x ≤ y < z → (if zle_lt x y z then a else b) = a.
Proof.
  intros. destruct (zle_lt x y z); trivial.
  inv o; omega.
Qed.

Lemma zle_le_true:
  ∀ (A: Type) (x y z: Z) (a b : A),
    x ≤ y ≤ z → (if zle_le x y z then a else b) = a.
Proof.
  intros. destruct (zle_le x y z); trivial.
  inv o; omega.
Qed.

Lemma zlt_lt_true:
  ∀ (A: Type) (x y z: Z) (a b : A),
    x < y < z → (if zlt_lt x y z then a else b) = a.
Proof.
  intros. destruct (zlt_lt x y z); trivial.
  inv o; omega.
Qed.

Lemma zlt_le_true:
  ∀ (A: Type) (x y z: Z) (a b : A),
    x < y ≤ z → (if zlt_le x y z then a else b) = a.
Proof.
  intros. destruct (zlt_le x y z); trivial.
  inv o; omega.
Qed.

Require Import List.

Function index {A} (f: A → bool) (n: nat) (l: list A) {struct l}: option nat :=
  match l with
  | nil ⇒ None
  | x :: l´ ⇒
    if f x then Some n else index f (S n) l´
  end.

Function replace {A} (a: A) (n: nat) (l: list A) {struct l} :=
  match n, l with
  | O, c :: tl ⇒ a :: tl
  | _, nil ⇒ nil
  | S n´, c :: tl ⇒ c :: (replace a n´ tl)
  end.

Lemma replace_replace:
  ∀ {A: Type} (a b: A) (n: nat) (l : list A),
    replace b n (replace a n l ) = replace b n l .
Proof.
  induction n.
  - intros. unfold replace. destruct l eqn: Hl; reflexivity.
  - intros. induction l.
    simpl. reflexivity.
    simpl. rewrite IHn. reflexivity.
Qed.

Lemma replace_same_comm:
  ∀ {A: Type} (a: A) (n: nat) (l : list A),
    replace a n (replace a n l ) = replace a n l .
Proof.
  intros. rewrite replace_replace. reflexivity.
Qed.

Lemma replace_comm:
  ∀ {A: Type} (a b: A) (n m: nat) (l : list A),
    n ≠ m →
    replace a n (replace b m l ) = replace b m (replace a n l ).
Proof.
  induction n.
  - destruct m.
    + intros. omega.
    + induction l.
      × simpl. trivial.
      × simpl. trivial.
  - destruct m.
    + induction l.
      × simpl. trivial.
      × simpl. trivial.
    + induction l.
      × trivial.
      × intros. simpl. rewrite IHn. reflexivity. omega.
Qed.

Lemma replace_preserves_Zlength:
  ∀ {A} l (e: A) i,
    Zlength (replace e i l) = Zlength l.
Proof.
  intros A.
  induction l.
  - simpl. destruct i; auto.
  - simpl. destruct i; intros.
    + reflexivity.
    + repeat rewrite Zlength_cons. rewrite IHl. reflexivity.
Qed.

Lemma nth_error_replace_gss: ∀ T n l, ∀ v: T,
                               (length l > n)%nat →
                               nth_error (replace v n l) n = value v.
Proof.
  Transparent replace nth_error.
  induction n.
  simpl.
  intros.
  destruct l.
  simpl in H.
  omega.
  reflexivity.
  simpl.
  intros.
  destruct l.
  simpl in H.
  xomega.
  simpl in ×.
  eapply IHn.
  xomega.
  Opaque replace nth_error.
Qed.

Lemma nth_error_replace_id: ∀ T n l, ∀ v: T,
                              nth_error l n = value v →
                              replace v n l = l.
Proof.
  Transparent replace nth_error.
  induction n.
  simpl.
  intros.
  destruct l.
  reflexivity.
  inv H.
  reflexivity.
  simpl.
  intros.
  destruct l.
  reflexivity.
  simpl.
  eapply IHn in H; eauto.
  rewrite H.
  reflexivity.
  Opaque replace nth_error.
Qed.

Lemma nth_error_replace_gso: ∀ T n1 n2 l, ∀ v: T,
                               n1 ≠ n2 →
                               nth_error (replace v n1 l) n2 = nth_error l n2.
Proof.
  Transparent replace nth_error.
  intros until n2.
  generalize dependent n1.
  induction n2.
  simpl.
  intros.
  destruct l.
  simpl.
  destruct n1.
  reflexivity.
  reflexivity.
  simpl.
  destruct n1.
  omega.
  reflexivity.
  simpl.
  intros.
  destruct l.
  replace (replace v n1 nil) with (nil: list T) by (destruct n1; reflexivity).
  reflexivity.
  simpl.
  destruct n1.
  reflexivity.
  eapply IHn2; eauto.
  Opaque replace nth_error.
Qed.

Lemma nth_replace_same:
  ∀ {A} n l x (dft: A),
    (n < length l)%nat →
    nth n (replace x n l) dft = x.
Proof.
  induction n.
  - destruct l.
    + simpl. intros. omega.
    + simpl. intros. reflexivity.
  - destruct l.
    + simpl. intros. omega.
    + simpl. intros. apply IHn. omega.
Qed.

Lemma nth_replace_different:
  ∀ {A} n i l x (dft: A),
    (n ≠ i) →
    nth n (replace x i l) dft = nth n l dft.
Proof.
  induction n.
  - destruct l.
    + simpl. destruct i.
      × simpl. intros. omega.
      × simpl. intros. reflexivity.
    + simpl. destruct i.
      × simpl. intros. omega.
      × simpl. intros. reflexivity.
  - destruct l.
    + simpl. destruct i.
      × simpl. intros. reflexivity.
      × simpl. intros. reflexivity.
    + simpl. destruct i.
      × simpl. intros. reflexivity.
      × simpl. intros. apply IHn. omega.
Qed.

Lemma replace_nth_eq:
  ∀ {A} n l (dft: A),
    replace (nth n l dft) n l = l.
Proof.
  Transparent replace.
  induction n.
  - destruct l.
    + simpl. intros. reflexivity.
    + simpl. intros. reflexivity.
  - destruct l.
    + simpl. intros. reflexivity.
    + simpl. intros. rewrite IHn. reflexivity.
Qed.
Opaque replace.

Lemma replace_same:
  ∀ {A} n l (dft: A) x,
    (0 ≤ n < length l)%nat →
    nth n l dft = x →
    replace x n l = l.
Proof.
  intros A n l dft x Hlen Hn.
  rewrite <- Hn. apply replace_nth_eq.
Qed.