Module LibMaps

Require Export Maps.
Require Import Coqlib.
Require Export LibPos.
Load Param.

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).
  intros ; omegaContradiction.
  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.