Module LibMaps

Require Export Maps.
Require Import Coqlib.
Require Export LibPos.

Section Maxindex.
Variable A: Type.

Theorem max_index : forall t : PTree.t A,
{i | forall j, t ! j <> None -> Plt j i}.
Proof.
intros.
cut {i | forall j x, In (j, x) (PTree.elements t) -> Plt j i}.
destruct 1.
exists x.
intros.
case_eq (t ! j).
intros.
generalize (PTree.elements_correct _ _ H0).
eauto.
congruence.
generalize (PTree.elements t).
clear t.
induction l ; simpl.
exists 1%positive.
tauto.
destruct IHl.
destruct a.
destruct (plt p0 x).
exists x.
inversion 1.
congruence.
eauto.
exists (Psucc p0).
inversion 1.
injection H0 ; intros ; subst.
apply Plt_succ.
generalize (p _ _ H0).
intros.
eapply Plt_trans with x.
assumption.
unfold Plt in *.
rewrite Zpos_succ_morphism.
unfold Zsucc.
omega.
Qed.

End Maxindex.

Section Progressive.

Variables A : Type.

Variable P : positive -> A -> Type.

Hypothesis f : forall
n
(t : PTree.t A)
(H_nonempty : forall i, Plt i n -> t ! i <> None)
(H_property : forall i c, t ! i = Some c -> P i c),
{y : _ & P n y}.

Theorem progressive : forall n,
{t : _ &
((forall i, Plt i n -> t ! i <> None) *
forall i c, t ! i = Some c -> P i c)%type}.
Proof.
intros.
destruct (peq n 1%positive).
subst.
exists (@PTree.empty A).
split.
intros.
unfold Plt in H.
destruct i ; compute in H ; congruence.
intros.
rewrite PTree.gempty in H.
congruence.
assert (Zpos n > 0) by (compute ; trivial).
assert (Zpos n <> 1) by congruence.
assert (Zpos n - 1 > 0) by omega.
revert H1.
case_eq (Zpos n - 1).
Focus 2.
intros.
apply False_rect.
compute in H2.
congruence.
intros.
assert (n = Psucc p).
cut (Zpos n = Zpos (Psucc p)).
congruence.
rewrite Psucc_Zsucc.
unfold Zsucc.
omega.
subst.
clear H2 n0 H H0 H1.
cut (
forall m t, Plt m (Psucc p) ->
(forall i, Plt i m -> t ! i <> None) ->
(forall i c, t ! i = Some c -> P i c)
->
{t' : _ &
((forall i, Plt i (Psucc p) -> t' ! i <> None) *
forall i c, t' ! i = Some c -> P i c)%type}
).
intros.
apply (X 1%positive (@PTree.empty A)).
unfold Plt.
rewrite Psucc_Zsucc.
unfold Zsucc.
assert (Zpos p > 0) by (compute; trivial).
omega.
intros.
unfold Plt in H.
destruct i ; compute in H ; congruence.
intros.
rewrite PTree.gempty in H.
congruence.
induction m using (well_founded_induction_type (bounded_gt_wf (Psucc p))).
intros.
generalize (f H0 X0).
destruct 1.
assert (Ple (Psucc m) (Psucc p)).
unfold Plt in H.
unfold Ple.
repeat rewrite Psucc_Zsucc in *.
unfold Zsucc in *.
omega.
assert (forall i, Plt i (Psucc m) -> ((PTree.set m x t) ! i <> None)).
intros.
destruct (peq i m).
subst.
rewrite PTree.gss.
congruence.
rewrite PTree.gso.
apply H0.
unfold Plt in *.
rewrite Psucc_Zsucc in *.
unfold Zsucc in *.
assert (Zpos i <> Zpos m) by congruence.
omega.
assumption.
assert (forall i c, (PTree.set m x t) ! i = Some c -> P i c).
intros i c.
destruct (peq m i).
subst.
rewrite PTree.gss.
congruence.
rewrite PTree.gso.
auto.
auto.
destruct (peq m p).
subst.
exists (PTree.set p x t).
auto.
assert (Plt (Psucc m) (Psucc p)).
unfold Ple, Plt in *.
repeat rewrite Psucc_Zsucc in *.
unfold Zsucc in *.
assert (Zpos m <> Zpos p) by congruence.
omega.
assert (bounded_gt (Psucc p) (Psucc m) m).
constructor.
apply Plt_succ.
assumption.
eapply X.
eassumption.
assumption.
eassumption.
assumption.
Qed.

End Progressive.