Library last

Require Import last_f.

Lemma last_last_f : ∀ {A} (l:list A) (a:A), last l a = last_f (fun x ⇒ x) l a.
Proof.
  intros. induction l.
  - reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

Lemma last_cons_not_nil : ∀ {A} (l:list A) (a1:A) (a2:A),
  l ≠ [] →
  last (a2::l) a1 = last l a1.
Proof.
  intros. rewrite 2!last_last_f. apply last_f_cons_not_nil; assumption.
Qed.

Lemma last_app_not_nil : ∀ {A} (l1 l2:list A) (a:A),
  l2 ≠ [] →
  last (l1++l2) a = last l2 a.
Proof.
  intros. rewrite 2!last_last_f. apply last_f_app_not_nil; assumption.
Qed.

Lemma last_not_default : ∀ {A} (l:list A) (a:A),
  last l a ≠ a → l ≠ [].
Proof.
  intros A l a. rewrite last_last_f. apply last_f_not_default.
Qed.

Lemma last_not_empty : ∀ {A} (l:list A),
  l ≠ [] → ∀ (a1 a2:A), last l a1 = last l a2.
Proof.
  intros. rewrite 2!last_last_f. apply last_f_not_empty; assumption.
Qed.

Lemma last_cons_change_default : ∀ {A} (l:list A) (a1:A) (a2:A),
  last (a2::l) a1 = last l a2.
Proof.
  intros. rewrite 2!last_last_f. apply last_f_cons_change_default.
Qed.

Lemma last_not_empty_In : ∀ {A} (l:list A) (a:A),
  l ≠ [] → In (last l a) l.
Proof.
  assert (∀ {A} (l:list A), map (fun x ⇒ x) l = l).
  { intros. induction l. reflexivity. simpl; rewrite IHl; reflexivity. }
  intros. rewrite last_last_f.
  rewrite <- H at 2.
  apply last_f_not_empty_In. assumption.
Qed.

Lemma last_map : ∀ {A B} (f:A→B) (l:list A) (a:A),
  last (map f l) (f a) = f (last l a).
Proof.
  intros A B f l. induction l; intros.
  - simpl. reflexivity.
  - simpl map. rewrite 2!last_cons_change_default. apply IHl.
Qed.

Lemma last_firstn : ∀ {A} (l:list A) n a,
  n < length l →
  last (firstn (S n) l) a = nth n l a.
Proof.
  intros A l. induction l; intros.
  - inversion H.
  - simpl firstn. destruct n.
    + reflexivity.
    + simpl in H. apply le_S_n in H. simpl nth.
      destruct l.
      × inversion H.
      × rewrite last_cons_not_nil by discriminate. apply IHl; assumption.
Qed.

Lemma last_filter : ∀ {A} (f:A→bool) (l:list A) (a:A),
  f (last l a) = true →
  last (filter f l) a = last l a.
Proof.
  intros A f l. induction l; intros.
  - simpl. reflexivity.
  - simpl filter. destruct (f a) eqn:Heqf.
    + rewrite 2!last_cons_change_default. apply IHl.
      rewrite last_cons_change_default in H. assumption.
    + assert (last (a::l) a0 = last l a0).
      { destruct l.
        × simpl in H. rewrite H in Heqf. discriminate Heqf.
        × reflexivity.
      }
      rewrite H0 in ×.
      apply IHl; assumption.
Qed.