D5: Więcej zabaw z listami [TODO]



From Typonomikon Require Export D5d.

Permutacje (TODO)

Permutacje jako ciągi transpozycji


Module Transpositions.

Inductive Perm {A : Type} : list A -> list A -> Prop :=
| Perm_refl : forall l : list A, Perm l l
| Perm_transp :
    forall (x y : A) (l1 l2 l3 l4 : list A),
      Perm (l1 ++ x :: l2 ++ y :: l3) l4 ->
        Perm (l1 ++ y :: l2 ++ x :: l3) l4.

Lemma Perm_cons :
  forall {A : Type} (h : A) (t1 t2 : list A),
    Perm t1 t2 -> Perm (h :: t1) (h :: t2).

Lemma Perm_trans :
  forall {A : Type} {l1 l2 l3 : list A},
    Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

Lemma Permutation_transpose :
  forall {A : Type} {x y : A} {l1 l2 l3 : list A},
    Permutation (l1 ++ x :: l2 ++ y :: l3) (l1 ++ y :: l2 ++ x :: l3).

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.

End Transpositions.

Permutacje jako ciągi transpozycji v2


Module InductiveTranspositions.

Inductive Transposition {A : Type} : list A -> list A -> Prop :=
| Transposition' :
    forall (l1 : list A) (x : A) (l2 : list A) (y : A) (l3 : list A),
      Transposition (l1 ++ x :: l2 ++ y :: l3) (l1 ++ y :: l2 ++ x :: l3).

Inductive Transposition2 {A : Type} : list A -> list A -> Prop :=
| Transposition2' :
    forall (l1 : list A) (x : A) (l2 : list A) (y : A) (l3 r1 r2: list A),
      r1 = l1 ++ x :: l2 ++ y :: l3 ->
      r2 = l1 ++ y :: l2 ++ x :: l3 ->
        Transposition2 r1 r2.

Inductive Perm {A : Type} : list A -> list A -> Prop :=
| Perm_refl : forall l : list A, Perm l l
| Perm_step_trans :
    forall l1 l2 l3 : list A,
      Transposition l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Perm_cons :
  forall (A : Type) (x : A) (l1 l2 : list A),
    Perm l1 l2 -> Perm (x :: l1) (x :: l2).

Lemma Perm_trans :
  forall (A : Type) (l1 l2 l3 : list A),
    Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Permutation_Perm :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> Perm l1 l2.

Lemma Perm_Permutation :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 -> Permutation l1 l2.

Lemma Perm_spec :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 <-> Permutation l1 l2.

Lemma Perm_count :
  forall (A : Type) (p : A -> bool) (l1 l2 : list A),
    Perm l1 l2 -> count p l1 = count p l2.

End InductiveTranspositions.

Permutacje jako ciągi transpozycji elementów sąsiednich


Module AdjacentTranspositions.

Inductive Perm {A : Type} : list A -> list A -> Prop :=
| Perm_refl : forall l : list A, Perm l l
| Perm_steptrans :
    forall (x y : A) (l1 l2 l3 : list A),
      Perm (l1 ++ y :: x :: l2) l3 -> Perm (l1 ++ x :: y :: l2) l3.

Lemma Perm_Permutation :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 -> Permutation l1 l2.

Lemma Perm_cons :
  forall {A : Type} (x : A) {l1 l2 : list A},
    Perm l1 l2 -> Perm (x :: l1) (x :: l2).

Lemma Perm_trans :
  forall {A : Type} {l1 l2 l3 : list A},
    Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

End AdjacentTranspositions.

Permutacje jako ciągi transpozycji elementów sąsiednich v2


Module Exchange.

Definition exchange {A : Type} (l1 l2 : list A) : Prop :=
  exists (x y : A) (r1 r2 : list A),
    l1 = r1 ++ x :: y :: r2 /\
    l2 = r1 ++ y :: x :: r2.

Inductive Perm {A : Type} : list A -> list A -> Prop :=
| Perm_refl : forall l : list A, Perm l l
| Perm_step_trans :
    forall l1 l2 l3 : list A,
      exchange l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Perm_cons :
  forall (A : Type) (x : A) (l1 l2 : list A),
    Perm l1 l2 -> Perm (x :: l1) (x :: l2).

Lemma Perm_trans :
  forall (A : Type) (l1 l2 l3 : list A),
    Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.

Lemma Permutation_Perm :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> Perm l1 l2.

Lemma Perm_Permutation :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 -> Permutation l1 l2.

Lemma Perm_spec :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 <-> Permutation l1 l2.

Lemma Perm_count :
  forall (A : Type) (p : A -> bool) (l1 l2 : list A),
    Perm l1 l2 -> count p l1 = count p l2.

End Exchange.

Permutacje za pomocą liczenia właściwości


Module Exactly.

Ltac inv H := inversion H; subst; clear H.

Definition Perm {A : Type} (l1 l2 : list A) : Prop :=
  forall (P : A -> Prop) (n : nat),
    Exactly P n l1 <-> Exactly P n l2.

Lemma Permutation_Exactly :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 ->
      forall (P : A -> Prop) (n : nat),
        Exactly P n l1 -> Exactly P n l2.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

Lemma Perm_front_ex :
  forall {A : Type} {h : A} {t l : list A},
    Perm (h :: t) l ->
      exists l1 l2 : list A,
        l = l1 ++ h :: l2 /\ Perm t (l1 ++ l2).

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.

End Exactly.

Permutacje za pomocą liczenia właściwości v2


Module AtLeast.

Ltac inv H := inversion H; subst; clear H.

Definition Perm {A : Type} (l1 l2 : list A) : Prop :=
  forall (P : A -> Prop) (n : nat),
    (AtLeast P n l1 <-> AtLeast P n l2).

#[global] Hint Constructors AtLeast : core.

Lemma Permutation_AtLeast :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 ->
      forall (P : A -> Prop) (n : nat),
        AtLeast P n l1 -> AtLeast P n l2.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.

Lemma AtLeast_1 :
  forall {A : Type} {P : A -> Prop} {l : list A},
    AtLeast P 1 l ->
      exists (x : A) (l1 l2 : list A),
        P x /\ l = l1 ++ x :: l2.

Lemma AtLeast_app_comm' :
  forall {A : Type} {P : A -> Prop} {n : nat} {l1 l2 : list A},
    AtLeast P n (l1 ++ l2) <-> AtLeast P n (l2 ++ l1).

Lemma AtLeast_cons_app :
  forall
    {A : Type} {P : A -> Prop} {n : nat}
    (x : A) (l1 l2 : list A),
      AtLeast P n (l1 ++ x :: l2) <->
      AtLeast P n (x :: l1 ++ l2).

Lemma Perm_front_ex :
  forall {A : Type} {h : A} {t l : list A},
    Perm (h :: t) l ->
      exists l1 l2 : list A,
        l = l1 ++ h :: l2 /\ Perm t (l1 ++ l2).

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.

#[global] Hint Constructors Exactly : core.

(* TODO *) Lemma AtLeast_Exactly :
  forall {A : Type} (l1 l2 : list A),
    (forall (P : A -> Prop) (n : nat),
      AtLeast P n l1 <-> AtLeast P n l2)
    <->
    (forall (P : A -> Prop) (n : nat),
      Exactly P n l1 <-> Exactly P n l2).

End AtLeast.

Permutacje, jeszcze dziwniej


Require Import Equality.

Module PermWeird.

(* Import H2z. *)

Inductive Elem {A : Type} (x : A) : list A -> Type :=
| Z : forall l : list A, Elem x (x :: l)
| S : forall {t : list A}, Elem x t -> forall h : A, Elem x (h :: t).

Arguments Z {A x} _.
Arguments S {A x t} _ _.

TODO: iso skopiowane z rozdziału o izomorfizmach typów.

Class iso (A B : Type) : Type :=
{
  coel : A -> B;
  coer : B -> A;
  coel_coer :
    forall a : A, coer (coel a) = a;
  coer_coel :
    forall b : B, coel (coer b) = b;
}.

Arguments coel {A B} _.
Arguments coer {A B} _.

Definition Perm {A : Type} (l1 l2 : list A) : Type :=
  forall x : A, iso (Elem x l1) (Elem x l2).


End PermWeird.

Permutacje za pomocą liczenia właściwości rozstrzygalnych


Module Count.

Definition perm {A : Type} (l1 l2 : list A) : Prop :=
  forall p : A -> bool, count p l1 = count p l2.

Lemma count_ex :
  forall (A : Type) (p : A -> bool) (l : list A),
    count p l = 0 \/
    exists (x : A) (l1 l2 : list A),
      p x = true /\ l = l1 ++ x :: l2.

Import Exchange.

Lemma Perm_perm :
  forall (A : Type) (l1 l2 : list A),
    Perm l1 l2 -> perm l1 l2.

Lemma perm_Perm :
  forall (A : Type) (l1 l2 : list A),
    perm l1 l2 -> Perm l1 l2.

End Count.

Permutacje przez wstawianie


Module Insert.

Inductive Insert {A : Type} (x : A) : list A -> list A -> Type :=
| Insert_here :
    forall l : list A, Insert x l (x :: l)
| Insert_there :
    forall (h : A) (t t' : list A), Insert x t t' -> Insert x (h :: t) (h :: t').

Inductive Perm {A : Type} : list A -> list A -> Prop :=
| Perm_nil : Perm [] []
| Perm_Insert :
    forall (x : A) (l1 l1' l2 l2' : list A),
      Insert x l1 l1' -> Insert x l2 l2' -> Perm l1 l2 -> Perm l1' l2'.

#[global] Hint Constructors Insert Perm : core.

Lemma Perm_refl :
  forall {A : Type} (l : list A),
    Perm l l.
Proof.
  induction l as [| h t]; econstructor; eauto.
Qed.

Lemma Perm_Insert' :
  forall {A : Type} (x : A) (l1 l2 : list A),
    Insert x l1 l2 -> Perm (x :: l1) l2.
Proof.
  induction 1.
    apply Perm_refl.
    econstructor; eauto. apply Perm_refl.
Qed.

Lemma Perm_trans :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> forall l3 : list A, Perm l2 l3 -> Perm l1 l3.
Proof.
  intros until 2. revert l1 H.
  induction H0; intros.
    assumption.
    {
      revert x l1 l2 l2' X X0 H0 IHPerm.
      induction H; intros.
        inv X.
        {
          apply Perm_Insert' in X.
          apply Perm_Insert' in X0.
          apply Perm_Insert' in X1.
          apply Perm_Insert' in X2.
Admitted.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.
Proof.
  induction 1.
    constructor.
    econstructor; eauto.
    econstructor; eauto. apply Perm_refl.
    eapply Perm_trans; eassumption.
Qed.

Lemma Permutation_Insert :
  forall {A : Type} (x : A) (l1 l2 : list A),
    Insert x l1 l2 -> Permutation (x :: l1) l2.
Proof.
  induction 1.
    reflexivity.
    econstructor; eauto.
Qed.

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.
Proof.
  induction 1.
    reflexivity.
    {
      apply Permutation_Insert in X.
      apply Permutation_Insert in X0.
      rewrite <- X, <- X0.
      constructor.
      assumption.
    }
Qed.

End Insert.

Permutacje przez wstawianie v2 (TODO)


Module Insert2.

(* Inductive Insert {A : Type} (x : A) : list A -> list A -> Type :=
| Insert_here :
    forall l : list A, Insert x l (x :: l)
| Insert_there :
    forall (h : A) (t t' : list A), Insert x t t' -> Insert x (h :: t) (h :: t').
 *)

Inductive Perm {A : Type} : list A -> list A -> Prop :=
| Perm_nil : Perm [] []
| Perm_insert :
    forall (x : A) (l1 l2 r1 r2 : list A),
      Perm (l1 ++ l2) (r1 ++ r2) -> Perm (l1 ++ x :: l2) (r1 ++ x :: r2).

#[global] Hint Constructors Perm : core.

Lemma Perm_refl :
  forall {A : Type} (l : list A),
    Perm l l.
Proof.
  induction l as [| h t].
    constructor.
    apply (Perm_insert h [] t [] t). cbn. assumption.
Qed.

Lemma Perm_sym :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Perm l2 l1.
Proof.
  induction 1.
    constructor.
    constructor. assumption.
Qed.

Lemma Perm_trans :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> forall l3 : list A, Perm l2 l3 -> Perm l1 l3.
Proof.
  intros until 2.
  revert l1 H.
  induction H0; intros.
    assumption.
    inv H.
      apply (f_equal length) in H3. rewrite length_app in H3. cbn in H3. lia.
Restart.
  induction 1 as [| x l1 l2 r1 r2 H12 IH].
    intros. assumption.
    {
      intros l3 H23. remember (r1 ++ x :: r2) as MID.
      revert l1 l2 H12 IH HeqMID.
      induction H23; intros.
        apply (f_equal length) in HeqMID. rewrite length_app in HeqMID. cbn in HeqMID. lia.
Admitted.

Lemma Permutation_Perm :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> Perm l1 l2.
Proof.
  induction 1.
    constructor.
    apply (Perm_insert x [] l [] l'). cbn. assumption.
    apply (Perm_insert x [y] l [] (y :: l)). cbn. apply Perm_refl.
    eapply Perm_trans; eassumption.
Qed.

Lemma Perm_Permutation :
  forall {A : Type} {l1 l2 : list A},
    Perm l1 l2 -> Permutation l1 l2.
Proof.
  induction 1.
    reflexivity.
    rewrite !Permutation_middle. constructor. assumption.
Qed.

End Insert2.

Znajdowanie wszystkich permutacji (TODO)

Znajdowanie permutacji przez selekcję


Module perms_select.

Fixpoint select {A : Type} (l : list A) : list (list A * list A) :=
match l with
| [] => [([], [])]
| h :: t => [([], l)] ++ map (fun '(a, b) => (h :: a, b)) (select t)
end.

Lemma select_app :
  forall {A : Type} {l1 l2 : list A},
    select (l1 ++ l2) =
      map (fun '(l, r) => (app l l2, r)) (select l1) ++
      map (fun '(l, r) => (app l1 l, r)) (select l2).

Fixpoint perms {A : Type} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| h :: t =>
    bind (fun ll =>
      map (fun '(l, r) => l ++ h :: r) (select ll)) (perms t)
end.

(* Compute select 1; 2; 3. *)
(* Compute perms 1; 2; 3. *)

Lemma Permutation_bind :
  forall {A B : Type} (f g : A -> list B),
    (forall x : A, Permutation (f x) (g x)) ->
      forall l : list A, Permutation (bind f l) (bind g l).

Lemma Permutation_select_app :
  forall {A : Type} {l1 l2 : list A},
    Permutation (select (l1 ++ l2)) (select (l2 ++ l1)).

Lemma map_select :
  forall {A B : Type} (f : A -> B) (l : list A),
    select (map f l)
      =
    map (fun '(L, R) => (map f L, map f R)) (select l).

Lemma Permutation_perms :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> Permutation (perms l1) (perms l2).

Lemma elem_perms :
  forall (A : Type) (l : list A),
    elem l (perms l).

Lemma Permutation_perms' :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> elem l1 (perms l2).

End perms_select.

Module perms_ins.

Znajdowanie permutacji przez wstawianie


Fixpoint ins {A : Type} (x : A) (l : list A) : list (list A) :=
match l with
| [] => [[x]]
| h :: t => [x :: h :: t] ++ map (cons h) (ins x t)
end.

Fixpoint perms {A : Type} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| h :: t => bind (ins h) (perms t)
end.

Lemma len_ins :
  forall (A : Type) (x : A) (l : list A),
    length (ins x l) = S (length l).

Fixpoint nsum (l : list nat) : nat :=
match l with
| [] => 0
| h :: t => h + nsum t
end.

Lemma len_join :
  forall (A : Type) (ll : list (list A)),
    length (join ll) = nsum (map length ll).

Lemma len_perms :
  forall (A : Type) (l : list A),
    length (perms l) = fact (length l).

Lemma map_ins :
  forall (A B : Type) (f : A -> B) (x : A) (l : list A),
    map (map f) (ins x l) = ins (f x) (map f l).

Lemma ins_app :
  forall (A : Type) (x : A) (l1 l2 : list A),
    l1 = [] \/
    l2 = [] \/
      ins x (l1 ++ l2) =
      map (fun l => app l l2) (ins x l1) ++
      map (app l1) (ins x l2).

Lemma ins_snoc :
  forall (A : Type) (x y : A) (l : list A),
    ins x (snoc y l) =
    snoc (snoc x (snoc y l)) (map (snoc y) (ins x l)).

Lemma map_ext_eq :
  forall {A B : Type} {f g : A -> B} {l : list A},
    (forall x : A, f x = g x) ->
      map f l = map g l.

Lemma ins_rev :
  forall (A : Type) (x : A) (l : list A),
    ins x (rev l) = rev (map rev (ins x l)).

Lemma elem_ins :
  forall (A : Type) (x : A) (l : list A),
    elem (x :: l) (ins x l).

Lemma elem_perms :
  forall (A : Type) (l : list A),
    elem l (perms l).

Lemma Permutation_elem_ins :
  forall (A : Type) (x : A) (l1 l2 : list A),
    elem l2 (ins x l1) -> Permutation (x :: l1) l2.

Lemma Permutation_bind :
  forall (A B : Type) (f g : A -> list B) (l1 l2 : list A),
    (forall x : A, Permutation (f x) (g x)) ->
      Permutation l1 l2 ->
        Permutation (bind f l1) (bind g l2).

Lemma count_join :
  forall (A : Type) (p : A -> bool) (l : list (list A)),
    count p (join l) = nsum (map (count p) l).

Lemma nsum_app :
  forall l1 l2 : list nat,
    nsum (l1 ++ l2) = nsum l1 + nsum l2.

Fixpoint deepcount
  {A : Type} (p : A -> bool) (l : list (list A)) : nat :=
match l with
| [] => 0
| h :: t => count p h + deepcount p t
end.

Lemma Permutation_bind_ins :
  forall {A : Type} (x y : A) (l : list A),
    Permutation (bind (ins x) (ins y l)) (bind (ins y) (ins x l)).

Lemma Permutation_perms :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> Permutation (perms l1) (perms l2).

Lemma Permutation_perms' :
  forall (A : Type) (l1 l2 : list A),
    Permutation l1 l2 -> elem l1 (perms l2).

Lemma perms_Permutation :
  forall {A : Type} {l1 l2 : list A},
    elem l1 (perms l2) -> Permutation l1 l2.

End perms_ins.

Znajdowanie permutacji przez cykle


Require Import FunctionalExtensionality.

Module perms_cycles.

Import cycles.

Fixpoint perms {A : Type} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| h :: t => join (map (fun t => cycles (cons h t)) (perms t))
end.

Compute cycles [1; 2].
Compute perms [3].
Compute perms [2; 3].
Compute cycles (map (cons 2) [[3]]).
Compute perms [1; 2; 3].
Compute perms [1; 2; 3; 4].

Fixpoint sum (l : list nat) : nat :=
match l with
| [] => 0
| h :: t => h + sum t
end.

Lemma len_join :
  forall {A : Type} (l : list (list A)),
    length (join l) = sum (map length l).

Lemma len_cycles_aux :
  forall {A : Type} (l : list A) (n : nat),
    length (cycles_aux n l) = n.

Lemma len_cycles :
  forall {A : Type} (l : list A),
    l <> [] -> length (cycles l) = length l.

Lemma sum_map_S :
  forall l : list nat,
    sum (map S l) = length l + sum l.

Lemma sum_replicate :
  forall n m : nat,
    sum (replicate n m) = n * m.

Lemma length_perms :
  forall {A : Type} (l : list A),
    length (perms l) = fact (length l) /\
      map length (perms l) =
      replicate (length (perms l)) (length l).

Lemma perms_spec :
  forall {A : Type} (l1 l2 : list A),
    elem l1 (perms l2) -> Permutation l1 l2.

Lemma perms_spec :
  forall {A : Type} (l1 l2 : list A),
    Permutation l1 l2 -> elem l1 (perms l2).

End perms_cycles.

Wut da fuk? (TODO)


Module Specs.

Import Count.

Import perms_select.

Lemma perm_perms :
  forall {A : Type} {l1 l2 : list A},
    perm l1 l2 -> elem l1 (perms l2).

End Specs.

Zbiory

Zbiory jako zdeduplikowane permutacje


(* Module SetPermDedup. *)

Inductive SameSet {A : Type} : list A -> list A -> Prop :=
| SameSet_nil : SameSet [] []
| SameSet_cons :
    forall (h : A) (t1 t2 : list A), SameSet t1 t2 -> SameSet (h :: t1) (h :: t2)
| SameSet_swap :
    forall (x y : A) (l : list A), SameSet (y :: x :: l) (x :: y :: l)
| SameSet_dedup :
    forall (h : A) (t : list A), SameSet (h :: t) (h :: h :: t)
| SameSet_trans :
    forall l1 l2 l3 : list A, SameSet l1 l2 -> SameSet l2 l3 -> SameSet l1 l3.

Lemma SameSet_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSet l1 l2 -> SetEquiv l1 l2.

Lemma Permutation_SameSet :
  forall {A : Type} {l1 l2 : list A},
    Permutation l1 l2 -> SameSet l1 l2.

(* End SetPermDedup. *)

Zbiory za pomocą Exists


Module SetExists.

Definition SameSetEx {A : Type} (l1 l2 : list A) : Prop :=
  forall P : A -> Prop, Exists P l1 <-> Exists P l2.

Lemma SameSetEx_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSetEx l1 l2 <-> SetEquiv l1 l2.

End SetExists.

Zbiory za pomocą transpozycji i deduplikacji


Module SetTranspositionDedup.

Inductive Transposition {A : Type} : list A -> list A -> Prop :=
| Transposition' :
    forall (x y : A) (l1 l2 l3 : list A),
      Transposition (l1 ++ x :: l2 ++ y :: l3) (l1 ++ y :: l2 ++ x :: l3).

Inductive Dedup {A : Type} : list A -> list A -> Prop :=
| Dedup' :
    forall (x : A) (l1 l2 l3 : list A),
      Dedup (l1 ++ x :: l2 ++ x :: l3) (l1 ++ x :: l2 ++ l3).

Inductive SameSetTD {A : Type} : list A -> list A -> Prop :=
| SameSetTD_refl :
    forall l : list A, SameSetTD l l
| SameSetTD_transp :
    forall l1 l2 l3 : list A,
      Transposition l1 l2 -> SameSetTD l2 l3 -> SameSetTD l1 l3
| SameSetTD_dedup :
    forall l1 l2 l3 : list A,
      Dedup l1 l2 -> SameSetTD l2 l3 -> SameSetTD l1 l3.

Lemma SameSetTD_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSetTD l1 l2 -> SetEquiv l1 l2.

End SetTranspositionDedup.

Zbiory za pomocą sąsiednich transpozycji i deduplikacji


Module SetAdjacentTranspositionDedup.

Inductive AdjacentTransposition {A : Type} : list A -> list A -> Prop :=
| AdjacentTransposition' :
    forall (x y : A) (l1 l2 : list A),
      AdjacentTransposition (l1 ++ x :: y :: l2) (l1 ++ y :: x :: l2).

Inductive AdjacentDedup {A : Type} : list A -> list A -> Prop :=
| AdjacentDedup' :
    forall (x : A) (l1 l2 : list A),
      AdjacentDedup (l1 ++ x :: x :: l2) (l1 ++ x :: l2).

Inductive SameSetATD {A : Type} : list A -> list A -> Prop :=
| SameSetATD_refl :
    forall l : list A, SameSetATD l l
| SameSetATD_transp :
    forall l1 l2 l3 : list A,
      AdjacentTransposition l1 l2 -> SameSetATD l2 l3 -> SameSetATD l1 l3
| SameSetATD_dedup :
    forall l1 l2 l3 : list A,
      AdjacentDedup l1 l2 -> SameSetATD l2 l3 -> SameSetATD l1 l3.

Lemma SameSetATD_trans :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD l1 l2 ->
      forall {l3 : list A}, SameSetATD l2 l3 -> SameSetATD l1 l3.

Lemma SameSetATD_SetEquiv :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD l1 l2 -> SetEquiv l1 l2.

Lemma AdjacentDedup_cons :
  forall {A : Type} {t1 t2 : list A},
    AdjacentDedup t1 t2 ->
      forall h : A, AdjacentDedup (h :: t1) (h :: t2).

Lemma SameSetATD_cons :
  forall {A : Type} {t1 t2 : list A},
    SameSetATD t1 t2 ->
      forall h : A, SameSetATD (h :: t1) (h :: t2).

Lemma SetEquiv_SameSetATD :
  forall {A : Type} {l1 l2 : list A},
    SetEquiv l1 l2 -> SameSetATD l1 l2.

Inductive SameSetATD' {A : Type} (l1 : list A) : list A -> Prop :=
| SameSetATD'_refl :
    SameSetATD' l1 l1
| SameSetATD'_transp :
    forall l2 l3 : list A,
      SameSetATD' l1 l2 -> AdjacentTransposition l2 l3 -> SameSetATD' l1 l3
| SameSetATD'_dedup :
    forall l2 l3 : list A,
      SameSetATD' l1 l2 -> AdjacentDedup l2 l3 -> SameSetATD' l1 l3.

Lemma SameSetATD'_trans :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD' l1 l2 ->
      forall {l3 : list A}, SameSetATD' l2 l3 -> SameSetATD' l1 l3.

Lemma SameSetATD'_spec :
  forall {A : Type} {l1 l2 : list A},
    SameSetATD' l1 l2 <-> SameSetATD l1 l2.

End SetAdjacentTranspositionDedup.