Coq's sumor Type

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

The sumor Type

sumor is also defined in the Specif module:
Inductive sumor (A:Type) (B:Prop) : Type :=
  | inleft : A -> A + {B}
  | inright : B -> A + {B}
 where "A + { B }" := (sumor A B) : type_scope.

Add Printing If sumor.
And described as:
sumor is an option type equipped with the justification of why it may not be a regular value
Set Implicit Arguments.
Let's start with a simple case: pred_sumor returns a nat or a proof of nullity:
Definition pred_sumor: forall n, nat + { n = 0 }.
refine (fun n =>
  match n with
    | O => inright _ _
    | S x => inleft _ x
  end); intuition.
Defined.
In the standard library, usually, sumor comes with another funny type. For instance:
Require Peano_dec.
Check Peano_dec.O_or_S.
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:
Definition pred_sumor_sig:
  forall n, { m : nat | S m = n } + { n = 0 }.
refine (fun n =>
  match n with
    | O => inright _ _
    | S x => inleft _ (exist _ x _)
  end); intuition.
Defined.
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.
Require Compare_dec.
Check Compare_dec.lt_eq_lt_dec.
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:
Require Omega.

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

refine (fix frec n m : {n < m} + {n = m} + {m < n} :=
  match n, m with
    | O, O => inleft _ (right _ _)
    | O, S _ => inleft _ (left _ _)
    | S _, O => inright _ _
    | S pn, S pm =>
      match frec pn pm with
        | inleft (left _) => inleft _ (left _ _)
        | inleft (right _) => inleft _ (right _ _)
        | inright _ => inright _ _
      end
  end
); omega.
Defined.
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:
Extraction lt_eq_lt_dec.
(** 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)

Notations

Let's try to choose some notations for sig, sumbool, sumor, and their combinations.
Notation "'Sumbool' 'left'" := (left _ _) (at level 42).
Notation "'Sumbool' 'right'" := (right _ _) (at level 42).
Notation "'Sumbool' 'reduce' x" :=
  (if x then Sumbool left else Sumbool right) (at level 42).
Notation "'Sig' 'no'" := (False_rec _ _) (at level 42).
Notation "'Sig' 'yes' e" := (exist _ e _) (at level 42).
Notation "'Sig' 'take' e" :=
  (match e with Sig yes ex => ex end) (at level 42).
(Sig map f) will be a function passing f inside a sig:
Notation "'Sig' 'map' f" :=
  (fun x => match x with Sig yes x => Sig yes (f x) end)
  (at level 42).
Notation "'Sumor' 'left' x " := (inleft _ x) (at level 42).
Notation "'Sumor' 'right'" := (inright _ _) (at level 42).
Notation "'Sumor' 'map' f 'in' x" :=
  (match x with
     | Sumor left ex => Sumor left (f ex)
     | Sumor right => Sumor right end) (at level 42).
(Sumorbool propagate stuff) embellishes things like the last match-with in our previously implemented lt_eq_lt_dec:
Notation "'Sumorbool' 'propagate' x" :=
  (match x with
     | Sumor left (Sumbool left) => Sumor left (Sumbool left)
     | Sumor left (Sumbool right) => Sumor left (Sumbool right)
     | Sumor right => Sumor right
   end) (at level 42).

Two Functions Like List.find

Now we build two List.find-like functions, with their specifications.
Require Import List.
We will use
We define another proposition telling who/what is the n-th element of a list:
Definition Nth_is A (l : list A) (i : nat) (a : A) : Prop :=
  forall b, nth_ok i l b = true /\ nth i l b = a.
A Hint Unfold should help auto-based tactics:
Hint Unfold Nth_is.
We just give a name to the type of functions which decide equality on a given type:
Definition Eq_decision A :=
  forall a b : A, { a = b } + { a <> b }.
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:
Definition find_one_index A (eq_dec: Eq_decision A):
  forall (l : list A) (a : A),
    { ia : nat | Nth_is l ia a } + { ~ In a l }.

refine (fix frec l a :
  { ia : nat | Nth_is l ia a } + { ~ In a l } :=
  match l with
    | nil => Sumor right
    | cons h t =>
      match eq_dec h a with
        | Sumbool left => Sumor left (Sig yes 0)
        | Sumbool right =>
          Sumor map (Sig map S) in (frec t a)
      end
  end);
  intuition;
  try match goal with | H: In _ _ |- False =>
        inversion H; intuition
      end.
Defined.
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:
Definition First_is_nth_wrong A (l : list A) (i : nat) (a : A) :=
    forall before, before < i -> ~ (Nth_is l before a)
    /\
    Nth_is l i a.
With parentheses it is much better:
Definition First_is_nth A (l : list A) (i : nat) (a : A) :=
    (forall before, before < i -> ~ (Nth_is l before a))
    /\
    Nth_is l i a.
Hint Unfold First_is_nth.
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.).
Definition find_first_index A (eq_dec: Eq_decision A):
  forall (l : list A) (a : A),
    { ia : nat | First_is_nth l ia a } + { ~ In a l }.
refine (fix frec l a :
  { ia : nat | First_is_nth l ia a } + { ~ In a l } :=
  match l with
    | nil => Sumor right
    | cons h t =>
      match eq_dec h a with
        | Sumbool left => Sumor left (Sig yes 0)
        | Sumbool right =>
          Sumor map (Sig map S) in (frec t a)
      end
  end
); clear frec; (* we need to remove frec from the context *)
unfold First_is_nth in *; unfold Nth_is in *;
intuition;
try match goal with | H: In _ _ |- False =>
      inversion H; intuition
    end;
try match goal with H: _ < 0 |- _ => inversion H end.
(* The tricky goal: *)
destruct before.
(* case 0 *)
  assert (nth 0 (h :: t) h = a) as first_is_a. apply (H2 h).
  simpl in first_is_a. intuition.
(* case S *)
  assert (before < x0) as before_lt_x0. omega.
  simpl in H2.
  apply H in before_lt_x0. auto.
  auto.
Defined.
Let's test find_first_index with lists of naturals:
Check Peano_dec.eq_nat_dec.
Peano_dec.eq_nat_dec
     : forall n m : nat, {n = m} + {n <> m}
Definition find_first_index_nat :=
  find_first_index Peano_dec.eq_nat_dec.
Eval compute in
  (find_first_index_nat (42 :: 51 :: 69 :: 82 :: nil) 51).
= Sumor left (Sig yes 1)
: {ia : nat | First_is_nth (42 :: 51 :: 69 :: 82 :: nil) ia 51} +
 {~ In 51 (42 :: 51 :: 69 :: 82 :: nil)}
Time Eval compute in
  (find_first_index_nat (42 :: 51 :: 69 :: 82 :: nil) 82).
= 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)
Time Eval compute in
  (find_first_index_nat (42 :: 51 :: 69 :: 82 :: nil) 666).
= 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:
Extract Inductive sumbool => "bool" ["true" "false"].
Extract Inductive sumor => "option" ["Some" "None"].
Extract Inductive list => "list" ["[]" "(::)"].
Recursive Extraction find_first_index.
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

Embedding a Comparison For 31-bit Integers

We make a three-options decision function ({ _ } + { _ } + { _ }) on the 31-bit integers of the standard library.
Require Import Int31.
We will wrap fancy types around the existing comparison function:
Print compare31.
compare31 = 
fun n m : int31 => (phi n ?= phi m)%Z
     : int31 -> int31 -> comparison

Argument scopes are [int31_scope int31_scope]
where
Print comparison.
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:
Definition int31_comparison:
  forall (a b : int31),
    { compare31 a b = Lt } +
    { compare31 a b = Eq } +
    { compare31 a b = Gt }.
Proof.
  intros.
  remember (compare31 a b) as cab.
  destruct cab;
  repeat match goal with
           | H: Lt = _ |- _ =>
             refine (Sumor left (Sumbool left))
           | H: Eq = _ |- _ =>
             refine (Sumor left (Sumbool right))
           | H: Gt = _ |- _ =>
             refine (Sumor right)
         end;
  auto.
Defined.
There we build the match-with by matching the goal and then using refine in each case. Finally, the OCaml is simple and stupid:
Extraction int31_comparison.
(** 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)

Conclusion

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

Sebastien Mondet


Menu:




Site generated thanks to bracetax, camlmix, sebib, and more …
Updated on Sat, 10 Dec 2011 12:46:34 -0500.
Sebastien Mondet

Powered by Caml