Library hydras.rpo.list_permut
Set Implicit Arguments.
From Coq Require Import List Multiset Arith Setoid.
From hydras Require Import decidable_set more_list.
Module Type Permut.
Declare Module DS : decidable_set.S.
Definition elt := DS.A.
Definition eq_elt_dec := DS.eq_A_dec.
Fixpoint list_to_multiset (l : list elt) {struct l} : multiset elt :=
match l with
| nil ⇒ EmptyBag elt
| h :: tl ⇒
munion (SingletonBag _ eq_elt_dec h) (list_to_multiset tl)
end.
Definition list_permut (l1 l2:list elt) : Prop :=
meq (list_to_multiset l1) (list_to_multiset l2).
End Permut.
Module Make (DS1 : decidable_set.S) <: Permut with Module DS:= DS1.
Module DS := DS1.
Import DS1.
Definition elt := DS.A.
Definition eq_elt_dec : ∀ t1 t2 : elt, {t1 = t2} + {t1 ≠ t2} := DS.eq_A_dec.
Fixpoint list_to_multiset (l : list elt) {struct l} : multiset elt :=
match l with
| nil ⇒ EmptyBag elt
| h :: tl ⇒
munion (SingletonBag _ eq_elt_dec h) (list_to_multiset tl)
end.
Definition list_permut (l1 l2:list elt) : Prop :=
meq (list_to_multiset l1) (list_to_multiset l2).
Module DS := DS1.
Import DS1.
Definition elt := DS.A.
Definition eq_elt_dec : ∀ t1 t2 : elt, {t1 = t2} + {t1 ≠ t2} := DS.eq_A_dec.
Fixpoint list_to_multiset (l : list elt) {struct l} : multiset elt :=
match l with
| nil ⇒ EmptyBag elt
| h :: tl ⇒
munion (SingletonBag _ eq_elt_dec h) (list_to_multiset tl)
end.
Definition list_permut (l1 l2:list elt) : Prop :=
meq (list_to_multiset l1) (list_to_multiset l2).
Properties over the multiplicity.
Lemma multiplicity_app :
∀ (l1 l2:list elt) (t : elt),
multiplicity (list_to_multiset (l1 ++ l2)) t =
multiplicity (list_to_multiset l1) t + multiplicity (list_to_multiset l2) t.
Lemma out_mult_O :
∀ (t : elt) (l:list elt), ¬ In t l → multiplicity (list_to_multiset l) t = 0.
Lemma in_mult_S :
∀ (t : elt) (l : list elt), In t l → multiplicity (list_to_multiset l) t ≥ 1.
∀ (l1 l2:list elt) (t : elt),
multiplicity (list_to_multiset (l1 ++ l2)) t =
multiplicity (list_to_multiset l1) t + multiplicity (list_to_multiset l2) t.
Lemma out_mult_O :
∀ (t : elt) (l:list elt), ¬ In t l → multiplicity (list_to_multiset l) t = 0.
Lemma in_mult_S :
∀ (t : elt) (l : list elt), In t l → multiplicity (list_to_multiset l) t ≥ 1.
Symetry.
Theorem list_permut_sym :
∀ l1 l2 : list elt, list_permut l1 l2 → list_permut l2 l1.
#[global] Hint Immediate list_permut_refl : core.
#[global] Hint Resolve list_permut_sym : core.
∀ l1 l2 : list elt, list_permut l1 l2 → list_permut l2 l1.
#[global] Hint Immediate list_permut_refl : core.
#[global] Hint Resolve list_permut_sym : core.
Transitivity.
Theorem list_permut_trans :
∀ l1 l2 l3 : list elt, list_permut l1 l2 → list_permut l2 l3 → list_permut l1 l3.
Add Relation (list elt) list_permut
reflexivity proved by list_permut_refl
symmetry proved by list_permut_sym
transitivity proved by list_permut_trans as LP.
∀ l1 l2 l3 : list elt, list_permut l1 l2 → list_permut l2 l3 → list_permut l1 l3.
Add Relation (list elt) list_permut
reflexivity proved by list_permut_refl
symmetry proved by list_permut_sym
transitivity proved by list_permut_trans as LP.
Permutation of an empty list.
Lemma in_permut_in :
∀ l1 l2 e, In e l1 → list_permut l1 l2 → In e l2.
Add Morphism (In (A :=elt)) with signature (eq ==> list_permut ==> iff) as in_morph.
Lemma cons_permut_in :
∀ l1 l2 e, list_permut (e :: l1) l2 → In e l2.
∀ l1 l2 e, In e l1 → list_permut l1 l2 → In e l2.
Add Morphism (In (A :=elt)) with signature (eq ==> list_permut ==> iff) as in_morph.
Lemma cons_permut_in :
∀ l1 l2 e, list_permut (e :: l1) l2 → In e l2.
Permutation is compatible with adding an element.
Lemma context_list_permut_cons :
∀ e l1 l2, list_permut l1 l2 → list_permut (e :: l1) (e :: l2).
Add Morphism (List.cons (A:=elt)) with signature (eq ==> list_permut ==> list_permut)
as add_elt_morph.
Lemma list_permut_add_inside :
∀ a l1 l2 l3 l4,
list_permut (l1 ++ l2) (l3 ++ l4) →
list_permut (l1 ++ a :: l2) (l3 ++ a :: l4).
Lemma list_permut_add_cons_inside :
∀ a l l1 l2,
list_permut l (l1 ++ l2) →
list_permut (a :: l) (l1 ++ a :: l2).
∀ e l1 l2, list_permut l1 l2 → list_permut (e :: l1) (e :: l2).
Add Morphism (List.cons (A:=elt)) with signature (eq ==> list_permut ==> list_permut)
as add_elt_morph.
Lemma list_permut_add_inside :
∀ a l1 l2 l3 l4,
list_permut (l1 ++ l2) (l3 ++ l4) →
list_permut (l1 ++ a :: l2) (l3 ++ a :: l4).
Lemma list_permut_add_cons_inside :
∀ a l l1 l2,
list_permut l (l1 ++ l2) →
list_permut (a :: l) (l1 ++ a :: l2).
Permutation is compatible with append.
Lemma context_list_permut_app1 :
∀ l l1 l2, list_permut l1 l2 → list_permut (l ++ l1) (l ++ l2).
Lemma context_list_permut_app2 :
∀ l l1 l2, list_permut l1 l2 → list_permut (l1 ++ l) (l2 ++ l).
Add Morphism (List.app (A:=elt))
with signature (list_permut ==> list_permut ==> list_permut) as app_morph.
Lemma list_permut_app_app :
∀ l1 l2, list_permut (l1 ++ l2) (l2 ++ l1).
∀ l l1 l2, list_permut l1 l2 → list_permut (l ++ l1) (l ++ l2).
Lemma context_list_permut_app2 :
∀ l l1 l2, list_permut l1 l2 → list_permut (l1 ++ l) (l2 ++ l).
Add Morphism (List.app (A:=elt))
with signature (list_permut ==> list_permut ==> list_permut) as app_morph.
Lemma list_permut_app_app :
∀ l1 l2, list_permut (l1 ++ l2) (l2 ++ l1).
Permutation is compatible with removal of common elements
Lemma remove_context_list_permut_cons :
∀ e l1 l2, list_permut (e :: l1) (e :: l2) → list_permut l1 l2.
Lemma remove_context_list_permut_app2 :
∀ l l1 l2, list_permut (l1 ++ l) (l2 ++ l) → list_permut l1 l2.
Lemma list_permut_remove_hd :
∀ l l1 l2 a,
list_permut (a :: l) (l1 ++ a :: l2) → list_permut l (l1 ++ l2).
∀ e l1 l2, list_permut (e :: l1) (e :: l2) → list_permut l1 l2.
Lemma remove_context_list_permut_app2 :
∀ l l1 l2, list_permut (l1 ++ l) (l2 ++ l) → list_permut l1 l2.
Lemma list_permut_remove_hd :
∀ l l1 l2 a,
list_permut (a :: l) (l1 ++ a :: l2) → list_permut l (l1 ++ l2).
Permutation is compatible with length.
Lemma list_permut_length :
∀ l1 l2, list_permut l1 l2 → length l1 = length l2.
Add Morphism (length (A:=elt)) with signature (list_permut ==> eq) as length_morph.
∀ l1 l2, list_permut l1 l2 → length l1 = length l2.
Add Morphism (length (A:=elt)) with signature (list_permut ==> eq) as length_morph.
Permutation is compatible with size.
Lemma list_permut_size :
∀ size l1 l2, list_permut l1 l2 → list_size size l1 = list_size size l2.
Add Parametric Morphism size : (@list_size elt size) with signature (list_permut ==> @eq nat) as list_size_morph.
∀ size l1 l2, list_permut l1 l2 → list_size size l1 = list_size size l2.
Add Parametric Morphism size : (@list_size elt size) with signature (list_permut ==> @eq nat) as list_size_morph.
Permutation is compatible with map.
Lemma list_permut_map :
∀ f l1 l2, list_permut l1 l2 → list_permut (map f l1) (map f l2).
Add Parametric Morphism f : (map f) with signature list_permut ==> list_permut as map_morph.
∀ f l1 l2, list_permut l1 l2 → list_permut (map f l1) (map f l2).
Add Parametric Morphism f : (map f) with signature list_permut ==> list_permut as map_morph.
Lemma list_permut_length_1:
∀ a b, list_permut (a :: nil) (b :: nil) → a = b.
Lemma list_permut_length_2 :
∀ a1 b1 a2 b2, list_permut (a1 :: b1 :: nil) (a2 :: b2 :: nil) →
(a1=a2 ∧ b1=b2) ∨ (a1=b2 ∧ a2=b1).
Lemma ac_syntactic_aux :
∀ (l1 l2 l3 l4 : list elt),
list_permut (l1 ++ l2) (l3 ++ l4) →
(∃ u1, ∃ u2, ∃ u3, ∃ u4,
list_permut l1 (u1 ++ u2) ∧
list_permut l2 (u3 ++ u4) ∧
list_permut l3 (u1 ++ u3) ∧
list_permut l4 (u2 ++ u4)).
Lemma ac_syntactic :
∀ (l1 l2 l3 l4 : list elt),
list_permut (l2 ++ l1) (l4 ++ l3) →
(∃ u1, ∃ u2, ∃ u3, ∃ u4,
list_permut l1 (u1 ++ u2) ∧
list_permut l2 (u3 ++ u4) ∧
list_permut l3 (u1 ++ u3) ∧
list_permut l4 (u2 ++ u4)).
Lemma list_permut_dec : ∀ l1 l2, {list_permut l1 l2}+{¬list_permut l1 l2}.
End Make.
∀ (l1 l2 l3 l4 : list elt),
list_permut (l1 ++ l2) (l3 ++ l4) →
(∃ u1, ∃ u2, ∃ u3, ∃ u4,
list_permut l1 (u1 ++ u2) ∧
list_permut l2 (u3 ++ u4) ∧
list_permut l3 (u1 ++ u3) ∧
list_permut l4 (u2 ++ u4)).
Lemma ac_syntactic :
∀ (l1 l2 l3 l4 : list elt),
list_permut (l2 ++ l1) (l4 ++ l3) →
(∃ u1, ∃ u2, ∃ u3, ∃ u4,
list_permut l1 (u1 ++ u2) ∧
list_permut l2 (u3 ++ u4) ∧
list_permut l3 (u1 ++ u3) ∧
list_permut l4 (u2 ++ u4)).
Lemma list_permut_dec : ∀ l1 l2, {list_permut l1 l2}+{¬list_permut l1 l2}.
End Make.