Set Implicit Arguments.
Require Import List Lia.
Import ListNotations.

Lemma list_decompose k {X} (A: list X):
  k length A A1 A2, A = length = k.
Proof.
  induction A in k |-*; intros.
  - exists nil. exists nil; cbn. destruct k; intuition.
  - destruct k.
    + exists nil; exists (a :: A); intuition.
    + cbn in *; assert (k length A) by . destruct (IHA _ ) as ( & & ?).
      intuition. exists (a :: ). exists . subst.
      intuition.
Qed.


Lemma list_decompose_alt k {X} (A: list X):
  k length A A1 A2, A = length = k.
Proof.
  intros H.
  assert (length A - k length A) by .
  destruct (list_decompose _ ) as ( & & ?).
  intuition. exists . exists . intuition.
  specialize (app_length ) as .
  rewrite in . rewrite in . .
Qed.


Lemma list_decompose_end {X} (A: list X):
  A = nil a' A', A = A' [a'].
Proof.
  induction A; intuition; subst.
  all: right; try destruct IH as (a' & A' & ?).
  + exists a. exists nil. reflexivity.
  + destruct H as (a' & A' & ?); subst.
    exists a'. exists (a :: A'). reflexivity.
Qed.


Lemma list_decompose_strong Y k (A: list Y):
  k length A { A1 & { A2 | A = length = k}}.
Proof.
  induction A in k |-*; intros H.
  - exists nil. exists nil. intuition.
  - destruct k.
    + exists nil. exists (a :: A). intuition.
    + cbn in H; eapply le_S_n in H.
      destruct (IHA _ H) as ( & & & ); subst.
      exists (a :: ). exists . intuition.
Qed.


Lemma list_pointwise_eq X (A B: list X):
  ( x, nth_error A x = nth_error B x) A = B.
Proof.
  induction A in B |-*; cbn; destruct B as [| b B]; eauto.
  - intros H; specialize (H 0); discriminate.
  - intros H; specialize (H 0); discriminate.
  - intros H.
    specialize (H 0) as H'; injection H' as .
    f_equal; eapply IHA.
    intros x; exact (H (S x)).
Qed.


Lemma list_end_ind:
   (A : Type) (P : list A Prop),
    P []
    ( (a : A) (l : list A), P l P (l [a])) l : list A, P l.
Proof.
  intros A P H IH l.
  specialize (rev_list_ind P H) as Ind.
  rewrite rev_involutive. eapply Ind.
  intros; cbn; now apply IH.
Qed.


Lemma app_injective {X} (A B C D: list X):
  length A = length C A B = C D A = C B = D.
Proof.
  induction A in C |-*; destruct C; try discriminate.
  cbn; intuition.
  injection 1 as ?. injection 1 as ?.
  subst. edestruct IHA; eauto; subst; intuition.
Qed.


Lemma app_injective_right Y (A1 A2 B1 B2 : list Y):
  length = length = = = .
Proof.
  intros H; induction in |-*; destruct ; cbn; eauto.
  1 - 2: intros; subst; cbn in H; autorewrite with list in H; .
  intros [= ? % ]; intuition; now subst.
Qed.