➲  Date: Sat, 10 Dec 2011 12:46:27 -0500; Tags: [ocaml; coq].

After the post on subsets (the sig type), and the one on decision procedures (the sumbool type)(and also after a few months moving to a new continent/country/city for a new job ;)), we now try to have a look at the sumor type. Again, this is a beginner's Coq development … feel free to criticise/correct/comment it.

sumor is also defined in the Specif module: And described as:

sumor is an option type equipped with the justification of why it may not be a regular value

Let's start with a simple case: pred_sumor returns a nat or a proof of nullity:

In the standard library, usually, sumor comes with another funny type. For instance:

Peano_dec.O_or_S
     : forall n : nat, {m : nat | S m = n} + {0 = n}

It is a sig inside a sumor. We can re-implement it with the same type: The type of pred_sumor_sig cannot be more expressive from an input/output point of view; it takes any natural and returns either a natural with a proof that it is the predecessor, or a proof that the input is zero.

Compare_dec.lt_eq_lt_dec
     : forall n m : nat, {n < m} + {n = m} + {m < n}

There, we have a sumbool inside a sumor. We can also re-implement it: Note the last match-with on the recursive call; it looks a bit silly but actually the underscores are filled differently by Coq and refine.

Let's check some OCaml code:

(** val lt_eq_lt_dec : nat -> nat -> sumbool sumor **)

let rec lt_eq_lt_dec n m =
  match n with
  | O ->
    (match m with
     | O -> Inleft Right
     | S n0 -> Inleft Left)
  | S pn ->
    (match m with
     | O -> Inright
     | S pm -> lt_eq_lt_dec pn pm)

Let's try to choose some notations for sig, sumbool, sumor, and their combinations.

(Sig map f) will be a function passing f inside a sig:

(Sumorbool propagate stuff) embellishes things like the last match-with in our previously implemented lt_eq_lt_dec:

Now we build two List.find-like functions, with their specifications. We will use

• nth: (nth i l d) returns the i-th element of l, or d in case of overflow.
• nth_ok: (nth i l d) returns true if there is no overflow.
• In: (In a l) is a Prop telling that a is an element of l.

We define another proposition telling who/what is the n-th element of a list: A Hint Unfold should help auto-based tactics:

We just give a name to the type of functions which decide equality on a given type:

And here is the first List.find. Given a list A, an element and an equality decision function, it returns either a natural which is the index at which the element was found, or a proof that the element is absent from the list: That was astonishingly easy.
The tactic intuition gets rid of all the true subgoals, the last False one just requires one inversion.

I tried to add mistakes to persuade myself … for instance, I replaced Sumor left (Sig yes 0) by Sumor right or by Sumor left (Sig yes 1), and, indeed, the proof was impossible in these cases (for instance, you may end up having to prove False without any contradiction in the hypotheses, etc.).

That was nice but this implementation can be used for an even more precise type: we can say that the index found is the one of the first element matching.

My first attempt at a specification got stuck in the mud because of an operator precedence problem: With parentheses it is much better:

The implementation of find_one_index has the same function body, but a more tedious proof.
First, one thing to remember: when using destruct or induction after the definition of a fixpoint, it is useful to remove the recursive call with a clear frec(The problem is that the thing deconstructed is also deconstructed inside the fixpoint, which is then kind of not equal to itself … you get a “Proof Completed” and then it breaks while type checking. See also the comments of bug 2558.).
Second, there is a tricky subgoal which is not discharged by intuition or inversion; I did not manage to clean that yet: it is bad proof which depends on the order of subgoals and references Coq-generated variable names (like H2, H3, x0, etc.).

Let's test find_first_index with lists of naturals:

Peano_dec.eq_nat_dec
     : forall n m : nat, {n = m} + {n <> m}

= Sumor left (Sig yes 1)
: {ia : nat | First_is_nth (42 :: 51 :: 69 :: 82 :: nil) ia 51} +
 {~ In 51 (42 :: 51 :: 69 :: 82 :: nil)}

= Sumor left (Sig yes 3)
: {ia : nat | First_is_nth (42 :: 51 :: 69 :: 82 :: nil) ia 82} +
 {~ In 82 (42 :: 51 :: 69 :: 82 :: nil)}
Finished transaction in 9. secs (0.u,9.163606s)

= Sumorright
: {ia : nat | First_is_nth (42 :: 51 :: 69 :: 82 :: nil) ia 666} +
 {~ In 666 (42 :: 51 :: 69 :: 82 :: nil)}
Finished transaction in 1. secs (0.u,0.636903s)

With a few Extract Inductive commands, the OCaml code is still quite pretty:

type nat =
| O
| S of nat

type 'a sig0 =
  'a
  (* singleton inductive, whose constructor was exist *)

type 'a eq_decision = 'a -> 'a -> bool

(** val find_first_index :
    'a1 eq_decision -> 'a1 list -> 'a1 -> nat option **)

let rec find_first_index eq_dec l a =
  match l with
  | [] -> None
  | h::t ->
    if eq_dec h a
    then Some O
    else (match find_first_index eq_dec t a with
          | Some ex -> Some (S ex)
          | None -> None)

Note that of course, without an .mli file, OCaml then infers a more permissive type:

val find_first_index :
  ('a -> 'b -> bool) -> 'a list -> 'b -> nat option

We make a three-options decision function ({ _ } + { _ } + { _ }) on the 31-bit integers of the standard library.

We will wrap fancy types around the existing comparison function:

compare31 = 
fun n m : int31 => (phi n ?= phi m)%Z
     : int31 -> int31 -> comparison

Argument scopes are [int31_scope int31_scope]

where

Inductive comparison : Set :=
    Eq : comparison | Lt : comparison | Gt : comparison

There is no algorithm per se, but we can learn a bit more to hack the construction of a function with tactics: There we build the match-with by matching the goal and then using refine in each case. Finally, the OCaml is simple and stupid:

(** val int31_comparison : int31 -> int31 -> bool option **)

let int31_comparison a b =
  let cab = compare31 a b in
  (match cab with
   | Eq -> Some false
   | Lt -> Some true
   | Gt -> None)

That's all for now with the sumors … With sig, sumbool, and sumor, I guess we can express almost anything useful, but as Adam Chlipala says we have only ‘scratched the tip of the iceberg’ … so, we'll continue digging in the following episodes.

---

blog comments powered by Disqus