Require Import Arith Lia List Permutation.

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

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

Set Implicit Arguments.

Reserved Notation "x ≡ y" (at level 70, no associativity).
Reserved Notation "x ⊆ y" (at level 70, no associativity).

Local Infix "~p" := (@Permutation _) (at level 70, no associativity).

Section seteq.

  Variable X : Type.


  Inductive seteq : list X -> list X -> Prop :=
    | seteq_nil : nil ≡ nil
    | seteq_skip : forall x l m, l ≡ m -> x::l ≡ x::m
    | seteq_swap : forall x y l, x::y::l ≡ y::x::l
    | seteq_dup : forall x l, x::x::l ≡ x::l
    | seteq_sym : forall l m, l ≡ m -> m ≡ l
    | seteq_trans : forall l m k, l ≡ m -> m ≡ k -> l ≡ k
  where "l ≡ m" := (seteq l m).

  Hint Constructors seteq : core.

  Fact perm_seteq l m : l ~p m -> l ≡ m.
  Proof. induction 1; eauto. Qed.

  Notation "l ⊆ m" := (incl l m).

  Fact incl_cons_mono (x : X) l m : l ⊆ m -> x::l ⊆ x::m.
  Proof. intros ? ? [ -> | ]; simpl; auto. Qed.

  Fact incl_swap (x y : X) l : x::y::l ⊆ y::x::l.
  Proof. intros ? [ -> | [ -> | ] ]; simpl; auto. Qed.

  Fact incl_cntr (x : X) l : x::x::l ⊆ x::l.
  Proof. intros ? [ -> | [ -> | ] ]; simpl; auto. Qed.

  Hint Resolve incl_refl incl_cons_mono incl_swap incl_cntr incl_tl : core.

  Fact seqeq_incl l m : l ≡ m -> l ⊆ m /\ m ⊆ l.
  Proof.
    induction 1 as [ | x l m H [] | x y l | x l
                   | l m H []
                   | l m k H1 IH1 H2 IH2 ]; auto.
    split; apply incl_tran with m; tauto.
  Qed.

  Lemma list_has_dup_seteq l : list_has_dup l -> exists m, m ≡ l /\ length m < length l.
  Proof.
    induction 1 as [ l x H | l x H (m & H1 & H2) ].
    + induction l as [ | y l IHl ].
      * exfalso; destruct H.
      * destruct H as [ -> | H ].
        - exists (x::l); simpl; split; auto; lia.
        - destruct (IHl H) as (m & H1 & H2).
          exists (y::m); simpl in *; split; try lia.
          apply seteq_trans with (y::x::l); auto.
    + exists (x::m); simpl; split; auto; lia.
  Qed.


  Lemma incl_seteq l m : l ⊆ m -> m ⊆ l -> l ≡ m.
  Proof.
    induction on l m as IH with measure (length l + length m).
    intros H1 H2.
    destruct (le_lt_dec (length l) (length m)) as [ H3 | H3 ];
      [ destruct length_le_and_incl_implies_dup_or_perm with (1 := H3)
        as [ H4 | H4 ]; auto | ].
    + destruct list_has_dup_seteq with (1 := H4) as (m' & H5 & H6).
      apply seteq_trans with m'; auto.
      apply seqeq_incl in H5; destruct H5.
      apply IH; try lia; apply incl_tran with m; auto.
    + apply seteq_sym, perm_seteq; auto.
    + generalize (finite_php_dup H3 H1); intros H4.
      destruct list_has_dup_seteq with (1 := H4) as (m' & H5 & H6).
      apply seteq_trans with m'; auto.
      apply seqeq_incl in H5; destruct H5.
      apply IH; try lia; apply incl_tran with l; auto.
  Qed.

  Hint Resolve seqeq_incl incl_seteq : core.


  Theorem seteq_bi_incl l m : l ≡ m <-> l ⊆ m /\ m ⊆ l.
  Proof. split; auto; intros []; auto. Qed.

End seteq.

Local Infix "≡" := seteq.
Local Infix "⊆" := incl.