Library list_extensions.math_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 Multiset.
Require Import Arith.
Require Import Setoid.
Require list_permut.
Definition permut (n : nat) (f : nat -> nat) :=
(forall i, n <= i -> f i = i) /\
(forall i, i < n -> f i < n) /\
(forall i j, i < n -> j < n -> f i = f j -> i = j).
Lemma adequacy :
forall (A : Set) (R : relation A) (l1 l2 : list A),
list_permut.permut R l1 l2 <->
(length l1 = length l2 /\
exists pi, (permut (length l1) pi) /\
forall i, i < length l1 ->
match (nth_error l1 i), (nth_error l2 (pi i)) with
| (Some ai), (Some bi) => R ai bi
| _, _ => False
end).
Proof.
intros A R l1; pattern l1; apply list_rec2; clear l1.
intro n; induction n as [ | n]; intros l1 L1 l2; split.
intros P; inversion P; subst.
split; trivial.
exists (fun (i : nat) => i); repeat split; trivial.
intros i L; simpl in L; inversion L.
simpl in L1; inversion L1.
intros [L _]; destruct l1 as [ | a1 l1].
destruct l2 as [ | a2 l2].
apply list_permut.Pnil.
simpl in L; discriminate.
simpl in L1; inversion L1.
intros P; inversion P as [ | a1 b1 l1' l2' l2'' a1_R_b1 Q ]; subst; split; trivial.
exists (fun (i : nat) => i); repeat split; trivial.
intros i L; simpl in L; inversion L.
rewrite (list_permut.permut_length P); trivial.
simpl in L1; generalize (le_S_n _ _ L1); clear L1; intro L1.
setoid_rewrite (IHn l1' L1 (l2' ++ l2'')) in Q.
destruct Q as [ L [pi [ Q H]]].
exists (fun (i : nat) =>
match i with
| 0 => length l2'
| S i =>
if le_lt_dec (length l2') (pi i)
then S (pi i)
else pi i
end); split.
unfold permut in *; repeat split.
intros [ | i] L'; simpl in L'.
inversion L'.
generalize (le_S_n _ _ L'); clear L'; intro L'.
destruct Q as [Q _].
rewrite (Q i L').
destruct (le_lt_dec (length l2') i) as [ll2'_le_i | ll2'_gt_i]; trivial.
rewrite L in L'.
absurd (length l2' < length l2'); auto with arith.
apply le_lt_trans with i; trivial.
apply le_trans with (length (l2' ++ l2'')); trivial.
rewrite length_app; auto with arith.
intros [ | i] L'.
simpl; rewrite L; unfold lt; apply le_n_S; rewrite length_app; auto with arith.
simpl in L'; generalize (le_S_n _ _ L'); clear L'; intro L'.
destruct Q as [_ [Q _]].
destruct (le_lt_dec (length l2') (pi i)) as [ll2'_le_pii | ll2'_gt_pii].
simpl; unfold lt; apply le_n_S; apply Q; trivial.
simpl; apply lt_le_trans with (length l1').
apply Q; trivial.
auto with arith.
destruct Q as [_ [_ Q]].
intros [ | i] [ | j] L' L'' H'; trivial.
destruct (le_lt_dec (length l2') (pi j)) as [ll2'_cmp_pij | ll2'_cmp_pij];
rewrite H' in ll2'_cmp_pij;
absurd (S (pi j) <= pi j); trivial; auto with arith.
destruct (le_lt_dec (length l2') (pi i)) as [ll2'_cmp_pii | ll2'_cmp_pii];
rewrite <- H' in ll2'_cmp_pii;
absurd (S (pi i) <= pi i); trivial; auto with arith.
destruct (le_lt_dec (length l2') (pi i)) as [ll2'_le_pii | ll2'_gt_pii];
destruct (le_lt_dec (length l2') (pi j)) as [ll2'_le_pij | ll2'_gt_pij].
apply (f_equal (fun n => S n)); apply Q.
simpl in L'; apply lt_S_n; trivial.
simpl in L''; apply lt_S_n; trivial.
injection H'; trivial.
absurd (length l2' < length l2'); auto with arith.
apply le_lt_trans with (pi j); trivial.
rewrite <- H'; auto with arith.
absurd (length l2' < length l2'); auto with arith.
apply le_lt_trans with (pi i); trivial.
rewrite H'; auto with arith.
apply (f_equal (fun n => S n)); apply Q; trivial.
simpl in L'; apply lt_S_n; trivial.
simpl in L''; apply lt_S_n; trivial.
intros [ | i] L'.
simpl; rewrite nth_error_at_pos; trivial.
simpl in L'; generalize (le_S_n _ _ L'); clear L'; intro L'.
simpl; rewrite (nth_error_remove b1 l2' l2'' (pi i)); apply H; trivial.
intros [L [pi [P H]]].
destruct l1 as [ | a1 l1].
destruct l2 as [ | a2 l2].
apply list_permut.Pnil.
simpl in L; discriminate.
assert (L' : 0 < length (a1 :: l1)).
simpl; auto with arith.
generalize (H 0 L'); simpl.
assert (H' := nth_error_ok_in (pi 0) l2).
destruct (nth_error l2 (pi 0)) as [ b1 | ].
intro a1_R_b1; destruct (H' _ (refl_equal _)) as [l2' [l2'' [L'' H'']]]; clear H'.
subst l2; apply list_permut.Pcons; trivial.
setoid_rewrite IHn.
simpl in L1; apply le_S_n; trivial.
split.
rewrite length_app in L; rewrite plus_comm in L; simpl in L; injection L;
intro L'''; rewrite L'''; rewrite plus_comm; rewrite length_app; trivial.
exists (fun i =>
if le_lt_dec (length l1) i
then i
else
if le_lt_dec (pi (S i)) (pi 0)
then pi (S i)
else (pi (S i)) -1); split.
unfold permut in *; repeat split.
intros i L''';
destruct (le_lt_dec (length l1) i) as [ll1_le_i | ll1_gt_i]; trivial.
absurd (i < i); auto with arith.
apply lt_le_trans with (length l1); trivial.
intros i L''';
destruct (le_lt_dec (length l1) i) as [ll1_le_i | _]; trivial.
assert (L'''' : S i < length (a1 :: l1)).
simpl; auto with arith.
destruct (le_lt_dec (pi (S i)) (pi 0)) as [piSi_le_pi0 | piSi_gt_pi0].
assert (piSi_lt_pi0 : pi (S i) < pi 0).
destruct (le_lt_or_eq _ _ piSi_le_pi0) as [L5 | E]; trivial.
destruct P as [_ [_ P]].
absurd (S i = 0).
discriminate.
apply (P (S i) 0); trivial.
apply lt_le_trans with (pi 0); trivial.
destruct P as [_ [P _]].
generalize (P 0 (lt_O_Sn _)); simpl; auto with arith.
destruct P as [_ [P _]].
generalize (P (S i) L''''); destruct (pi (S i)) as [ | p]; simpl.
intros _; apply le_lt_trans with i; auto with arith.
rewrite <- minus_n_O; auto with arith.
intros i j Li Lj;
destruct (le_lt_dec (length l1) i) as [ll1_le_i | _];
destruct (le_lt_dec (length l1) j) as [ll1_le_j | _];
trivial.
absurd (i < i); auto with arith.
apply lt_le_trans with (length l1); trivial.
absurd (j < j); auto with arith.
apply lt_le_trans with (length l1); trivial.
destruct P as [_ [_ P]];
destruct (le_lt_dec (pi (S i)) (pi 0)) as [piSi_le_pi0 | piSi_gt_pi0];
destruct (le_lt_dec (pi (S j)) (pi 0)) as [piSj_le_pi0 | piSj_gt_pi0].
intro piSi_eq_piSj; assert (Si_eq_Sj : S i = S j).
apply (P (S i) (S j)); simpl; auto with arith.
injection Si_eq_Sj; trivial.
destruct (le_lt_or_eq _ _ piSi_le_pi0) as [L5 | E]; clear piSi_le_pi0.
destruct (pi (S j)) as [ | pj].
absurd (pi 0 < 0); auto with arith.
simpl; rewrite <- minus_n_O.
intro H'; rewrite H' in L5.
absurd (S pj < S pj); auto with arith.
apply le_lt_trans with (pi 0); auto with arith.
absurd (S i = 0).
discriminate.
apply (P (S i) 0); trivial.
simpl; auto with arith.
destruct (le_lt_or_eq _ _ piSj_le_pi0) as [L5 | E]; clear piSj_le_pi0.
destruct (pi (S i)) as [ | qi].
absurd (pi 0 < 0); auto with arith.
simpl; rewrite <- minus_n_O.
intro H'; rewrite <- H' in L5.
absurd (S qi < S qi); auto with arith.
apply le_lt_trans with (pi 0); auto with arith.
absurd (S j = 0).
discriminate.
apply (P (S j) 0); trivial.
simpl; auto with arith.
intro piSi_eq_piSj; assert (Si_eq_Sj : S i = S j).
apply (P (S i) (S j)); simpl; auto with arith.
destruct (pi (S i)) as [ | qi].
absurd (pi 0 < 0); auto with arith.
destruct (pi (S j)) as [ | pj].
absurd (pi 0 < 0); auto with arith.
simpl in piSi_eq_piSj; do 2 rewrite <- minus_n_O in piSi_eq_piSj; subst; trivial.
injection Si_eq_Sj; trivial.
intros i Li;
destruct (le_lt_dec (length l1) i) as [ll1_lt_i | _].
absurd (i < i); auto with arith.
apply lt_le_trans with (length l1); trivial.
generalize (H (S i) (lt_n_S _ _ Li)); simpl.
destruct (nth_error l1 i) as [ai | ]; trivial.
generalize (nth_error_ok_in (pi (S i)) (l2' ++ b1 :: l2''));
destruct (nth_error (l2' ++ b1 :: l2'') (pi (S i))) as [bi | ];
[idtac | contradiction].
intros H' ai_R_bi; destruct (H' _ (refl_equal _)) as [k2 [k2' [Lk2 H'']]]; clear H'.
destruct (in_in_split_set b1 bi l2' l2'' k2 k2' H'') as [[H''' | H'''] | H''']; clear H''.
destruct H''' as [l [H3 H4]]; subst.
rewrite <- ass_app; rewrite <- Lk2; rewrite <- L''; simpl.
destruct (le_lt_dec (length k2) (length (k2 ++ bi :: l))) as [Ok | Ko].
rewrite nth_error_at_pos; trivial.
absurd (length k2 < length k2); auto with arith.
apply le_lt_trans with (length (k2 ++ bi :: l)); trivial.
rewrite length_app; auto with arith.
destruct H''' as [l [H3 H4]]; subst.
rewrite <- Lk2; rewrite <- L''; simpl.
destruct (le_lt_dec (length (l2' ++ b1 :: l)) (length l2')) as [Ko | Ok].
absurd (length l2' < length l2'); auto with arith.
apply lt_le_trans with (length (l2' ++ b1 :: l)); trivial.
rewrite length_app; rewrite plus_comm; simpl; auto with arith.
rewrite (length_app l2' (b1 :: l)).
rewrite plus_comm; simpl; rewrite <- minus_n_O; rewrite plus_comm;
rewrite <- length_app.
rewrite ass_app; rewrite nth_error_at_pos; trivial.
destruct H''' as [_ [H3 H4]]; subst;
absurd (0 = S i).
discriminate.
destruct P as [_ [_ P]].
apply P; simpl; auto with arith.
rewrite <- Lk2; rewrite L''; subst; trivial.
intro; contradiction.
Qed.
Section defs.
Variable A : Set.
Variable eqA : relation A.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
Let emptyBag := EmptyBag A.
Let singletonBag := SingletonBag _ eqA_dec.
contents of a list
Fixpoint list_contents (l:list A) : multiset A :=
match l with
| nil => emptyBag
| a :: l => munion (singletonBag a) (list_contents l)
end.
Definition permutation (l m:list A) :=
meq (list_contents l) (list_contents m).
End defs.
Lemma permut_closure : forall (A : Set) eqA
(eqA_dec : forall a1 a2, {eqA a1 a2}+{~eqA a1 a2}),
forall a1 a2, @permutation A eqA eqA_dec (a1 :: nil) (a2 :: nil) <->
(forall a, eqA a1 a <-> eqA a2 a).
Proof.
intros A eqA eqA_dec; unfold permutation, meq; simpl.
intros a1 a2; split.
intros H a; assert (Ha := H a); clear H; do 2 rewrite <- plus_n_O in Ha.
destruct (eqA_dec a1 a) as [a1_eq_a | a1_diff_a];
destruct (eqA_dec a2 a) as [a2_eq_a | a2_diff_a].
intuition.
discriminate.
discriminate.
intuition.
intros H a;
destruct (eqA_dec a1 a) as [a1_eq_a | a1_diff_a];
destruct (eqA_dec a2 a) as [a2_eq_a | a2_diff_a]; trivial.
absurd (eqA a2 a); trivial; setoid_rewrite <- (H a); trivial.
absurd (eqA a1 a); trivial; setoid_rewrite (H a); trivial.
Qed.