# Library FingerTree.DigitModule

## Digits

Section Digit.
Variable A : Type.

A digit is simply a buffer of one to four values.

Inductive digit : Type :=
| One : A -> digit
| Two : A -> A -> digit
| Three : A -> A -> A -> digit
| Four : A -> A -> A -> A -> digit.

We build simple functional predicates on digits for use in specifications.

Definition full (x : digit) :=
match x with Four _ _ _ _ => True | _ => False end.

We now define addition of an element to the left of a digit.

Program Definition add_digit_left (a : A)
(d : digit | ~ full d) : digit :=
match d with
| One x => Two a x
| Two x y => Three a x y
| Three x y z => Four a x y z
| Four _ _ _ _ => !
end.

It has become a little more interesting here, as we define our first function. We can add to a digit if and only if it is not already full. So, we require the argument digit to be accompanied by a proof that it is not full. We will use it to prove that the last branch is inaccessible ; we use the notation ! ('bang') to denote inaccessible program points, which are points where False can be proved. Note that we can pattern-match on d as if it was just a digit: properties have no influence on code, only on proofs.

The generated obligation (figure \ref{fig:}) is easily solved, as we have a contradiction in the context: both ~ full d and d = Four _ _ _ _ are present. We can define in a similar fashion addition on the right and the various accessors on digits (head, tail, last and liat). From now on we will omit the proof scripts used to solve obligations.

Next Obligation.
intros ; simpl in H ; auto.
Qed.