Library list_extensions.list_permut
Add LoadPath "basis".
Set Implicit Arguments.
Require Import decidable_set.
Require Import List.
Require Import more_list.
Require Import equiv_list.
Require Import Relations.
Require Import Arith.
Require Import Setoid.
Inductive permut (A B : Set) (R : A -> B -> Prop) : (list A -> list B -> Prop) :=
| Pnil : permut R nil nil
| Pcons : forall a b l l1 l2, R a b -> permut R l (l1 ++ l2) ->
permut R (a :: l) (l1 ++ b :: l2).
Lemma permut_nil :
forall (A B : Set) (R : A -> B -> Prop) l, permut R l nil -> l = nil.
Proof.
intros A B R l P; inversion P as [ | a b l' l1 l2 a_R_b P']; trivial.
destruct l1; discriminate.
Qed.
Lemma permut_impl :
forall (A B : Set) (R R' : A -> B -> Prop) l1 l2,
(forall a b, R a b -> R' a b) -> permut R l1 l2 -> permut R' l1 l2.
Proof.
intros A B R R' l1; induction l1 as [ | a1 l1]; intros l2 Compat P;
inversion P as [ | a b k k1 k2 a_R_b Q]; subst.
apply Pnil.
apply Pcons.
apply Compat; trivial.
apply IHl1; trivial.
Qed.
Lemma permut_strong :
forall (A B : Set) (R : A -> B -> Prop) a1 a2 l1 k1 l2 k2,
R a1 a2 -> permut R (l1 ++ k1) (l2 ++ k2) ->
permut R (l1 ++ a1 :: k1) (l2 ++ a2 :: k2).
Proof.
intros A B R a1 a2 l1; induction l1 as [ | u1 l1];
intros k1 l2 k2 a1_R_a2 P.
apply (@Pcons _ _ R a1 a2 k1 l2 k2); trivial.
inversion P as [ | b1 b2 l k k' b1_R_b2 Q]; clear P; subst.
destruct (split_list _ _ _ _ H) as [H' | H']; clear H.
destruct H' as [l [H1 H2]]; subst; simpl.
assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) (l2 ++ a2 :: l) k' b1_R_b2).
do 2 rewrite <- ass_app in Q'; simpl in Q'; apply Q'.
apply IHl1; trivial.
rewrite ass_app; trivial.
destruct H' as [l [H1 H2]]; subst; simpl.
destruct l as [ | u l].
simpl in H2; subst k2; rewrite <- app_nil_end.
assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) (k ++ a2 :: nil) k' b1_R_b2).
do 2 rewrite <- ass_app in Q'; simpl in Q'; apply Q'.
apply IHl1; trivial.
simpl in H2; injection H2; clear H2; intros H2 b2_eq_u; subst u k'.
assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) k (l ++ a2 :: k2) b1_R_b2).
rewrite <- ass_app; simpl; apply Q'.
rewrite ass_app; apply IHl1; trivial.
rewrite <- ass_app; trivial.
Qed.
Lemma permut_inv_left_strong :
forall (A B : Set) (R : A -> B -> Prop) a l1' l1'' l2,
permut R (l1' ++ a :: l1'') l2 -> exists b, exists l2', exists l2'',
(R a b /\ l2 = l2' ++ b :: l2'' /\ permut R (l1' ++ l1'') (l2' ++ l2'')).
Proof.
intros A B R a l1'; generalize a; clear a;
induction l1' as [ | a1 l1']; intros a l1'' l2 P.
inversion P as [ | a' b l' l2' l2'' a_R_b Q H]; clear P; subst.
exists b; exists l2'; exists l2''; repeat split; trivial.
inversion P as [ | a1' b l' l2' l2'' a1_R_b Q H]; clear P; subst.
destruct (IHl1' _ _ _ Q) as [b' [k2' [k2'' [a_R_b' [H Q']]]]]; clear Q.
destruct (split_list _ _ _ _ H) as [H' | H']; clear H.
destruct H' as [[ | b'' l] [H1 H2]]; simpl in *; subst.
exists b'; exists (k2' ++ b :: nil); exists k2''; repeat split; trivial.
rewrite <- app_nil_end; rewrite <- ass_app; simpl; trivial.
rewrite <- ass_app; simpl; apply Pcons; trivial.
injection H2; clear H2; intros; subst.
exists b''; exists k2'; exists (l ++ b :: l2''); repeat split; trivial.
rewrite <- ass_app; simpl; trivial.
rewrite ass_app; apply Pcons; trivial; rewrite <- ass_app; trivial.
destruct H' as [l [H1 H2]]; subst.
exists b'; exists (l2' ++ b :: l); exists k2''; repeat split; trivial.
rewrite <- ass_app; simpl; trivial.
rewrite <- ass_app.
do 2 rewrite <- app_comm_cons; apply Pcons; trivial; rewrite ass_app; trivial.
Qed.
Lemma permut_inv_right :
forall (A : Set) (R : relation A) b l1 l2,
permut R l1 (b :: l2) -> exists a, exists l1', exists l1'',
(R a b /\ l1 = l1' ++ a :: l1'' /\ permut R (l1' ++ l1'') l2).
Proof.
intros A R b l1; generalize b; clear b;
induction l1 as [ | a1 l1]; intros b l2 P;
inversion P as [ | a b' l' l1' l2' a_R_b' Q H]; subst.
destruct l1' as [ | a1' l1']; injection H2; clear H2; intros; subst.
exists a1; exists (@nil A); exists l1; repeat split; trivial.
simpl in Q; destruct (IHl1 _ _ Q) as [a [k1' [k1'' [a_R_b [H Q']]]]]; subst.
exists a; exists (a1 :: k1'); exists k1''; repeat split; trivial.
simpl; apply (@Pcons _ _ R a1 b' (k1' ++ k1'') l1' l2'); trivial.
Qed.
Lemma permut_inv_right_strong :
forall (A B : Set) (R : A -> B -> Prop) b l1 l2' l2'',
permut R l1 (l2' ++ b :: l2'') -> exists a, exists l1', exists l1'',
(R a b /\ l1 = l1' ++ a :: l1'' /\ permut R (l1' ++ l1'') (l2' ++ l2'')).
Proof.
intros A B R b l1; generalize b; clear b;
induction l1 as [ | a1 l1]; intros b l2' l2'' P;
inversion P as [ | a b' l' l1' k2 a_R_b' Q H]; subst.
destruct l2'; discriminate.
destruct (in_in_split_set _ _ _ _ _ _ H2) as [[H2' | H2'] | H2']; clear H2.
destruct H2' as [l [H2 H3]]; subst.
rewrite <- ass_app in Q; simpl in Q;
destruct (IHl1 b _ _ Q) as [a [l1' [l1'' [a_R_b [H Q']]]]]; subst.
exists a; exists (a1 :: l1'); exists l1''; repeat split; trivial.
simpl; rewrite ass_app; apply Pcons; trivial.
rewrite <- ass_app; trivial.
destruct H2' as [l [H2 H3]]; subst.
rewrite ass_app in Q.
destruct (IHl1 b _ _ Q) as [a [k1' [k1'' [a_R_b [H Q']]]]]; subst.
exists a; exists (a1 :: k1'); exists k1''; repeat split; trivial.
rewrite <- ass_app; simpl; apply Pcons; trivial.
rewrite ass_app; trivial.
destruct H2' as [b'_eq_b [H2 H3]]; subst.
exists a1; exists (@nil A); exists l1; repeat split; trivial.
Qed.
Lemma permut_rev :
forall (A B : Set) (R : A -> B -> Prop) l1 l2, permut R l1 l2 ->
permut (fun b a => R a b) l2 l1.
Proof.
intros A B R l1; induction l1 as [ | a1 l1]; intros l2 P;
inversion P as [ | a b l1' l2' l2'' a_R_b Q]; subst.
apply Pnil.
apply (@permut_strong B A (fun b a => R a b) b a1 l2' l2'' (@nil _) l1); trivial.
simpl; apply IHl1; trivial.
Qed.
Permutation is compatible with length.
Lemma permut_length :
forall (A : Set) (R : relation A) l1 l2, permut R l1 l2 -> length l1 = length l2.
Proof.
intros A R l; induction l as [ | a l]; intros l' P; inversion P; trivial.
subst.
rewrite length_app; simpl; rewrite plus_comm; simpl; rewrite plus_comm.
rewrite <- length_app; rewrite (IHl (l1 ++ l2)); trivial.
Qed.
Lemma permut_refl :
forall (A : Set) (R : relation A) l,
(forall a, In a l -> R a a) -> permut R l l.
Proof.
intros A R l refl_R; induction l as [ | a l].
apply Pnil.
apply (@Pcons _ _ R a a l nil l).
apply refl_R; left; trivial.
simpl; apply IHl; intros; apply refl_R; right; trivial.
Qed.
Lemma permut_sym :
forall (A : Set) (R : relation A) l1 l2,
(forall a b, In a l1 -> In b l2 -> R a b -> R b a) ->
permut R l1 l2 -> permut R l2 l1.
Proof.
intros A R l1; induction l1 as [ | a1 l1]; intros l2 sym_R P;
inversion P as [ | a b l1' l2' l2'' a_R_b Q]; subst.
apply Pnil.
apply (permut_strong (R := R) b a1 l2' l2'' (@nil A) l1).
apply sym_R; trivial; [left | apply in_or_app; right; left]; trivial.
simpl; apply IHl1; trivial.
intros; apply sym_R; trivial; [right | apply in_insert]; trivial.
Qed.
Lemma permut_trans :
forall (A : Set) (R : relation A) l1 l2 l3,
(forall a b c, In a l1 -> In b l2 -> In c l3 -> R a b -> R b c -> R a c) ->
permut R l1 l2 -> permut R l2 l3 -> permut R l1 l3.
Proof.
intros A R l1 l2; generalize l1; clear l1;
induction l2 as [ | a2 l2]; intros l1 l3 trans_R P1 P2.
inversion_clear P2; trivial.
destruct (permut_inv_right P1) as [a1 [l1' [l1'' [a1_R_a2 [H Q1]]]]]; subst l1.
inversion P2 as [ | a2' a3 l2' l3' l3'' a2_R_a3 Q2]; subst.
apply permut_strong.
apply trans_R with a2; trivial.
apply in_or_app; right; left; trivial.
left; trivial.
apply in_or_app; right; left; trivial.
apply IHl2; trivial.
intros a b c; intros; apply trans_R with b; trivial.
apply in_insert; trivial.
right; trivial.
apply in_insert; trivial.
Qed.
Lemma permut_cons_inside :
forall (A B : Set) (R : A -> B -> Prop) a b l l1 l2,
(forall a1 b1 a2 b2, In a1 (a :: l) -> In b1 (l1 ++ b :: l2) ->
In a2 (a :: l) -> In b2 (l1 ++ b :: l2) ->
R a1 b1 -> R a2 b1 -> R a2 b2 -> R a1 b2) ->
R a b -> permut R (a :: l) (l1 ++ b :: l2) -> permut R l (l1 ++ l2).
Proof.
intros A B R a b l l1 l2 trans_R a_R_b P;
destruct (permut_inv_right_strong (R := R) _ _ _ P) as [a' [l1' [l1'' [a'_R_b [H P']]]]].
destruct l1' as [ | a1' l1']; injection H; clear H; intros; subst; trivial.
inversion P' as [ | a'' b' l' k1' k2' a''_R_b' P'']; subst.
apply permut_strong; trivial.
apply trans_R with b a1'; trivial.
right; apply in_or_app; right; left; trivial.
apply in_or_app; right; left; trivial.
left; trivial.
apply in_insert; rewrite <- H; apply in_or_app; right; left; trivial.
Qed.
Lemma permut_add_inside :
forall (A B : Set) (R : A -> B -> Prop) a b l1 l1' l2 l2',
(forall a1 b1 a2 b2, In a1 (l1 ++ a :: l1') -> In b1 (l2 ++ b :: l2') ->
In a2 (l1 ++ a :: l1') -> In b2 (l2 ++ b :: l2') ->
R a1 b1 -> R a2 b1 -> R a2 b2 -> R a1 b2) ->
R a b -> permut R (l1 ++ a :: l1') (l2 ++ b :: l2') -> permut R (l1 ++ l1') (l2 ++ l2').
Proof.
intros A B R a b l1 l1' l2 l2' trans_R a_R_b P.
destruct (permut_inv_left_strong (R := R) _ _ _ P) as [b' [k2 [k2' [a_R_b' [H P']]]]].
destruct (in_in_split_set _ _ _ _ _ _ H) as [[H' | H'] | H']; clear H.
destruct H' as [l [H1 H2]]; subst.
rewrite ass_app in P'.
destruct (permut_inv_right_strong (R := R) _ _ _ P') as [a' [k1' [k1'' [a'_R_b' [H P'']]]]].
rewrite H; rewrite <- ass_app; simpl; apply permut_strong.
apply trans_R with b a; trivial.
apply in_insert; rewrite H; apply in_or_app; right; left; trivial.
apply in_or_app; right; left; trivial.
apply in_or_app; right; left; trivial.
apply in_or_app; left; apply in_or_app; right; left; trivial.
rewrite ass_app; trivial.
destruct H' as [l [H1 H2]]; subst.
rewrite <- ass_app in P'; simpl in P'.
destruct (permut_inv_right_strong (R := R) _ _ _ P') as [a' [k1' [k1'' [a'_R_b' [H P'']]]]].
rewrite H; rewrite ass_app; simpl; apply permut_strong.
apply trans_R with b a; trivial.
apply in_insert; rewrite H; apply in_or_app; right; left; trivial.
apply in_or_app; right; left; trivial.
apply in_or_app; right; left; trivial.
apply in_or_app; right; right; apply in_or_app; right; left; trivial.
rewrite <- ass_app; trivial.
destruct H' as [H1 [H2 H3]]; subst; trivial.
Qed.
Lemma exists_dec :
forall (A : Set) (P : A -> Prop) (l : list A),
(forall a, In a l -> {P a}+{~P a}) ->
{a | In a l /\ P a}+{~exists a, In a l /\ P a}.
Proof.
intros A P l P_dec; induction l as [ | a l].
right; intros [a [a_in_nil _]]; absurd (In a nil); auto.
destruct (P_dec a) as [Pa | not_Pa].
left; trivial.
left; exists a; split; trivial; left; trivial.
destruct IHl as [Ok | Ko].
intros; apply P_dec; right; trivial.
destruct Ok as [b [b_in_l P_b]].
left; exists b; split; trivial; right; trivial.
right; intros [b [[b_eq_a | b_in_l] Pb]].
subst; apply not_Pa; trivial.
apply Ko; exists b; split; trivial.
Defined.
Fixpoint split_all (A : Set) (l : list A) : list (A * (list A * list A)) :=
match l with
| nil => @nil _
| a :: l =>
(a,(@nil _, l)) ::
(map (fun bl' => match bl' with (b,(l',l'')) => (b, (a :: l',l'')) end) (split_all l))
end.
Lemma split_all_is_sound :
forall (A : Set) (l : list A) b l' l'', In (b,(l',l'')) (split_all l) <-> l = l' ++ b :: l''.
Proof.
intros A l; induction l as [ | a l]; intros b l' l''.
split; intro H.
contradiction.
destruct l'; discriminate.
simpl; split; intro H.
setoid_rewrite in_map_iff in H; destruct H as [ H | H ].
injection H; intros; subst; trivial.
destruct H as [[c [k' k'']] [H H']].
injection H; intros; subst.
simpl; apply (f_equal (fun l => a :: l)).
setoid_rewrite <- (IHl b k' l''); trivial.
setoid_rewrite in_map_iff; destruct l' as [ | a' l'];
simpl in H; injection H; intros; subst.
left; trivial.
right; exists (b,(l',l'')); split; trivial.
setoid_rewrite (IHl b l' l''); trivial.
Qed.
Lemma permut_dec :
forall (A B : Set) (R : A -> B -> Prop),
forall l1 l2, (forall a1 a2, In a1 l1 -> In a2 l2 -> {R a1 a2}+{~R a1 a2}) ->
{permut R l1 l2}+{~permut R l1 l2}.
Proof.
intros A B R l1; induction l1 as [ | a1 l1]; intros l2 R_dec.
destruct l2 as [ | a2 l2].
left; apply Pnil.
right; intro P; inversion P.
assert (P_dec : forall a : B * (list B * list B),
In a (split_all l2) ->
{(fun bll' : B * (list B * list B) =>
let (b, y) := bll' in let (l, l') := y in R a1 b /\ permut R l1 (l ++ l'))
a} +
{~
(fun bll' : B * (list B * list B) =>
let (b, y) := bll' in let (l, l') := y in R a1 b /\ permut R l1 (l ++ l'))
a}).
intros [b [l l']] H; setoid_rewrite split_all_is_sound in H.
destruct (R_dec a1 b) as [a1_R_b | not_a1_R_b].
left; trivial.
subst l2; apply in_or_app; right; left; trivial.
destruct (IHl1 (l ++ l')) as [P | not_P].
intros; apply R_dec.
right; trivial.
subst l2; apply in_insert; trivial.
left; split; trivial.
right; intros [_ P]; apply not_P; trivial.
right; intros [a1_R_b _]; apply not_a1_R_b; trivial.
assert (H := list_exists_rest_is_sound
(fun bll' =>
match bll' with
| (b,(l,l')) => R a1 b /\ permut R l1 (l ++ l')
end) (split_all l2) P_dec).
destruct (list_exists_rest
(fun bll' : B * (list B * list B) =>
let (b, y) := bll' in
let (l, l') := y in R a1 b /\ permut R l1 (l ++ l')) (split_all l2) P_dec).
left.
destruct ((proj1 H) (refl_equal _)) as [[b [l l']] [H' [a1_R_b P]]].
setoid_rewrite split_all_is_sound in H'; subst l2; apply Pcons; trivial.
right; intro P; inversion P; subst.
assert (false = true).
setoid_rewrite H; exists (b,(l0,l3)); split; trivial.
setoid_rewrite split_all_is_sound; trivial.
split; trivial.
discriminate.
Defined.
Lemma permut_map :
forall (A B A' B': Set) (R : A -> B -> Prop) (R' : A' -> B' -> Prop) (f1 : A -> A') (f2 : B -> B')
l1 l2, (forall a b, In a l1 -> In b l2 -> R a b -> R' (f1 a) (f2 b)) ->
permut R l1 l2 -> permut R' (map f1 l1) (map f2 l2).
Proof.
intros A B A' B' R R' f1 f2 l1; induction l1 as [ | a1 l1];
intros l2 Compat P; inversion P as [ | a' b l1' l2' l2'' a_R_b P' H]; subst.
simpl; apply Pnil.
rewrite map_app; simpl; apply Pcons.
apply Compat; trivial.
left; trivial.
apply in_or_app; right; left; trivial.
rewrite <- map_app; apply IHl1; trivial.
intros a b' a_in_l1 b'_in_l2; apply Compat.
right; trivial.
apply in_insert; trivial.
Qed.
Lemma permut_length_1:
forall (A B : Set) (R : A -> B -> Prop) a b, permut R (a :: nil) (b :: nil) -> R a b.
Proof.
intros A B R a b P; inversion P as [ | a' b' l' l1' l2' a_R_b' P' H1 H']; subst.
destruct l1' as [ | a1' [ | b1' l1']].
injection H'; intros; subst; trivial.
discriminate.
discriminate.
Qed.
Lemma permut_length_2 :
forall (A B : Set) (R : A -> B -> Prop) a1 b1 a2 b2,
permut R (a1 :: b1 :: nil) (a2 :: b2 :: nil) ->
(R a1 a2 /\ R b1 b2) \/ (R a1 b2 /\ R b1 a2).
Proof.
intros A B R a1 b1 a2 b2 P;
inversion P as [ | a b l l1 l2 a_R_b P' H1 H']; subst.
destruct l1 as [ | c1 l1].
destruct l2 as [ | c2 [ | d2 l2]].
discriminate.
injection H'; intros; subst.
left; split; trivial.
apply (permut_length_1 P').
discriminate.
destruct l1 as [ | d1 l1].
destruct l2 as [ | c2 l2].
injection H'; intros; subst.
right; split; trivial.
apply (permut_length_1 P').
discriminate.
destruct l1; discriminate.
Qed.
Lemma permut_size :
forall (A B : Set) (R : A -> B -> Prop) size size' l1 l2,
(forall a a', In a l1 -> In a' l2 -> R a a' -> size a = size' a') ->
permut R l1 l2 -> list_size size l1 = list_size size' l2.
Proof.
intros A B R size size' l1; induction l1 as [ | a1 l1 ]; intros l2 E P;
inversion P as [ | a b l1' l2' l2'' a_R_b P']; subst; trivial.
rewrite list_size_app; simpl.
rewrite (E a1 b); trivial.
rewrite (IHl1 (l2' ++ l2'')); trivial.
rewrite list_size_app; simpl.
rewrite plus_comm.
rewrite <- plus_assoc.
apply (f_equal (fun n => list_size size' l2' + n)).
apply plus_comm.
intros a a' a_in_la a_in_l'; apply E; trivial.
right; trivial.
apply in_insert; trivial.
left; trivial.
apply in_or_app; right; left; trivial.
Qed.
Lemma in_permut_in :
forall (A : Set) l1 l2, permut (@eq A) l1 l2 -> (forall a, In a l1 <-> In a l2).
Proof.
assert (H : forall (A : Set) l1 l2, permut (@eq A) l1 l2 -> forall a, In a l2 -> In a l1).
intros A l1 l2 P a a_in_l2;
destruct (In_split _ _ a_in_l2) as [l2' [l2'' H]]; subst.
destruct (permut_inv_right_strong (R := @eq A) _ _ _ P)
as [a' [l1' [l1'' [a_eq_a' [H _]]]]]; subst.
apply in_or_app; right; left; trivial.
intros A l1 l2 P a; split; apply H; trivial.
apply permut_sym; trivial; intros; subst; trivial.
Qed.
Permutation is compatible with append.
Lemma permut_app :
forall (A B : Set) (R : A -> B -> Prop) l1 l1' l2 l2',
permut R l1 l2 -> permut R l1' l2' -> permut R (l1 ++ l1') (l2 ++ l2').
Proof.
intros A B R l1; induction l1 as [ | a1 l1];
intros l1' l2 l2' P P'.
inversion_clear P; trivial.
inversion P as [ | a b l1'' l2'' l2''' a_R_b Q]; subst.
simpl; rewrite <- ass_app; simpl; apply Pcons; trivial.
rewrite ass_app; apply IHl1; trivial.
Qed.
Lemma permut_swapp :
forall (A B : Set) (R : A -> B -> Prop) l1 l1' l2 l2',
permut R l1 l2 -> permut R l1' l2' -> permut R (l1 ++ l1') (l2' ++ l2).
Proof.
intros A B R l1; induction l1 as [ | a1 l1];
intros l1' l2 l2' P P'.
inversion_clear P; rewrite <- app_nil_end; trivial.
inversion P as [ | a b l1'' l2'' l2''' a_R_b Q]; subst.
simpl; rewrite ass_app; apply Pcons; trivial.
rewrite <- ass_app; apply IHl1; trivial.
Qed.
Lemma permut_app1 :
forall (A : Set) (R : relation A), equivalence _ R ->
forall l l1 l2, permut R l1 l2 <-> permut R (l ++ l1) (l ++ l2).
Proof.
intros A R E l l1 l2; split; intro P.
induction l as [ | u l]; trivial.
simpl; apply (@Pcons _ _ R u u (l ++ l1) (@nil A) (l ++ l2)); trivial.
apply (equiv_refl _ _ E).
induction l as [ | u l]; trivial.
apply IHl.
apply (@permut_cons_inside A A R u u (l ++ l1) (@nil _) (l ++ l2)); trivial.
intros a1 b1 a2 b2 _ _ _ _ a1_R_b1 a2_R_b1 a2_R_b2;
apply (equiv_trans _ _ E) with b1; trivial.
apply (equiv_trans _ _ E) with a2; trivial.
apply (equiv_sym _ _ E); trivial.
apply (equiv_refl _ _ E).
Qed.
Lemma permut_app2 :
forall (A : Set) (R : relation A), equivalence _ R ->
forall l l1 l2, permut R l1 l2 <-> permut R (l1 ++ l) (l2 ++ l).
Proof.
intros A R E l l1 l2; split; intro P.
induction l as [ | u l].
do 2 rewrite <- app_nil_end; trivial.
apply permut_strong; trivial.
apply (equiv_refl _ _ E).
induction l as [ | u l].
do 2 rewrite <- app_nil_end in P; trivial.
apply IHl.
apply (@permut_add_inside A A R u u); trivial.
intros a1 b1 a2 b2 _ _ _ _ a1_R_b1 a2_R_b1 a2_R_b2;
apply (equiv_trans _ _ E) with b1; trivial.
apply (equiv_trans _ _ E) with a2; trivial.
apply (equiv_sym _ _ E); trivial.
apply (equiv_refl _ _ E).
Qed.
Lemma permut_list_exists :
forall (A B : Set) (R : A -> B -> Prop) f f', (forall t t', R t t' -> f t = f' t') ->
forall l l', permut R l l' -> list_exists f l = list_exists f' l'.
Proof.
intros A B R f f' E l; induction l as [ | a l]; simpl; intros l' P;
inversion P as [ | a' b l1 l2' l2'' a_R_b Q]; subst; simpl; trivial.
rewrite list_exists_app; simpl.
rewrite (E _ _ a_R_b).
destruct (f' b); simpl.
destruct (list_exists f' l2'); simpl; trivial.
rewrite <- list_exists_app; apply IHl; trivial.
Qed.
Lemma permut_list_forall_exists :
forall (A B A' B': Set) (R : A -> B -> Prop) (R' : A' -> B' -> Prop) f f',
(forall ta ta' tb tb', R ta tb -> R' ta' tb' -> f ta ta' = f' tb tb') ->
forall la la' lb lb', permut R la lb -> permut R' la' lb' ->
list_forall (fun t1 => list_exists (fun t2 => f t1 t2) la') la =
list_forall (fun t1 => list_exists (fun t2 => f' t1 t2) lb') lb.
Proof.
intros A B A' B' R R' f f' E la; induction la as [ | a la];
intros la' lb lb' P P';
inversion P as [ | a' b k1 k2' k2'' a_R_b Q]; subst; simpl; trivial.
rewrite list_forall_app; simpl.
rewrite (IHla la' (k2' ++ k2'') lb' Q P').
rewrite list_forall_app; simpl.
assert (E' : forall (t : A') (t' : B'), R' t t' -> f a t = f' b t').
intros; apply E; trivial.
rewrite (@permut_list_exists _ _ R' (fun t2 : A' => f a t2) (fun t2 : B' => f' b t2) E' _ _ P').
destruct (list_exists (fun t2 : B' => f' b t2) lb'); simpl; trivial.
destruct (list_forall (fun t1 : B => list_exists (fun t2 : B' => f' t1 t2) lb') k2'); simpl; trivial.
Qed.
Module Type S.
Declare Module Import EDS : decidable_set.ES.
Notation permut := (permut eq_A).
Fixpoint mem (e : A) (l : list A) {struct l} : Prop :=
match l with
| nil => False
| e' :: l => (eq_A e e') \/ mem e l
end.
Axiom permut_refl :
forall (l : list A), permut l l.
Axiom permut_sym :
forall l1 l2 : list A, permut l1 l2 -> permut l2 l1.
Axiom permut_trans :
forall l1 l2 l3 : list A, permut l1 l2 -> permut l2 l3 -> permut l1 l3.
Hint Immediate permut_refl.
Hint Resolve permut_sym.
Function remove_equiv (l1 l2 : list A) {struct l1} : (list A) * (list A) :=
match l1 with
| nil => (l1, l2)
| x1 :: l1' =>
match remove _ eq_dec x1 l2 with
| Some l2' => remove_equiv l1' l2'
| None =>
match remove_equiv l1' l2 with
| (l1'', l2'') => ((x1 :: l1'') , l2'')
end
end
end.
Axiom in_impl_mem : forall e l, In e l -> mem e l.
Axiom mem_dec : forall a l, {mem a l}+{~ mem a l}.
Axiom mem_split_set :
forall a l, mem a l -> {a' : A & {l' : list A & {l'' | eq_A a a' /\ l = l' ++ a' :: l''}}}.
Axiom mem_or_app :
forall l m a, mem a l \/ mem a m <-> mem a (l ++ m).
Axiom mem_insert :
forall l1 l2 e a, mem a (l1 ++ l2) -> mem a (l1 ++ e :: l2).
Axiom diff_mem_remove :
forall l1 l2 e a, ~eq_A a e -> mem a (l1 ++ e :: l2) -> mem a (l1 ++ l2).
Axiom mem_permut_mem :
forall l1 l2 e, permut l1 l2 -> (mem e l1 <-> mem e l2).
Axiom cons_permut_mem :
forall l1 l2 e1 e2, eq_A e1 e2 -> permut (e1 :: l1) l2 -> mem e2 l2.
Axiom permut_cons :
forall e1 e2 l1 l2, eq_A e1 e2 ->
(permut l1 l2 <-> permut (e1 :: l1) (e2 :: l2)).
Axiom permut_add_inside :
forall e1 e2 l1 l2 l3 l4, eq_A e1 e2 ->
(permut (l1 ++ l2) (l3 ++ l4) <->
permut (l1 ++ e1 :: l2) (l3 ++ e2 :: l4)).
Axiom permut_cons_inside :
forall e1 e2 l l1 l2, eq_A e1 e2 ->
(permut l (l1 ++ l2) <-> permut (e1 :: l) (l1 ++ e2 :: l2)).
Axiom permut_app1 :
forall l l1 l2, permut l1 l2 <-> permut (l ++ l1) (l ++ l2).
Axiom permut_app2 :
forall l l1 l2, permut l1 l2 <-> permut (l1 ++ l) (l2 ++ l).
Axiom list_permut_app_app :
forall l1 l2, permut (l1 ++ l2) (l2 ++ l1).
Axiom ac_syntactic :
forall (l1 l2 l3 l4 : list A),
permut (l2 ++ l1) (l4 ++ l3) ->
(exists u1, exists u2, exists u3, exists u4,
permut l1 (u1 ++ u2) /\
permut l2 (u3 ++ u4) /\
permut l3 (u1 ++ u3) /\
permut l4 (u2 ++ u4)).
Axiom permut_dec :
forall (l1 l2 : list A), {permut l1 l2}+{~permut l1 l2}.
Axiom remove_is_sound :
forall x l, match remove _ eq_dec x l with
| None => ~mem x l
| Some l' => permut l (x :: l')
end.
Axiom remove_equiv_is_sound:
forall l1 l2, match remove_equiv l1 l2 with
| (l1', l2') => exists l, permut l1 (l ++ l1') /\ permut l2 (l ++ l2') /\
(forall x, mem x l1' -> mem x l2' -> False)
end.
Add Relation (list A) permut
reflexivity proved by permut_refl
symmetry proved by permut_sym
transitivity proved by permut_trans as LP.
Add Morphism mem
with signature eq_A ==> permut ==> iff
as mem_morph.
Add Morphism (List.app (A:=A))
with signature permut ==> permut ==> permut
as app_morph.
Add Morphism (List.cons (A:=A))
with signature eq_A ==> permut ==> permut
as add_A_morph.
End S.
Module Make (EDS1 : decidable_set.ES) : S with Module EDS:= EDS1.
Module Import EDS <: decidable_set.ES := EDS1.
Notation permut := (permut eq_A).
Fixpoint mem (e : A) (l : list A) {struct l} : Prop :=
match l with
| nil => False
| e' :: l => (eq_A e e') \/ mem e l
end.
Theorem permut_refl :
forall (l : list A), permut l l.
Proof.
intro l; apply permut_refl.
intros a _; reflexivity.
Qed.
Symetry.
Theorem permut_sym :
forall l1 l2 : list A, permut l1 l2 -> permut l2 l1.
Proof.
intros l1 l2 P; apply permut_sym; trivial.
intros a b _ _ a_eq_b; symmetry; trivial.
Qed.
Hint Immediate permut_refl.
Hint Resolve permut_sym.
Transitivity.
Theorem permut_trans :
forall l1 l2 l3 : list A, permut l1 l2 -> permut l2 l3 -> permut l1 l3.
Proof.
intros l1 l2 l3 P1 P2; apply permut_trans with l2; trivial.
intros a b c _ _ _ a_eq_b b_eq_c; transitivity b; trivial.
Qed.
Add Relation (list A) permut
reflexivity proved by permut_refl
symmetry proved by permut_sym
transitivity proved by permut_trans as LP.
Lemma in_impl_mem : forall e l, In e l -> mem e l.
Proof.
intros e l; induction l as [ | a l].
contradiction.
intros [e_eq_a | e_in_l].
left; subst; reflexivity.
right; apply IHl; trivial.
Qed.
Lemma mem_dec : forall a l, {mem a l}+{~ mem a l}.
Proof.
intros a l; induction l as [ | e l]; simpl.
right; intro; trivial.
destruct (eq_dec a e) as [a_eq_e | a_diff_e].
left; left; trivial.
destruct IHl as [a_mem_l | a_not_mem_l].
left; right; trivial.
right; intros [a_eq_e | a_mem_l].
apply a_diff_e; trivial.
apply a_not_mem_l; trivial.
Defined.
Lemma mem_split_set :
forall a l, mem a l -> {a' : A & {l' : list A & {l'' | eq_A a a' /\ l = l' ++ a' :: l''}}}.
Proof.
intros a l; induction l as [ | e l]; intro a_mem_l.
contradiction.
destruct (eq_dec a e) as [a_eq_e | a_diff_e].
exists e; exists (@nil A); exists l; split; trivial.
assert (a_mem_l' : mem a l).
destruct a_mem_l as [a_eq_e | a_mem_l]; trivial.
absurd (eq_A a e); trivial.
destruct (IHl a_mem_l') as [e' [l' [l'' [a_eq_e' H]]]];
simpl in a_eq_e'; simpl in H; subst l.
exists e'; exists (e :: l'); exists l''; split; trivial.
Qed.
Lemma mem_or_app :
forall l m a, mem a l \/ mem a m <-> mem a (l ++ m).
Proof.
intros l m a; split.
induction l as [ | e l]; intros [a_mem_l | a_mem_m].
contradiction.
simpl; trivial.
destruct a_mem_l as [a_eq_e | a_mem_l].
simpl; left; trivial.
simpl; right; apply IHl; left; trivial.
simpl; right; apply IHl; right; trivial.
induction l as [ | e l]; intro a_mem_lm.
right; trivial.
simpl in a_mem_lm; destruct a_mem_lm as [a_eq_e | a_mem_lm].
left; left; trivial.
destruct (IHl a_mem_lm) as [a_mem_l | a_mem_m].
left; right; trivial.
right; trivial.
Qed.
Lemma mem_insert :
forall l1 l2 e a, mem a (l1 ++ l2) -> mem a (l1 ++ e :: l2).
Proof.
intro l1; induction l1 as [ | e1 l1]; intros l2 e a a_mem_l1l2.
simpl; right; trivial.
simpl in a_mem_l1l2; destruct a_mem_l1l2 as [a_eq_e1 | a_mem_l1l2].
simpl; left; trivial.
simpl; right; apply IHl1; trivial.
Qed.
Lemma diff_mem_remove :
forall l1 l2 e a, ~eq_A a e -> mem a (l1 ++ e :: l2) -> mem a (l1 ++ l2).
Proof.
intros l1; induction l1 as [ | e1 l1]; simpl; intros l2 e a a_diff_e a_in_l1el2.
destruct a_in_l1el2 as [e_eq_a | a_mem_l2]; trivial.
absurd (eq_A a e); trivial; symmetry; trivial.
destruct a_in_l1el2 as [e1_eq_a | a_mem_l1el2].
left; trivial.
right; apply (IHl1 l2 e); trivial.
Qed.
Lemma mem_permut_mem :
forall l1 l2 e, permut l1 l2 -> (mem e l1 <-> mem e l2).
Proof.
assert (forall l1 l2 e, permut l1 l2 -> mem e l1 -> mem e l2).
intro l1; induction l1 as [ | a1 l1]; intros l2 e P e_mem_l1.
contradiction.
inversion P as [ | a' b l' l1' l2' a1_eq_b P' H1 H']; subst.
destruct e_mem_l1 as [e_eq_a1 | e_mem_l1].
setoid_rewrite <- mem_or_app.
right; left; transitivity a1; trivial.
apply mem_insert; apply IHl1; trivial.
intros l1 l2 e P; split; apply H; trivial.
apply permut_sym; trivial.
Qed.
Add Morphism mem
with signature eq_A ==> permut ==> iff
as mem_morph.
Proof.
intros e1 e2 e1_eq_e2 l1 l2 P.
setoid_rewrite (mem_permut_mem e1 P).
clear l1 P; assert (H : forall e1 e2, eq_A e1 e2 -> mem e1 l2 -> mem e2 l2).
clear e1 e2 e1_eq_e2; intros e1 e2 e1_eq_e2;
induction l2 as [ | a l]; simpl; trivial.
intros [e1_eq_a | e1_mem_l]; [left | right; trivial].
transitivity e1; trivial.
symmetry; trivial.
apply IHl; trivial.
split; apply H; trivial.
symmetry; trivial.
Qed.
Lemma cons_permut_mem :
forall l1 l2 e1 e2, eq_A e1 e2 -> permut (e1 :: l1) l2 -> mem e2 l2.
Proof.
intros l1 l2 e1 e2 e1_eq_e2 P; setoid_rewrite <- P; left; trivial.
symmetry; trivial.
Qed.
Permutation is compatible with addition and removal of common elements
Lemma permut_cons :
forall e1 e2 l1 l2, eq_A e1 e2 ->
(permut l1 l2 <-> permut (e1 :: l1) (e2 :: l2)).
Proof.
intros e1 e2 l1 l2 e1_eq_e2; split; intro P.
apply (@Pcons _ _ eq_A e1 e2 l1 (@nil A) l2); trivial.
replace l2 with (nil ++ l2); trivial;
apply permut_cons_inside with e1 e2; trivial.
intros a1 b1 a2 b2 _ _ _ _ a1_eq_b1 a2_eq_b1 a2_eq_b2;
transitivity a2; trivial.
transitivity b1; trivial.
symmetry; trivial.
Qed.
Add Morphism (List.cons (A:=A))
with signature eq_A ==> permut ==> permut
as add_A_morph.
Proof.
intros e1 e2 e1_eq_e2 l1 l2 P; setoid_rewrite <- (@permut_cons e1 e2 l1 l2); trivial.
Qed.
Lemma permut_add_inside :
forall e1 e2 l1 l2 l3 l4, eq_A e1 e2 ->
(permut (l1 ++ l2) (l3 ++ l4) <->
permut (l1 ++ e1 :: l2) (l3 ++ e2 :: l4)).
Proof.
intros e1 e2 l1 l2 l3 l4 e1_eq_e2; split; intro P.
apply permut_strong; trivial.
apply permut_add_inside with e1 e2; trivial.
intros a1 b1 a2 b2 _ _ _ _ a1_eq_b1 a2_eq_b1 a2_eq_b2;
transitivity a2; trivial.
transitivity b1; trivial.
symmetry; trivial.
Qed.
Lemma permut_cons_inside :
forall e1 e2 l l1 l2, eq_A e1 e2 ->
(permut l (l1 ++ l2) <-> permut (e1 :: l) (l1 ++ e2 :: l2)).
Proof.
intros e1 e2 l l1 l2 e1_eq_e2; apply (permut_add_inside nil l l1 l2 e1_eq_e2).
Qed.
Permutation is compatible with append.
Lemma permut_app1 :
forall l l1 l2, permut l1 l2 <-> permut (l ++ l1) (l ++ l2).
Proof.
intros l l1 l2; apply permut_app1.
apply EDS.eq_proof.
Qed.
Lemma permut_app2 :
forall l l1 l2, permut l1 l2 <-> permut (l1 ++ l) (l2 ++ l).
Proof.
intros l l1 l2; apply permut_app2.
apply EDS.eq_proof.
Qed.
Add Morphism (List.app (A:=A))
with signature permut ==> permut ==> permut
as app_morph.
Proof.
intros.
apply permut_trans with (x1 ++ x3).
setoid_rewrite <- permut_app1; trivial.
setoid_rewrite <- permut_app2; trivial.
Qed.
Lemma list_permut_app_app :
forall l1 l2, permut (l1 ++ l2) (l2 ++ l1).
Proof.
intros l1 l2; apply permut_swapp; apply permut_refl.
Qed.
Lemma ac_syntactic_aux :
forall (l1 l2 l3 l4 : list A),
permut (l1 ++ l2) (l3 ++ l4) ->
(exists u1, exists u2, exists u3, exists u4,
permut l1 (u1 ++ u2) /\
permut l2 (u3 ++ u4) /\
permut l3 (u1 ++ u3) /\
permut l4 (u2 ++ u4)).
Proof.
induction l1 as [ | a1 l1]; intros l2 l3 l4 P.
exists (nil : list A); exists (nil : list A); exists l3; exists l4; simpl; intuition.
simpl in P.
assert (a1_in_l3l4 := cons_permut_mem (equiv_refl _ _ eq_proof a1) P).
setoid_rewrite <- mem_or_app in a1_in_l3l4;
destruct a1_in_l3l4 as [a1_in_l3 | a1_in_l4].
destruct (mem_split_set _ _ a1_in_l3) as [a1' [l3' [l3'' [a1_eq_a1' H]]]];
simpl in a1_eq_a1'; simpl in H; subst l3.
rewrite app_ass in P; rewrite <- app_comm_cons in P;
setoid_rewrite <- permut_cons_inside in P; trivial.
rewrite <- app_ass in P;
destruct (IHl1 l2 (l3' ++ l3'') l4 P) as [u1 [u2 [u3 [u4 [P1 [P2 [P3 P4]]]]]]];
exists (a1 :: u1); exists u2; exists u3; exists u4; intuition; simpl; trivial.
setoid_rewrite <- P1; auto.
apply permut_sym; setoid_rewrite <- permut_cons_inside; auto.
destruct (mem_split_set _ _ a1_in_l4) as [a1' [l4' [l4'' [a1_eq_a1' H]]]];
simpl in a1_eq_a1'; simpl in H; subst l4.
rewrite <- app_ass in P;
setoid_rewrite <- permut_cons_inside in P; trivial.
rewrite app_ass in P;
destruct (IHl1 l2 l3 (l4' ++ l4'') P) as [u1 [u2 [u3 [u4 [P1 [P2 [P3 P4]]]]]]];
exists u1; exists (a1 :: u2); exists u3; exists u4; intuition; simpl; trivial.
setoid_rewrite <- permut_cons_inside; trivial.
reflexivity.
apply permut_sym;
setoid_rewrite <- permut_cons_inside; trivial;
apply permut_sym; trivial.
Qed.
Lemma ac_syntactic :
forall (l1 l2 l3 l4 : list A),
permut (l2 ++ l1) (l4 ++ l3) ->
(exists u1, exists u2, exists u3, exists u4,
permut l1 (u1 ++ u2) /\
permut l2 (u3 ++ u4) /\
permut l3 (u1 ++ u3) /\
permut l4 (u2 ++ u4)).
Proof.
intros l1 l2 l3 l4 P; apply ac_syntactic_aux.
apply permut_trans with (l2 ++ l1).
apply list_permut_app_app.
apply permut_trans with (l4 ++ l3); trivial.
apply list_permut_app_app.
Qed.
Lemma permut_dec : forall (l1 l2 : list A), {permut l1 l2}+{~permut l1 l2}.
Proof.
intro l1; induction l1 as [ | a1 l1]; intro l2.
destruct l2.
left; apply Pnil.
right; intro P; inversion P.
destruct (mem_dec a1 l2) as [a1_in_l2 | a1_not_in_l2].
destruct (mem_split_set _ _ a1_in_l2) as [a2 [l2' [l2'' [a1_eq_a2 H]]]]; subst l2.
destruct (IHl1 (l2' ++ l2'')) as [Ok | Ko].
left; apply Pcons; trivial.
right; intro P; apply Ko.
setoid_rewrite <- permut_cons_inside in P; trivial.
right; intro P; apply a1_not_in_l2.
apply cons_permut_mem with l1 a1; trivial.
reflexivity.
Defined.
Lemma remove_is_sound :
forall x l, match remove _ eq_dec x l with
| None => ~mem x l
| Some l' => permut l (x :: l')
end.
Proof.
intros x l; generalize (in_remove _ eq_dec x l);
destruct (remove _ eq_dec x l) as [ k | ].
intros [x' [l' [l'' [x_eq_x' [H1 H2]]]]]; injection H2; intros; subst.
symmetry; setoid_rewrite <- permut_cons_inside; auto.
induction l as [ | e l].
intros _ F; contradiction.
intros H [e_eq_x | x_mem_l].
apply (H e); trivial.
left; trivial.
apply IHl; trivial.
intros a' x_eq_a' a'_in_l; apply (H a'); trivial; right; trivial.
Qed.
Function remove_equiv (l1 l2 : list A) {struct l1} : (list A) * (list A) :=
match l1 with
| nil => (l1, l2)
| x1 :: l1' =>
match remove _ eq_dec x1 l2 with
| Some l2' => remove_equiv l1' l2'
| None =>
match remove_equiv l1' l2 with
| (l1'', l2'') => ((x1 :: l1'') , l2'')
end
end
end.
Lemma remove_equiv_is_sound:
forall l1 l2, match remove_equiv l1 l2 with
| (l1', l2') => exists l, permut l1 (l ++ l1') /\ permut l2 (l ++ l2') /\
(forall x, mem x l1' -> mem x l2' -> False)
end.
Proof.
intros l1 l2;
functional induction (remove_equiv l1 l2)
as [ (* Case 1 *)
| (* Case 2 *) H1 l2 e1 l1 H2 l2' H H'
| (* Case 3 *) H1 l2 e1 l1 H2 H H' l1'' l2'' H''].
exists (@nil A); simpl; intuition.
destruct (remove_equiv l1 l2') as [l1'' l2'']; destruct H' as [l [P1 [P2 H']]].
exists (e1 :: l); simpl; split.
setoid_rewrite P1; auto.
split; trivial.
setoid_rewrite <- P2;
assert (H'' := remove_is_sound e1 l2); rewrite H in H''; trivial.
destruct (remove_equiv l1 l2) as [l1' l2']; injection H''; clear H''; intros; subst l1'' l2'';
destruct H' as [l [P1 [P2 H']]]; exists l; split.
setoid_rewrite <- permut_cons_inside; trivial.
reflexivity.
split; trivial.
intros x [x_eq_e1 | x_mem_l1'] x_mem_l2'.
assert (H'' := remove_is_sound e1 l2); rewrite H in H''.
absurd (mem e1 l2); trivial.
setoid_rewrite <- x_eq_e1.
setoid_rewrite P2.
setoid_rewrite <- mem_or_app; right; trivial.
apply (H' x); trivial.
Qed.
End Make.