Library SumList
Require Export List.
Require Export Omega.
Require Export PosInf.
Section sumlist.
Variable A:Set.
Variable mes:A->nat.
Fixpoint sumlist (l:list A) : nat :=
match l with
nil => 0
| cons a q => (mes a) + (sumlist q)
end.
Lemma sumlist_bound : forall l M,
(forall x, In x l -> (mes x)<= M) ->
(sumlist l) <= (length l)*M.
induction l; simpl; intros.
auto.
assert (forall x : A, In x l -> mes x <= M).
intuition.
generalize (IHl _ H0); intros.
assert (mes a <= M).
intuition.
omega.
Qed.
End sumlist.
Implicit Arguments sumlist [A].
Lemma sumlist_bound2 : forall (A:Set) mes1 mes2 l,
(forall x:A, In x l -> mes1 x <= mes2 x) ->
(sumlist mes1 l) <= (sumlist mes2 l).
induction l; simpl; intros.
auto.
assert (sumlist mes1 l <= sumlist mes2 l).
intuition.
assert (mes1 a <= mes2 a).
intuition.
omega.
Qed.
Fixpoint insere (m:Word) (pc:Word) (l:list (Word*(list Word))) {struct l} : list (Word*(list Word)) :=
match l with
nil => (m,pc::nil)::nil
| (m1,l1)::q =>
match eq_word_dec m m1 with
left _ => (m1,pc::l1)::q
| right _ => (m1,l1)::(insere m pc q)
end
end.
Fixpoint factorize (l:list (Word*Word)) : list (Word*(list Word)) :=
match l with
nil => nil
| (m,pc)::q => insere m pc (factorize q)
end.
Lemma sumlist_factorize : forall l,
length l = sumlist (fun ml:Word*(list Word) => let (m,l):=ml in length l)
(factorize l).
induction l; simpl.
auto.
set (f:=(fun ml : Word * list Word => let (_, l) := ml in length l)) in *.
rewrite IHl.
destruct a as [m pc].
generalize (factorize l).
induction l0; simpl; intros.
auto.
destruct a as [m1 l1].
case (eq_word_dec m m1); simpl; intros.
auto.
omega.
Qed.
Fixpoint insere_in_multiset (pc:Word) (l:list (Word*nat)) {struct l} : list (Word*nat) :=
match l with
nil => (pc,1)::nil
| (pc',n)::q =>
match eq_word_dec pc pc' with
left _ => (pc',S n)::q
| right _ => (pc',n)::(insere_in_multiset pc q)
end
end.
Fixpoint list2multiset (l:list Word) : list (Word*nat) :=
match l with
nil => nil
| pc::q => insere_in_multiset pc (list2multiset q)
end.
Lemma sumlist_list2multiset : forall l,
length l = sumlist (fun pcn:(Word*nat) => let (pc,n) := pcn in n) (list2multiset l).
induction l; simpl; auto.
rewrite IHl.
set (f:=(fun pcn : Word * nat => let (_, n) := pcn in n)).
clear IHl.
induction (list2multiset l); simpl; auto.
destruct a0 as [pc' n].
case (eq_word_dec a pc'); simpl; intros; auto.
rewrite <- IHl0; auto.
Qed.
Lemma eq_sumlist : forall (A:Set) (f1 f2:A->nat),
(forall x, f1 x = f2 x) -> forall l, sumlist f1 l = sumlist f2 l.
induction l; simpl; intros; auto.
Qed.
Lemma sumlist_final : forall l,
length l = sumlist (fun ml:Word*(list Word) => let (m,l):=ml in
sumlist (fun pcn:(Word*nat) => let (pc,n) := pcn in n) (list2multiset l))
(factorize l).
intros l.
replace (sumlist
(fun ml : Word * list Word =>
let (_, l0) := ml in
sumlist (fun pcn : Word * nat => let (_, n) := pcn in n)
(list2multiset l0)) (factorize l))
with (sumlist
(fun ml : Word * list Word =>
let (_, l0) := ml in length l0) (factorize l)).
apply sumlist_factorize.
apply eq_sumlist.
intros (m,l1).
apply sumlist_list2multiset.
Qed.
Inductive nb_m_pc (m':Word) (pc':Word) : list (Word*Word) -> nat -> Prop :=
nb_m_pc0 : nb_m_pc m' pc' nil 0
| nb_m_pc1 : forall m pc l n,
eq_word m' m -> eq_word pc' pc -> nb_m_pc m' pc' l n ->
nb_m_pc m' pc' ((m,pc)::l) (S n)
| nb_m_pc2 : forall m pc l n,
(~ eq_word m' m \/ ~ eq_word pc' pc) -> nb_m_pc m' pc' l n ->
nb_m_pc m' pc' ((m,pc)::l) n.
Inductive m_distincts : list (Word*(list Word)) -> Prop :=
m_distincts0 : m_distincts nil
| m_distincts1 : forall m lp l,
~(exists m', exists lp', In (m',lp') l /\ eq_word m m') ->
m_distincts l ->
m_distincts ((m,lp)::l).
Hint Constructors m_distincts.
Lemma in_insere_simpl : forall l m' m lp' pc,
In (m', lp') (insere m pc l) ->
eq_word m' m \/
(exists m'' : Word,
(exists lp'' : list Word, In (m'', lp'') l /\ eq_word m' m'')).
induction l; simpl; intros.
intuition.
injection H0; intros; subst; intuition.
destruct a.
generalize H; clear H; case eq_word_dec; intros.
elim H; clear H; intros.
injection H; clear H; intros; subst.
left; apply eq_word_sym; auto.
right; eauto.
elim H; clear H; intros.
injection H; clear H; intros; subst.
right; eauto.
elim (IHl _ _ _ _ H); intros.
auto.
generalize H0; clear H0; intros (m'',(lp'',(H1',H2'))).
right; exists m''; exists lp''; intuition.
Qed.
Lemma m_distincts_insere : forall m pc l,
m_distincts l -> m_distincts (insere m pc l).
induction l; simpl; intros.
constructor; auto.
red; intros (m',(lp',(H1,H2))).
inversion H1.
inversion_clear H.
case eq_word_dec; intros; constructor; auto.
red; intros (m',(lp',(H3,H4))).
elim (in_insere_simpl _ _ _ _ _ H3); intros.
elim n; apply eq_word_sym; apply eq_word_trans with m'; auto.
elim H0; auto.
generalize H; clear H; intros (m'',(lp'',(H1',H2'))).
exists m''; exists lp''; split; auto.
apply eq_word_trans with m'; auto.
Qed.
Lemma in_insere : forall l m lp m1 pc1,
In (m, lp) (insere m1 pc1 l) ->
m_distincts l ->
(In (m, lp) l /\ ~ eq_word m m1) \/
exists lp', (
(lp'=nil /\ forall m'' l'', In (m'',l'') l -> ~ eq_word m1 m'')
\/ In (m,lp') l) /\ eq_word m m1 /\ lp=(pc1::lp').
induction l; simpl; intros.
intuition.
injection H1; clear H1; intros; subst.
right.
exists (nil (A:=Word)); split; auto.
destruct a as [m2 lp2].
generalize H; clear H; case eq_word_dec; simpl; intros.
elim H; clear H; intros.
injection H; clear H; intros; subst.
right; exists lp2; split; intuition.
left; split; auto.
red; intros; inversion_clear H0.
elim H2; exists m; exists lp; split; auto.
apply eq_word_sym; apply eq_word_trans with m1; auto.
elim H; clear H; intros.
injection H; clear H; intros; subst.
left; split; auto.
elim (IHl _ _ _ _ H); intros.
intuition.
elim H1; clear H1; intros lp' (H4,(H2,H3)).
right.
elim H4; clear H4; intros.
exists lp'; decompose [and] H1.
split; auto.
left; split; auto.
intros.
elim H6; clear H6; intros.
injection H6; clear H6; intros; subst; auto.
apply H5 with l''; auto.
exists lp'; auto.
inversion_clear H0; auto.
Qed.
Lemma in_insere2 : forall l m lp m' pc',
In (m,lp) l ->
exists m'', exists lp' : list Word,
In (m'', lp') (insere m' pc' l) /\ incl lp lp' /\ eq_word m m''.
induction l; simpl; intros.
elim H.
elim H; clear H; intros.
subst; simpl.
case eq_word_dec; intros.
exists m; exists (pc'::lp); split; auto with datatypes.
exists m; exists lp; split; auto with datatypes.
destruct a; simpl.
case eq_word_dec; intros.
exists m; exists lp; split; auto with datatypes.
elim (IHl _ _ m' pc' H); intros m'' (lp',(H1,(H2,H3))).
exists m''; exists lp'; split; auto with datatypes.
Qed.
Lemma in_factorize : forall m pc l,
In (m,pc) l ->
exists m', exists lp,
In (m',lp) (factorize l) /\
eq_word m m' /\
In pc lp.
induction l; simpl; intros.
inversion H.
elim H; clear H; intros.
subst; simpl.
clear IHl; induction (factorize l); simpl.
exists m; exists (pc::nil); intuition.
destruct a; simpl.
case eq_word_dec; intros; simpl.
exists w; exists (pc::l1); intuition.
elim IHl0; intros m' (lp,(H1,(H2,H3))).
exists m'; exists lp; intuition.
elim (IHl H); clear IHl; intros m' (lp,(H1,(H2,H3))).
destruct a; simpl.
elim (in_insere2 _ _ _ w w0 H1); intros m'' (lp',(H1',(H2',H3'))).
exists m''; exists lp'; intuition.
apply eq_word_trans with m'; auto.
Qed.
Lemma m_pc_not_in : forall l m pc,
(forall m' pc', In (m',pc') l -> ~ eq_word pc pc' \/ ~ eq_word m m') ->
nb_m_pc m pc l 0.
induction l; simpl; intros.
constructor.
destruct a; constructor; intuition.
elim (H w w0); intuition.
Qed.
Inductive pc_distincts : list (Word*nat) -> Prop :=
pc_distincts0 : pc_distincts nil
| pc_distincts1 : forall pc n l,
~(exists pc', exists n', In (pc',n') l /\ eq_word pc pc') ->
pc_distincts l ->
pc_distincts ((pc,n)::l).
Hint Constructors pc_distincts.
Lemma in_insere_in_multiset : forall pc pc0 n l,
In (pc,n) (insere_in_multiset pc0 l) ->
eq_word pc0 pc
\/
(~ eq_word pc0 pc /\ In (pc,n) l).
induction l; simpl; intros.
elim H; clear H; intros.
injection H; clear H; intros; subst.
left; intuition.
elim H.
destruct a.
generalize H; clear H; case eq_word_dec; intros.
case (eq_word_dec pc0 pc); intros.
left; auto.
elim H; clear H; intros.
injection H; clear H; intros; subst.
elim n1 ;auto.
right; auto.
case (eq_word_dec pc0 pc); intros.
left; auto.
right; elim H; clear H; intros.
injection H; clear H; intros; subst.
auto.
elim (IHl H); intros.
elim n2; auto.
intuition.
Qed.
Lemma insere_in_multiset_distincts : forall pc l,
pc_distincts l -> pc_distincts (insere_in_multiset pc l).
induction l; simpl; intros.
constructor; auto.
red; intros.
elim H0; intros pc' (n',(H1,H2)).
inversion H1.
destruct a; simpl.
case eq_word_dec; intros.
inversion_clear H.
constructor; auto.
inversion_clear H.
constructor; auto.
red; intros (pc',(n',(H3,H2))).
elim (in_insere_in_multiset _ _ _ _ H3); intros.
elim n0; apply eq_word_trans with pc'; auto.
elim H0; exists pc'; exists n'; intuition.
Qed.
Lemma in_insere_in_multiset_eq : forall pc pc0 n l,
pc_distincts l ->
In (pc,n) (insere_in_multiset pc0 l) ->
eq_word pc0 pc ->
( n=1 /\ forall pc' n', In (pc',n') l -> ~ eq_word pc pc')
\/
exists pc', exists n', In (pc',n') l /\ eq_word pc pc' /\ n = S n'.
induction l; simpl; intros.
elim H0; intros.
injection H2; intros; subst.
left; split; intuition.
elim H2.
destruct a.
generalize H0; clear H0; case eq_word_dec; intros.
elim H0; clear H0; intros.
injection H0; clear H0; intros; subst.
right; exists pc; exists n0; intuition.
inversion_clear H.
elim H2; exists pc; exists n; intuition.
apply eq_word_sym; apply eq_word_trans with pc0; auto.
elim H0; clear H0; intros.
injection H0; clear H0; intros; subst.
elim n1; auto.
inversion_clear H.
elim (IHl H3 H0); intros; auto.
decompose [and] H.
left; split; auto.
intros.
elim H6; intros; auto.
injection H7; clear H6 H7; intros; subst.
red; intros ;elim n1; apply eq_word_trans with pc; auto.
eauto.
elim H; clear H; intros pc' (n',(H1',(H2',H3'))).
subst.
right.
exists pc'; exists n'; intuition.
Qed.
Lemma list2multiset_distinct : forall l, pc_distincts (list2multiset l).
induction l; simpl; try constructor.
apply insere_in_multiset_distincts; auto.
Qed.
Lemma factorize_distinct : forall l, m_distincts (factorize l).
induction l; simpl; try constructor.
destruct a.
apply m_distincts_insere; auto.
Qed.
Lemma in_list2multiset : forall l pc n,
In (pc,n) (list2multiset l) -> exists pc', In pc' l /\ eq_word pc' pc.
induction l; simpl; intros.
elim H.
elim (in_insere_in_multiset _ a _ _ H); intros.
exists a; split; auto.
decompose [and] H0.
elim (IHl _ _ H2); intuition eauto.
Qed.
Lemma in_factorize2: forall l m lp,
In (m, lp) (factorize l) ->
forall pc, In pc lp -> exists m',
eq_word m m' /\ In (m',pc) l.
induction l; simpl; intros.
elim H.
destruct a.
elim (in_insere _ _ _ _ _ H).
intros (H1,H2).
elim (IHl _ _ H1 pc H0); intros m' (H3,H4).
eauto.
intros (lp',(H1,(H2,H3))).
subst.
elim H0; clear H0; intros; subst.
exists w; auto.
elim H1; clear H1; intros.
elim H1; clear H1; intros.
subst; inversion H0.
elim (IHl _ _ H1 pc H0); intros m' (H3,H4).
eauto.
apply factorize_distinct.
Qed.
Lemma in_list2multiset_factorize : forall l lp m' pc n,
In (m',lp) (factorize l) ->
In (pc,n) (list2multiset lp) ->
exists m'', exists pc', In (m'',pc') l /\ eq_word m' m'' /\ eq_word pc' pc.
intros.
elim (in_list2multiset _ _ _ H0); intros pc' (H1,H2).
elim (in_factorize2 _ _ _ H pc' H1); intros m'' (H3,H4).
eauto.
Qed.
Lemma in_m_distinct : forall m1 m2 lp1 lp2 l,
m_distincts l ->
In (m1,lp1) l ->
In (m2,lp2) l ->
eq_word m1 m2 -> lp1=lp2.
induction 1; intros.
inversion H.
elim H1; clear H1; intros.
elim H2; clear H2; intros.
injection H1; injection H2; intros; subst; auto.
elim H; exists m2; exists lp2; split; auto.
injection H1; intros; subst; auto.
elim H2; clear H2; intros.
injection H2; intros; subst; auto.
elim H; exists m1; exists lp1; split; auto.
auto.
Qed.
Lemma in_insere_in_multiset2: forall l pc,
In pc l ->
exists pc', exists n, In (pc',n) (list2multiset l) /\ eq_word pc pc'.
induction l; simpl; intros.
elim H.
elim H; clear H; intros.
subst; clear IHl.
induction (list2multiset l); simpl.
exists pc; exists 1; auto.
destruct a.
case eq_word_dec; intros.
exists w; exists (S n); auto with datatypes.
elim IHl0; intros pc' (n',(H1,H2)).
exists pc'; exists n'; auto with datatypes.
elim (IHl _ H); intros pc' (n,(H1,H2)).
clear IHl.
induction (list2multiset l); simpl.
inversion H1.
destruct a0.
case eq_word_dec; intros.
elim H1; intros.
injection H0; intros; subst.
exists pc'; exists (S n).
auto with datatypes.
exists pc'; exists n.
auto with datatypes.
elim H1; clear H1; intros.
injection H0; clear H0; intros; subst.
exists pc'; exists n; auto with datatypes.
elim (IHl0 H0); intros pc'' (n',(H1,H3)).
exists pc''; exists n'; auto with datatypes.
Qed.
Lemma nb_m_pc_eq : forall m1 m2 pc1 pc2 l n,
eq_word m1 m2 -> eq_word pc1 pc2 ->
nb_m_pc m1 pc1 l n -> nb_m_pc m2 pc2 l n.
induction 3; constructor; auto.
apply eq_word_trans with m1; auto.
apply eq_word_sym; auto.
apply eq_word_trans with pc1; auto.
elim H1; clear H1; intros.
left; red; intros.
elim H1; apply eq_word_trans with m2; auto.
right; red; intros.
elim H1; apply eq_word_trans with pc2; auto.
Qed.
Lemma nb_m_pc_in_list : forall l m pc lp n,
In (m,lp) (factorize l) ->
In (pc,n) (list2multiset lp) -> nb_m_pc m pc l n.
induction l; simpl; intros.
elim H.
destruct a as [m1 pc1].
elim (in_insere _ _ _ _ _ H); clear H; intros.
elim H; clear H; intros.
constructor; auto.
apply IHl with lp; auto.
elim H; clear H; intros lp' (H1,(H2,H3)); subst.
elim H1; clear H1; intros.
decompose [and] H; clear H; subst.
simpl in H0.
elim H0; clear H0; intros.
injection H; clear H; intros; subst.
constructor; auto.
apply m_pc_not_in; intros.
elim (in_factorize _ _ _ H); intros m'' (lp',(H1',(H2',H3'))).
right; red; intros.
elim (H3 _ _ H1').
apply eq_word_trans with m'; auto.
apply eq_word_trans with m; auto.
elim H.
simpl in H0.
elim (in_insere_in_multiset _ _ _ _ H0); intros.
elim (in_insere_in_multiset_eq pc pc1 n(list2multiset lp')); auto; intros.
elim H3; clear H3; intros; subst.
constructor; auto.
apply m_pc_not_in.
intros.
case (eq_word_dec m m'); intros; auto.
left.
elim (in_factorize _ _ _ H3).
intros m'' (lp'',(H5,(H6,H7))).
assert (lp''=lp').
apply in_m_distinct with m'' m (factorize l); auto.
apply factorize_distinct.
apply eq_word_sym; apply eq_word_trans with m'; auto.
subst.
elim (in_insere_in_multiset2 _ _ H7).
intros pc'' (n'',(H8,H9)).
red; intros.
elim (H4 _ _ H8).
apply eq_word_trans with pc'; auto.
elim H3; clear H3; intros pc' (n',(H4,(H5,H6))).
subst.
constructor; auto.
apply nb_m_pc_eq with m pc'; auto.
apply IHl with lp'; auto.
apply list2multiset_distinct.
elim H1; clear H1; intros.
constructor.
right; red; intros; elim H1; apply eq_word_sym; auto.
apply IHl with lp'; auto.
apply factorize_distinct.
Qed.
Index
This page has been generated by coqdoc