➲  Date: Wed, 31 Aug 2011 09:59:59 +0200; Tags: [ocaml; coq].

Today, let's investigate the sumbool type. This post follows the one on the sig type. It is also a Coq development available on-line. All the disclaimers still apply here (coq-beginner, nothing “new”, etc.).

It is defined in the Specif module. sumbool ‘is a boolean type equipped with the justification of their value’: Indeed, like bool and many other 2-constructors types it can use the “if ... then ... else ...” construct; with the Add Printing If it is also printed this way.

It is used everywhere in Coq's standard library. Just by importing standard lists, we get quite a bunch of decision procedures: The search gives about 100 lines of output. Let's have a closer look at one of them:

Compare_dec.zerop
     : forall n : nat, {n = 0} + {0 < n}

We can use it in programs:

= 69
: nat

and extraction works as expected:

(** val zerop : nat -> sumbool **)

let zerop = function
| O -> Left
| S n0 -> Right

Note that it can be made more practical:

(** val zerop : nat -> bool **)

let zerop = function
| O -> true
| S n0 -> false

In proofs, sumbool gives us something more: the “justifications”. Let's compare it with this classical bool version: If we are proving something (even stupid): There, we have a hypothesis in the context (i.e. as a Prop with Coq's default “=”):

  e : 42 = 0
  ============================
   51 = 69

So, that's easy. Whereas with bool_zerop: we don't have the knowledge:

  
  ============================
   51 = 69

It is not impossible (requires a remember, and then a few theorems) but much more tedious.

Before going further, let's add a few notations:

The common example is the decision about equality of natural numbers eq_nat_dec (also explained in CPDT). The fixpoint just compares the numbers like anyone would do. All the goals generated by refine are equalities and non-equalities, they can be solved by the congruence tactic which ‘is a decision procedure for ground equalities with uninterpreted symbols’.

Let's make a few tests:

= Decide_left
: {42 = 42} + {42 <> 42}

= Decide_right
: {42 = 51} + {42 <> 51}

and have a look at some OCaml code:

(** val eq_nat_dec : nat -> nat -> bool **)

let rec eq_nat_dec n m =
  match n with
  | O ->
    (match m with
     | O -> true
     | S n0 -> false)
  | S n' ->
    (match m with
     | O -> false
     | S m' -> eq_nat_dec n' m')

For automatically dealing with this kind of functions, there is a tactic called decide equality. It solves ‘a goal of the form forall x y:R, {x=y}+{~x=y}, where R is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types’: In this case, the code is as beautiful as before:

(** val eq_nat_autodec : nat -> nat -> bool **)

let rec eq_nat_autodec n m0 =
  match n with
  | O ->
    (match m0 with
     | O -> true
     | S n0 -> false)
  | S n0 ->
    (match m0 with
     | O -> false
     | S n1 -> eq_nat_autodec n0 n1)

Let's try to do something with the sumbool type … In the same time, we start exploring some stuff from the standard library: Ascii and String. It gives us where So, strings here are lists of 8-bits integers, lower bits on the left.

Let's write string_eq_dec, the equality between strings, using the lower-lever ascii_dec:

ascii_dec
     : forall a b : ascii, {a = b} + {a <> b}

Here one single decide equality does not seem to be enough, but repeating it gives something: The problem is that the repeat goes too far inside the Ascii characters. It gives an ugly piece of code comparing every single bit of Ascii character:

(** val string_eq_autodec : string -> string -> bool **)

let rec string_eq_autodec s sb0 =
  match s with
  | EmptyString ->
    (match sb0 with
     | EmptyString -> true
     | String (a, s0) -> false)
  | String (a, s0) ->
    (match sb0 with
     | EmptyString -> false
     | String (a0, s1) ->
       let Ascii (x, x0, x1, x2, x3, x4, x5, x6) = a in
       let Ascii (b7, b8, b9, b10, b11, b12, b13, b14) = a0 in
       (match x with
        | True ->
          (match b7 with
           | True ->
             (match x0 with
              | True ->
              
                  (* ... hundreds of lines ... *)

The hand-written one looks much better:

(** val string_eq_dec : string -> string -> bool **)

let rec string_eq_dec sa sb =
  match sa with
  | EmptyString ->
    (match sb with
     | EmptyString -> true
     | String (a, s) -> false)
  | String (ch_a, tl_a) ->
    (match sb with
     | EmptyString -> false
     | String (ch_b, tl_b) ->
       if ascii_dec ch_a ch_b then
         string_eq_dec tl_a tl_b
       else
         false)

We now try to specify and implement the lexicographic order on strings.

For the order on Ascii characters, we will use nat_of_ascii and then the order on naturals. There are a few theorems on that embedding:

ascii_nat_embedding
     : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a

nat_ascii_embedding
     : forall n : nat,
         n < 256 -> nat_of_ascii (ascii_of_nat n) = n

We first specify what it means for 2 strings to be in lexicographic order.

We add the 4 constructors to auto's database.

Let's check it with a few examples(Of course, it is by doing the examples that I got the inductive definition right little by little ;)) … ex_lex_03 made me fight a bit. Here is the first version: After forcing the unfolding of not,

• we invert all the hypotheses using our inductive proposition;
• we force the computation of the nat_of_ascii functions;
• we invert the (false) inequalities.

We use Time to see that this makes a lot of steps:

Proof completed.
Finished transaction in 1. secs (0.u,1.71174s)

The type-checking of the proof gets even worse:

ex_lex_03 is defined
Finished transaction in 8. secs (6.997937u,0.046993s)

The problem is the last repeated step, on the inequalities. Just remember, when we play with naturals, omega is our friend.

ex_lex_03' is defined
Finished transaction in 0. secs (0.040994u,0.s)

ex_lex_05 works like ex_lex_03:

That was the specification; now the implementation. We just give a name to the intended return type:

First, we will need this lemma about nat_of_ascii.

nat_of_ascii_injective is used to prove the following one, which will allow intuition auto to finish its job nicely:

And now is the definition of decide_lex_order. We use Compare_dec.lt_dec to compare naturals, it has a sumbool type too(Note that there is also lt_eq_lt_dec but we are not ready to use it for now (it is a sumbool embedded in a sumor, so, maybe another time :)).):

forall n m : nat, {n < m} + {~ n < m}

Just for the record, the following is how looked my first “Proof Complete” on that one. The idea is to explore with wild ugly tactics or inline lemmas, and then do the factorisation, cleaning, and optimisations. We can give it a try:

     = Decide_left
     : lexicographic_decision "AAA" "BBB"

     = Decide_left
     : lexicographic_decision "AAA" "ABB"
Finished transaction in 4. secs (0.u,3.544461s)

     = Decide_left
     : lexicographic_decision "AAA" "AAB"
Finished transaction in 9. secs (0.u,8.202753s)

     = Decide_right
     : lexicographic_decision "AA" "A"
Finished transaction in 13. secs (0.u,12.995024s)

The tactic vm_compute does not seem to improve the speed there. But anyway, the important performance-wise is the OCaml code, and it looks pretty good:

(** val decide_lex_order : 
      string -> string -> lexicographic_decision **)

let rec decide_lex_order a b =
  match a with
  | EmptyString -> true
  | String (c1, s1) ->
    (match b with
     | EmptyString -> false
     | String (c2, s2) ->
       if lt_dec (nat_of_ascii c1) (nat_of_ascii c2)
       then true
       else if lt_dec (nat_of_ascii c2) (nat_of_ascii c1)
            then false
            else decide_lex_order s1 s2)

Now we have subsets ({ _ : _ | _ }) and decisions ({ _ } + { _ }); next time we will try to play with the sumor type.

---

blog comments powered by Disqus