## Coq's sumor Type

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.

| inleft : A -> A + {B}

| inright : B -> A + {B}

where "A + { B }" := (sumor A B) : type_scope.

Add Printing If sumor.

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

Set Implicit Arguments.

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

refine (fun n =>

match n with

| O => inright _ _

| S x => inleft _ x

end); intuition.

Defined.

In the standard library, usually, The type of

`sumor`comes with another funny type. For instance:
Require Peano_dec.

Check Peano_dec.O_or_S.

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.

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.

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

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.

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.

`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 "'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).

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`will be a function passing

*f*)*f*inside a

`sig`:

Notation "'Sig' 'map' f" :=

(fun x => match x with Sig yes x => Sig yes (f x) end)

(at level 42).

(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).

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`embellishes things like the last match-with in our previously implemented

*stuff*)`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).

(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 We will use

`List.find`-like functions, with their specifications.
Require Import List.

We define another proposition telling who/what is the A

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

forall b, nth_ok i l b = true /\ nth i l b = 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 }.

forall a b : A, { a = b } + { a <> b }.

And here is the first That was astonishingly easy.

The tactic

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

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.

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:

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.

forall before, before < i -> ~ (Nth_is l before a)

/\

Nth_is l i a.

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.

(forall before, before < i -> ~ (Nth_is l before a))

/\

Nth_is l i a.

Hint Unfold First_is_nth.

The implementation of

First, one thing to remember: when using

Second, there is a tricky subgoal which is not discharged by

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

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.

find_first_index Peano_dec.eq_nat_dec.

Eval compute in

(find_first_index_nat (42 :: 51 :: 69 :: 82 :: nil) 51).

(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).

(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).

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

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 There we build the

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

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.

*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.# Sebastien Mondet

**Menu:**

Site generated thanks to bracetax, camlmix, sebib, and more …

Updated on Sat, 10 Dec 2011 12:46:34 -0500.

Sebastien Mondet

Updated on Sat, 10 Dec 2011 12:46:34 -0500.

Sebastien Mondet