Library RelationAlgebra.positives

positives: basic facts about binary positive numbers

Require Export BinNums.
Require Import comparisons.

positives as a cmpType

Fixpoint eqb_pos i j :=
  match i,j with
    | xH,xHtrue
    | xI i,xI j | xO i, xO jeqb_pos i j
    | _,_false

Lemma eqb_pos_spec: i j, reflect (i=j) (eqb_pos i j).
Proof. induction i; intros [j|j|]; simpl; (try case IHi); constructor; congruence. Qed.

Fixpoint pos_compare i j :=
  match i,j with
    | xH, xHEq
    | xO i, xO j | xI i, xI jpos_compare i j
    | xH, _Lt
    | _, xHGt
    | xO _, _Lt
    | _,_Gt

Lemma pos_compare_spec: i j, compare_spec (i=j) (pos_compare i j).
Proof. induction i; destruct j; simpl; try case IHi; try constructor; congruence. Qed.

Canonical Structure cmp_pos := mk_cmp _ eqb_pos_spec _ pos_compare_spec.

positive maps (for making environments) we redefine such trees here rather than importing them from the standard library: since we do not need any proof about them, this avoids us a heavy Require Import
Section e.
Variable A: Type.
Inductive sigma := sigma_empty | N(l: sigma)(o: option A)(r: sigma).
Fixpoint sigma_get default m i :=
  match m with
    | N l o r
      match i with
        | xHmatch o with Nonedefault | Some aa end
        | xO isigma_get default l i
        | xI isigma_get default r i
    | _default
Fixpoint sigma_add i v m :=
    match m with
    | sigma_empty
        match i with
        | xHN sigma_empty (Some v) sigma_empty
        | xO iN (sigma_add i v sigma_empty) None sigma_empty
        | xI iN sigma_empty None (sigma_add i v sigma_empty)
    | N l o r
        match i with
        | xHN l (Some v) r
        | xO iN (sigma_add i v l) o r
        | xI iN l o (sigma_add i v r)
End e.