Library JordanCurveTheorem.Jordan2
Require Export Jordan1.
Inductive set:Set:=
Vs : set | Is : set → dart → set.
Fixpoint exds(s:set)(z:dart){struct s}:Prop:=
match s with
Vs ⇒ False
| Is s0 x ⇒ x=z ∨ exds s0 z
end.
Lemma exds_dec: ∀(s:set)(z:dart),
{exds s z}+{¬exds s z}.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intro.
generalize (eq_dart_dec d z).
generalize (IHs z).
tauto.
Qed.
Lemma not_exds_Vs: ∀ s:set,
(∀ z:dart, ¬exds s z) → s = Vs.
Proof.
intros.
induction s.
tauto.
generalize (H d).
simpl in |- ×.
tauto.
Qed.
Lemma not_exds_diff: ∀(s:set)(z:dart),
¬exds s z →
∀(t:dart), exds s t → z ≠ t.
Proof.
intros.
induction s.
simpl in H0.
tauto.
simpl in H0.
simpl in H.
elim H0.
intros.
rewrite <- H1.
intro.
symmetry in H2.
tauto.
apply IHs.
tauto.
Qed.
Fixpoint Ds(s:set)(z:dart){struct s}:set:=
match s with
Vs ⇒ Vs
| Is s0 x ⇒
if eq_dart_dec x z then (Ds s0 z)
else Is (Ds s0 z) x
end.
Lemma not_exds_Ds:∀(s:set)(z:dart),
¬exds (Ds s z) z.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d z).
intro.
apply (IHs z).
simpl in |- ×.
generalize (IHs z).
tauto.
Qed.
Lemma exds_Ds:∀(s:set)(x z:dart),
x ≠ z →
(exds s z ↔ exds (Ds s x) z).
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d x).
intro.
rewrite a.
generalize (IHs x z).
tauto.
intro.
simpl in |- ×.
generalize (IHs x z).
tauto.
Qed.
Lemma exds_Ds_diff:∀(s:set)(x z:dart),
exds (Ds s x) z → x ≠ z.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros x z.
elim (eq_dart_dec d x).
intro.
apply IHs.
simpl in |- ×.
intros.
elim H.
intro.
rewrite <- H0.
intro.
rewrite H1 in b.
tauto.
apply IHs.
Qed.
Lemma Ds_s:∀(s:set)(z:dart),
¬exds s z ↔ Ds s z = s.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d z).
intro.
rewrite a.
generalize (IHs z).
intros.
split.
tauto.
intro.
assert (exds (Is s z) z).
simpl in |- ×.
tauto.
rewrite <- H0 in H1.
absurd (exds (Ds s z) z).
apply not_exds_Ds.
tauto.
intro.
split.
intros.
generalize (IHs z).
intros.
assert (Ds s z = s).
tauto.
rewrite H1.
tauto.
intros.
injection H.
generalize (IHs z).
tauto.
Qed.
Lemma not_exds_Ds_bis:∀(s:set)(x z:dart),
¬exds s z → ¬exds (Ds s x) z.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d x).
intro.
apply IHs.
tauto.
simpl in |- ×.
intro.
generalize (IHs x z).
tauto.
Qed.
Lemma exds_Ds_exds:∀(s:set)(x z:dart),
exds (Ds s x) z → exds s z.
Proof.
intros.
generalize (exds_dec s z).
intro.
generalize (exds_dec (Ds s x) z).
intro.
generalize (not_exds_Ds_bis s x z).
tauto.
Qed.
Fixpoint card(s:set):nat:=
match s with
Vs ⇒ 0%nat
| Is s0 x ⇒
if exds_dec s0 x then card s0
else (1 + card s0)%nat
end.
Lemma card_Ds:∀ (s:set)(z:dart),
(card (Ds s z) ≤ card s)%nat.
Proof.
induction s.
simpl in |- ×.
intro.
omega.
simpl in |- ×.
intro.
elim (eq_dart_dec d z).
intro.
elim (exds_dec s d).
intro.
apply IHs.
intro.
generalize (IHs z).
intro.
omega.
simpl in |- ×.
elim (exds_dec s d).
elim (exds_dec (Ds s z) d).
intros.
apply IHs.
intros.
generalize (exds_Ds s z d).
assert (z ≠ d).
intro.
rewrite H in b0.
tauto.
tauto.
elim (exds_dec (Ds s z) d).
intros.
generalize (IHs z).
intro.
omega.
intros.
generalize (IHs z).
intro.
omega.
Qed.
Lemma not_exds_card_Ds:∀ (s:set)(z:dart),
¬exds s z → card (Ds s z) = card s.
Proof.
intros.
generalize (Ds_s s z).
intros.
assert (Ds s z = s).
tauto.
rewrite H1.
tauto.
Qed.
Lemma exds_card_pos:∀ (s:set)(z:dart),
exds s z → (0 < card s)%nat.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s d).
intro.
apply (IHs d a); tauto.
intro.
omega.
Qed.
Lemma exds_card_Ds:∀ (s:set)(z:dart),
exds s z → card (Ds s z) = (card s - 1)%nat.
Proof.
induction s.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (eq_dart_dec d z).
intro.
elim (exds_dec s d).
intro.
rewrite a in a0.
apply IHs.
tauto.
intro.
rewrite a in b.
rewrite not_exds_card_Ds.
omega.
tauto.
simpl in |- ×.
elim (exds_dec (Ds s z) d).
elim (exds_dec s d).
intros.
rewrite IHs.
tauto.
tauto.
intros.
generalize (exds_Ds s z d).
assert (z ≠ d).
intro.
rewrite H0 in b0.
tauto.
tauto.
elim (exds_dec s d).
intros.
generalize (exds_Ds s z d).
assert (z ≠ d).
intro.
rewrite H0 in b0.
tauto.
tauto.
intros.
rewrite IHs.
assert (0 < card s)%nat.
apply exds_card_pos with z.
tauto.
omega.
tauto.
Qed.
Lemma exds_card_Ds_inf:∀ (s:set)(z:dart),
exds s z → (card (Ds s z) < card s)%nat.
Proof.
intros.
generalize (exds_card_pos s z H).
generalize (exds_card_Ds s z H).
intros.
omega.
Qed.
Fixpoint fmap_to_set(m:fmap):set:=
match m with
V ⇒ Vs
| I m0 x _ _ ⇒ Is (fmap_to_set m0) x
| L m0 _ _ _ ⇒ (fmap_to_set m0)
end.
Lemma exd_exds:∀(m:fmap)(z:dart),
exd m z ↔ exds (fmap_to_set m) z.
Proof.
induction m.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
generalize (IHm z); tauto.
simpl in |- ×.
tauto.
Qed.
Fixpoint ndN (m:fmap):nat:=
match m with
V ⇒ 0%nat
| I m0 x _ _ ⇒
if exd_dec m0 x then ndN m0
else (1 + ndN m0)%nat
| L m0 _ _ _ ⇒ ndN m0
end.
Lemma nd_card:∀(m:fmap),
ndN m = card (fmap_to_set m).
Proof.
induction m.
simpl in |- ×.
tauto.
simpl in |- ×.
elim (exd_dec m d).
elim (exds_dec (fmap_to_set m) d).
tauto.
intros.
generalize (exd_exds m d).
tauto.
elim (exds_dec (fmap_to_set m) d).
intros.
generalize (exd_exds m d).
tauto.
rewrite IHm.
tauto.
simpl in |- ×.
tauto.
Qed.
Fixpoint set_minus(s1 s2:set){struct s1}:set:=
match s1 with
Vs ⇒ Vs
| Is s0 x ⇒
if exds_dec s2 x then set_minus s0 s2
else Is (set_minus s0 s2) x
end.
Lemma not_exds_minus: ∀(s1 s2:set)(z:dart),
¬ exds s1 z →
¬ exds (set_minus s1 s2) z.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s2 d).
intro.
apply IHs1.
tauto.
simpl in |- ×.
intro.
generalize (IHs1 s2 z).
tauto.
Qed.
Lemma exds_set_minus: ∀(s1 s2:set)(z:dart),
exds s1 z → ¬exds s2 z →
exds (set_minus s1 s2) z.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s2 d).
intro.
elim H.
intro.
rewrite H1 in a.
tauto.
intro.
apply IHs1.
tauto.
tauto.
simpl in |- ×.
intro.
elim H.
tauto.
generalize (IHs1 s2 z).
tauto.
Qed.
Lemma not_exds_set_minus: ∀(s1 s2:set)(z:dart),
exds s2 z → ¬exds (set_minus s1 s2) z.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec s2 d).
intro.
apply IHs1.
tauto.
simpl in |- ×.
intro.
generalize (IHs1 s2 z).
intro.
assert (d ≠ z).
intro.
rewrite H1 in b.
tauto.
tauto.
Qed.
Lemma exds_set_minus_eq:∀(s1 s2:set)(z:dart),
(exds s1 z ∧ ¬exds s2 z) ↔ exds (set_minus s1 s2) z.
Proof.
intros.
generalize (not_exds_set_minus s1 s2 z).
generalize (exds_set_minus s1 s2 z).
generalize (exds_dec s2 z).
generalize (exds_dec (set_minus s1 s2) z).
generalize (exds_dec s1 z).
generalize (not_exds_minus s1 s2 z).
tauto.
Qed.
Inductive incls(s1 s2:set):Prop:=
exds2 : (∀ z:dart, exds s1 z → exds s2 z)
→ incls s1 s2.
Lemma set_minus_s_Ds :∀(s1 s2:set)(x:dart),
¬ exds s1 x → exds s2 x →
set_minus s1 (Ds s2 x) = set_minus s1 s2.
Proof.
induction s1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exds_dec (Ds s2 x) d).
elim (exds_dec s2 d).
intros.
apply IHs1.
tauto.
tauto.
intros.
generalize (exds_Ds s2 x d).
intros.
assert (x ≠ d).
intro.
rewrite H2 in H.
tauto.
tauto.
elim (exds_dec s2 d).
intros.
generalize (exds_Ds s2 x d).
intros.
assert (x ≠ d).
intro.
rewrite H2 in H.
tauto.
tauto.
intros.
rewrite IHs1.
tauto.
tauto.
tauto.
Qed.
Lemma card_minus_set:∀(s1 s2:set),
incls s2 s1 →
(card (set_minus s1 s2) + card s2 = card s1)%nat.
Proof.
induction s1.
simpl in |- ×.
intros.
inversion H.
simpl in H0.
generalize (not_exds_Vs s2 H0).
intro.
rewrite H1.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
inversion H.
simpl in H0.
elim (exds_dec s2 d).
elim (exds_dec s1).
intros.
apply IHs1.
constructor.
intros.
elim (H0 z H1).
intro.
rewrite <- H2.
tauto.
tauto.
intros.
generalize (IHs1 (Ds s2 d)).
intros.
inversion H.
assert (incls (Ds s2 d) s1).
constructor.
intros.
assert (d ≠ z).
intro.
rewrite H4 in H3.
apply (not_exds_Ds s2 z H3).
generalize (exds_Ds s2 d z H4).
intro.
assert (exds s2 z).
tauto.
assert (exds (Is s1 d) z).
apply H2.
tauto.
simpl in H7.
tauto.
generalize (set_minus_s_Ds s1 s2 d b a).
intro.
rewrite H4 in H1.
generalize (exds_card_Ds s2 d a).
intro.
rewrite H5 in H1.
rewrite <- H1.
generalize (exds_card_pos s2 d a).
intro.
omega.
tauto.
intro.
simpl in |- ×.
elim (exds_dec (set_minus s1 s2) d).
elim (exds_dec s1 d).
intros.
apply IHs1.
constructor.
intros.
elim (H0 z H1).
intro.
rewrite H2 in b.
tauto.
tauto.
intros.
generalize (exds_set_minus_eq s1 s2 d).
tauto.
elim (exds_dec s1 d).
intros.
elim b0.
apply (exds_set_minus s1 s2 d a b).
intros.
rewrite <- IHs1 with s2.
omega.
constructor.
intros.
elim (H0 z).
intro.
rewrite H2 in b.
tauto.
tauto.
tauto.
Qed.
Definition impls(s1 s2:set):Prop:=
∀ z:dart, exds s1 z → exds s2 z.
Definition eqs(s1 s2:set):Prop:=
∀ z:dart, exds s1 z ↔ exds s2 z.
Definition disjs(s1 s2:set):Prop:=
∀ z:dart, exds s1 z → exds s2 z → False.
Definition Rs(sy sx:set):=
(card sy < card sx)%nat.
Lemma Acc_set:∀ s:set, Acc Rs s.
Proof.
induction s.
apply Acc_intro.
unfold Rs at 1 in |- ×.
simpl in |- ×.
intros.
inversion H.
apply Acc_intro.
intro y.
unfold Rs at 1 in |- ×.
simpl in |- ×.
inversion IHs.
intro.
elim (eq_nat_dec (card y) (card s)).
intro.
apply Acc_intro.
intro y0.
unfold Rs at 1 in |- ×.
rewrite a.
intro.
apply H.
unfold Rs in |- ×.
tauto.
intro.
apply Acc_intro.
unfold Rs at 1 in |- ×.
intros.
generalize H0.
clear H0.
elim (exds_dec s d).
intros.
apply H.
unfold Rs in |- ×.
omega.
intros.
apply H.
unfold Rs in |- ×.
omega.
Qed.
Lemma Rs_wf : well_founded Rs.
Proof.
unfold well_founded in |- ×.
apply Acc_set.
Qed.
Lemma exds_Rs_Ds:
∀(s:set)(z:dart),
exds s z → Rs (Ds s z) s.
Proof.
unfold Rs in |- ×.
simpl in |- ×.
intros.
apply exds_card_Ds_inf.
tauto.
Qed.
Fixpoint Iter(g:dart→dart)(n:nat)(z:dart){struct n}:dart:=
match n with
0%nat ⇒ z
| S n0 ⇒ g (Iter g n0 z)
end.
Module Type Sigf.
Parameter f : fmap → dart → dart.
Parameter f_1 : fmap → dart → dart.
Axiom exd_f:∀ (m:fmap)(z:dart),
inv_hmap m → (exd m z ↔ exd m (f m z)).
Axiom bij_f : ∀ m:fmap,
inv_hmap m → bij_dart (exd m) (f m).
Axiom exd_f_1:∀ (m:fmap)(z:dart),
inv_hmap m → (exd m z ↔ exd m (f_1 m z)).
Axiom bij_f_1 : ∀ m:fmap,
inv_hmap m → bij_dart (exd m) (f_1 m).
Axiom f_1_f : ∀ (m:fmap)(z:dart),
inv_hmap m → exd m z → f_1 m (f m z) = z.
Axiom f_f_1 : ∀ (m:fmap )(z:dart),
inv_hmap m → exd m z → f m (f_1 m z) = z.
End Sigf.
Module Mf(M:Sigf)<:Sigf
with Definition f:=M.f
with Definition f_1:=M.f_1.
Definition f:=M.f.
Definition f_1:=M.f_1.
Definition exd_f:=M.exd_f.
Definition exd_f_1:=M.exd_f_1.
Definition bij_f:=M.bij_f.
Definition bij_f_1:=M.bij_f_1.
Definition f_1_f:=M.f_1_f.
Definition f_f_1:=M.f_f_1.
Lemma exd_Iter_f:∀(m:fmap)(n:nat)(z:dart),
inv_hmap m → (exd m z ↔ exd m (Iter (f m) n z)).
Proof.
induction n.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
generalize (exd_f m (Iter (f m) n z)).
generalize (IHn z).
generalize (IHn (Iter (f m) n z)).
tauto.
Qed.
Lemma exd_Iter_f_1:∀(m:fmap)(n:nat)(z:dart),
inv_hmap m → (exd m z ↔ exd m (Iter (f_1 m) n z)).
Proof.
induction n.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
generalize (exd_f_1 m (Iter (f_1 m) n z)).
generalize (IHn z).
generalize (IHn (Iter (f_1 m) n z)).
tauto.
Qed.
Theorem Iter_rem_F :
∀ (m:fmap)(z:dart),
∀ sx: set, (∀ sy: set, Rs sy sx → set)
→ set.
Proof.
intros m z.
refine
(fun sx F ⇒
let n:= ((ndN m)-(card sx))%nat in
let zn := Iter (f m) n z in
match exds_dec sx zn with
left _ ⇒ F (Ds sx zn) _
| right _ ⇒ sx
end).
apply exds_Rs_Ds.
tauto.
Defined.
Definition Iter_rem_aux(m:fmap)(z:dart):
set → set
:= Fix Rs_wf (fun _:set ⇒ set) (Iter_rem_F m z).
Definition Iter_upb_aux(m:fmap)(z:dart)(s:set):nat:=
((ndN m) - (card (Iter_rem_aux m z s)))%nat.
Definition Iter_rem(m:fmap)(z:dart):set:=
Iter_rem_aux m z (fmap_to_set m).
Definition Iter_upb(m:fmap)(z:dart):nat:=
((ndN m) - (card (Iter_rem m z)))%nat.
Definition Iter_orb_aux(m:fmap)(z:dart)(s:set):set:=
set_minus (fmap_to_set m) (Iter_rem_aux m z s).
Definition Iter_orb(m:fmap)(z:dart):set:=
set_minus (fmap_to_set m) (Iter_rem m z).
Theorem Iter_rem_aux_equation :
∀(m:fmap)(z:dart)(sx:set),
Iter_rem_aux m z sx =
let n := ((ndN m) - (card sx))%nat in
let zn := Iter (f m) n z in
if exds_dec sx zn
then Iter_rem_aux m z (Ds sx zn)
else sx.
Proof.
intros m z sx.
unfold Iter_rem_aux in |- ×.
rewrite Fix_eq.
auto.
intros x0 f0 g0 Heqfg.
unfold Iter_rem_F in |- ×.
destruct (exds_dec x0 (Iter (f m)
((ndN m - card x0))%nat z)).
rewrite Heqfg.
trivial.
trivial.
Qed.
Definition P1
(m:fmap)(z:dart)(s:set):Prop:=
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
¬ exds sr (Iter (f m) n z).
Lemma not_exds_rem_upb :
∀(m:fmap)(z:dart)(s:set),
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
¬ exds sr (Iter (f m) n z).
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P1 m z) _).
unfold P1 in |- ×.
unfold Iter_upb_aux in |- ×.
simpl in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
simpl in |- ×.
apply exds_card_Ds_inf.
tauto.
tauto.
Qed.
Lemma not_exds_Iter_rem_upb :
∀(m:fmap)(z:dart),
let n:= Iter_upb m z in
¬ exds (Iter_rem m z) (Iter (f m) n z).
Proof.
unfold Iter_rem in |- ×.
unfold Iter_upb in |- ×.
intros m z.
unfold Iter_rem in |- ×.
generalize (not_exds_rem_upb m z (fmap_to_set m)).
simpl in |- ×.
unfold Iter_upb_aux in |- ×.
tauto.
Qed.
Lemma exd_Iter_upb:
∀(m:fmap)(z:dart), inv_hmap m →
exd m z → exd m (Iter (f m) (Iter_upb m z) z).
Proof.
intros.
generalize (exd_Iter_f m (Iter_upb m z) z).
tauto.
Qed.
Lemma exd_Iter_orb_upb :
∀(m:fmap)(z:dart),
inv_hmap m → exd m z →
let n:= Iter_upb m z in
exds (Iter_orb m z) (Iter (f m) n z).
Proof.
unfold Iter_orb in |- ×.
intros.
apply exds_set_minus.
generalize (exd_exds m (Iter (f m) (Iter_upb m z) z)).
intro.
generalize (exd_Iter_upb m z H H0).
tauto.
apply not_exds_Iter_rem_upb.
Qed.
Lemma exds_rem_orb:∀(m:fmap)(z t:dart),
inv_hmap m → exd m t →
(¬exds (Iter_rem m z) t ↔ exds (Iter_orb m z) t).
Proof.
intros.
unfold Iter_orb in |- ×.
generalize (exds_set_minus_eq (fmap_to_set m) (Iter_rem m z) t).
generalize (exd_exds m t).
tauto.
Qed.
Definition R3
(m:fmap)(z t:dart)(s:set):Prop:=
¬ exds s t →
let sr := Iter_rem_aux m z s in
¬ exds sr t.
Lemma LR3:∀(m:fmap)(z t:dart)(s:set),
¬ exds s t →
let sr := Iter_rem_aux m z s in
¬ exds sr t.
Proof.
intros m z t.
refine (well_founded_ind Rs_wf (R3 m z t) _).
unfold R3 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
apply not_exds_Ds_bis.
tauto.
tauto.
Qed.
Definition R2
(m:fmap)(z:dart)(s:set):Prop:=
let sr := Iter_rem_aux m z s in
¬ exds sr (Iter (f m) (ndN m - card s)%nat z).
Lemma LR2 :
∀(m:fmap)(z:dart)(s:set),
let sr := Iter_rem_aux m z s in
¬ exds sr (Iter (f m) (ndN m - card s)%nat z).
Proof.
intros m z.
simpl in |- ×.
refine (well_founded_ind Rs_wf (R2 m z) _).
unfold R2 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply LR3.
apply not_exds_Ds.
tauto.
Qed.
Definition R1
(m:fmap)(z:dart)(i:nat)(s:set):Prop:=
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
(ndN m - card s ≤ i ≤ n)%nat →
¬ exds sr (Iter (f m) i z).
Lemma LR1 :
∀(m:fmap)(z:dart)(i:nat)(s:set),
let sr := Iter_rem_aux m z s in
let n := Iter_upb_aux m z s in
(ndN m - card s ≤ i ≤ n)%nat →
¬ exds sr (Iter (f m) i z).
Proof.
intros m z i.
refine (well_founded_ind Rs_wf (R1 m z i) _).
unfold R1 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
elim (eq_nat_dec i (ndN m - card x)%nat).
intro.
rewrite a.
apply LR2.
intro.
generalize H0.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intros.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
split.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x)%nat z) a).
intro.
rewrite H2.
elim H0.
intros.
clear H a H1 H2 H0 H4.
omega.
tauto.
intros.
clear H H0 b0.
omega.
Qed.
Lemma not_exds_Iter_f_i :
∀(m:fmap)(z:dart)(i:nat),
let sr := Iter_rem m z in
let n := Iter_upb m z in
(i ≤ n)%nat → ¬ exds sr (Iter (f m) i z).
Proof.
simpl in |- ×.
unfold Iter_upb in |- ×.
unfold Iter_rem in |- ×.
intros.
apply LR1.
generalize (nd_card m).
intro.
rewrite H0.
simpl in |- ×.
unfold Iter_upb in |- ×.
unfold Iter_upb_aux in |- ×.
omega.
Qed.
Lemma exds_Iter_f_i :
∀(m:fmap)(z:dart)(i:nat),
inv_hmap m → exd m z →
let s := Iter_orb m z in
let n := Iter_upb m z in
(i ≤ n)%nat → exds s (Iter (f m) i z).
Proof.
intros.
assert (exd m (Iter (f m) i z)).
generalize (exd_Iter_f m i z H).
intro.
tauto.
generalize (exds_rem_orb m z (Iter (f m) i z) H H2).
unfold s in |- ×.
intros.
generalize (not_exds_Iter_f_i m z i).
simpl in |- ×.
tauto.
Qed.
Definition P2
(m:fmap)(z:dart)(s:set):Prop:=
(card s < ndN m →
card (Iter_rem_aux m z s) < ndN m)%nat.
Lemma card_rem_aux:∀(m:fmap)(z:dart)(s:set),
(card s < ndN m →
card (Iter_rem_aux m z s) < ndN m)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P2 m z) _).
unfold P2 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
omega.
tauto.
Qed.
Definition P2_bis
(m:fmap)(z:dart)(s:set):Prop:=
(card s ≤ ndN m →
card (Iter_rem_aux m z s) ≤ ndN m)%nat.
Lemma card_rem_aux_bis:∀(m:fmap)(z:dart)(s:set),
(card s ≤ ndN m →
card (Iter_rem_aux m z s) ≤ ndN m)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P2_bis m z) _).
unfold P2_bis in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
omega.
tauto.
Qed.
Lemma upb_pos_aux:∀(m:fmap)(z:dart),
exd m z →
(card (Iter_rem m z) < ndN m)%nat.
Proof.
intros.
unfold Iter_rem in |- ×.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec (fmap_to_set m) (Iter (f m) (ndN m - card (fmap_to_set m)) z)).
intro.
apply card_rem_aux.
assert
(card (Ds (fmap_to_set m)
(Iter (f m) (ndN m - card (fmap_to_set m)) z)) <
card (fmap_to_set m))%nat.
apply exds_card_Ds_inf.
tauto.
generalize (nd_card m).
intro.
omega.
intro.
generalize (nd_card m).
intro.
assert (ndN m - card (fmap_to_set m) = 0)%nat.
omega.
rewrite H1 in b.
simpl in b.
generalize (exd_exds m z).
intro.
generalize (exds_dec (fmap_to_set m) z).
tauto.
Qed.
Theorem upb_pos:∀(m:fmap)(z:dart),
exd m z → (0 < Iter_upb m z)%nat.
Proof.
unfold Iter_upb in |- ×.
intros.
generalize (upb_pos_aux m z).
intros.
generalize (H0 H).
intro.
omega.
Qed.
Definition Q1(m:fmap)(z:dart)(s:set):Prop:=
(card (Iter_rem_aux m z s) ≤ card s)%nat.
Lemma LQ1:∀(m:fmap)(z:dart)(s:set),
(card (Iter_rem_aux m z s) ≤ card s)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (Q1 m z) _).
unfold Q1 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
assert (card (Ds x (Iter (f m)
(ndN m - card x) z)) < card x)%nat.
apply exds_card_Ds_inf.
tauto.
assert
(card (Iter_rem_aux m z
(Ds x (Iter (f m) (ndN m - card x) z))) ≤
card (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
apply H.
unfold Rs in |- ×.
tauto.
omega.
intro.
omega.
Qed.
Definition Q2(m:fmap)(z:dart)(s:set):Prop:=
exds s (Iter (f m) (ndN m - card s)%nat z) →
(card (Iter_rem_aux m z s) < card s)%nat.
Lemma LQ2:∀(m:fmap)(z:dart)(s:set),
exds s (Iter (f m) (ndN m - card s) z) →
(card (Iter_rem_aux m z s) < card s)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (Q2 m z) _).
unfold Q2 in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intro.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
assert
(card (Iter_rem_aux m z (Ds x (Iter (f m)
(ndN m - card x) z))) ≤
card (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
apply LQ1.
omega.
tauto.
Qed.
Definition PL2(m:fmap)(z t:dart)(x:set):Prop:=
inv_hmap m → exd m z → exds x t →
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t →
exds x zn0 →
¬ exds (Iter_rem_aux m z (Ds x zn0)) t.
Lemma L2:∀(m:fmap)(z t:dart)(x:set),
inv_hmap m → exd m z → exds x t →
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t →
exds x zn0 →
¬ exds (Iter_rem_aux m z (Ds x zn0)) t.
Proof.
intros m z t.
refine (well_founded_ind Rs_wf (PL2 m z t) _).
unfold PL2 in |- ×.
intros.
generalize H3.
clear H3.
rewrite (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
tauto.
tauto.
Qed.
Definition PL3(m:fmap)(z t:dart)(x:set):Prop:=
inv_hmap m → exd m z → exds x t →
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t →
exds x zn0.
Lemma L3:∀(m:fmap)(z t:dart)(x:set),
inv_hmap m → exd m z → exds x t →
let sr:= Iter_rem_aux m z x in
let zn0 := (Iter (f m) (ndN m - card x)%nat z) in
¬exds sr t →
exds x zn0.
Proof.
intros m z t.
refine (well_founded_ind Rs_wf (PL3 m z t) _).
unfold PL3 in |- ×.
intros.
generalize H3.
clear H3.
rewrite (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
tauto.
tauto.
Qed.
Definition P4(m:fmap)(z t:dart)(s:set):Set:=
inv_hmap m → exd m z → exds s t →
(card s ≤ ndN m)%nat →
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
¬ exds sr t →
{i:nat | (i < nr)%nat ∧ Iter (f m) i z = t}.
Lemma ex_i_aux :∀(m:fmap)(z t:dart)(s:set),
inv_hmap m → exd m z → exds s t →
(card s ≤ ndN m)%nat →
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
¬ exds sr t →
{i:nat | (i < nr)%nat ∧ Iter (f m) i z = t}.
Proof.
intros m z t.
refine (well_founded_induction Rs_wf (P4 m z t) _).
unfold P4 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
rewrite Iter_rem_aux_equation.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x)%nat z)).
intro.
elim (eq_dart_dec (Iter (f m) (ndN m - card x)%nat z) t).
intro.
split with (ndN m - card x)%nat.
split.
assert
(card (Iter_rem_aux m z (Ds x (Iter (f m)
(ndN m - card x) z))) ≤
card (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
apply LQ1.
generalize (exds_card_Ds_inf x
(Iter (f m) (ndN m - card x)%nat z)).
intros.
generalize (H6 a).
intro.
omega.
tauto.
intro.
apply H.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
tauto.
tauto.
generalize (exds_Ds x (Iter (f m) (ndN m - card x)%nat z) t).
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
< card x)%nat.
apply exds_card_Ds_inf.
tauto.
omega.
apply L2.
tauto.
tauto.
tauto.
tauto.
tauto.
intro.
absurd (exds x (Iter (f m) (ndN m - card x)%nat z)).
tauto.
eapply L3.
tauto.
tauto.
apply H2.
tauto.
Qed.
Lemma ex_i :∀(m:fmap)(z t:dart),
inv_hmap m → exd m z → exd m t →
let sr:= Iter_rem m z in
let nr:= Iter_upb m z in
¬ exds sr t →
{i : nat | (i < nr)%nat ∧ Iter (f m) i z = t}.
Proof.
unfold Iter_rem in |- ×.
unfold Iter_upb in |- ×.
intros.
generalize ex_i_aux.
simpl in |- ×.
unfold Iter_rem in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
apply H3.
tauto.
tauto.
generalize (exd_exds m t).
tauto.
rewrite nd_card.
omega.
tauto.
Qed.
Lemma ex_i_upb :∀(m:fmap)(z:dart),
inv_hmap m → exd m z →
let nr:= Iter_upb m z in
{i : nat | (i < nr)%nat ∧ Iter (f m) i z = Iter (f m) nr z}.
Proof.
intros.
unfold nr in |- ×.
apply ex_i.
tauto.
tauto.
generalize (exd_Iter_f m (Iter_upb m z) z).
tauto.
generalize not_exds_rem_upb.
simpl in |- ×.
intros.
unfold Iter_rem in |- *; unfold Iter_upb in |- ×.
unfold Iter_rem in |- ×.
unfold Iter_upb_aux in H1.
apply H1.
Qed.
Lemma Iter_plus:∀(m:fmap)(z:dart)(p i:nat),
inv_hmap m → exd m z →
Iter (f m) (p + i)%nat z = Iter (f m) i z →
Iter (f m) p z = z.
Proof.
induction i.
simpl in |- ×.
assert (p + 0 = p)%nat.
omega.
rewrite H.
tauto.
simpl in |- ×.
assert (p + S i = S (p + i))%nat.
omega.
rewrite H.
simpl in |- ×.
clear H.
intros.
assert
(f_1 m (f m (Iter (f m) (p + i)%nat z)) =
f_1 m (f m (Iter (f m) i z))).
rewrite H1.
tauto.
rewrite f_1_f in H2.
rewrite f_1_f in H2.
apply IHi.
tauto.
tauto.
tauto.
tauto.
generalize (exd_Iter_f m i z).
tauto.
tauto.
generalize (exd_Iter_f m (p + i) z).
tauto.
Qed.
Lemma Iter_plus_inv:∀(m:fmap)(z:dart)(p i:nat),
inv_hmap m → exd m z →
Iter (f m) p z = z →
Iter (f m) (p + i)%nat z = Iter (f m) i z.
Proof.
induction i.
simpl in |- ×.
assert (p + 0 = p)%nat.
omega.
rewrite H.
tauto.
simpl in |- ×.
assert (p + S i = S (p + i))%nat.
omega.
rewrite H.
simpl in |- ×.
clear H.
intros.
rewrite IHi.
tauto.
tauto.
tauto.
tauto.
Qed.
Lemma Iter_mult:∀(m:fmap)(z:dart)(n p:nat),
inv_hmap m → exd m z →
Iter (f m) p z = z → Iter (f m) (n×p)%nat z = z.
Proof.
induction n.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
rewrite Iter_plus_inv.
apply (IHn p H H0 H1).
tauto.
tauto.
tauto.
Qed.
Lemma Iter_plus_mult:∀(m:fmap)(z:dart)(n p i:nat),
inv_hmap m → exd m z →
Iter (f m) p z = z →
Iter (f m) (i + n×p)%nat z = Iter (f m) i z.
Proof.
intros.
induction n.
simpl in |- ×.
assert (i + 0 = i)%nat.
omega.
rewrite H2.
tauto.
simpl in |- ×.
assert (i + (p + n × p) = p + (i + n × p))%nat.
omega.
rewrite H2.
rewrite Iter_plus_inv.
tauto.
tauto.
tauto.
tauto.
Qed.
Lemma Iter_comp:∀(m:fmap)(i j:nat)(z:dart),
Iter (f m) (i+j)%nat z = Iter (f m) i (Iter (f m) j z).
Proof.
induction i.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
rewrite IHi.
tauto.
Qed.
Lemma f_1_Iter_f:∀(m:fmap)(i:nat)(z:dart),
inv_hmap m → exd m z →
(f_1 m) (Iter (f m) (S i) z) = Iter (f m) i z.
Proof.
induction i.
simpl in |- ×.
intros.
apply f_1_f.
trivial.
trivial.
simpl in |- ×.
intros.
rewrite f_1_f.
tauto.
tauto.
assert (f m (Iter (f m) i z) = Iter (f m) (S i) z).
simpl in |- ×.
tauto.
rewrite H1.
generalize (exd_Iter_f m (S i) z).
tauto.
Qed.
Lemma Iter_f_f_1 :∀(m:fmap)(i j:nat)(z:dart),
inv_hmap m → exd m z → (j ≤ i)%nat →
Iter (f_1 m) j (Iter (f m) i z) =
Iter (f m) (i - j)%nat z.
Proof.
induction i.
intros.
assert (j = 0)%nat.
omega.
rewrite H2.
simpl in |- ×.
trivial.
induction j.
simpl in |- ×.
tauto.
intros.
simpl in |- ×.
assert (f m (Iter (f m) i z) = Iter (f m) (S i) z).
simpl in |- ×.
tauto.
rewrite H2.
rewrite IHj.
assert (S i - j = S (i - j))%nat.
omega.
rewrite H3.
apply f_1_Iter_f.
trivial.
trivial.
trivial.
trivial.
omega.
Qed.
Lemma Iter_f_f_1_i:∀(m:fmap)(i:nat)(z:dart),
inv_hmap m → exd m z →
Iter (f_1 m) i (Iter (f m) i z) = z.
Proof.
intros.
rewrite Iter_f_f_1.
assert (i - i = 0)%nat.
omega.
rewrite H1.
simpl in |- ×.
trivial.
trivial.
trivial.
omega.
Qed.
Lemma Iter_f_Si:∀(m:fmap)(i:nat)(z:dart),
inv_hmap m → exd m z →
Iter (f m) (S i) z = Iter (f m) i (f m z).
Proof.
simpl in |- ×.
intros.
induction i.
simpl in |- ×.
tauto.
simpl in |- ×.
rewrite IHi in |- ×.
tauto.
Qed.
Lemma Iter_f_1_Si:∀(m:fmap)(i:nat)(z:dart),
inv_hmap m → exd m z →
Iter (f_1 m) (S i) z = Iter (f_1 m) i (f_1 m z).
Proof.
simpl in |- ×.
intros.
induction i.
simpl in |- ×.
tauto.
simpl in |- ×.
rewrite IHi in |- ×.
tauto.
Qed.
Definition diff_int_aux
(m:fmap)(z:dart)(a b:nat)(t:dart): Prop:=
∀ i : nat, (a ≤ i ≤ b)%nat →
Iter (f m) i z ≠ t.
Lemma diff_int_aux_dec:∀(m:fmap)(z:dart)(a b:nat)(t:dart),
{diff_int_aux m z a b t} + {¬diff_int_aux m z a b t}.
Proof.
intros.
elim (le_gt_dec b a).
intro.
elim (eq_nat_dec a b).
intro.
rewrite <- a1.
elim (eq_dart_dec (Iter (f m) a z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a2.
apply H.
omega.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
assert (i = a).
omega.
rewrite H0.
tauto.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
omega.
induction b.
intro.
absurd (0 > a)%nat.
omega.
tauto.
intro.
elim (eq_nat_dec a b).
intro.
rewrite a0.
elim (eq_dart_dec (Iter (f m) b z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a1.
apply H.
omega.
intro.
elim (eq_dart_dec (Iter (f m) (S b) z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a1.
apply H.
omega.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
assert (i = b ∨ i = S b).
omega.
elim H0.
intro.
rewrite H1.
tauto.
intro.
rewrite H1.
tauto.
intro.
assert (b > a)%nat.
omega.
elim (IHb H).
intro.
elim (eq_dart_dec (Iter (f m) (S b) z) t).
intro.
right.
unfold diff_int_aux in |- ×.
intro.
generalize a1.
apply H0.
omega.
intro.
left.
unfold diff_int_aux in |- ×.
intros.
unfold diff_int_aux in a0.
elim (eq_nat_dec i (S b)).
intro.
rewrite a1.
tauto.
intro.
assert (a ≤ i ≤ b)%nat.
omega.
apply (a0 i H1).
intro.
right.
unfold diff_int_aux in |- ×.
unfold diff_int_aux in b2.
intro.
apply b2.
intros.
apply H0.
omega.
Qed.
Definition diff_int
(m:fmap)(z:dart)(a b:nat): Prop:=
∀ i j : nat, (a ≤ i ∧ i < j ∧ j ≤ b)%nat →
Iter (f m) i z ≠ Iter (f m) j z.
Lemma diff_int_le:∀(m:fmap)(z:dart)(a b:nat),
(b ≤ a)%nat → diff_int m z a b.
Proof.
intros.
unfold diff_int in |- ×.
intros.
omega.
Qed.
Lemma diff_int_dec:∀(m:fmap)(z:dart)(a b:nat),
{diff_int m z a b} + {¬diff_int m z a b}.
Proof.
intros.
induction b.
left.
unfold diff_int in |- ×.
intros.
omega.
elim IHb.
intro.
generalize (diff_int_aux_dec m z a b (Iter (f m) (S b) z)).
intros.
elim H.
intro.
clear IHb H.
left.
unfold diff_int in |- ×.
intros.
unfold diff_int in a0.
unfold diff_int_aux in a1.
elim (eq_nat_dec j (S b)).
intro.
rewrite a2.
apply a1.
omega.
intro.
apply a0.
omega.
intro.
clear IHb H.
unfold diff_int_aux in b0.
right.
unfold diff_int in |- ×.
intro.
apply b0.
intros.
apply H.
omega.
intro.
unfold diff_int in b0.
right.
unfold diff_int in |- ×.
intro.
apply b0.
intros.
apply H.
omega.
Qed.
Definition exds_int(m:fmap)(z:dart)(a b:nat)(s:set):Prop:=
∀ i:nat, (a ≤ i ≤ b)%nat →
exds s (Iter (f m) i z).
Lemma exds_int_gt:∀(m:fmap)(z:dart)(a b:nat)(s:set),
(b < a)%nat → exds_int m z a b s.
Proof.
intros.
unfold exds_int in |- ×.
intros.
absurd (b < a)%nat.
omega.
tauto.
Qed.
Lemma exds_int_dec : ∀(m:fmap)(z:dart)(a b:nat)(s:set),
{exds_int m z a b s} + {¬exds_int m z a b s}.
Proof.
intros.
elim (le_gt_dec a b).
intro.
induction b.
elim (exds_dec s z).
intro.
left.
unfold exds_int in |- ×.
intros.
assert (i = 0)%nat.
omega.
rewrite H0.
simpl in |- ×.
tauto.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b.
assert (exds s (Iter (f m) 0%nat z)).
apply H.
omega.
simpl in H0.
tauto.
elim (eq_nat_dec a (S b)).
intro.
rewrite <- a1.
elim (exds_dec s (Iter (f m) a z)).
intro.
left.
unfold exds_int in |- ×.
intros.
assert (i = a).
omega.
rewrite H0.
tauto.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b0.
apply H.
omega.
intro.
assert (a ≤ b)%nat.
omega.
elim (IHb H).
intro.
elim (exds_dec s (Iter (f m) (S b) z)).
intro.
left.
unfold exds_int in |- ×.
intros.
elim (eq_nat_dec i (S b)).
intro.
rewrite a3.
tauto.
intro.
unfold exds_int in a1.
apply a1.
omega.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b1.
apply H0.
omega.
intro.
right.
unfold exds_int in |- ×.
intro.
apply b1.
unfold exds_int in |- ×.
intros.
apply H0.
omega.
intro.
left.
apply exds_int_gt.
omega.
Qed.
Lemma rem_1_step :∀(m:fmap)(z:dart)(s:set),
inv_hmap m →
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
(card sr + 1 ≤ card s ↔
exds s (Iter (f m) (ndN m - card s) z))%nat.
Proof.
simpl in |- ×.
intros.
generalize (Iter_rem_aux_equation m z s).
simpl in |- ×.
intro.
split.
intro.
generalize H0.
elim (exds_dec s (Iter (f m) (ndN m - card s) z)).
tauto.
intros.
rewrite H2 in H1.
absurd (card s + 1 ≤ card s)%nat.
omega.
tauto.
intro.
generalize (LQ2 m z s H1).
intro.
omega.
Qed.
Lemma rem_2_steps :∀(m:fmap)(z:dart)(s:set),
inv_hmap m →
let sr:= Iter_rem_aux m z s in
let nr:= Iter_upb_aux m z s in
(card sr + 2 ≤ card s →
exds (Ds s (Iter (f m) (ndN m - card s) z))
(Iter (f m) (ndN m + 1 - card s) z))%nat.
Proof.
intros.
generalize (rem_1_step m z
(Ds s (Iter (f m) (ndN m - card s)%nat z)) H).
simpl in |- ×.
generalize (rem_1_step m z s H).
simpl in |- ×.
intros.
assert (card (Iter_rem_aux m z s) + 1 ≤ card s)%nat.
unfold sr in H0. clear H1 H2.
omega.
assert (exds s (Iter (f m) (ndN m - card s)%nat z)).
tauto.
generalize (Iter_rem_aux_equation m z s).
simpl in |- ×.
elim (exds_dec s (Iter (f m) (ndN m - card s) z)).
intros.
assert (card (Ds s (Iter (f m) (ndN m - card s) z)) + 1
= card s)%nat.
rewrite exds_card_Ds.
clear H1 H2 H3 H4 a H5.
omega.
tauto.
assert (card (Ds s (Iter (f m) (ndN m - card s) z))
= card s - 1)%nat.
clear H1 H2 H3 H4 a H5.
omega.
unfold sr in H0.
rewrite H7 in H2.
rewrite <- H5 in H2.
assert (card (Iter_rem_aux m z s) + 1 ≤ card s - 1)%nat.
clear H1 H2 H3 H4 a H5 H6 H7.
omega.
assert (ndN m + 1 - card s = ndN m - (card s - 1))%nat.
clear H1 H2 H3 H4 a H5 H6 H7 H8.
omega.
rewrite <- H9 in H2.
tauto.
tauto.
Qed.
Definition P6(m:fmap)(z:dart)(s:set):Prop:=
inv_hmap m →
(card s ≤ ndN m →
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z) →
exds_int m z n0 (nr - 1) s)%nat.
Lemma LP6:∀(m:fmap)(z:dart)(s:set),
inv_hmap m →
(card s ≤ ndN m →
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z) →
exds_int m z n0 (nr - 1) s)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P6 m z) _).
unfold P6 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
generalize (LQ1 m z x).
intro.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
intro.
rewrite H4.
generalize H4.
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intros.
clear H4.
generalize
(exds_card_Ds x (Iter (f m) (ndN m - card x)%nat z) a).
intro.
generalize (H (Ds x (Iter (f m) (ndN m - card x)%nat z))).
intros.
generalize (rem_1_step m z x H0).
simpl in |- ×.
intros.
assert (card (Iter_rem_aux m z x) + 1 ≤ card x)%nat.
tauto.
clear H7.
elim (eq_nat_dec (card (Iter_rem_aux m z x) + 1)
(card x))%nat.
intro.
rewrite <- H5.
assert (ndN m - card (Iter_rem_aux m z x) - 1
= ndN m - card x)%nat.
clear H3 H4 H8.
omega.
rewrite H7.
unfold exds_int in |- ×.
intros.
assert (i = ndN m - card x)%nat.
clear H1 H3 H4 H8 a0 H7.
omega.
rewrite H10.
tauto.
intro.
assert (card (Iter_rem_aux m z x) + 2 ≤ card x)%nat.
clear H1 H3 H4.
omega.
generalize (rem_2_steps m z x H0 H7).
intro.
rewrite H4 in H6.
assert (ndN m - (card x - 1) = ndN m + 1 - card x)%nat.
clear H3 H4 H5 H8 b.
omega.
rewrite H10 in H6.
rewrite <- H5.
rewrite <- H5 in H6.
unfold exds_int in |- ×.
intros.
elim (eq_nat_dec (ndN m - card x) i)%nat.
intro.
rewrite <- a0.
tauto.
intro.
assert
(exds_int m z (ndN m + 1 - card x)
(ndN m - card (Iter_rem_aux m z x) - 1)
(Ds x (Iter (f m) (ndN m - card x) z)))%nat.
apply H6.
unfold Rs in |- ×.
clear H1 H3 H5 H8 b H10 H11 b0.
omega.
tauto.
clear H3 H5 H4 H8 H7 H10 H11 b0.
omega.
tauto.
unfold exds_int in H12.
assert (exds (Ds x (Iter (f m)
(ndN m - card x) z)) (Iter (f m) i z))%nat.
apply H12.
clear H10.
clear H1 H3 H5 H4 H8 H7 H8 b.
omega.
eapply exds_Ds_exds.
apply H13.
tauto.
Qed.
Definition P7(m:fmap)(z:dart)(s:set):Prop:=
inv_hmap m →
(card s ≤ ndN m →
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z) →
∀ j:nat, n0 < j ≤ nr - 1 →
Iter (f m) n0 z ≠ Iter (f m) j z)%nat.
Lemma LP7:∀(m:fmap)(z:dart)(s:set),
inv_hmap m →
(card s ≤ ndN m →
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z) →
∀ j:nat, n0 < j ≤ nr - 1 →
Iter (f m) n0 z ≠ Iter (f m) j z)%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P7 m z) _).
unfold P7 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
generalize (LQ1 m z x).
generalize (rem_1_step m z x H0).
simpl in |- ×.
intro.
assert (card (Iter_rem_aux m z x) + 1 ≤ card x)%nat.
tauto.
clear H4.
intro.
clear H4.
elim (eq_nat_dec (card (Iter_rem_aux m z x) + 1)
(card x))%nat.
intro.
clear H5.
omega.
intro.
assert (card (Iter_rem_aux m z x) + 2 ≤ card x)%nat.
omega.
generalize (rem_2_steps m z x H0 H4).
intro.
clear b H5.
elim
(eq_dart_dec (Iter (f m) (ndN m - card x) z)
(Iter (f m)
(ndN m - card (Iter_rem_aux m z x) - 1) z))%nat.
intros.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
= card x - 1)%nat.
rewrite exds_card_Ds.
tauto.
tauto.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
≤ ndN m)%nat.
omega.
generalize (LP6 m z
(Ds x (Iter (f m) (ndN m - card x) z)) H0 H7)%nat.
simpl in |- ×.
intros.
rewrite H5 in H8.
unfold Iter_upb_aux in H8.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z)).
intros.
clear a0.
rewrite <- H9 in H8.
assert (ndN m - (card x - 1) =
ndN m + 1 - card x)%nat.
clear H3 a H5 H7 H9.
omega.
rewrite H10 in H8.
generalize (H8 H6).
intro.
clear H8.
unfold exds_int in H11.
assert
(exds (Ds x (Iter (f m) (ndN m - card x) z))
(Iter (f m)
(ndN m - card (Iter_rem_aux m z x) - 1) z))%nat.
apply H11.
split.
clear H3 a H H7 H9 H10.
omega.
apply le_refl.
rewrite <- a in H8.
absurd
(exds (Ds x (Iter (f m) (ndN m - card x) z))
(Iter (f m) (ndN m - card x) z))%nat.
apply not_exds_Ds.
tauto.
tauto.
intros.
elim (eq_nat_dec
(ndN m - card (Iter_rem_aux m z x) - 1) j)%nat.
intro.
rewrite <- a.
tauto.
intro.
generalize (H (Ds x (Iter (f m)
(ndN m - card x) z)))%nat.
intro.
assert
(∀ j : nat,
ndN m - card (Ds x (Iter (f m) (ndN m - card x) z))
< j ≤ ndN m - card (Iter_rem_aux m z
(Ds x (Iter (f m) (ndN m - card x) z))) - 1 →
Iter (f m)
(ndN m - card (Ds x (Iter (f m) (ndN m - card x) z))) z ≠
Iter (f m) j z)%nat.
apply H5.
unfold Rs in |- ×.
rewrite exds_card_Ds.
clear H1 H3 b b0.
omega.
tauto.
tauto.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x) z) H2)%nat.
intro.
rewrite H7.
clear H3 H4 b b0 H7.
omega.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x) z) H2)%nat.
intro.
rewrite H7.
assert (ndN m - (card x - 1) =
ndN m + 1 - card x)%nat.
clear H3 b b0 H7.
omega.
rewrite H8.
tauto.
clear H5.
generalize (exds_card_Ds x
(Iter (f m) (ndN m - card x) z) H2)%nat.
intro.
rewrite H5 in H7.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z))%nat.
intros.
clear a.
rewrite <- H8 in H7.
assert (ndN m - (card x - 1) = ndN m + 1 - card x)%nat.
clear H3 b b0 H5 H8.
omega.
rewrite H9 in H7.
intro.
assert (Iter (f m) (S (ndN m - card x)) z
= Iter (f m) (S j) z)%nat.
simpl in |- ×.
rewrite H10.
tauto.
generalize H11.
assert (S (ndN m - card x) = ndN m + 1 - card x)%nat.
clear H9.
clear H5.
clear H3 b b0 H8 H10 H11.
omega.
rewrite H12.
apply H7.
split.
rewrite <- H12.
apply lt_n_S.
tauto.
clear H12.
clear H9.
clear H5.
clear H4.
clear H1 b H8 H10 H11.
elim H3.
intros.
clear H1.
clear H3.
omega.
tauto.
Qed.
Definition P8(m:fmap)(z:dart)(s:set):Prop:=
inv_hmap m →
(card s ≤ ndN m →
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z) →
diff_int m z n0 (nr - 1))%nat.
Lemma LP8:∀(m:fmap)(z:dart)(s:set),
inv_hmap m →
(card s ≤ ndN m →
let n0:= ndN m - card s in
let nr:= Iter_upb_aux m z s in
exds s (Iter (f m) n0 z) →
diff_int m z n0 (nr - 1))%nat.
Proof.
intros m z.
refine (well_founded_ind Rs_wf (P8 m z) _).
unfold P8 in |- ×.
unfold Iter_upb_aux in |- ×.
intros.
generalize (rem_1_step m z x H0).
simpl in |- ×.
intro.
assert (card (Iter_rem_aux m z x) + 1 ≤ card x)%nat.
tauto.
clear H3.
elim (eq_nat_dec (card (Iter_rem_aux m z x) + 1)
(card x))%nat.
intro.
clear H4.
assert (ndN m - card (Iter_rem_aux m z x) - 1
= ndN m - card x)%nat.
omega.
rewrite H3.
apply diff_int_le.
apply le_refl.
intro.
assert (card (Iter_rem_aux m z x) + 2 ≤ card x)%nat.
omega.
clear b H4.
generalize (rem_2_steps m z x H0 H3).
intro.
generalize (LP7 m z x H0 H1 H2).
intro.
unfold diff_int in |- ×.
intros.
elim (eq_nat_dec (ndN m - card x) i)%nat.
intro.
rewrite <- a.
unfold Iter_upb_aux in H5.
apply H5.
split.
rewrite a.
tauto.
tauto.
intro.
assert (card (Ds x (Iter (f m) (ndN m - card x) z))
= card x - 1)%nat.
rewrite exds_card_Ds.
tauto.
tauto.
generalize (Iter_rem_aux_equation m z x).
simpl in |- ×.
elim (exds_dec x (Iter (f m) (ndN m - card x) z))%nat.
intros.
clear a.
clear H5.
generalize (H (Ds x (Iter (f m) (ndN m - card x) z)))%nat.
intros.
assert
(diff_int m z
(ndN m - card (Ds x (Iter (f m) (ndN m - card x) z)))
(ndN m -
card (Iter_rem_aux m z
(Ds x (Iter (f m) (ndN m - card x) z))) -
1))%nat.
apply H5.
unfold Rs in |- ×.
apply exds_card_Ds_inf.
tauto.
tauto.
rewrite H7.
omega.
rewrite H7.
assert (ndN m - (card x - 1) = ndN m + 1 - card x)%nat.
clear H5.
clear H.
clear H8.
omega.
rewrite H9.
tauto.
clear H5 H.
rewrite <- H8 in H9.
unfold diff_int in H9.
rewrite H7 in H9.
apply H9.
split.
clear H8 H9.
clear H1 H3 H4.
clear H0.
omega.
tauto.
tauto.
Qed.
Definition diff_orb(m:fmap)(z:dart):Prop:=
let nr:= Iter_upb_aux m z (fmap_to_set m) in
(diff_int m z 0 (nr - 1))%nat.
Theorem exd_diff_orb:∀(m:fmap)(z:dart),
inv_hmap m → exd m z →
diff_orb m z.
intros.
unfold diff_orb in |- ×.
generalize (nd_card m).
intro.
assert (ndN m - card (fmap_to_set m) = 0)%nat.
rewrite H1.
omega.
cut
(diff_int m z (ndN m - card (fmap_to_set m))
(Iter_upb_aux m z (fmap_to_set m) - 1))%nat.
rewrite H2.
tauto.
apply LP8.
tauto.
rewrite H1.
apply le_refl.
rewrite H2.
simpl in |- ×.
generalize (exd_exds m z).
tauto.
Qed.
Theorem Iter_upb_period:∀(m:fmap)(z:dart),
inv_hmap m → exd m z →
let nr:= Iter_upb m z in
Iter (f m) nr z = z.
Proof.
simpl in |- ×.
intros.
generalize (ex_i_upb m z H H0).
simpl in |- ×.
intros.
elim H1.
intros i Hi.
clear H1.
elim (eq_nat_dec i 0%nat).
intro.
rewrite a in Hi.
simpl in Hi.
symmetry in |- ×.
tauto.
intro.
decompose [and] Hi.
clear Hi.
assert (f_1 m (Iter (f m) i z) =
f_1 m (Iter (f m) (Iter_upb m z) z)).
rewrite H2.
tauto.
set (i1 := (i - 1)%nat) in |- ×.
set (nr1 := (Iter_upb m z - 1)%nat) in |- ×.
assert (i = S i1).
unfold i1 in |- ×.
omega.
assert (Iter_upb m z = S nr1).
unfold nr1 in |- ×.
omega.
rewrite H5 in H3.
rewrite H4 in H3.
simpl in H3.
rewrite f_1_f in H3.
rewrite f_1_f in H3.
unfold i1 in H3.
unfold nr1 in H3.
absurd (Iter (f m) (i - 1)%nat z =
Iter (f m) (Iter_upb m z - 1)%nat z).
generalize (LP8 m z (fmap_to_set m) H).
simpl in |- ×.
intros.
unfold diff_int in H6.
assert
(∀ i j : nat,
ndN m - card (fmap_to_set m) ≤ i ∧
i < j ≤ Iter_upb_aux m z (fmap_to_set m) - 1 →
Iter (f m) i z ≠ Iter (f m) j z)%nat.
apply H6.
rewrite nd_card.
apply le_refl.
assert (ndN m - card (fmap_to_set m) = 0)%nat.
rewrite nd_card.
simpl in |- ×.
omega.
rewrite H7.
simpl in |- ×.
generalize (exd_exds m z).
tauto.
apply H7.
split.
clear H6.
clear H7.
clear H2.
rewrite nd_card.
omega.
clear H7 H6.
clear H2.
split.
omega.
unfold Iter_upb in |- ×.
unfold Iter_upb_aux in |- ×.
unfold Iter_rem in |- ×.
apply le_refl.
tauto.
tauto.
generalize (exd_Iter_f m nr1 z).
tauto.
tauto.
generalize (exd_Iter_f m i1 z).
tauto.
Qed.
Lemma Iter_period:∀(m:fmap)(z:dart)(i n:nat),
inv_hmap m → exd m z →
let p:= Iter_upb m z in
Iter (f m) (i + n×p)%nat z = Iter (f m) i z.
Proof.
intros.
intros.
assert (Iter (f m) p z = z).
unfold p in |- ×.
apply Iter_upb_period.
tauto.
tauto.
rewrite Iter_plus_mult.
trivial.
assumption.
assumption.
assumption.
Qed.
Require Import Euclid.
Lemma mod_p:∀(m:fmap)(z:dart)(i:nat),
inv_hmap m → exd m z →
let p := Iter_upb m z in
{j :nat | Iter (f m) i z = Iter (f m) j z ∧ (j < p)%nat}.
Proof.
intros.
assert (p > 0)%nat.
unfold p in |- ×.
generalize (upb_pos m z H0).
intro.
omega.
generalize (modulo p H1 i).
intro.
elim H2.
intros r Hr.
split with r.
elim Hr.
intros q Hq.
elim Hq.
clear Hq.
intros.
split.
rewrite H3.
rewrite plus_comm.
unfold p in |- ×.
rewrite Iter_period.
trivial.
tauto.
tauto.
omega.
Qed.
Require Export Compare.
Lemma period_uniform : ∀(m:fmap)(z:dart)(i:nat),
inv_hmap m → exd m z →
Iter_upb m z = Iter_upb m (Iter (f m) i z).
Proof.
intros.
set (zi := Iter (f m) i z) in |- ×.
set (p := Iter_upb m z) in |- ×.
set (q := Iter_upb m zi) in |- ×.
generalize (Iter_upb_period m z H H0).
simpl in |- ×.
fold p in |- ×.
intro.
assert (exd m zi).
unfold zi in |- ×.
generalize (exd_Iter_f m i z H).
tauto.
generalize (Iter_upb_period m zi H H2).
simpl in |- ×.
fold q in |- ×.
intro.
assert (Iter (f m) (i + q)%nat z = Iter (f m) q zi).
unfold zi in |- ×.
rewrite plus_comm.
apply Iter_comp.
assert (Iter (f m) q z = z).
apply (Iter_plus m z q i H H0).
fold zi in |- ×.
rewrite plus_comm.
rewrite <- H3.
tauto.
assert (Iter (f m) p zi = zi).
unfold zi in |- ×.
rewrite <- Iter_comp.
rewrite plus_comm.
assert (i + p = i + 1 × p)%nat.
omega.
rewrite H6.
unfold p in |- ×.
rewrite Iter_period.
trivial.
trivial.
trivial.
clear H4.
elim (lt_eq_lt_dec p q).
intro.
elim a.
clear a.
intro.
generalize (exd_diff_orb m zi H H2).
unfold diff_orb in |- ×.
unfold Iter_upb in q.
unfold Iter_rem in q.
unfold Iter_upb_aux in |- ×.
fold q in |- ×.
unfold diff_int in |- ×.
intros.
absurd (Iter (f m) p zi = zi).
intro.
symmetry in H7.
replace zi with (Iter (f m) 0%nat zi) in H7.
generalize H7.
clear H7.
apply H4.
split.
omega.
split.
unfold p in |- ×.
apply upb_pos.
tauto.
omega.
simpl in |- ×.
trivial.
tauto.
tauto.
intro.
generalize (exd_diff_orb m z H H0).
unfold diff_orb in |- ×.
unfold Iter_upb in p.
unfold Iter_rem in p.
unfold Iter_upb_aux in |- ×.
fold p in |- ×.
unfold diff_int in |- ×.
intros.
symmetry in H5.
absurd (z = Iter (f m) q z).
replace z with (Iter (f m) 0%nat z).
apply H4.
split.
omega.
split.
unfold q in |- ×.
apply upb_pos.
tauto.
omega.
simpl in |- ×.
trivial.
tauto.
Qed.
Lemma unicity_mod_p:∀(m:fmap)(z:dart)(j k:nat),
inv_hmap m → exd m z →
let p := Iter_upb m z in
(j < p)%nat → (k < p)%nat →
Iter (f m) j z = Iter (f m) k z → j = k.
Proof.
intros.
generalize (exd_diff_orb m z H H0).
unfold diff_orb in |- ×.
unfold Iter_upb in p.
unfold Iter_upb_aux in |- ×.
unfold Iter_rem in p.
fold p in |- ×.
unfold diff_int in |- ×.
intros.
elim (le_gt_dec j k).
elim (eq_nat_dec j k).
intros.
tauto.
intros.
absurd (Iter (f m) j z = Iter (f m) k z).
apply (H4 j k).
omega.
tauto.
intro.
symmetry in H3.
absurd (Iter (f m) k z = Iter (f m) j z).
apply (H4 k j).
omega.
tauto.
Qed.
Definition expo(m:fmap)(z t:dart):Prop:=
exd m z ∧ ∃ i:nat, Iter (f m) i z = t.
Definition expo1
(m:fmap)(z t:dart):Prop:=
exd m z ∧
let p:= Iter_upb m z in
∃ j:nat, (j < p)%nat ∧ Iter (f m) j z = t.
Lemma expo_expo1:
∀(m:fmap)(z t:dart), inv_hmap m →
(expo m z t ↔ expo1 m z t).
Proof.
unfold expo in |- ×.
unfold expo1 in |- ×.
intros.
unfold expo in |- ×.
unfold expo1 in |- ×.
intros.
split.
intros.
elim H0.
clear H0.
intros.
split.
tauto.
elim H1.
intros i Hi.
clear H1.
generalize (mod_p m z i H H0).
simpl in |- ×.
intros.
elim H1.
intros j Hj.
split with j.
split.
tauto.
rewrite Hi in Hj.
symmetry in |- ×.
tauto.
intros.
elim H0.
clear H0.
intros.
split.
tauto.
elim H1.
intros.
split with x.
tauto.
Qed.
Definition modulo(m:fmap)(z:dart)(i:dart)
(hi:inv_hmap m)(he:exd m z):nat.
Proof.
intros.
assert
(let p := Iter_upb m z in
{j : nat | Iter (f m) i z = Iter (f m) j z ∧ (j < p)%nat}).
apply mod_p.
tauto.
tauto.
simpl in H.
elim H.
intros.
apply x.
Defined.
Lemma expo_exd:
∀(m:fmap)(z t:dart),
inv_hmap m → expo m z t → exd m t.
Proof.
unfold expo in |- ×.
intros.
decompose [and] H0.
elim H2.
intros i Hi.
rewrite <- Hi.
generalize (exd_Iter_f m i z).
tauto.
Qed.
Lemma expo_refl:
∀(m:fmap)(z:dart), exd m z → expo m z z.
Proof.
intros.
unfold expo in |- ×.
split.
tauto.
split with 0%nat.
simpl in |- ×.
tauto.
Qed.
Lemma expo_trans:
∀(m:fmap)(z t u:dart),
expo m z t → expo m t u → expo m z u.
Proof.
unfold expo in |- ×.
intros.
intuition.
elim H2.
intros j Hj.
elim H3.
intros i Hi.
split with (i + j)%nat.
rewrite Iter_comp.
rewrite Hj.
tauto.
Qed.
Lemma expo_symm:∀(m:fmap)(z t:dart),
inv_hmap m →
expo m z t → expo m t z.
Proof.
intros m z t Hm He.
assert (exd m t).
apply expo_exd with z.
tauto.
tauto.
unfold expo in |- ×.
unfold expo in He.
intuition.
elim H1.
intros i Hi.
rewrite <- Hi.
clear H1.
generalize (mod_p m z i Hm H0).
intro.
simpl in H1.
elim H1.
intros r Hr.
elim Hr.
clear Hr H1.
intros.
split with (Iter_upb m z - r)%nat.
rewrite H1.
rewrite <- Iter_comp.
assert (Iter_upb m z - r + r = Iter_upb m z)%nat.
omega.
rewrite H3.
apply Iter_upb_period.
tauto.
tauto.
Qed.
Fixpoint ex_j
(m:fmap)(z t:dart)(n:nat){struct n}:Prop:=
match n with
0%nat ⇒ z = t
| S n0 ⇒ Iter (f m) n z = t ∨ ex_j m z t n0
end.
Lemma ex_j_dec:
∀(m:fmap)(z t:dart)(n:nat),
{ex_j m z t n} + {¬ex_j m z t n}.
Proof.
induction n.
simpl in |- ×.
apply eq_dart_dec.
simpl in |- ×.
generalize (eq_dart_dec (f m (Iter (f m) n z)) t).
tauto.
Qed.
Lemma ex_j_exist_j:∀(m:fmap)(z t:dart)(n:nat),
ex_j m z t n ↔
∃ j :nat, (j ≤ n)%nat ∧ Iter (f m) j z = t.
Proof.
induction n.
simpl in |- ×.
split.
intro.
split with 0%nat.
split.
omega.
simpl in |- ×.
tauto.
intro.
elim H.
intros j Hj.
intuition.
inversion H0.
rewrite H2 in H1.
simpl in |- ×.
simpl in H1.
tauto.
simpl in |- ×.
split.
intro.
elim H.
intro.
split with (S n).
split. clear IHn H H0.
omega.
simpl in |- ×.
tauto.
intro.
assert (∃ j : nat, (j ≤ n)%nat
∧ Iter (f m) j z = t).
tauto.
elim H1.
intros j Hj.
split with j.
split. decompose [and] Hj. clear H H0 H1 Hj H3 IHn.
omega.
tauto.
intros.
elim H.
intros j Hj.
elim (eq_nat_dec j (S n)).
intro.
rewrite a in Hj.
simpl in Hj.
tauto.
intro.
assert (∃ j : nat, (j ≤ n)%nat
∧ Iter (f m) j z = t).
split with j.
split. clear IHn.
omega.
tauto.
tauto.
Qed.
Lemma expo1_ex_j:
∀(m:fmap)(z t:dart), inv_hmap m → exd m z →
let p:= Iter_upb m z in
(ex_j m z t (p - 1)%nat ↔ expo1 m z t).
Proof.
intros.
generalize (Iter_upb_period m z H H0).
generalize (upb_pos m z H0).
rename H into hm.
rename H0 into hz.
fold p in |- ×.
intros Hp1 Hp2.
generalize (ex_j_exist_j m z t (p - 1)%nat).
unfold expo1 in |- ×.
fold p in |- ×.
intros.
split.
intro.
assert (∃ j : nat, (j ≤ p - 1)%nat
∧ Iter (f m) j z = t).
tauto.
elim H1.
intros j Hj.
split.
tauto.
split with j.
split. clear H H0.
omega.
tauto.
intro.
elim H0.
intros.
elim H2.
clear H0 H2.
intros i Hj.
assert (∃ j : nat, (j ≤ p - 1)%nat
∧ Iter (f m) j z = t).
split with i.
split. clear H.
omega.
tauto.
tauto.
Qed.
Lemma expo1_dec :
∀ (m:fmap)(z t:dart),
inv_hmap m → exd m z →
{expo1 m z t} + {¬expo1 m z t}.
Proof.
intros.
set (p := Iter_upb m z) in |- ×.
generalize (ex_j_dec m z t (p - 1)).
intro.
elim H1.
intro.
left.
generalize (expo1_ex_j m z t H H0).
simpl in |- ×.
fold p in |- ×.
tauto.
intro.
right.
intro.
generalize (expo1_ex_j m z t H H0).
simpl in |- ×.
fold p in |- ×.
tauto.
Qed.
Lemma expo_dec: ∀(m:fmap)(z t:dart),
inv_hmap m →
{expo m z t} + {¬expo m z t}.
Proof.
intros m z t hm.
generalize (expo_expo1 m z t hm).
generalize (expo1_dec m z t hm).
intros.
elim (exd_dec m z).
tauto.
unfold expo in |- ×.
tauto.
Qed.
Theorem period_expo : ∀(m:fmap)(z t:dart),
inv_hmap m → expo m z t →
Iter_upb m z = Iter_upb m t.
Proof.
unfold expo in |- ×.
intros.
elim H0.
clear H0.
intros.
elim H1.
intros i Hi.
rewrite <- Hi.
apply period_uniform.
tauto.
tauto.
Qed.
Open Scope nat_scope.
Theorem period_lub : ∀(m:fmap)(z:dart),
inv_hmap m → exd m z →
let nr:= Iter_upb m z in
0 < nr ∧ Iter (f m) nr z = z ∧
∀ i:nat, 0 < i < nr → Iter (f m) i z ≠ z.
Proof.
intros.
split.
unfold nr in |- ×.
apply upb_pos.
tauto.
split.
unfold nr in |- ×.
apply Iter_upb_period.
tauto.
tauto.
intros.
generalize (exd_diff_orb m z).
unfold diff_orb in |- ×.
unfold Iter_upb in nr.
unfold Iter_rem in nr.
unfold Iter_upb_aux in |- ×.
fold nr in |- ×.
unfold diff_int in |- ×.
intros.
assert
(∀ i j : nat,
0 ≤ i ∧ i < j ≤ nr - 1 →
Iter (f m) i z ≠ Iter (f m) j z).
tauto.
clear H2.
generalize (H3 0 i).
intros.
simpl in H2.
intro.
symmetry in H4.
apply H2.
split.
omega.
omega.
assumption.
Qed.
Require Import Recdef.
Open Scope nat_scope.
Lemma ndN_pos:∀(m:fmap)(z:dart),
exd m z → 0 < ndN m.
Proof.
induction m.
simpl in |- ×.
tauto.
simpl in |- ×.
intros.
elim (exd_dec m d).
intro.
apply IHm with d.
tauto.
intro.
omega.
simpl in |- ×.
tauto.
Qed.
Function degree_aux(m:fmap)(z:dart)(n:nat)
{measure (fun i:nat ⇒ ndN m - i) n}:nat:=
if le_lt_dec n (ndN m)
then if eq_dart_dec z (Iter (f m) n z) then n
else if eq_nat_dec n (ndN m) then (ndN m) + 1
else degree_aux m z (n+1)
else (ndN m) + 1.
Proof.
intros.
omega.
Defined.
Definition degree(m:fmap)(z:dart):=
degree_aux m z 1.
Definition P_degree_pos(m:fmap)(z:dart)(n1 n2:nat):
Prop:= exd m z → 0 < n1 → 0 < n2.
Lemma degree_pos_aux:∀(m:fmap)(z:dart),
P_degree_pos m z 1 (degree m z).
Proof.
unfold degree in |- ×.
intros.
apply degree_aux_ind.
intros.
unfold P_degree_pos in |- ×.
tauto.
intros.
unfold P_degree_pos in |- ×.
intros.
omega.
intros.
unfold P_degree_pos in |- ×.
unfold P_degree_pos in H.
assert (0 < n + 1).
omega.
tauto.
intros.
unfold P_degree_pos in |- ×.
intros.
omega.
Qed.
Theorem degree_pos:∀(m:fmap)(z:dart),
exd m z → 0 < degree m z.
Proof.
unfold degree in |- ×.
intros.
generalize (degree_pos_aux m z).
unfold P_degree_pos in |- ×.
unfold degree in |- ×.
intros.
assert (0 < 1).
omega.
tauto.
Qed.
Definition P_degree_diff(m:fmap)(z:dart)(n1 n2:nat):
Prop:= inv_hmap m → exd m z → 0 < n1 →
∀ i:nat, n1 ≤ i < n2 → Iter (f m) i z ≠ z.
Lemma degree_diff_aux:∀(m:fmap)(z:dart),
P_degree_diff m z 1 (degree m z).
Proof.
unfold degree in |- ×.
intros.
apply degree_aux_ind.
intros.
unfold P_degree_diff in |- ×.
intros.
omega.
intros.
unfold P_degree_diff in |- ×.
intros.
rewrite _x1 in H2.
assert (i = n).
rewrite _x1 in |- ×.
omega.
rewrite H3 in |- ×.
intro.
symmetry in H4.
assert (z ≠ Iter (f m) n z).
apply _x0.
tauto.
intros.
unfold P_degree_diff in |- ×.
unfold P_degree_diff in H.
intros.
elim (eq_nat_dec n i).
intro.
rewrite <- a in |- ×.
intro.
assert (z ≠ Iter (f m) n z).
apply _x0.
symmetry in H4.
tauto.
intro.
apply H.
tauto.
tauto.
omega.
split.
omega.
tauto.
intros.
unfold P_degree_diff in |- ×.
intros.
omega.
Qed.
Theorem degree_diff: ∀ (m:fmap)(z:dart),
inv_hmap m → exd m z →
∀ i:nat, 0 < i < (degree m z) →
Iter (f m) i z ≠ z.
Proof.
intros.
generalize (degree_diff_aux m z).
unfold P_degree_diff in |- ×.
intros.
assert (∀ i : nat, 1 ≤ i < degree m z → Iter (f m) i z ≠ z).
apply H2.
tauto.
tauto.
omega.
apply H3.
omega.
Qed.
Lemma degree_bound: ∀ (m:fmap)(z:dart),
inv_hmap m → exd m z → degree m z ≤ ndN m.
Proof.
intros.
elim (le_lt_dec (degree m z) (ndN m)).
tauto.
intro.
generalize (degree_diff m z H H0).
intro.
set (nr := Iter_upb m z) in |- ×.
assert (Iter (f m) nr z = z).
unfold nr in |- ×.
apply Iter_upb_period.
tauto.
tauto.
assert (nr ≤ ndN m).
unfold nr in |- ×.
unfold Iter_upb in |- ×.
omega.
absurd (Iter (f m) nr z = z).
apply H1.
split.
unfold nr in |- ×.
apply upb_pos.
tauto.
omega.
tauto.
Qed.
Definition P_degree_per(m:fmap)(z:dart)(n1 n2:nat):
Prop:= inv_hmap m → exd m z → 0 < n1 → n2 ≤ ndN m →
Iter (f m) n2 z = z.
Lemma degree_per_aux: ∀(m:fmap)(z:dart),
P_degree_per m z 1 (degree m z).
Proof.
unfold degree in |- ×.
intros.
apply degree_aux_ind.
intros.
unfold P_degree_per in |- ×.
symmetry in |- ×.
tauto.
intros.
unfold P_degree_per in |- ×.
intros.
absurd (ndN m + 1 ≤ ndN m).
omega.
tauto.
intros.
unfold P_degree_per in |- ×.
unfold P_degree_per in H.
intros.
apply H.
tauto.
tauto.
omega.
tauto.
intros.
unfold P_degree_per in |- ×.
intros.
absurd (ndN m + 1 ≤ ndN m).
omega.
tauto.
Qed.
Theorem degree_per: ∀ (m:fmap)(z:dart),
inv_hmap m → exd m z →
Iter (f m) (degree m z) z = z.
Proof.
intros.
apply degree_per_aux.
tauto.
tauto.
omega.
apply degree_bound.
tauto.
tauto.
Qed.
Theorem degree_lub: ∀(m:fmap)(z:dart),
inv_hmap m → exd m z →
let p:= degree m z in
0 < p ∧ Iter (f m) p z = z ∧
∀ i:nat, 0 < i < p → Iter (f m) i z ≠ z.
Proof.
intros.
unfold p in |- ×.
split.
apply degree_pos.
tauto.
split.
apply degree_per.
tauto.
tauto.
apply degree_diff.
tauto.
tauto.
Qed.
Require Import Arith.
Theorem upb_eq_degree:∀(m:fmap)(z:dart),
inv_hmap m → exd m z →
Iter_upb m z = degree m z.
Proof.
intros.
set (p := degree m z) in |- ×.
set (nr := Iter_upb m z) in |- ×.
generalize (period_lub m z H H0).
generalize (degree_lub m z H H0).
simpl in |- ×.
fold p in |- ×.
fold nr in |- ×.
intros.
decompose [and] H1.
clear H1.
decompose [and] H2.
clear H2.
elim (lt_eq_lt_dec nr p).
intro.
elim a.
intro.
absurd (Iter (f m) nr z = z).
apply H6.
omega.
tauto.
tauto.
intro.
absurd (Iter (f m) p z = z).
apply H8.
omega.
tauto.
Qed.
Theorem expo_degree : ∀(m:fmap)(z t:dart),
inv_hmap m → expo m z t →
degree m z = degree m t.
Proof.
intros.
generalize (period_expo m z t H H0).
rewrite upb_eq_degree in |- ×.
rewrite upb_eq_degree in |- ×.
tauto.
tauto.
apply (expo_exd m z t H H0).
tauto.
unfold expo in H0.
tauto.
Qed.
Theorem degree_uniform : ∀(m:fmap)(z:dart)(i:nat),
inv_hmap m → exd m z →
degree m z = degree m (Iter (f m) i z).
Proof.
intros.
generalize (period_uniform m z i H H0).
rewrite upb_eq_degree in |- ×.
rewrite upb_eq_degree in |- ×.
tauto.
tauto.
generalize (exd_Iter_f m i z).
tauto.
tauto.
tauto.
Qed.
Theorem degree_unicity:∀(m:fmap)(z:dart)(j k:nat),
inv_hmap m → exd m z →
let p := degree m z in
j < p → k < p →
Iter (f m) j z = Iter (f m) k z → j = k.
Proof.
intros.
generalize (unicity_mod_p m z j k H H0).
simpl in |- ×.
rewrite upb_eq_degree in |- ×.
fold p in |- ×.
tauto.
tauto.
tauto.
Qed.
Open Scope R_scope.
Lemma incls_orbit:∀(m:fmap)(x:dart),
inv_hmap m → exd m x →
incls (Iter_orb m x) (fmap_to_set m).
Proof.
intros.
apply exds2.
intro.
unfold Iter_orb in |- ×.
generalize (exds_set_minus_eq (fmap_to_set m)
(Iter_rem m x) z).
tauto.
Qed.
Lemma exds_orb_exd:∀(m:fmap)(x z:dart),
inv_hmap m → exd m x →
exds (Iter_orb m x) z → exd m z.
Proof.
intros.
generalize (incls_orbit m x H H0).
intro.
inversion H2.
generalize (H3 z H1).
intro.
generalize (exd_exds m z).
tauto.
Qed.
Lemma incls_rem:∀(m:fmap)(x:dart),
inv_hmap m → exd m x →
incls (Iter_rem m x) (fmap_to_set m).
Proof.
unfold Iter_rem in |- ×.
intros.
apply exds2.
intro.
intro.
generalize (LR3 m x z (fmap_to_set m)).
simpl in |- ×.
generalize (exds_dec (fmap_to_set m) z).
generalize (exds_dec (Iter_rem_aux m x (fmap_to_set m)) z).
tauto.
Qed.
Lemma card_orbit:∀(m:fmap)(x:dart),
inv_hmap m → exd m x →
card (Iter_orb m x) = Iter_upb m x.
Proof.
unfold Iter_orb in |- ×.
unfold Iter_upb in |- ×.
intros.
generalize (incls_rem m x H H0).
intros.
rewrite nd_card in |- ×.
generalize (card_minus_set (fmap_to_set m) (Iter_rem m x) H1).
intro.
omega.
Qed.
Lemma exds_orb_ex :∀(m:fmap)(z t:dart),
inv_hmap m → exd m z →
let s:= Iter_orb m z in
let p:= Iter_upb m z in
exds s t →
{i : nat | (i < p)%nat ∧ Iter (f m) i z = t}.
Proof.
intros.
intros.
assert (exd m t).
generalize (incls_orbit m z H H0).
intro.
inversion H2.
generalize (H3 t H1).
intro.
generalize (exd_exds m t).
tauto.
assert (¬ exds (Iter_rem m z) t).
generalize (exds_rem_orb m z t H H2).
tauto.
apply (ex_i m z t H H0 H2 H3).
Qed.
Theorem exds_orb_eq_ex :∀(m:fmap)(z t:dart),
inv_hmap m → exd m z →
let s:= Iter_orb m z in
let p:= Iter_upb m z in
(exds s t ↔
∃ i:nat,(i < p)%nat ∧ Iter (f m) i z = t).
Proof.
split.
intro.
generalize (exds_orb_exd m z t H H0 H1).
intro.
generalize (exds_orb_ex m z t H H0 H1).
intro.
elim H3.
intros.
split with x.
tauto.
intros.
elim H1.
intros i Hi.
clear H1.
decompose [and] Hi.
clear Hi.
rewrite <- H2 in |- ×.
apply exds_Iter_f_i.
tauto.
tauto.
omega.
Qed.
Open Scope nat_scope.
Theorem exds_orb_eq_ex_large :∀(m:fmap)(z t:dart),
inv_hmap m → exd m z →
let s:= Iter_orb m z in
let p:= Iter_upb m z in
(exds s t ↔ ∃ i:nat, Iter (f m) i z = t).
Proof.
split.
intro.
generalize (exds_orb_exd m z t H H0 H1).
intro.
generalize (exds_orb_eq_ex m z t H H0).
simpl in |- ×.
intro.
assert (∃ i : nat,
i < Iter_upb m z ∧ Iter (f m) i z = t).
tauto.
clear H3.
elim H4.
intros.
split with x.
tauto.
intro.
assert (expo m z t).
unfold expo in |- ×.
split.
tauto.
tauto.
generalize (expo_expo1 m z t H).
unfold expo1 in |- ×.
intro.
assert (∃ j : nat,
j < Iter_upb m z ∧ Iter (f m) j z = t).
tauto.
generalize (exds_orb_eq_ex m z t H H0).
simpl in |- ×.
tauto.
Qed.
Theorem expo_eq_exds_orb :∀(m:fmap)(z t:dart),
inv_hmap m → exd m z →
(expo m z t ↔ exds (Iter_orb m z) t).
Proof.
intros.
generalize (exds_orb_eq_ex_large m z t H H0).
simpl in |- ×.
intro.
unfold expo in |- ×.
tauto.
Qed.
Theorem expo1_eq_exds_orb :∀(m:fmap)(z t:dart),
inv_hmap m → exd m z →
(expo1 m z t ↔ exds (Iter_orb m z) t).
Proof.
intros.
generalize (exds_orb_eq_ex m z t H H0).
simpl in |- ×.
intro.
unfold expo1 in |- ×.
tauto.
Qed.
Lemma impls_orb:∀(m:fmap)(x y:dart),
inv_hmap m → exd m x →
expo m x y →
impls (Iter_orb m x) (Iter_orb m y).
Proof.
unfold impls in |- ×.
intros.
assert (exd m y).
generalize (expo_exd m x y).
tauto.
generalize (exds_orb_eq_ex_large m x z H H0).
intros.
generalize (exds_orb_eq_ex_large m y z H H3).
intro.
assert (exd m z).
generalize (exd_exds m z).
intro.
generalize (incls_orbit m x H H0).
intro.
inversion H7.
generalize (H8 z H2).
tauto.
simpl in H4.
assert (∃ i : nat, Iter (f m) i x = z).
tauto.
elim H7.
clear H7.
intros i Hi.
assert (expo m x z).
unfold expo in |- ×.
split.
tauto.
split with i.
tauto.
assert (expo m y z).
apply expo_trans with x.
apply expo_symm.
tauto.
tauto.
tauto.
assert (∃ i : nat, Iter (f m) i y = z).
unfold expo in H8.
tauto.
simpl in H5.
tauto.
Qed.
Lemma eqs_orb:∀(m:fmap)(x y:dart),
inv_hmap m →
expo m x y →
eqs (Iter_orb m x) (Iter_orb m y).
Proof.
unfold eqs in |- ×.
intros.
assert (exd m x).
unfold expo in H0.
tauto.
assert (exd m y).
apply expo_exd with x.
tauto.
tauto.
split.
generalize (impls_orb m x y H H1 H0).
unfold impls in |- ×.
intro.
apply H3.
assert (expo m y x).
apply expo_symm.
tauto.
tauto.
generalize (impls_orb m y x H H2 H3).
unfold impls in |- ×.
intro.
apply H4.
Qed.
Lemma orb_impls_expo:∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y →
impls (Iter_orb m x) (Iter_orb m y) → expo m x y.
Proof.
intros.
unfold impls in H2.
generalize (H2 x).
intro.
assert (exds (Iter_orb m x) x).
generalize (expo_eq_exds_orb m x x H H0).
intro.
assert (expo m x x).
apply expo_refl.
tauto.
tauto.
apply expo_symm.
tauto.
generalize (expo_eq_exds_orb m y x H H1).
tauto.
Qed.
Theorem expo_eq_eqs_orb:∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y →
(expo m x y ↔ eqs (Iter_orb m x) (Iter_orb m y)).
Proof.
split.
apply (eqs_orb m x y H).
unfold eqs in |- ×.
intro.
generalize (orb_impls_expo m x y H H0 H1).
unfold impls in |- ×.
intro.
assert (∀ z : dart,
exds (Iter_orb m x) z → exds (Iter_orb m y) z).
intro.
intro.
generalize (H2 z).
tauto.
tauto.
Qed.
Lemma disjs_orb:∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y →
¬expo m x y →
disjs (Iter_orb m x) (Iter_orb m y).
Proof.
unfold disjs.
intros.
assert (exd m z).
generalize (incls_orbit m x H H0).
intro.
inversion H5.
clear H5.
generalize (H6 z).
intro.
assert (exds (fmap_to_set m) z).
tauto.
clear H6 H5.
generalize (exd_exds m z).
tauto.
generalize (exds_orb_eq_ex m x z H H0).
generalize (exds_orb_eq_ex m y z H H1).
simpl in |- ×.
set (px := Iter_upb m x) in |- ×.
set (py := Iter_upb m y) in |- ×.
intros.
assert (∃ i : nat, i < py ∧ Iter (f m) i y = z).
tauto.
clear H6.
assert (∃ i : nat, i < px ∧ Iter (f m) i x = z).
tauto.
clear H7.
elim H8.
intros i Hi.
clear H8.
elim H6.
intros j Hj.
clear H6.
decompose [and] Hi.
clear Hi.
intros.
decompose [and] Hj.
clear Hj.
intros.
assert (expo m y z).
unfold expo in |- ×.
split.
tauto.
split with i.
tauto.
assert (expo m x z).
unfold expo in |- ×.
split.
tauto.
split with j.
tauto.
elim H2.
apply expo_trans with z.
tauto.
apply expo_symm.
tauto.
tauto.
Qed.
Lemma disjs_orb_not_expo:∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y →
disjs (Iter_orb m x) (Iter_orb m y) → ¬expo m x y.
Proof.
unfold disjs in |- ×.
intros.
generalize (H2 x).
intros.
assert (exds (Iter_orb m x) x).
generalize (expo_eq_exds_orb m x x H H0).
intro.
assert (expo m x x).
apply expo_refl.
tauto.
tauto.
intro.
assert (expo m y x).
apply expo_symm.
tauto.
tauto.
generalize (expo_eq_exds_orb m y x H H1).
tauto.
Qed.
Theorem not_expo_disjs_orb:∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y →
(¬expo m x y ↔
disjs (Iter_orb m x) (Iter_orb m y)).
Proof.
split.
apply (disjs_orb m x y H H0 H1).
apply (disjs_orb_not_expo m x y H H0 H1).
Qed.
Lemma incls_minus: ∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y →
¬expo m x y →
let s:= fmap_to_set m in
let sx:= Iter_orb m x in
let sy:= Iter_orb m y in
incls sy (set_minus s sx).
Proof.
intros.
apply exds2.
intros.
apply exds_set_minus.
generalize (incls_orbit m y H H1).
intro.
inversion H4.
fold s in H5.
apply H5.
fold sy in |- ×.
tauto.
intro.
generalize (disjs_orb m x y H H0 H1 H2).
unfold disjs in |- ×.
intro.
apply (H5 z H4 H3).
Qed.
Open Scope nat_scope.
Theorem upb_sum_bound: ∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y → ¬expo m x y →
Iter_upb m x + Iter_upb m y ≤ ndN m.
Proof.
intros.
rewrite <- card_orbit in |- ×.
rewrite <- card_orbit in |- ×.
set (s := fmap_to_set m) in |- ×.
set (sx := Iter_orb m x) in |- ×.
set (sy := Iter_orb m y) in |- ×.
generalize (incls_minus m x y H H0 H1 H2).
simpl in |- ×.
fold s in |- ×.
fold sx in |- ×.
fold sy in |- ×.
intro.
generalize (incls_orbit m x H H0).
fold s in |- ×.
fold sx in |- ×.
intro.
generalize (card_minus_set s sx H4).
intro.
generalize (card_minus_set (set_minus s sx) sy H3).
intro.
generalize (nd_card m).
intro.
fold s in H7.
rewrite H7 in |- ×.
clear H7.
omega.
tauto.
tauto.
tauto.
tauto.
Qed.
Theorem degree_sum_bound: ∀(m:fmap)(x y:dart),
inv_hmap m → exd m x → exd m y → ¬expo m x y →