Require Import Arith List Wellfounded.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import php.

From Undecidability.Shared.Libs.DLW.Wf
  Require Import acc_irr measure_ind wf_chains.

Set Implicit Arguments.


Section sincl.


  Variable (X : Type).

  Implicit Type (l m : list X).


  Definition sincl l m := incl l m /\ exists x, ~ In x l /\ In x m.


  Lemma sincl_chain n m l :
       chain sincl n m l -> incl m l
                         /\ exists ll, ~ list_has_dup ll
                                      /\ length ll = n
                                      /\ incl ll l
                                      /\ forall x, In x m -> In x ll -> False.
  Proof.
    induction 1 as [ m | n m l k H1 H2 (H7 & ll & H3 & H4 & H5 & H6) ].
    + split.
      * intros ?; auto.
      * exists nil; simpl; repeat split; auto.
        - inversion 1.
        - intros _ [].
    + split.
      * intros ? ?; apply H7, H1; auto.
      * destruct H1 as (G1 & x & G2 & G3).
        exists (x::ll); simpl; repeat split; auto.
        - contradict H3.
          apply list_has_dup_cons_inv in H3.
          destruct H3 as [ H3 | ]; auto.
          destruct (H6 x); auto.
        - apply incl_cons; auto.
        - intros y F1 [ F2 | F2 ]; subst.
          ** tauto.
          ** apply (H6 y); auto.
  Qed.


  Corollary sincl_chain_bounded l m n : chain sincl n m l -> n <= length l.
  Proof.
    intros H.
    apply sincl_chain in H.
    destruct H as (_ & ll & H1 & H2 & H3 & _).
    destruct (le_lt_dec n (length l)) as [ | C ]; auto.
    subst; destruct H1.
    apply finite_php_dup with l; auto.
  Qed.


  Theorem wf_sincl : well_founded sincl.
  Proof.
    apply wf_chains.
    intros l; exists (length l).
    intros ? ?; apply sincl_chain_bounded.
  Qed.

End sincl.

Arguments wf_sincl {X}.

Section rincl_fin.



  Variable (X : Type) (M : list X).


  Definition rincl_fin l m := (forall x, In x m -> In x M -> In x l)
                            /\ exists x, ~ In x m /\ In x l /\ In x M.


  Lemma rincl_fin_chains n m l : chain rincl_fin n m l
                   -> exists ll, ~ list_has_dup ll
                                /\ incl ll M
                                /\ length ll = n
                                /\ incl ll m.
  Proof.
    induction 1 as [ x | n m k l H1 H2 (ll & H3 & H4 & H5 & H6) ].
    + exists nil.
      repeat split; simpl; auto; inversion 1.
    + destruct H1 as (H1 & a & G1 & G2 & G3).
      exists (a::ll).
      repeat split.
      * contradict H3.
        apply list_has_dup_cons_inv in H3.
        destruct H3 as [ H3 | ]; auto.
        destruct G1; apply H6; auto.
      * apply incl_cons; auto.
      * simpl; f_equal; auto.
      * apply incl_cons; auto.
        intros ? ?; auto.
  Qed.


  Corollary rincl_fin_chain_bounded l m n : chain rincl_fin n m l -> n <= length M.
  Proof.
    intros H.
    apply rincl_fin_chains in H.
    destruct H as (ll & H1 & H2 & H3 & _).
    destruct (le_lt_dec n (length M)) as [ | C ]; auto.
    subst n; destruct H1.
    apply finite_php_dup with M; auto.
  Qed.

  Theorem wf_rincl_fin : well_founded rincl_fin.
  Proof.
    apply wf_chains.
    intros l; exists (length M).
    intros ? ?; apply rincl_fin_chain_bounded.
  Qed.

End rincl_fin.

Arguments wf_rincl_fin {X}.