2023-1-13.v

Require Import List.
Require Import Nat.
Require Import Bool.
Import ListNotations.

Inductive subseq : list nat -> list nat -> Prop :=
  | hl1 : subseq [] []
  | hl2 lst1 lst2 (H: subseq lst1 lst2) : forall (x : nat),
      subseq lst1 (x :: lst2)
  | hl3 lst1 lst2 (H: subseq lst1 lst2) : forall (x : nat),
      subseq (x :: lst1) (x :: lst2).

Fixpoint subseqb (lst1 l2 : list nat) : bool :=
  match lst1, l2 with
    | [], [] => true
    | [], y :: ys => true
    | x :: xs, [] => false
    | x :: xs, y :: ys => match x =? y with
                            | true => subseqb xs ys
                            | false => subseqb lst1 ys
                          end
  end.

Theorem nat_decidable : forall (n m : nat), (n = m) + (n <> m).
Proof.
    induction n; destruct m.
    - left. auto.
    - right. intro H. discriminate.
    - right. intro H. discriminate.
    - pose proof (IHn m).
      destruct H.
      + subst. left. auto.
      + right. intro H. inversion H. auto.
Qed.  

Lemma list_lemma : forall (x y : nat) l1 l2, (x::l1) = (y::l2) -> x = y /\ l1 = l2.
Proof.
    intros x y l1 l2 H.
    induction l1; inversion H; subst; split; exact eq_refl.
Qed.

Ltac subst_list x y l1 l2 H :=
    pose proof (proj1 (list_lemma x y l1 l2 H));
    pose proof (proj2 (list_lemma x y l1 l2 H));
    subst.

Lemma cons_cancel_subseq : forall {x : nat} {lst1 lst2 : list nat},
    subseq (x :: lst1) (x :: lst2) -> subseq lst1 lst2.
Proof.
    intros x l1 l2 H.
    remember (x :: l1) as l1'.
    remember (x :: l2) as l2'.
    destruct H.
    inversion Heql1'. (* hl1 is easy *)
    2: { (* so is hl3 *)
        subst_list x0 x lst1 l1 Heql1'.
        subst_list x x lst2 l2 Heql2'.
        exact H. 
    }
    (* hl2 is harder *)
    subst_list x0 x lst2 l2 Heql2'.
    induction l2. (* need to dig into l2 *)
    1: { inversion H. }
    destruct (nat_decidable x a).
    1: { (* = *)
        subst.
        remember (a :: l1) as l1'.
        remember (a :: l2) as l2'.
        destruct H.
        - inversion Heql1'.
        - subst_list x a lst2 l2 Heql2'0.
          pose proof (IHl2 H eq_refl).
          exact (hl2 l1 l2 H0 a).
        - subst_list x a lst1 l1 Heql1'.
          subst_list a a lst2 l2 Heql2'0.
          exact (hl2 l1 l2 H a).
    }
    (* != *)
    remember (x :: l1) as l1'.
    remember (a :: l2) as l2'.
    destruct H.
    - inversion Heql1'.
    - subst_list x0 a lst2 l2 Heql2'0.
      pose proof (IHl2 H eq_refl).
      exact (hl2 l1 l2 H0 a).
    - subst_list x0 x lst1 l1 Heql1'.
      subst_list x a lst2 l2 Heql2'0.
      contradict n.
      auto.
Qed.