Proofs about leftpad inspired by ezrakilty -- https://github.com/ezrakilty/hillel-challenge

leftpad.v

Require Import Lists.List.
Require Import Arith.Arith.

Require Import Omega.

Set Implicit Arguments.

Fixpoint replicate A (n : nat) (x : A) : list A :=
  match n with
  | O => nil
  | S n => cons x (replicate n x)
  end.

Fixpoint drop A (n : nat) (xs : list A) : list A :=
  match n with
  | O => xs
  | S n => match xs with
          | nil => nil
          | cons _ xs => drop n xs
          end
  end.

Fixpoint take A (n : nat) (xs : list A) : list A :=
  match n with
  | O => nil
  | S n => match xs with
          | nil => nil
          | cons x xs => cons x (take n xs)
          end
  end.

Lemma replicate_length :
  forall A (x : A) (n : nat),
    length (replicate n x) = n.
Proof.
  induction n; simpl; firstorder.
Qed.

Lemma Forall_replicate :
  forall (A : Type) (x : A) (n : nat),
    Forall (fun c => c = x) (replicate n x).
Proof.
  induction n; simpl; firstorder.
Qed.

Lemma drop_app:
  forall A n (xs ys : list A),
    length xs = n ->
    drop n (xs ++ ys) = ys.
Proof.
  intros A n.
  induction n; destruct xs; intros ys Hlen;
    try discriminate;
    firstorder.
Qed.

Lemma take_app:
  forall A n (xs ys : list A),
    length xs = n ->
    take n (xs ++ ys) = xs.
Proof.
  intros A n.
  induction n; destruct xs; intros ys Hlen; simpl;
    try discriminate;
    f_equal;
    firstorder.
Qed.

Hint Rewrite Forall_replicate take_app drop_app app_length replicate_length app_nil_r : helper.
Hint Resolve Forall_replicate : helper.

Definition leftpad A (x : A) (xs : list A) (n : nat) : list A :=
  replicate (n - length xs) x ++ xs.

Lemma leftpad_length :
  forall (A : Type) (x : A) xs n,
    length xs <= n ->
    length (leftpad x xs n) = n.
Proof with (try omega; repeat autorewrite with helper).
  intros A x xs n Hlen.
  unfold leftpad; simpl...
  destruct (length xs)...
Qed.

Lemma leftpad_length_max :
  forall (A : Type) (x : A) (xs : list A) (n : nat),
    length (leftpad x xs n) = max n (length xs).
Proof with (try omega; repeat autorewrite with helper).
  intros A x xs n.
  destruct (le_lt_dec n (length xs)); unfold leftpad; simpl...
  - rewrite max_r...
  - rewrite max_l...
Qed.

Lemma leftpad_drop :
  forall (A : Type) (x : A) (xs : list A) (n : nat),
    drop (n - length xs) (leftpad x xs n) = xs.
Proof with (repeat autorewrite with helper; try reflexivity).
  intros A x xs n.
  unfold leftpad...
Qed.

Lemma leftpad_take :
  forall (A : Type) (x : A) (xs : list A) (n : nat),
    Forall (fun c => c = x) (take (n - length xs) (leftpad x xs n)).
Proof with (repeat autorewrite with helper; firstorder).
  intros A x xs n.
  unfold leftpad...
Qed.