foo.v

Require Import Wellfounded Relations List.
Import ListNotations.

Arguments slexprod {_ _} _ _ _ _.

Section EmptyRel.
  Definition emptyrel A : relation A := fun _ _ => False.

  Lemma wf_emptyrel A : well_founded (emptyrel A).
  Proof.
    constructor. contradiction.
  Qed.
End EmptyRel.

Section OptRel.
  Context {A} (R:relation A).

  Definition opt_rel : relation (option A) :=
    fun x y =>
      match x, y with
      | Some x, Some y => R x y
      | None, Some _ => True
      | Some _, None => False
      | None, None => False
      end.

  Lemma Acc_opt_rel_None : Acc opt_rel None.
  Proof.
    constructor;intros [y|] H;simpl in H;contradiction.
  Defined.

  Lemma Acc_opt_rel_Some x (a:Acc R x) : Acc opt_rel (Some x).
  Proof.
    induction a.
    constructor.
    intros [y|] Hy;simpl in Hy.
    - auto.
    - apply Acc_opt_rel_None.
  Defined.

  Lemma wf_opt_rel : @well_founded A R -> well_founded opt_rel.
  Proof.
    intros H [x|].
    - apply Acc_opt_rel_Some,H.
    - apply Acc_opt_rel_None.
  Defined.

End OptRel.

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.

Fixpoint vector x : Set :=
  match x with
  | 0 => unit
  | S x => option (nat * vector x)
  end.

Fixpoint tovec x (l:list nat) : vector x :=
  match x, l with
  | 0, _ => tt
  | S _, [] => None
  | S x, v :: tl => Some (v, tovec x tl)
  end.

Fixpoint veclt x : relation (vector x) :=
  match x with
  | 0 => emptyrel unit
  | S x => opt_rel (slexprod lt (veclt x))
  end.

Lemma wf_veclt x : well_founded (veclt x).
Proof.
  induction x as [|x IH].
  - apply wf_emptyrel.
  - simpl.
    apply wf_opt_rel, wf_slexprod.
    + exact PeanoNat.Nat.lt_wf_0.
    + assumption.
Defined.

Lemma PrefixLt_veclt x l1 l2 : PrefixLt x l1 l2 -> veclt x (tovec x l1) (tovec x l2).
Proof.
  intros H.
  apply PrefixLt_to' in H.
  destruct H as [(prefix & n & n' & tl1 & tl2 & IH1 & IH2 & IH3) [Hlen1 Hlen2]].
  subst.
  induction prefix as [|p prefix IH] in x, Hlen1, Hlen2 |- *;simpl in *.
  - destruct x as [|x];try solve [inversion Hlen1].
    simpl.
    constructor 1;assumption.
  - destruct x as [|x];try solve [inversion Hlen1].
    simpl.
    constructor 2.
    apply IH;apply le_S_n;assumption.
Qed.

Lemma wf_PrefixLt x : well_founded (PrefixLt x).
Proof.
  eapply wf_incl.
  - exact (PrefixLt_veclt x).
  - apply wf_inverse_image,wf_veclt.
Qed.