# 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
end.

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
end.

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
end
| _default
end.
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)
end
| 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
end.
End e.