prefixlt alt

foo.v

Require Import Wellfounded Relations List.
Import ListNotations.

Inductive PrefixLt (x: nat): relation (list nat) :=
| p_head (m m': list nat) (n n': nat):
  length (n :: m) <= x ->
  length (n' :: m') <= x ->
  n < n' ->
  PrefixLt x (n :: m) (n' :: m')
| p_tail (m m': list nat) (n n': nat):
  length (n :: m) <= x ->
  length (n' :: m') <= x ->
  n = n' ->
  PrefixLt x m m' ->
  PrefixLt x (n :: m) (n' :: m').

Definition PrefixLt0 l1 l2 :=
  exists prefix n n' tl1 tl2, n < n' /\ l1 = prefix ++ [n] ++ tl1 /\ l2 = prefix ++ [n'] ++ tl2.

Definition PrefixLt' x l1 l2 :=
  PrefixLt0 l1 l2 /\ length l1 <= x /\ length l2 <= x.

Lemma PrefixLt_len x l1 l2 : PrefixLt x l1 l2 -> length l1 <= x /\ length l2 <= x.
Proof.
  destruct 1;auto.
Qed.

Lemma PrefixLt_to0 x l1 l2 : PrefixLt x l1 l2 -> PrefixLt0 l1 l2.
Proof.
  induction 1 as [|??? k ???? IH].
  - exists []. repeat eexists;eauto.
  - subst. destruct IH as (prefix & n & n' & tl1 & tl2 & IH1 & IH2 & IH3).
    exists (k::prefix), n, n', tl1, tl2;subst;simpl. eauto.
Qed.

Lemma PrefixLt_to' x l1 l2 : PrefixLt x l1 l2 -> PrefixLt' x l1 l2.
Proof.
  intros H;split.
  - eapply PrefixLt_to0;eassumption.
  - apply PrefixLt_len;assumption.
Qed.

Lemma PrefixLt_from' x l1 l2 : PrefixLt' x l1 l2 -> PrefixLt x l1 l2.
Proof.
  intros H. destruct H as [(prefix & n & n' & tl1 & tl2 & IH1 & IH2 & IH3) [Hlen1 Hlen2]].
  subst.
  induction prefix in x, Hlen1, Hlen2 |- *;simpl in *.
  - constructor 1;simpl;assumption.
  - constructor 2;auto.
    apply IHprefix;etransitivity;try apply PeanoNat.Nat.le_succ_diag_r;assumption.
Qed.