Injectivity of list concatenation from first principles in Coq

ListAppInj.v

(* Proving injectivity of list concatenation from first
   principles - no stdlib, no automation *)

(* Definition of a list *)
Inductive list (A : Type) : Type :=
  | nil
  | cons (x : A) (xs : list A).

Arguments nil {A}.
Arguments cons {A} _ _.

Notation "x :: y" := (cons x y)
  (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).

Example one_two_three : list nat := [1; 2; 3].
Example true_false : list bool := [true; false].

(* Definition of list concatenation *)
Fixpoint app {A} (l l' : list A) : list A :=
  match l with
  | [] => l'
  | x :: xs => x :: app xs l'
  end.

Notation "xs ++ ys" := (app xs ys)
  (at level 60, right associativity).

Compute ([1; 2; 3] ++ [4; 5; 6]).

(* Useful lemmas for establishing the main theorems *)
Lemma app_nil_r : forall {A} (xs : list A),
  xs ++ [] = xs.
Proof.
  induction xs.
  - reflexivity.
  - simpl.
    rewrite IHxs.
    reflexivity.
Qed.

Lemma app_assoc : forall {A} (xs ys zs : list A),
  (xs ++ ys) ++ zs = xs ++ ys ++ zs.
Proof.
  induction xs.
  - reflexivity.
  - intros.
    simpl.
    rewrite IHxs.
    reflexivity.
Qed.

Lemma app_cons_x_xs_ys_neq_ys : forall {A} (x : A) xs ys,
  x :: xs ++ ys = ys ->
  False.
Proof.
  intros.
  generalize dependent xs.
  generalize dependent x.
  induction ys.
  - intros.
    replace (x :: xs ++ []) with ((x :: xs) ++ []) in H.
    + rewrite app_nil_r in H.
      discriminate H.
    + reflexivity.
  - intros.
    injection H.
    intros.
    rewrite H1 in *.
    destruct xs.
    + simpl in *.
      replace (x :: ys) with (x :: [] ++ ys) in H0.
      * apply IHys with (x := x) (xs := []).
        apply H0.
      * reflexivity.
    + replace ((x1 :: xs) ++ x :: ys)
        with (x1 :: (xs ++ [x]) ++ ys) in H0.
      * apply IHys with (x := x1) (xs := xs ++ [x]).
        apply H0.
      * simpl.
        rewrite app_assoc.
        reflexivity.
Qed.

(* Main theorem #1: Left-injectivity of list concatenation *)
Theorem app_inj_l : forall {A} (xs xs' ys : list A),
  xs ++ ys = xs' ++ ys ->
  xs = xs'.
Proof.
  induction xs.
  - intros.
    destruct xs'.
    + reflexivity.
    + symmetry in H.
      exfalso.
      apply (app_cons_x_xs_ys_neq_ys _ _ _ H).
  - intros.
    destruct xs'.
    + exfalso.
      apply (app_cons_x_xs_ys_neq_ys _ _ _ H).
    + injection H.
      intros.
      apply IHxs in H0.
      rewrite H0.
      rewrite H1.
      reflexivity.
Qed.

(* Main theorem #2: Right-injectivity of list concatenation *)
Theorem app_inj_r : forall {A} (xs ys ys' : list A),
  xs ++ ys = xs ++ ys' ->
  ys = ys'.
Proof.
  induction xs.
  - intros.
    apply H.
  - intros.
    simpl in H.
    injection H.
    intros.
    apply IHxs.
    apply H0.
Qed.

Print Assumptions app_inj_l.
Print Assumptions app_inj_r.