remove last algorithm equivalence proof

removelast.coq

Require Import Coq.Lists.List.
Import Coq.Lists.List.ListNotations


Fixpoint my_remove_last {A : Type} (l : list A) : list A:= 
  match l with
    | [] => []
    | x :: [] => []
    | x :: xs => x :: (my_remove_last xs)
  end.

Definition bad_remove_last {A : Type} (l : list A) : list A :=
  match rev l with
    | [] => []
    | _ :: xs => rev xs
  end.

Theorem  equivalent_remove_last : forall (A : Type) (l : list A), 
  my_remove_last l = bad_remove_last l.
Proof.
  intros. induction l.
  - unfold bad_remove_last. reflexivity.
  - simpl. rewrite -> IHl. destruct l.
    + reflexivity.
    + unfold bad_remove_last. simpl. destruct (rev l).
      * reflexivity.
      * simpl. 
          rewrite -> rev_app_distr. 
          rewrite -> rev_app_distr. 
          rewrite -> rev_app_distr. reflexivity.
Qed.