Module FiniteMaps

Require Import Coqlib.
Require Import Maps.

Section FINITE.

Variable A: Type.

Lemma ptree_finite:
  forall (t: PTree.t A), exists p, forall n, (p <= n)%positive -> PTree.get n t = None.

Lemma ptree_finite_type:
  forall (t: PTree.t A), {p:positive & forall n, (p <= n)%positive -> PTree.get n t = None}.

Lemma pmap_finite:
  forall (m: PMap.t A), exists p, forall n, (p <= n)%positive -> PMap.get n m = fst m.

Lemma pmap_finite_type:
  forall (m: PMap.t A), { p: positive & forall n, (p <= n)%positive -> PMap.get n m = fst m}.

Lemma pmap_construct:
  forall (f: positive -> A) hi dfl,
  (forall n, (n >= hi)%positive -> f n = dfl) ->
  exists m: PMap.t A, forall n, PMap.get n m = f n.

Lemma zmap_finite:
  forall (m: ZMap.t A), exists lo, exists hi, forall n, n < lo \/ n > hi -> ZMap.get n m = fst m.

Lemma zmap_finite_type:
  forall (m: ZMap.t A),
  {lo : Z & { hi: Z & forall n, n < lo \/ n > hi -> ZMap.get n m = fst m }}.

Require Import Zwf.

Lemma zmap_construct:
  forall (f: Z -> A) lo hi dfl,
  (forall n, n < lo \/ n > hi -> f n = dfl) ->
  exists m: ZMap.t A, forall n, ZMap.get n m = f n.

Lemma zmap_construct_type:
  forall (f: Z -> A) lo hi dfl,
  (forall n, n < lo \/ n > hi -> f n = dfl) ->
  sigT (fun (m:ZMap.t A) => forall n, ZMap.get n m = f n).

End FINITE.




Section FINITE_CONSTRUCTIVE.

Variable A: Type.

Fixpoint p_tree_finite_c (t: PTree.t A) : positive :=
  match t with
    PTree.Leaf => 1%positive
  | PTree.Node l _ r => Pos.max (xO (p_tree_finite_c l)) (xI (p_tree_finite_c r))
  end.

Lemma ptree_finite_c_sound:
  forall (t: PTree.t A) n, ((p_tree_finite_c t) <= n)%positive -> PTree.get n t = None.

Definition pmap_finite_c (m: PMap.t A) : positive :=
           p_tree_finite_c (snd m).

Lemma pmap_finite_sound_c:
  forall (m: PMap.t A) n, ((pmap_finite_c m) <= n)%positive -> PMap.get n m = fst m.

Definition REC_p (f: positive -> A) (hi:positive) (dfl:A)
  (OUTSIDE: forall n, (n >= hi)%positive -> f n = dfl):
 forall x, (x <= hi)%positive ->
   {m: PMap.t A | fst m = dfl /\
                  forall n, (n < x \/ n >= hi)%positive ->
                            PMap.get n m = f n}.

Definition pmap_construct_c
          (f: positive -> A) hi dfl
          (OUTSIDE: forall n, (n >= hi)%positive -> f n = dfl):
   {m: PMap.t A | fst m = dfl /\
                  forall n, PMap.get n m = f n}.

Definition REC_d (f: positive -> A) (hi:positive) (dfl:positive -> A)
  (OUTSIDE: forall n, (n >= hi)%positive -> f n = dfl hi):
 forall x, (x <= hi)%positive ->
   {m: PMap.t A | fst m = (dfl hi) /\
                  forall n, (n < x \/ n >= hi)%positive ->
                            PMap.get n m = f n}.

Definition pmap_construct_dep
          (f: positive -> A) hi (dfl : positive -> A)
          (OUTSIDE: forall n, (n >= hi)%positive -> f n = dfl hi):
   {m: PMap.t A | fst m = dfl hi /\
                  forall n, PMap.get n m = f n}.

Definition zmap_finite_c (m: ZMap.t A): Z * Z :=
  (-2 * Z.pos (pmap_finite_c m), 2 * Z.pos (pmap_finite_c m)).

Lemma zmap_finite_sound_c:
  forall (m: ZMap.t A) lo hi, zmap_finite_c m = (lo,hi) ->
    forall n, n < lo \/ n > hi -> ZMap.get n m = fst m.

Definition REC (f: Z -> A) (lo hi:Z) (dfl:A)
  (OUTSIDE: forall n, n < lo \/ n > hi -> f n = dfl):
 forall x,
  x <= hi -> {m: ZMap.t A | fst m = dfl /\ forall n, n <= x \/ n > hi -> ZMap.get n m = f n}.
intros x0; pattern x0.
apply (well_founded_induction_type (Zwf_well_founded lo)); intros.
    destruct (zlt x lo).
  -
     exists (ZMap.init dfl).
      split. reflexivity.
      intros. rewrite ZMap.gi.
              symmetry. apply OUTSIDE. omega.
  -
    destruct (X (x - 1)) as [m [Pdef P]].
    red. omega. omega.
    exists (ZMap.set x (f x) m); intros.
    simpl.
    split; trivial.
    intros. rewrite ZMap.gsspec. unfold ZIndexed.eq.
    destruct (zeq n x).
           congruence.
           apply P. omega.
Defined.