Library last_f

Require Export List.
Export ListNotations.

Fixpoint last_f {A B} (f:A → B) (l:list A) (b:B) : B :=
  match l with
  | [] ⇒ b
  | [x] ⇒ f x
  | _ :: (_ :: _) as l' ⇒ last_f f l' b
  end.

Lemma last_f_cons_not_nil : ∀ {A B} (f:A → B) (l:list A) (b:B) (a:A),
  l ≠ [] →
  last_f f (a::l) b = last_f f l b.
Proof.
  intros. destruct l.
  - contradiction H. reflexivity.
  - reflexivity.
Qed.

Lemma last_f_app_not_nil : ∀ {A B} (f:A → B) (l1 l2:list A) (b:B),
  l2 ≠ [] →
  last_f f (l1++l2) b = last_f f l2 b.
Proof.
  intros A B f l1. induction l1; intros.
  - reflexivity.
  - simpl app. rewrite last_f_cons_not_nil.
    + apply IHl1; assumption.
    + destruct l1.
      × assumption.
      × discriminate.
Qed.

Lemma last_f_not_default : ∀ {A B} (f:A → B) (l:list A) (b:B),
  last_f f l b ≠ b → l ≠ [].
Proof.
  intros. destruct l.
  - contradiction H. reflexivity.
  - discriminate.
Qed.

Lemma last_f_not_empty : ∀ {A B} (f:A → B) (l:list A),
  l ≠ [] → ∀ (b1 b2:B), last_f f l b1 = last_f f l b2.
Proof.
  intros A B f l. induction l; intros.
  - contradiction H; reflexivity.
  - destruct l.
    + simpl. reflexivity.
    + rewrite last_f_cons_not_nil;
        [ symmetry; rewrite last_f_cons_not_nil; [ apply IHl |] |];
        discriminate.
Qed.

Lemma last_f_cons_change_default : ∀ {A B} (f:A → B) (l:list A) (b:B) (a:A),
  last_f f (a::l) b = last_f f l (f a).
Proof.
  intros. destruct l.
  - reflexivity.
  - rewrite last_f_cons_not_nil by discriminate. apply last_f_not_empty; discriminate.
Qed.

Lemma last_f_not_empty_In : ∀ {A B} (f: A → B) (l : list A),
  l ≠ [] → ∀ (b : B), In (last_f f l b) (map f l).
Proof.
  intros A B f l. induction l; intros.
  - contradiction H; reflexivity.
  - destruct l eqn:Heql.
    + simpl. left; reflexivity.
    + rewrite <- Heql in ×. rewrite last_f_cons_change_default.
      simpl. right. apply IHl. rewrite Heql; discriminate.
Qed.

Lemma last_f_is_map : ∀ {A B} (f:A→B) (l:list A) (b:B),
  last_f f l b = last (map f l) b.
Proof.
  intros A B f l.
  induction l; intros.
  - reflexivity.
  - simpl. rewrite IHl. destruct l; reflexivity.
Qed.

Lemma last_f_map : ∀ {A B} (f:A→B) (l:list A) (a:A),
  last_f f l (f a) = f (last l a).
Proof.
  intros A B f l. induction l; intros.
  - reflexivity.
  - simpl. rewrite IHl. destruct l; reflexivity.
Qed.