Library Stdlib.Wellfounded.List_Extension

Require Import List.
Require Import Relation_Operators Operators_Properties.
Import ListNotations.

Section WfList_Extension.

  Variable A : Type.
  Variable ltA : A -> A -> Prop.

  Inductive list_ext : list A -> list A -> Prop :=
    | list_ext_intro a (bs : list A) l1 l2 :
        Forall (fun b => ltA b a) bs -> list_ext (l1 ++ bs ++ l2) (l1 ++ a :: l2).

  Lemma list_ext_inv l l' : list_ext l l' ->
    exists a bs l1 l2, l = l1 ++ bs ++ l2 /\ l' = l1 ++ a :: l2 /\ Forall (fun b => ltA b a) bs.

  Lemma list_ext_nil_r l : not (list_ext l []).

  Lemma Acc_list_ext_app l1 l2 : Acc list_ext l1 -> Acc list_ext l2 -> Acc list_ext (l1 ++ l2).

  Lemma Acc_list_ext l : Forall (Acc ltA) l -> Acc list_ext l.

  Theorem wf_list_ext : well_founded ltA -> well_founded list_ext.

  #[local] Notation "list_ext ^+" := (clos_trans (list A) list_ext).
  #[local] Notation "list_ext ^*" := (clos_refl_trans (list A) list_ext).

  Lemma clos_trans_list_ext_nil_l l : l <> [] -> list_ext ^+ [] l.

  Lemma list_ext_app_r l1 l2 l : list_ext l1 l2 -> list_ext (l1 ++ l) (l2 ++ l).

  Lemma list_ext_app_l l l1 l2 : list_ext l1 l2 -> list_ext (l ++ l1) (l ++ l2).

  Lemma clos_refl_trans_list_ext_app_r l1 l2 l : list_ext ^* l1 l2 -> list_ext ^* (l1 ++ l) (l2 ++ l).

  Lemma clos_refl_trans_list_ext_app_l l l1 l2 : list_ext ^* l1 l2 -> list_ext ^* (l ++ l1) (l ++ l2).

  Lemma clos_trans_list_ext_app_l l1 l2 l3 l4 : list_ext ^+ l1 l3 -> list_ext ^* l2 l4 -> list_ext ^+ (l1 ++ l2) (l3 ++ l4).

  Lemma clos_trans_list_ext_app_r l1 l2 l3 l4 : list_ext ^* l1 l3 -> list_ext ^+ l2 l4 -> list_ext ^+(l1 ++ l2) (l3 ++ l4).

End WfList_Extension.