Library last_state

Require Import last_f.

Definition last_state {A B} (l:list (A×B)) (b:B) := last_f snd l (b:B).

Arguments last_state _ _ _ _ /.


Lemma last_last_cons_not_nil : ∀ {A B} (l:list (A×B)) (b:B) (ab:A×B),
  l ≠ [] →
  last_state (ab::l) b = last_state l b.
Proof.
  intros. apply last_f_cons_not_nil; assumption.
Qed.

Lemma last_state_app_not_nil : ∀ {A B} (l1 l2:list (A×B)) (b:B),
  l2 ≠ [] →
  last_state (l1++l2) b = last_state l2 b.
Proof.
  intros. apply last_f_app_not_nil; assumption.
Qed.

Lemma last_state_not_default : ∀ {A B} (l:list (A×B)) (b:B),
  last_state l b ≠ b → l ≠ [].
Proof.
  intros A B l b. apply last_f_not_default.
Qed.

Lemma last_state_not_empty : ∀ {A B} (l:list (A×B)),
  l ≠ [] → ∀ (b1 b2:B), last_state l b1 = last_state l b2.
Proof.
  intros. apply last_f_not_empty; assumption.
Qed.

Lemma last_state_cons_change_default : ∀ {A B} (l:list (A×B)) (b:B) (ab:A×B),
  last_state (ab::l) b = last_state l (snd ab).
Proof.
  intros. apply last_f_cons_change_default.
Qed.

Lemma last_f_not_empty_In : ∀ {A B} (l : list (A×B)),
  l ≠ [] → ∀ (b : B), In (last_state l b) (map snd l).
Proof.
  intros. apply last_f_not_empty_In; assumption.
Qed.

Lemma last_state_is_map : ∀ {A B} (l:list (A×B)) (b:B),
  last_state l b = last (map snd l) b.
Proof.
  intros. apply last_f_is_map.
Qed.

Lemma last_state_map : ∀ {A B} (l:list (A×B)) (a:A) (b:B),
  last_state l b = snd (last l (a,b)).
Proof.
  intros. replace b with (snd (a, b)) by reflexivity.
  apply last_f_map.
Qed.