Library list_extensions.dickson
Add LoadPath "basis".
Set Implicit Arguments.
Require Import Relations.
Require Import List.
Require Import closure.
Require Import more_list.
Require Import Multiset.
Require Import list_permut.
Require Import ordered_set.
Require Import Arith.
Module Type D.
Declare Module Import DS : decidable_set.S.
Declare Module Import LP : list_permut.S with Definition EDS.A := DS.A
with Definition EDS.eq_A := (@eq DS.A).
Inductive multiset_extension_step (R : relation A) : list A -> list A -> Prop :=
| rmv_case :
forall l1 l2 l la a, (forall b, mem b la -> R b a) ->
permut l1 (la ++ l) -> permut l2 (a :: l) ->
multiset_extension_step R l1 l2.
multiset_extension_step is compatible with permutation.
Axiom list_permut_multiset_extension_step_1 :
forall R l1 l2 l, permut l1 l2 ->
multiset_extension_step R l1 l -> multiset_extension_step R l2 l.
Axiom list_permut_multiset_extension_step_2 :
forall R l1 l2 l, permut l1 l2 ->
multiset_extension_step R l l1 -> multiset_extension_step R l l2.
Add Morphism multiset_extension_step
with signature permut ==> permut ==> iff
as mult_morph.
Axiom list_permut_acc :
forall R l1 l2, permut l2 l1 ->
Acc (multiset_extension_step R) l1 -> Acc (multiset_extension_step R) l2.
Main lemma.
Axiom dickson :
forall R, well_founded R -> well_founded (multiset_extension_step R).
Axiom dickson_strong :
forall R l, (forall a, In a l -> Acc R a) -> Acc (multiset_extension_step R) l.
Axiom context_trans_clos_multiset_extension_step_app1 :
forall R l1 l2 l, trans_clos (multiset_extension_step R) l1 l2 ->
trans_clos (multiset_extension_step R) (l ++ l1) (l ++ l2).
Function consn (ll : list (A * list A)) : list A :=
match ll with
| nil => nil
| (e,_) :: ll => e:: (consn ll)
end.
Function appendn (ll : list (A * list A)) : list A :=
match ll with
| nil => nil
| (_,l) :: ll => l ++ (appendn ll)
end.
Axiom multiset_closure :
forall R, (forall x y, {R x y}+{~R x y}) -> transitive _ R ->
forall p q, trans_clos (multiset_extension_step R) p q ->
exists l, exists pq,
permut p ((appendn l) ++ pq) /\
permut q ((consn l) ++ pq) /\
l <> nil /\
(forall a, forall la, In (a,la) l -> forall b, mem b la -> R b a) /\
((forall a, ~R a a) -> forall a, mem a (consn l) -> mem a (appendn l) -> False).
End D.
Module Make (DS1 : decidable_set.S) : D with Module DS := DS1
with Definition LP.EDS.A := DS1.A
with Definition LP.EDS.eq_A := (@eq DS1.A).
Module Import DS := DS1.
Module Import EDS := decidable_set.Convert (DS).
Module Import LP := list_permut.Make (EDS).
Inductive multiset_extension_step (R : relation A) : list A -> list A -> Prop :=
| rmv_case :
forall l1 l2 l la a, (forall b, mem b la -> R b a) ->
permut l1 (la ++ l) -> permut l2 (a :: l) ->
multiset_extension_step R l1 l2.
multiset_extension_step is compatible with permutation.
Lemma list_permut_multiset_extension_step_1 :
forall R l1 l2 l, permut l1 l2 ->
multiset_extension_step R l1 l -> multiset_extension_step R l2 l.
Proof.
intros R l1 l2 l P M1; inversion M1; subst.
apply (rmv_case (l1:=l2) (l2:=l) (l:=l4) R la H); trivial;
setoid_rewrite <- P; trivial.
Qed.
Lemma list_permut_multiset_extension_step_2 :
forall R l1 l2 l, permut l1 l2 ->
multiset_extension_step R l l1 -> multiset_extension_step R l l2.
Proof.
intros R l1 l2 l P M1; inversion M1; subst.
apply (rmv_case (l1:=l) (l2:=l2) (l:=l4) R la H); trivial;
setoid_rewrite <- P; trivial.
Qed.
Add Morphism multiset_extension_step
with signature permut ==> permut ==> iff
as mult_morph.
Proof.
intros R l1 l2 P12 l3 l4 P34; split; [intro R13 | intro R24].
apply list_permut_multiset_extension_step_2 with l3; trivial.
apply list_permut_multiset_extension_step_1 with l1; trivial.
apply list_permut_multiset_extension_step_2 with l4; auto;
apply list_permut_multiset_extension_step_1 with l2; auto.
Qed.
If n << {a} U m, then
either, there exists n' such that n = {a} U n' and n' << m,
or, there exists k, such that n = k U m, and k << {a}.
Lemma two_cases :
forall R a m n,
multiset_extension_step R n (a :: m) ->
(exists n', permut n (a :: n') /\
multiset_extension_step R n' m) \/
(exists k, (forall b, mem b k -> R b a) /\
permut n (k ++ m)).
Proof.
intros R a m n M; inversion_clear M as [x1 x2 l la b H H0 H1];
destruct (eq_dec a b) as [a_eq_b | a_diff_b]; subst.
unfold eq_A in a_eq_b; subst b.
setoid_rewrite <- permut_cons in H1; [idtac | reflexivity].
right; exists la; split; trivial.
setoid_rewrite H0.
setoid_rewrite <- permut_app1; auto.
left; destruct (mem_dec b m) as [b_in_m | b_not_in_m].
destruct (mem_split_set _ _ b_in_m) as [b' [m' [m'' [b_eq_b' H']]]].
simpl in b_eq_b'; simpl in H'; subst m.
setoid_rewrite <- (permut_add_inside (e1 := b') (e2 := b) (a :: m') m'' (@nil A) l) in H1;
simpl in H1.
exists (la ++ m' ++ m''); split.
setoid_rewrite H0.
transitivity (la ++ a :: m' ++ m'').
setoid_rewrite <- permut_app1; symmetry; trivial.
symmetry; setoid_rewrite <- permut_cons_inside; auto.
reflexivity.
apply (rmv_case (l1:=la ++ m' ++ m'') (l2:= m' ++ b' :: m'') (l:= m' ++ m'') R la H); auto;
apply permut_sym; setoid_rewrite <- permut_cons_inside; auto.
symmetry; trivial.
absurd (mem b m); trivial.
destruct (cons_permut_mem (refl_equal _) (permut_sym H1))
as [b_eq_a | b_mem_m]; trivial.
unfold EDS.eq_A, eq_A in b_eq_a; absurd (a = b); subst; trivial.
Qed.
Lemma list_permut_acc :
forall R l1 l2, permut l2 l1 ->
Acc (multiset_extension_step R) l1 -> Acc (multiset_extension_step R) l2.
Proof.
intros R l1 l2 Meq A1; apply Acc_intro; intros l M2;
inversion A1; apply H; subst;
setoid_rewrite <- Meq; trivial.
Qed.
Lemma dickson_aux1 :
forall (R : relation A) a,
(forall b, R b a ->
forall m, Acc (multiset_extension_step R) m ->
Acc (multiset_extension_step R) (b :: m)) ->
forall m, Acc (multiset_extension_step R) m ->
(forall m', (multiset_extension_step R) m' m ->
Acc (multiset_extension_step R) (a :: m')) ->
Acc (multiset_extension_step R) (a :: m).
Proof.
intros R a IH2_a m Acc_m IHa_M; apply Acc_intro;
intros n H; elim (two_cases H); clear H.
intros [n' [P M]]; refine (list_permut_acc P _); apply IHa_M; trivial.
intros [k [M P]]; refine (list_permut_acc P _); clear P; induction k; trivial; simpl;
apply IH2_a.
apply M; left; reflexivity.
apply IHk; intros; apply M; right; trivial.
Qed.
Lemma dickson_aux2 :
forall R m,
Acc (multiset_extension_step R) m ->
forall a, (forall b, R b a ->
forall m, Acc (multiset_extension_step R) m ->
Acc (multiset_extension_step R) (b :: m)) ->
Acc (multiset_extension_step R) (a :: m).
Proof.
intros R m Acc_m a IH2_a;
apply (Acc_iter (R:= multiset_extension_step R)
(fun m => Acc (multiset_extension_step R) m ->
Acc (multiset_extension_step R) (a :: m))); trivial;
clear m Acc_m;
intros m H Acc_m; apply dickson_aux1; trivial;
intros; apply H; trivial;
apply Acc_inv with m; trivial.
Qed.
Lemma dickson_aux3 :
forall R a, Acc R a -> forall m, Acc (multiset_extension_step R) m ->
Acc (multiset_extension_step R) (a :: m).
Proof.
intros R a Acc_a;
apply (Acc_iter (R:= R)
(fun a => Acc R a -> forall m, Acc (multiset_extension_step R) m ->
Acc (multiset_extension_step R) (a :: m))); trivial;
clear a Acc_a;
intros a H Acc_a m Acc_m; apply dickson_aux2; trivial;
intros; apply H; trivial;
apply Acc_inv with a; trivial.
Qed.
Main lemma.
Lemma dickson :
forall R, well_founded R -> well_founded (multiset_extension_step R).
Proof.
intros R Wf_R; unfold well_founded in *;
intros m; induction m as [ | a m].
apply Acc_intro; intros m H; inversion_clear H;
absurd (a :: l = nil).
discriminate.
apply (permut_nil (R := eq_A)).
apply permut_sym; trivial.
apply dickson_aux3; trivial.
Qed.
Lemma dickson_strong :
forall R l, (forall a, In a l -> Acc R a) -> Acc (multiset_extension_step R) l.
Proof.
intros R m; induction m as [ | a m].
intros _; apply Acc_intro; intros m H; inversion_clear H;
absurd (a :: l = nil).
discriminate.
apply (permut_nil (R := eq_A)).
apply permut_sym; trivial.
intros; apply dickson_aux3.
apply H; left; trivial.
apply IHm; intros; apply H; right; trivial.
Qed.
Lemma list_permut_trans_clos_multiset_extension_step_1 :
forall R l1 l2 l, permut l1 l2 ->
(trans_clos (multiset_extension_step R)) l1 l ->
(trans_clos (multiset_extension_step R)) l2 l.
Proof.
intros R l1 l1' l P H; induction H as [ l1 l2 H | l1 l2 l3 H1 H2 H3].
apply t_step; apply list_permut_multiset_extension_step_1 with l1; trivial.
apply t_trans with l2; trivial; apply list_permut_multiset_extension_step_1 with l1; trivial.
Qed.
Lemma list_permut_trans_clos_multiset_extension_step_2 :
forall R l1 l2 l, permut l1 l2 ->
(trans_clos (multiset_extension_step R)) l l1 ->
(trans_clos (multiset_extension_step R)) l l2.
Proof.
intros R l1 l3 l P H; induction H as [ l1 l2 H | l1 l2 l3' H1 H2 H3].
apply t_step; apply list_permut_multiset_extension_step_2 with l2; trivial.
apply t_trans with l2; trivial; apply H3; trivial.
Qed.
Lemma context_multiset_extension_step_app1 :
forall R l1 l2 l, multiset_extension_step R l1 l2 ->
multiset_extension_step R (l ++ l1) (l ++ l2).
Proof.
intros R l1 l2 l H; destruct H as [l1 l2 l12 la a H P1 P2].
apply (@rmv_case R (l++l1) (l++l2) (l++l12) la a); trivial.
transitivity (l ++ la ++ l12).
setoid_rewrite <- permut_app1; trivial.
do 2 rewrite <- app_ass; setoid_rewrite <- permut_app2; trivial.
apply list_permut_app_app.
transitivity (l ++ a :: l12).
setoid_rewrite <- permut_app1; trivial.
apply permut_sym; setoid_rewrite <- permut_cons_inside; reflexivity.
Qed.
Lemma context_trans_clos_multiset_extension_step_app1 :
forall R l1 l2 l, trans_clos (multiset_extension_step R) l1 l2 ->
trans_clos (multiset_extension_step R) (l ++ l1) (l ++ l2).
Proof.
intros R l1 l2 l H; induction H.
apply t_step; apply context_multiset_extension_step_app1; trivial.
apply t_trans with (l ++ y); trivial.
apply context_multiset_extension_step_app1; trivial.
Qed.
Lemma context_multiset_extension_step_cons :
forall R, (forall a, ~R a a) ->
forall a l1 l2, multiset_extension_step R (a :: l1) (a :: l2) ->
multiset_extension_step R l1 l2.
Proof.
intros R irrefl_R a l1 l2 H;
inversion H as [a_l1 a_l2 lc lb b H' P1 P2 H2 H3]; subst.
assert (a_mem_blc : mem a (b :: lc)).
apply cons_permut_mem with l2 a; trivial; reflexivity.
simpl in a_mem_blc; destruct a_mem_blc as [a_eq_b | a_mem_lc].
unfold EDS.eq_A, eq_A in a_eq_b; subst b.
assert (a_mem_lb_lc : mem a (lb ++ lc)).
apply cons_permut_mem with l1 a; trivial; reflexivity.
setoid_rewrite <- mem_or_app in a_mem_lb_lc.
destruct a_mem_lb_lc as [a_mem_lb | a_mem_lc].
absurd (R a a); [apply (irrefl_R a) | apply H'; trivial].
destruct (mem_split_set _ _ a_mem_lc) as [a' [lc' [lc'' [a_eq_a' H'']]]];
simpl in a_eq_a'; simpl in H''; unfold EDS.eq_A, eq_A in a_eq_a'; subst a' lc.
apply (rmv_case R (l1:=l1) (l2:= l2) (l:=lc' ++ lc'') lb (a:=a)); trivial.
rewrite <- app_ass in P1;
setoid_rewrite <- (permut_cons_inside) in P1.
rewrite <- ass_app in P1; trivial.
reflexivity.
rewrite app_comm_cons in P2;
setoid_rewrite <- (permut_cons_inside) in P2; trivial.
reflexivity.
destruct (mem_split_set _ _ a_mem_lc) as [a' [lc' [lc'' [a_eq_a' H'']]]];
simpl in a_eq_a'; simpl in H''; unfold EDS.eq_A, eq_A in a_eq_a'; subst a' lc.
apply (rmv_case R (l1:=l1) (l2:= l2) (l:=lc' ++ lc'') lb (a:=b)); trivial.
rewrite <- app_ass in P1;
setoid_rewrite <- (permut_cons_inside) in P1.
rewrite <- ass_app in P1; trivial.
reflexivity.
rewrite app_comm_cons in P2;
setoid_rewrite <- (permut_cons_inside) in P2.
simpl in P2; trivial.
reflexivity.
Qed.
Lemma remove_context_multiset_extension_step_app1 :
forall R, (forall a, ~R a a) ->
forall l1 l2 l, multiset_extension_step R (l ++ l1) (l ++ l2) ->
multiset_extension_step R l1 l2.
Proof.
intros R irrefl_R l1 l2 l; generalize l1 l2; clear l1 l2;
induction l as [ | a l]; trivial.
intros l1 l2 H;
assert (H' : multiset_extension_step R (a :: l1) (a :: l2)).
apply IHl.
apply list_permut_multiset_extension_step_2 with ((a :: l) ++ l2).
simpl; setoid_rewrite <- permut_cons_inside; auto.
reflexivity.
apply list_permut_multiset_extension_step_1 with ((a :: l) ++ l1); trivial.
simpl; setoid_rewrite <- permut_cons_inside; auto.
reflexivity.
apply context_multiset_extension_step_cons with a; trivial.
Qed.
Lemma context_multiset_extension_step_app2 :
forall R l1 l2 l, multiset_extension_step R l1 l2 ->
multiset_extension_step R (l1 ++ l) (l2 ++ l).
Proof.
intros R l1 l2 l H; destruct H as [l1 l2 l12 la a H P1 P2].
apply (@rmv_case R (l1++l) (l2++l) (l12++l) la a); trivial.
rewrite <- app_ass; setoid_rewrite <- permut_app2; trivial.
rewrite app_comm_cons; setoid_rewrite <- permut_app2; trivial.
Qed.
Function consn (ll : list (A * list A)) : list A :=
match ll with
| nil => nil
| (e,_) :: ll => e:: (consn ll)
end.
Lemma mem_consn :
forall a ll, mem a (consn ll) <-> exists la, In (a,la) ll.
Proof.
intros a ll; split; intro H;
functional induction (consn ll)
as [ | H1 b lb ll H2 IH].
contradiction.
destruct H as [a_eq_b | a_in_cnsl].
exists lb; unfold EDS.eq_A, eq_A in a_eq_b; subst; left; trivial.
destruct (IH a_in_cnsl) as [la H].
exists la; right; trivial.
destruct H; contradiction.
destruct H as [la [ala_eq_blb | ala_in_ll]].
injection ala_eq_blb; intros; subst; left; reflexivity; trivial.
right; apply IH; exists la; trivial.
Qed.
Lemma consn_app :
forall ll1 ll2, consn (ll1 ++ ll2) = consn ll1 ++ consn ll2.
Proof.
intros ll1; induction ll1 as [ | [a la] ll1]; simpl; trivial; simpl;
intros; rewrite IHll1; trivial.
Qed.
Function appendn (ll : list (A * list A)) : list A :=
match ll with
| nil => nil
| (_,l) :: ll => l ++ (appendn ll)
end.
Lemma appendn_app :
forall ll1 ll2, appendn (ll1 ++ ll2) = appendn ll1 ++ appendn ll2.
Proof.
intros ll1; induction ll1 as [ | [a la] ll1]; simpl; trivial; simpl;
intros; rewrite IHll1; rewrite ass_app; trivial.
Qed.
Lemma in_appendn :
forall a ll, mem a (appendn ll) -> exists b, exists lb, In (b,lb) ll /\ mem a lb.
Proof.
intros a ll H;
functional induction (appendn ll)
as [ | H1 b lb ll H2 IH].
contradiction.
rewrite <- mem_or_app in H; destruct H as [a_mem_lb | a_mem_appl].
exists b; exists lb; split; trivial; left; trivial.
destruct (IH a_mem_appl) as [c [lc [H1 H2]]];
exists c; exists lc; split; trivial; right; trivial.
Qed.
Lemma multiset_closure_aux :
forall (R : relation A) p q l pq,
permut p ((appendn l) ++ pq) ->
permut q ((consn l) ++ pq) ->
l <> nil ->
(forall a, forall la, In (a,la) l -> forall b, mem b la -> R b a) ->
trans_clos (multiset_extension_step R) p q.
Proof.
intros R p q l; generalize p q; clear p q; induction l as [ | [x lx] l].
simpl; intros p q pq Pp Pq H; absurd (@nil (A * list A) = nil); trivial.
simpl; intros p q pq Pp Pq _ H.
assert (lx_lt_x : forall b, mem b lx -> R b x).
apply H; left; trivial.
destruct l as [ | [y ly] l]; simpl in *.
rewrite <- app_nil_end in Pp.
simpl in Pq; apply t_step.
exact (rmv_case R lx lx_lt_x Pp Pq).
apply t_trans with (x :: ly ++ (appendn l) ++ pq).
do 2 rewrite app_ass in Pp;
refine (rmv_case R lx lx_lt_x Pp (permut_refl _)).
refine (list_permut_trans_clos_multiset_extension_step_2
(permut_sym Pq) _).
apply (@context_trans_clos_multiset_extension_step_app1 R
(ly ++ appendn l ++ pq) (y :: consn l ++ pq) (x :: nil));
apply (@IHl (ly ++ appendn l ++ pq) (y :: consn l ++ pq) pq); auto.
rewrite ass_app; auto.
discriminate.
intros a la H1 b b_in_la; apply (H a la); trivial; right; trivial.
Qed.
Lemma multiset_closure_aux2 :
forall (R : relation A) p q le l pq,
permut p ((appendn l) ++ pq) ->
permut q (le ++ (consn l) ++ pq) ->
l <> nil \/ le <> nil ->
(forall a, forall la, In (a,la) l -> forall b, mem b la -> R b a) ->
trans_clos (multiset_extension_step R) p q.
Proof.
intros R p q le l pq Pp Pq H H';
apply (@multiset_closure_aux R p q ((map (fun x => (x, @nil A)) le) ++ l) pq).
setoid_rewrite Pp; setoid_rewrite <- permut_app2;
rewrite appendn_app; clear Pq H; induction le as [ | e le]; simpl; auto.
setoid_rewrite Pq; setoid_rewrite ass_app; setoid_rewrite <- permut_app2;
rewrite consn_app; clear Pq H; induction le as [ | e le]; simpl; auto.
setoid_rewrite <- permut_cons; trivial.
reflexivity.
intro H''; destruct (app_eq_nil _ _ H'') as [ l_eq_nil le_eq_nil];
destruct H as [le_diff_nil | l_diff_nil].
absurd (l = nil); trivial.
destruct le as [ | e le].
absurd (@nil A = nil); trivial.
discriminate.
clear Pq H; induction le as [ | e le]; simpl; trivial.
intros a la [H | H] b b_in_la;
[injection H; intros; subst; contradiction | apply (IHle a la); trivial].
Qed.
Module LDS.
Definition A := (A * (list A))%type.
Definition eq_A := @eq A.
Lemma eq_dec : forall a1 a2 : A, {a1 = a2} + {a1 <> a2}.
Proof.
intros [e1 l1] [e2 l2]; destruct (eq_dec e1 e2) as [e1_eq_e2 | e1_diff_e2].
destruct (list_eq_dec eq_dec l1 l2) as [l1_eq_l2 | l1_diff_l2].
left; unfold Make.EDS.eq_A in *; subst; trivial.
right; intro H; apply l1_diff_l2; injection H; trivial.
right; intro H; apply e1_diff_e2; injection H; trivial.
Defined.
Lemma eq_proof : equivalence A eq_A.
unfold eq_A; split.
intro; reflexivity.
intros a1 a2 a3 H1 H2; transitivity a2; trivial.
intros a1 a2 H; symmetry; trivial.
Qed.
Add Relation A eq_A
reflexivity proved by (equiv_refl _ _ eq_proof)
symmetry proved by (equiv_sym _ _ eq_proof)
transitivity proved by (equiv_trans _ _ eq_proof) as EQA.
End LDS.
Module LEDS := decidable_set.Convert(LDS).
Module LLP := list_permut.Make (LEDS).
Lemma permut_consn :
forall ll1 ll2, LLP.permut ll1 ll2 -> permut (consn ll1) (consn ll2).
Proof.
intros ll1; induction ll1 as [ | [a la] ll1]; simpl; intros ll2 P.
rewrite (permut_nil (LLP.permut_sym P)); simpl; auto.
assert (ala_in_ll2 : In (a,la) ll2).
setoid_rewrite <- (in_permut_in P); left; trivial.
destruct (In_split _ _ ala_in_ll2) as [ll2' [ll2'' H]]; subst.
setoid_rewrite <- LLP.permut_cons_inside in P.
rewrite consn_app; simpl; setoid_rewrite <- permut_cons_inside.
reflexivity.
rewrite <- consn_app; apply IHll1; trivial.
reflexivity.
Qed.
Lemma permut_appendn :
forall ll1 ll2, LLP.permut ll1 ll2 -> permut (appendn ll1) (appendn ll2).
Proof.
intros ll1; induction ll1 as [ | [a la] ll1]; simpl; intros ll2 P.
rewrite (permut_nil (LLP.permut_sym P)); simpl; auto.
assert (ala_in_ll2 : In (a,la) ll2).
setoid_rewrite <- (in_permut_in P); left; trivial.
destruct (In_split _ _ ala_in_ll2) as [ll2' [ll2'' H]]; subst.
rewrite appendn_app; simpl.
refine (permut_trans _ (list_permut_app_app _ _)).
rewrite <- ass_app.
setoid_rewrite <- permut_app1.
refine (permut_trans _ (list_permut_app_app _ _)).
rewrite <- appendn_app; apply IHll1; trivial.
setoid_rewrite <- LLP.permut_cons_inside in P; trivial.
reflexivity.
Qed.
Lemma multiset_closure_aux3 :
forall l lc cns, permut (consn l) (lc ++ cns) ->
exists ll, exists ll', LLP.permut l (ll ++ ll') /\
permut (consn ll) lc /\
permut (consn ll') cns.
Proof.
intro l; induction l as [ | [e le] l]; intros lc cns P.
exists (@nil (A * list A)); exists (@nil (A * list A)).
simpl in P; destruct (app_eq_nil _ _ (permut_nil (permut_sym P))); subst;
simpl; repeat split; auto.
assert (e_in_lc_cns : mem e (lc ++ cns)).
simpl in P; apply (cons_permut_mem (equiv_refl _ _ eq_proof e) P).
setoid_rewrite <- mem_or_app in e_in_lc_cns.
destruct e_in_lc_cns as [e_in_lc | e_in_cns].
destruct (mem_split_set _ _ e_in_lc) as [e' [lc' [lc'' [e_eq_e' H]]]];
simpl in e_eq_e'; simpl in H; subst lc.
rewrite <- ass_app in P; simpl in P; setoid_rewrite <- permut_cons_inside in P; trivial.
rewrite ass_app in P;
destruct (IHl (lc' ++ lc'') cns P) as [ll [ll' [P' [H1 H2]]]].
exists ((e,le) :: ll); exists ll'; repeat split; auto.
simpl; setoid_rewrite <- LLP.permut_cons; trivial.
reflexivity.
simpl; setoid_rewrite <- permut_cons_inside; trivial.
destruct (mem_split_set _ _ e_in_cns) as [e' [cns' [cns'' [e_eq_e' H]]]];
simpl in e_eq_e'; simpl in H; subst cns.
rewrite ass_app in P; simpl in P; setoid_rewrite <- permut_cons_inside in P; trivial.
rewrite <- ass_app in P;
destruct (IHl lc (cns' ++ cns'') P) as [ll [ll' [P' [H1 H2]]]].
exists ll; exists ((e,le) :: ll'); repeat split; auto.
setoid_rewrite <- LLP.permut_cons_inside; trivial.
reflexivity.
simpl; setoid_rewrite <- permut_cons_inside; trivial.
Qed.
Lemma multiset_closure :
forall R, (forall x y, {R x y}+{~R x y}) -> transitive _ R ->
forall p q, trans_clos (multiset_extension_step R) p q ->
exists l, exists pq,
permut p ((appendn l) ++ pq) /\
permut q ((consn l) ++ pq) /\
l <> nil /\
(forall a, forall la, In (a,la) l -> forall b, mem b la -> R b a) /\
((forall a, ~R a a) -> forall a, mem a (consn l) -> mem a (appendn l) -> False).
Proof.
intros R R_dec trans_R p q p_lt_q; induction p_lt_q as [p q p_lt_q | p q r p_lt_q q_lt_r].
destruct p_lt_q as [p q pq la a la_lt_a Pp Pq].
exists ((a,la) :: nil); exists pq; simpl; repeat split; auto.
rewrite <- app_nil_end; auto.
discriminate.
intros x lx [H | H] b b_in_lx;
[injection H; intros; subst; apply la_lt_a; trivial | contradiction].
rewrite <- app_nil_end;
intros irrefl_R b [a_eq_b | Abs] b_in_la.
unfold EDS.eq_A, eq_A in a_eq_b; subst b.
apply (irrefl_R a); apply la_lt_a; trivial.
contradiction.
destruct p_lt_q as [p q pq la a la_lt_a Pp Pq].
destruct IHq_lt_r as [l [qr [Pq' [Pr [l_diff_nil [app_lt_cns app_disj_cns]]]]]].
assert (a_in_appl_qr : mem a ((appendn l) ++ qr)).
setoid_rewrite <- Pq'; setoid_rewrite Pq; left; trivial.
reflexivity.
setoid_rewrite <- mem_or_app in a_in_appl_qr.
destruct (mem_dec a (appendn l)) as [a_in_appl | a_not_in_appl].
destruct (in_appendn _ _ a_in_appl) as [x [lx [xlx_in_l a_in_lx]]].
destruct (mem_split_set _ _ a_in_lx) as [a' [lx' [lx'' [a_eq_a' H]]]].
simpl in a_eq_a'; simpl in H; subst lx.
destruct (In_split _ _ xlx_in_l) as [l' [l'' H]]; subst l.
rewrite appendn_app in Pq'; simpl in Pq'; do 3 rewrite <- ass_app in Pq'.
simpl in Pq'; rewrite ass_app in Pq'; setoid_rewrite Pq in Pq'.
setoid_rewrite <- permut_cons_inside in Pq'.
rewrite <- ass_app in Pq'.
generalize (remove_equiv_is_sound (consn (l' ++ l'')) la);
destruct (remove_equiv (consn (l' ++ l'')) la) as [cns la'];
intros [lc [Pcns [Pla cns_disj_la']]];
destruct (multiset_closure_aux3 (l' ++ l'') lc cns Pcns) as [ll [ll' [P' [H1 H2]]]];
exists ((x, lx' ++ lx'' ++ la' ++ (appendn ll)) :: ll'); exists (lc ++ qr); split.
setoid_rewrite Pp; simpl.
transitivity ((lc ++ la') ++ pq).
setoid_rewrite <- permut_app2; trivial.
transitivity ((lc ++ la') ++ (appendn l' ++ lx' ++ lx'' ++ appendn l'' ++ qr)).
setoid_rewrite <- permut_app1; trivial.
do 5 rewrite ass_app; setoid_rewrite <- permut_app2.
refine (permut_trans _ (list_permut_app_app _ _)).
do 5 rewrite <- ass_app; setoid_rewrite <- permut_app1.
rewrite ass_app.
refine (permut_trans (list_permut_app_app _ _) _).
do 3 rewrite <- ass_app; do 2 setoid_rewrite <- permut_app1.
refine (permut_trans (list_permut_app_app _ _) _).
do 2 rewrite <- ass_app; setoid_rewrite <- permut_app1.
do 2 rewrite <- appendn_app; apply permut_appendn; trivial.
split.
rewrite ass_app; setoid_rewrite Pr; setoid_rewrite <- permut_app2;
rewrite consn_app; simpl; apply permut_sym;
setoid_rewrite <- permut_cons_inside.
reflexivity.
setoid_rewrite H2;
refine (permut_trans (list_permut_app_app _ _) _);
setoid_rewrite <- Pcns; rewrite consn_app; auto.
split.
discriminate.
split.
simpl; intros y ly [yly_eq_xly | yly_in_ll''] b b_in_ly.
injection yly_eq_xly; intros; subst y ly; clear yly_eq_xly.
rewrite ass_app in b_in_ly;
setoid_rewrite <- mem_or_app in b_in_ly.
destruct b_in_ly as [b_in_lx | b_in_la_app].
apply (app_lt_cns x (lx' ++ a' :: lx'')); trivial.
apply mem_insert; trivial.
setoid_rewrite <- mem_or_app in b_in_la_app.
destruct b_in_la_app as [b_in_la | b_in_app].
apply trans_R with a.
apply la_lt_a.
setoid_rewrite Pla; setoid_rewrite <- mem_or_app; right; trivial.
apply (app_lt_cns x (lx' ++ a' :: lx'')); trivial.
destruct (in_appendn _ _ b_in_app) as [y [ly [yly_in_ll b_in_ly]]].
apply trans_R with y.
apply (app_lt_cns y ly); trivial; apply in_insert.
setoid_rewrite (list_permut.in_permut_in P'); apply in_or_app; left; trivial.
assert (y_in_lc : mem y lc).
setoid_rewrite <- (mem_permut_mem y H1).
setoid_rewrite mem_consn; exists ly; trivial.
apply trans_R with a.
apply la_lt_a; setoid_rewrite Pla; setoid_rewrite <- mem_or_app; left; trivial.
apply (app_lt_cns x (lx' ++ a' :: lx'')).
apply in_or_app; right; left; reflexivity.
setoid_rewrite <- mem_or_app; right; left; trivial.
apply (app_lt_cns y ly); trivial; apply in_insert; trivial.
setoid_rewrite (list_permut.in_permut_in P').
apply in_or_app; right; trivial.
simpl; intros irrefl_R b [x_eq_b | b_in_cns] b_in_lx_la_app;
do 3 rewrite <- ass_app in b_in_lx_la_app; do 2 rewrite ass_app in b_in_lx_la_app.
unfold EDS.eq_A, eq_A in x_eq_b; subst b.
setoid_rewrite <- mem_or_app in b_in_lx_la_app.
destruct b_in_lx_la_app as [b_in_lx_la | b_in_app].
setoid_rewrite <- mem_or_app in b_in_lx_la.
destruct b_in_lx_la as [b_in_lx | b_in_la].
apply (irrefl_R x); apply (app_lt_cns x (lx' ++ a' :: lx'')).
apply in_or_app; right; left; reflexivity.
apply mem_insert; trivial.
apply (irrefl_R x); apply trans_R with a.
apply la_lt_a; setoid_rewrite Pla; setoid_rewrite <- mem_or_app; right; trivial.
apply (app_lt_cns x (lx' ++ a' :: lx'')).
apply in_or_app; right; left; reflexivity.
setoid_rewrite <- mem_or_app; right; left; trivial.
apply (app_disj_cns irrefl_R x).
rewrite consn_app; setoid_rewrite <- mem_or_app; right; left.
reflexivity.
rewrite <- appendn_app in b_in_app.
setoid_rewrite <- (mem_permut_mem x (permut_appendn P')) in b_in_app.
rewrite appendn_app; setoid_rewrite <- mem_or_app.
rewrite appendn_app in b_in_app; setoid_rewrite <- mem_or_app in b_in_app.
destruct b_in_app as [b_in_app | b_in_app].
left; trivial.
right; simpl; setoid_rewrite <- mem_or_app; right; trivial.
simpl; setoid_rewrite <- mem_or_app in b_in_lx_la_app.
destruct b_in_lx_la_app as [b_in_lx_la | b_in_app].
simpl; setoid_rewrite <- mem_or_app in b_in_lx_la.
destruct b_in_lx_la as [b_in_lx | b_in_la].
apply (app_disj_cns irrefl_R b).
rewrite consn_app; simpl; apply mem_insert;
rewrite <- consn_app; setoid_rewrite (permut_consn P');
rewrite consn_app; setoid_rewrite <- mem_or_app; right; trivial.
rewrite appendn_app; setoid_rewrite <- mem_or_app; right;
simpl; setoid_rewrite <- mem_or_app; left; apply mem_insert; trivial.
apply (cns_disj_la' b); trivial; setoid_rewrite <- H2; trivial.
apply (app_disj_cns irrefl_R b).
rewrite consn_app; simpl; apply mem_insert;
rewrite <- consn_app; setoid_rewrite (permut_consn P');
rewrite consn_app; setoid_rewrite <- mem_or_app; right; trivial.
rewrite <- appendn_app in b_in_app;
setoid_rewrite <- (mem_permut_mem b (permut_appendn P')) in b_in_app.
rewrite appendn_app; setoid_rewrite <- mem_or_app;
rewrite appendn_app in b_in_app.
setoid_rewrite <- mem_or_app in b_in_app;
destruct b_in_app as [b_in_app | b_in_app];
[left | simpl; right; setoid_rewrite <- mem_or_app; right]; trivial.
trivial.
assert (a_in_qr : mem a qr).
destruct a_in_appl_qr as [a_in_appl | a_in_qr]; trivial.
absurd (mem a (appendn l)); trivial.
destruct (mem_split_set _ _ a_in_qr) as [a' [qr' [qr'' [a_eq_a' H]]]]; subst qr;
setoid_rewrite Pq in Pq'; rewrite ass_app in Pq';
setoid_rewrite <- permut_cons_inside in Pq'; rewrite <- ass_app in Pq'.
generalize (remove_equiv_is_sound (consn l) la);
destruct (remove_equiv (consn l) la) as [cns la'];
intros [lc [Pcns [Pla cns_disj_la']]];
destruct (multiset_closure_aux3 l lc cns Pcns) as [ll [ll' [P' [H1 H2]]]].
exists ((a, la' ++ (appendn ll)) :: ll'); exists (lc ++ (qr' ++ qr'')); split.
setoid_rewrite Pp; setoid_rewrite Pq'; simpl; do 4 rewrite ass_app;
do 2 setoid_rewrite <- permut_app2; setoid_rewrite Pla; rewrite <- ass_app;
refine (permut_trans (list_permut_app_app _ _) _);
setoid_rewrite <- permut_app2; rewrite <- ass_app;
rewrite <- appendn_app; setoid_rewrite <- (permut_appendn P'); auto.
split.
setoid_rewrite Pr; simpl; rewrite ass_app; apply permut_sym;
setoid_rewrite <- permut_cons_inside.
trivial.
do 2 rewrite ass_app;
do 2 setoid_rewrite <- permut_app2; setoid_rewrite <- H1;
setoid_rewrite (permut_consn P'); rewrite consn_app;
apply list_permut_app_app.
split.
discriminate.
split.
intros y ly [yly_eq_aly | yly_in_ll'] b b_in_ly.
injection yly_eq_aly; intros; subst y ly; clear yly_eq_aly.
setoid_rewrite <- mem_or_app in b_in_ly.
destruct b_in_ly as [b_in_la' | b_in_app].
apply la_lt_a; setoid_rewrite Pla; setoid_rewrite <- mem_or_app; right; trivial.
destruct (in_appendn _ _ b_in_app) as [z [lz [zlz_in_ll b_in_lz]]].
apply trans_R with z.
apply (app_lt_cns z lz); trivial.
setoid_rewrite (list_permut.in_permut_in P').
apply in_or_app; left; trivial.
apply la_lt_a; setoid_rewrite Pla; setoid_rewrite <- mem_or_app; left.
setoid_rewrite <- H1.
setoid_rewrite mem_consn; exists lz; trivial.
apply (app_lt_cns y ly); trivial;
setoid_rewrite (list_permut.in_permut_in P'); apply in_or_app; right; trivial.
intros irrefl_R; simpl; rewrite <- ass_app; rewrite ass_app;
intros b b_in_a_cns b_in_la_app.
setoid_rewrite <- mem_or_app in b_in_la_app.
destruct b_in_la_app as [b_in_la | b_in_app].
destruct b_in_a_cns as [b_eq_a | b_in_cns].
setoid_rewrite <- mem_or_app in b_in_la.
destruct b_in_la as [b_in_la' | b_in_app].
apply (irrefl_R a); apply la_lt_a; setoid_rewrite Pla;
setoid_rewrite <- mem_or_app; right;
unfold EDS.eq_A, eq_A in b_eq_a; subst; trivial.
destruct (in_appendn _ _ b_in_app) as [z [lz [zlz_in_ll b_in_lz]]].
apply (irrefl_R a); apply trans_R with z.
apply (app_lt_cns z lz); subst; trivial.
setoid_rewrite (list_permut.in_permut_in P').
apply in_or_app; left; trivial.
unfold EDS.eq_A, eq_A in b_eq_a; subst; trivial.
apply la_lt_a; setoid_rewrite Pla;
setoid_rewrite <- mem_or_app; left; setoid_rewrite <- H1.
setoid_rewrite mem_consn; exists lz; trivial.
setoid_rewrite <- mem_or_app in b_in_la.
destruct b_in_la as [b_in_la' | b_in_app].
apply (cns_disj_la' b); trivial; setoid_rewrite <- H2; trivial.
apply (app_disj_cns irrefl_R b).
setoid_rewrite (permut_consn P'); rewrite consn_app;
setoid_rewrite <- mem_or_app; right; trivial.
setoid_rewrite (permut_appendn P'); rewrite appendn_app;
setoid_rewrite <- mem_or_app; left; trivial.
destruct b_in_a_cns as [b_eq_a | b_in_cns].
unfold EDS.eq_A, eq_A in b_eq_a; subst b.
apply a_not_in_appl;
setoid_rewrite (mem_permut_mem a (permut_appendn P'));
rewrite appendn_app; setoid_rewrite <- mem_or_app; right; trivial.
apply (app_disj_cns irrefl_R b).
setoid_rewrite (permut_consn P'); rewrite consn_app;
setoid_rewrite <- mem_or_app; right; trivial.
setoid_rewrite (permut_appendn P'); rewrite appendn_app;
setoid_rewrite <- mem_or_app; right; trivial.
simpl; trivial.
Qed.
Lemma context_trans_clos_multiset_extension_step_cons :
forall R, (forall x y, {R x y}+{~R x y}) -> transitive _ R -> (forall a, ~R a a) ->
forall a l1 l2, trans_clos (multiset_extension_step R) (a :: l1) (a :: l2) ->
trans_clos (multiset_extension_step R) l1 l2.
Proof.
intros R dec_R trans_R irrefl_R a l1 l2 H.
destruct (multiset_closure dec_R trans_R H)
as [ll [q [P1 [P2 [p_diff_nil [app_lt_cns cns_disj_app]]]]]].
destruct (mem_dec a q) as [a_in_q | a_not_in_q].
destruct (mem_split_set _ _ a_in_q) as [a' [q' [q'' [a_eq_a' H']]]];
simpl in a_eq_a'; simpl in H'; subst q.
rewrite ass_app in P1; setoid_rewrite <- permut_cons_inside in P1;
rewrite <- ass_app in P1.
rewrite ass_app in P2; setoid_rewrite <- permut_cons_inside in P2;
rewrite <- ass_app in P2.
apply (multiset_closure_aux R (q' ++ q'') P1 P2 p_diff_nil).
intros a'' la ala'_in_ll; apply app_lt_cns; trivial.
trivial.
trivial.
assert False; [idtac | contradiction].
apply (cns_disj_app irrefl_R a).
assert (a_in_cns_ll_q : mem a (consn ll ++ q)).
setoid_rewrite <- (mem_permut_mem a P2); left; trivial.
reflexivity.
setoid_rewrite <- mem_or_app in a_in_cns_ll_q.
destruct a_in_cns_ll_q as [a_in_cns_ll | a_in_q];
[trivial | absurd (mem a q); trivial; intro].
assert (a_in_app_ll_q : mem a (appendn ll ++ q)).
setoid_rewrite <- (mem_permut_mem a P1); left; trivial.
reflexivity.
setoid_rewrite <- mem_or_app in a_in_app_ll_q.
destruct a_in_app_ll_q as [a_in_app_ll | a_in_q];
[trivial | absurd (mem a q); trivial].
Qed.
Lemma remove_context_trans_clos_multiset_extension_step_app1 :
forall R, (forall x y, {R x y}+{~R x y}) -> transitive _ R -> (forall a, ~R a a) ->
forall l1 l2 l, trans_clos (multiset_extension_step R) (l ++ l1) (l ++ l2) ->
trans_clos (multiset_extension_step R) l1 l2.
Proof.
intros R dec_R trans_R irrefl_R l1 l2 l; generalize l1 l2; clear l1 l2;
induction l as [ | a l]; trivial.
intros l1 l2 H; apply IHl;
apply context_trans_clos_multiset_extension_step_cons with a; trivial.
Qed.
Definition R_or_eq_dec (R : relation A) (R_dec : forall e1 e2, {R e1 e2}+{~R e1 e2}) e1 e2 : comp :=
if eq_dec e1 e2
then Equivalent
else
if R_dec e1 e2
then Less_than
else
if R_dec e2 e1
then Greater_than
else Uncomparable.
Lemma R_or_eq_dec_is_sound :
forall R R_dec e1 e2,
match R_or_eq_dec R R_dec e1 e2 with
| Equivalent => eq_A e1 e2
| Less_than => R e1 e2
| Greater_than => R e2 e1
| Uncomparable => ~ eq_A e1 e2 /\ ~R e1 e2 /\ ~R e2 e1
end.
Proof.
intros R R_dec e1 e2; unfold R_or_eq_dec;
destruct (eq_dec e1 e2) as [e1_eq_e2 | e1_diff_e2]; trivial.
destruct (R_dec e1 e2) as [e1Re2 | not_e1Re2]; trivial.
destruct (R_dec e2 e1) as [e2Re1 | not_e2Re1]; intuition.
Qed.
Definition mult (R : relation A) (R_dec : forall e1 e2, {R e1 e2}+{~R e1 e2})
(l1 l2 : list A) : comp :=
match remove_equiv l1 l2 with
| (nil, nil) => Equivalent
| (l1, l2) =>
match (list_forall
(fun t2 =>
list_exists
(fun t1 =>
match R_or_eq_dec R R_dec t1 t2 with
| Greater_than => true
| _ => false
end) l1) l2) with
| true => Greater_than
| false =>
match (list_forall
(fun t1 =>
list_exists
(fun t2 =>
match R_or_eq_dec R R_dec t2 t1 with
| Greater_than => true
| _ => false
end) l2) l1) with
| true => Less_than
| false => Uncomparable
end
end
end.
Lemma nil_is_the_smallest :
forall R e l, trans_clos (multiset_extension_step R) nil (e :: l).
Proof.
intros R e' l; generalize e'; clear e'; induction l as [ | e l].
intros e; apply t_step; refine (@rmv_case _ _ _ nil nil e _ _ _); auto; contradiction.
intros e'; apply trans_clos_is_trans with (e' :: l); trivial.
apply t_step; refine (@rmv_case _ _ _ (e' :: l) nil e _ _ _); auto.
contradiction.
setoid_rewrite <- (permut_cons_inside (e1 := e') (e2 := e') (e :: l) (e :: nil) l).
reflexivity.
auto.
Qed.
Lemma R_dec_sym :
forall R R_dec, transitive _ R -> (forall a, ~R a a) ->
forall e1 e2,
R_or_eq_dec R R_dec e2 e1 = match R_or_eq_dec R R_dec e1 e2 with
| Equivalent => Equivalent
| Less_than => Greater_than
| Greater_than => Less_than
| Uncomparable => Uncomparable
end.
intros R R_dec trans_R irrefl_R e1 e2;
generalize (R_or_eq_dec_is_sound R R_dec e1 e2);
generalize (R_or_eq_dec_is_sound R R_dec e2 e1);
destruct (R_or_eq_dec R R_dec e1 e2);
destruct (R_or_eq_dec R R_dec e2 e1);
unfold eq_A; trivial.
intros; subst e2; absurd (R e1 e1); trivial; apply irrefl_R.
intros; subst e2; absurd (R e1 e1); trivial; apply irrefl_R.
intros [e2_diff_e1 _] e1_eq_e2; subst e2; absurd (e1 = e1); trivial.
intros; subst e2; absurd (R e1 e1); trivial; apply irrefl_R.
intros; absurd (R e1 e1); [apply irrefl_R | apply trans_R with e2; trivial].
intros [_ [_ not_e1_R_e2]] e1_R_e2; absurd (R e1 e2); trivial.
intros; subst e2; absurd (R e1 e1); trivial; apply irrefl_R.
intros; absurd (R e1 e1); [apply irrefl_R | apply trans_R with e2; trivial].
intros [_ [not_e2_R_e1 _]] e2_R_e1; absurd (R e2 e1); trivial.
intros e2_eq_e1 [e1_diff_e2 _]; subst e2; absurd (e1 = e1); trivial.
intros e2_R_e1 [_ [_ not_e2_R_e1]]; absurd (R e2 e1); trivial.
intros e1_R_e2 [_ [not_e1_R_e2 _]]; absurd (R e1 e2); trivial.
Qed.
Lemma greater_case :
forall R R_dec l1 l2,
list_forall
(fun t2 =>
list_exists
(fun t1 =>
match R_or_eq_dec R R_dec t1 t2 with
| Greater_than => true
| _ => false
end) l1) l2 = true ->
exists le, exists ll, permut l1 (consn ll ++ le) /\
permut l2 (appendn ll) /\
(forall a la, In (a,la) ll -> forall b, mem b la -> R b a).
Proof.
intros R R_dec l1 l2; generalize l1; clear l1;
induction l2 as [ | e2 l2].
intros l1 _; exists l1; exists (@nil (A * list A)); simpl; intuition.
intros l1; simpl.
generalize (list_exists_is_sound (fun t1 : A =>
match R_or_eq_dec R R_dec t1 e2 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) l1);
destruct (list_exists (fun t1 : A =>
match R_or_eq_dec R R_dec t1 e2 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) l1).
intro H; generalize (proj1 H (refl_equal _)); clear H;
intros [a1 [a1_in_l1 e2_R_a1]]; generalize (IHl2 l1); simpl.
destruct (list_forall
(fun t2 : A =>
list_exists
(fun t1 : A =>
match R_or_eq_dec R R_dec t1 t2 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) l1) l2).
intro H; generalize (H (refl_equal _)); clear H;
intros [le [ll [P1 [P2 app_lt_cns]]]] _.
assert (a1_mem_cns_ll_le : mem a1 (consn ll ++ le)).
setoid_rewrite <- (mem_permut_mem a1 P1); apply in_impl_mem; trivial.
assert (e2_R_a1' : R e2 a1).
generalize (R_or_eq_dec_is_sound R R_dec a1 e2);
destruct (R_or_eq_dec R R_dec a1 e2); trivial;
absurd (false = true); trivial; discriminate.
setoid_rewrite <- mem_or_app in a1_mem_cns_ll_le.
destruct a1_mem_cns_ll_le as [a1_mem_cns_ll | a1_mem_le].
destruct (proj1 (mem_consn _ _) a1_mem_cns_ll) as [la ala_in_ll].
destruct (In_split _ _ ala_in_ll) as [ll' [ll'' H]]; subst ll.
exists le; exists (ll' ++ (a1, e2 :: la) :: ll''); split.
rewrite consn_app; simpl; rewrite consn_app in P1; simpl in P1; trivial.
split.
rewrite appendn_app; simpl; setoid_rewrite <- permut_cons_inside;
rewrite appendn_app in P2; simpl in P2; trivial.
reflexivity.
intros x lx xlx_in_ll b b_in_lx;
destruct (in_app_or _ _ _ xlx_in_ll) as [xlx_ll' | [xlx_eq_a1la | xlx_in_ll'']].
apply (app_lt_cns x lx); trivial; apply in_or_app; left; trivial.
injection xlx_eq_a1la; intros; subst x lx.
destruct b_in_lx as [b_eq_e2 | b_in_la];
[unfold EDS.eq_A, eq_A in b_eq_e2; subst b | apply (app_lt_cns a1 la)]; trivial.
apply (app_lt_cns x lx); trivial; apply in_or_app; do 2 right; trivial.
destruct (mem_split_set _ _ a1_mem_le) as [a1' [le' [le'' [a1_eq_a1' H]]]];
simpl in a1_eq_a1'; simpl in H; subst le.
exists (le' ++ le''); exists ((a1, e2 :: nil) :: ll); split.
simpl; setoid_rewrite P1; rewrite ass_app; apply permut_sym;
setoid_rewrite <- permut_cons_inside.
trivial.
rewrite ass_app; auto.
split.
simpl; setoid_rewrite <- permut_cons; trivial.
reflexivity.
intros x lx [xlx_eq_a1_e2 | xlx_in_ll] b b_in_lx.
injection xlx_eq_a1_e2; intros; subst x lx;
destruct b_in_lx as [b_eq_e2 | Abs];
[unfold EDS.eq_A, eq_A in b_eq_e2; subst b; trivial | contradiction].
apply (app_lt_cns x lx); trivial; right; trivial.
intros; absurd (false = true); trivial.
discriminate.
simpl; intros; absurd (false = true); trivial; discriminate.
Qed.
Lemma mult_is_sound :
forall R R_dec l1 l2,
match mult R R_dec l1 l2 with
| Equivalent => permut l1 l2
| Less_than => trans_clos (multiset_extension_step R) l1 l2
| Greater_than => trans_clos (multiset_extension_step R) l2 l1
| _ => True
end.
intros R R_dec l1 l2; unfold mult; simpl;
generalize (remove_equiv_is_sound l1 l2);
destruct (remove_equiv l1 l2) as [l1' l2'];
intros [l [P1 [P2 H]]];
destruct l1' as [ | e1' l1'];
destruct l2' as [ | e2' l2'].
setoid_rewrite P1; setoid_rewrite P2; auto.
simpl; rewrite <- app_nil_end in P1;
apply (multiset_closure_aux2 R (p := l1) (q := l2)
(le := e2' :: l2') (l := nil) l); simpl; auto.
setoid_rewrite P2; rewrite app_comm_cons; apply list_permut_app_app.
right; discriminate.
intros; contradiction.
simpl; rewrite <- app_nil_end in P2;
apply (multiset_closure_aux2 R (p := l2) (q := l1)
(le := e1' :: l1') (l := nil) l); simpl; auto.
setoid_rewrite P1; rewrite app_comm_cons; apply list_permut_app_app.
right; discriminate.
intros; contradiction.
generalize (greater_case R R_dec (e1' :: l1') (e2' :: l2'));
destruct (list_forall
(fun t2 : A =>
list_exists
(fun t1 : A =>
match R_or_eq_dec R R_dec t1 t2 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) (e1' :: l1')) (e2' :: l2')).
intro H'; generalize (H' (refl_equal _)); clear H'; intros [le [ll [P1' [P2' app_lt_cns]]]].
apply (multiset_closure_aux2 R (p := l2) (q := l1) (le := le) (l := ll) l); simpl; auto.
setoid_rewrite P2; setoid_rewrite P2'; apply list_permut_app_app.
setoid_rewrite P1; setoid_rewrite P1';
apply permut_trans with (l ++ le ++ consn ll).
setoid_rewrite <- permut_app1; apply list_permut_app_app.
rewrite (ass_app le); apply list_permut_app_app.
destruct ll as [ | [x lx] ll].
destruct le as [ | e le].
generalize (permut_length P1'); simpl; intro;
absurd (S (length l1') = 0); trivial; discriminate.
right; discriminate.
left; discriminate.
intros _; generalize (greater_case R R_dec (e2' :: l2') (e1' :: l1'));
destruct (list_forall
(fun t1 : A =>
list_exists
(fun t2 : A =>
match R_or_eq_dec R R_dec t2 t1 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) (e2' :: l2')) (e1' :: l1')).
intro H'; generalize (H' (refl_equal _)); clear H'; intros [le [ll [P2' [P1' app_lt_cns]]]].
apply (multiset_closure_aux2 R (p := l1) (q := l2) (le := le) (l := ll) l); simpl; auto.
setoid_rewrite P1; setoid_rewrite P1'; apply list_permut_app_app.
setoid_rewrite P2; setoid_rewrite P2';
apply permut_trans with (l ++ le ++ consn ll).
setoid_rewrite <- permut_app1; apply list_permut_app_app.
rewrite (ass_app le); apply list_permut_app_app.
destruct ll as [ | [x lx] ll].
destruct le as [ | e le].
generalize (permut_length P2'); simpl; intro;
absurd (S (length l2') = 0); trivial; discriminate.
right; discriminate.
left; discriminate.
trivial.
Qed.
Lemma mult_is_complete_equiv :
forall R R_dec l1 l2, permut l1 l2 -> mult R R_dec l1 l2 = Equivalent.
Proof.
intros R R_dec l1 l2 P; unfold mult;
generalize (remove_equiv_is_sound l1 l2);
destruct (remove_equiv l1 l2) as [l1' l2'];
intros [l [P1 [P2 H]]].
destruct l1' as [ | e1' l1'].
destruct l2' as [ | e2' l2'].
trivial.
setoid_rewrite P in P1; rewrite <- app_nil_end in P1; setoid_rewrite P1 in P2;
generalize (permut_length P2); rewrite length_app;
rewrite <- (plus_0_r (length l)); rewrite <- plus_assoc;
intro H'; generalize (plus_reg_l _ _ _ H'); clear H';
intro H'; simpl in H'; absurd (0 = S (length l2')); trivial; discriminate.
setoid_rewrite P in P1; setoid_rewrite P1 in P2;
setoid_rewrite <- permut_app1 in P2;
assert False; [apply (H e1') | contradiction].
left; reflexivity.
setoid_rewrite <- P2; left; reflexivity.
Qed.
Lemma mult_is_complete_greater :
forall (R : relation A) R_dec, transitive _ R -> (forall a, ~ R a a) ->
forall l l1 l2, (forall a, mem a l1 -> mem a l2 -> False) ->
trans_clos (multiset_extension_step R) (l ++ l2) (l ++ l1) ->
(list_forall
(fun t2 =>
list_exists
(fun t1 =>
match R_or_eq_dec R R_dec t1 t2 with
| Greater_than => true
| _ => false
end) l1) l2) = true.
Proof.
intros R R_dec trans_R irrefl_R l l1 l2 l2_disj_l1 ll2_lt_ll1.
assert (l2_lt_l1 := remove_context_trans_clos_multiset_extension_step_app1
R_dec trans_R irrefl_R l2 l1 l ll2_lt_ll1).
clear ll2_lt_ll1.
destruct (multiset_closure R_dec trans_R l2_lt_l1)
as [ll [lc [P2 [P1 [ll_diff_nil [app_lt_cns cns_disj_app]]]]]].
assert (lc_eq_nil : lc = nil).
destruct lc as [ | c lc].
trivial.
assert False; [idtac | contradiction].
apply (l2_disj_l1 c).
setoid_rewrite (mem_permut_mem c P1); setoid_rewrite <- mem_or_app; right; left; reflexivity.
setoid_rewrite (mem_permut_mem c P2); setoid_rewrite <- mem_or_app; right; left; reflexivity.
subst lc; rewrite <- app_nil_end in P1; rewrite <- app_nil_end in P2.
assert (Dummy1 : forall t1 t2 t1' t2' : EDS.A,
EDS.eq_A t1 t1' ->
EDS.eq_A t2 t2' ->
(fun t3 t4 : DS1.A =>
match R_or_eq_dec R R_dec t4 t3 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) t1 t2 =
(fun t3 t4 : DS1.A =>
match R_or_eq_dec R R_dec t4 t3 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) t1' t2').
intros t1 t1' t2 t2'; unfold EDS.eq_A, eq_A; intros; subst; trivial.
assert (Dummy2 := permut_list_forall_exists _ _ Dummy1).
unfold EDS.A, A in *.
rewrite (Dummy2 _ _ _ _ P2 P1); clear Dummy1 Dummy2.
clear P1 P2 ll_diff_nil; induction ll as [ | [a la] ll]; simpl; trivial.
rewrite list_forall_app.
assert (Dummy := list_forall_impl
(fun t1 : A =>
list_exists
(fun t2 : A =>
match R_or_eq_dec R R_dec t2 t1 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) (consn ll))
(fun t1 : A =>
Bool.ifb
match R_or_eq_dec R R_dec a t1 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end true
(list_exists
(fun t2 : A =>
match R_or_eq_dec R R_dec t2 t1 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) (consn ll))) (appendn ll)).
unfold A in *; rewrite Dummy; clear Dummy; trivial.
generalize la (app_lt_cns a la (or_introl _ (refl_equal _)));
clear la app_lt_cns cns_disj_app;
intros la la_lt_a; induction la as [ | b la]; trivial.
simpl; destruct (list_forall
(fun t1 : DS.A =>
Bool.ifb
match R_or_eq_dec R R_dec a t1 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end true
(list_exists
(fun t2 : DS.A =>
match R_or_eq_dec R R_dec t2 t1 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) (consn ll))) la); simpl.
generalize (R_or_eq_dec_is_sound _ R_dec a b).
destruct (R_or_eq_dec R R_dec a b).
unfold eq_A; intro a_eq_b; subst b; absurd (R a a); [apply (irrefl_R a) | apply la_lt_a; left; trivial].
reflexivity.
intro; absurd (R a a);
[apply (irrefl_R a) | apply trans_R with b; trivial; apply la_lt_a; left; trivial].
reflexivity.
simpl; trivial.
intros [_ [_ not_b_R_a]]; absurd (R b a); trivial; apply la_lt_a; left; reflexivity.
simpl in IHla;
absurd (false = true); [discriminate | apply IHla; intros; apply la_lt_a; right; trivial].
intros b b_in_app; destruct (R_or_eq_dec R R_dec a b); trivial.
apply IHll.
intros b lb blb_in_ll c c_in_lb; apply (app_lt_cns b lb); trivial.
right; trivial.
intros _ b b_in_cns b_in_appn;
apply (cns_disj_app irrefl_R b).
right; trivial.
simpl; setoid_rewrite <- mem_or_app; right; trivial.
Qed.
Lemma mult_is_complete :
forall (R : relation A) R_dec, transitive _ R -> (forall a, ~ R a a) ->
forall l1 l2,
match mult R R_dec l1 l2 with
| Uncomparable => ~ permut l1 l2 /\
~trans_clos (multiset_extension_step R) l1 l2 /\
~trans_clos (multiset_extension_step R) l2 l1
| _ => True
end.
Proof.
intros R R_dec trans_R irrefl_R l1 l2.
unfold mult.
generalize (remove_equiv_is_sound l1 l2); destruct (remove_equiv l1 l2) as [l1' l2'].
intros [l [P1 [P2 l1'_disj_l2']]].
assert (l2'_disj_l1' : forall x, mem x l2' -> mem x l1' -> False).
intros x H1 H2; apply (l1'_disj_l2' x); trivial.
generalize (@mult_is_complete_equiv R R_dec l1 l2)
(@mult_is_complete_greater R R_dec trans_R irrefl_R l l1' l2' l1'_disj_l2')
(@mult_is_complete_greater R R_dec trans_R irrefl_R l l2' l1' l2'_disj_l1').
destruct l1' as [ | e1' l1'].
destruct l2' as [ | e2' l2']; simpl; trivial.
destruct (list_forall
(fun t2 : A =>
list_exists
(fun t1 : A =>
match R_or_eq_dec R R_dec t1 t2 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) (e1' :: l1')) l2'); trivial.
destruct (list_forall
(fun t1 : A =>
list_exists
(fun t2 : A =>
match R_or_eq_dec R R_dec t2 t1 with
| Equivalent => false
| Less_than => false
| Greater_than => true
| Uncomparable => false
end) l2') (e1' :: l1')); trivial.
intros H1 H2 H3; repeat split; intro H.
setoid_rewrite H in P1; setoid_rewrite P1 in P2;
setoid_rewrite <- permut_app1 in P2;
apply (l1'_disj_l2' e1'); [idtac | setoid_rewrite <- P2]; left; reflexivity.
absurd (false = true); [discriminate | apply H3];
apply list_permut_trans_clos_multiset_extension_step_2 with l2; trivial;
apply list_permut_trans_clos_multiset_extension_step_1 with l1; trivial.
absurd (false = true); [discriminate | apply H2];
apply list_permut_trans_clos_multiset_extension_step_2 with l1; trivial;
apply list_permut_trans_clos_multiset_extension_step_1 with l2; trivial.
Qed.
End Make.
Module NatMul := Make (ordered_set.Nat).