The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

Yes you are right, it is a general pattern, and I use it for every function
for which I want to perform case analysis. I even wrote a small extension 
which
helps using such specifications automatically.
For instance, here are the specifications of the functions [choose]
and [min_elt]
in my typeclass-based version of FSets:

  Inductive choose_spec : option elt -> Prop :=
  | choose_spec_Some : forall x (Hin : In x s), choose_spec (Some x)
  | choose_Spec_None : forall (Hempty : Empty s), choose_spec None.
  Property choose_dec : choose_spec (choose s).

  Inductive min_elt_spec : option elt -> Prop :=
  | min_elt_spec_Some :
    forall x (Hin : In x s) (Hmin : forall y, In y s -> ~y <<< x),
      min_elt_spec (Some x)
  | min_elt_spec_None :
    forall (Hempty : Empty s), min_elt_spec None.
  Property min_elt_dec : min_elt_spec (min_elt s).

In your 'forallb' example, you are not taking the opportunity of using
the inductive
to already decompose existentials and conjunctions:

Inductive forallb_spec {A} (f: A -> bool) (ls: list A): bool -> Prop :=
| forallb_true: (forall x, In x ls -> f x = true) -> forallb_spec f ls true
| forallb_false: forall x, In x ls -> f x = false -> forallb_spec f ls false.

That's another story but I actually almost never use 'exists' if
there's more than one existential
quantifier, or if there is more than one condition following. An
inductive makes it easier to destruct
an hypothesis without using complex patterns and by giving meaningful
default names to the
different elements.

Back to the topic of this discussion: there's one condition one the
inductive specification
for this method to work flawlessly. The arguments of the function need
to be parameters
of the inductive, not indices, and only the result should be an index.
In other words, the
arguments should be variables in the type of each constructor,
otherwise [destruct] will lose
information, and using [inversion] is not really convenient (+
inversion lemmas are big and
introduce a lot of equalities that cant always be substituted). So for
instance, if you write
the function [oapply f ox] which applies f to an option, its spec should not 
be:

Inductive oapply_spec {A B} (f : A -> B) : option A -> option B -> Prop :=
| oapply_spec_None : oapply_spec f None None
| oapply_spec_Some : forall a, oapply_spec f (Some a) (Some (f a)).

but rather:

Inductive oapply_spec {A B} (f : A -> B) (oa : option A) : option B -> Prop :=
| oapply_spec_None : oa = None -> oapply_spec f oa None
| oapply_spec_Some : forall a, oa = Some a -> oapply_spec f oa (Some (f a)).

- Stéphane

2010/10/13 Aaron Bohannon 
<bohannon AT cis.upenn.edu>:
> Stéphane, thank you for your explanation!  I've also been inclined to
> separate programs and proofs, although I hadn't considered going as
> far as giving up the sumbool type.  I haven't really seen this "trick"
> before in Coq, but, if your argument is valid, then it sounds like
> this technique should be generally useful whenever you might want to
> do case analysis on the result of a function.  So if, for example, I
> wanted to write a program using "forallb" from the List library (and
> prove something about it), then I guess I might first want to define
> and prove the following:
>
> Inductive forallb_spec {A} (f: A -> bool) (ls: list A): bool -> Prop :=
> | forallb_true: (forall x, In x ls -> f x = true) -> forallb_spec f ls true
> | forallb_false: (exists x, In x ls /\ f x = false) -> forallb_spec f ls 
> false.
>
> Lemma forallb_obeys_spec: forall {A} (f: A -> bool) (ls: list A),
>  forallb_spec f ls (forallb f ls).
>
> I'll have to experiment with this a bit more to see exactly how much
> it simplifies things.
>
>  - Aaron
>
> 2010/10/12 Stéphane Lescuyer 
>Â <stephane.lescuyer AT polytechnique.org>:
>> Hi Aaron,
>>
>> Well I'm afraid there is no consensus about this issue, but is
>> there any consensus on any design issue in Coq ? :-) Here are
>> some of the considerations that make me think the version I
>> propose is "simpler" (in the sense of more convenient, more
>> practical, not in a logical sense).
>>
>> First, I strongly recommend the use of typeclasses (thus
>> discarding your option #1): as you notice it allows an overloaded
>> generic notation for all operations related to the considered
>> class, but it is just the tip of the iceberg. The big advantage
>> is the ability to declare generic instances of EqDec and let the
>> system automatically infer decidable equality for compound
>> types. For instance, you would write generic instances for
>> [option A], [A * B], [A + B], [list A], etc, based on instances
>> on [A] and [B], and you could then use complex types built with
>> these operators as types with a decidable equality. I wrote a
>> library of ordered types in that fashion and it's just invaluable
>> when programming in Coq (more or less your typical OCaml's
>> Pervasives.compare).
>>
>> Now that you are convinced (or so I hope :)) that using
>> typeclasses is the way to go, there remains to see what exactly
>> the EqDec class should be. Note that options #2 and #4 are
>> actually the same, it's just that #4 is more generalized but it
>> wouldn't make much difference in practice (only, you couldn't
>> write generic lemmas that would be true for Leibniz equality but
>> not for all setoid equalities). In the end, what we want that
>> class to provide is a function deciding the equality between two
>> elements, and a proof that that function is correct. Maybe the
>> most intuitive way of doing so is:
>>
>> Class EqDec (A : Type) := {
>>  equal : A -> A -> bool;
>>  equal_iff : forall x y, equal x y = true <-> x = y
>> }.
>>
>> Most people will then typically write two oriented lemmas
>> [equal_1] and [equal_2] instead of [equal_iff] because it's
>> easier to reason with. But not yet easy enough. If you have a
>> goal with an equality test [equal t u], it's tedious to perform
>> case analysis on the result of this test, you need to eliminate
>> it with something like [case_eq (equal t u)] in order to be able
>> to explicitely use the lemmas [equal_*] later. This is why,
>> instead of using a boolean test, people use a function returning
>> a proof as well:
>>
>> Class EqDec (A : Type) := {
>>  eq_dec : forall (x y : A), {x = y} + {x <> y}
>> }.
>>
>> Destructing [eq_dec t u] then does both case analysis in your
>> programs and adds the logical consequence of each case. But the
>> fact that reasoning is less cumbersome is really the only reason
>> to do that instead of using [equal] as above, because other than
>> that, having a function like [eq_dec] only raises more issues in
>> my opinion.
>>
>> Indeed, the less I mix proofs and programs, the more happy I
>> am :) Since [eq_dec] contains proofs, you will typically write it
>> in proof mode, which is not satisfactory: you cannot easily read
>> how the equality test is performed, and [Print]ing the definition
>> won't help much either. Unless you have taken extra care,
>> computing these tests will end up being slower than a purely
>> computational function. If it computes, that is, because we have
>> all experienced the dreadful "computation which never ends
>> because there must be a Qed somewhere instead of Defined but I
>> dont know where, it might even be down in the standard
>> library". Of course, you can discipline yourself into only
>> writing such functions in two steps, in the following way:
>>
>> Definition equal (x y : A) : bool := ...
>> Lemma equal_1 (x y : A) : equal x y = true -> x = y.
>> Lemma equal_2 (x y : A) : equal x y = false -> x <> y.
>> Definition eq_dec (x y : A) : {x = y} + {x <> y}.
>>  case_eq (equal x y); intro H.
>>  left; exact (equal_1 _ _ H).
>>  right; exact (equal_2 _ _ H).
>> Defined.
>>
>> but the truth is, if we were trusting our own discipline, we
>> wouldn't be using formal methods or Coq in the first
>> place... There were actually a lot of *_eq_dec or *_compare_dec
>> lemmas in the standard library which were not written in this way.
>> We think of the equality test (and use it) as a boolean function and
>> there is no reason to not implement it as a such just for the sake
>> of practical ease of reasoning.
>> For these reasons, I much prefer having a regular boolean
>> equality test, but the issue of easy reasoning by analysis
>> remains. This is why I define the inductive [equal_spec] as in
>> option #3:
>>
>> Inductive equal_spec {A} (x y : A) : bool -> Prop :=
>> | equal_true : forall (Heq: x = y), equal_spec x y true
>> | equal_false : forall (Hneq: x <> y), equal_spec x y false.
>> Class EqDec (A:Type) := {
>>  equal : A -> A -> bool;
>>  eq_dec : forall x y, equal_spec x y (equal x y)
>> }.
>>
>> and use it to specify the boolean equality test. By destructing a
>> term of type [equal_spec x y (equal x y)], you are, in one step,
>> destructing all occurrences of [equal x y] in your goal, and
>> getting the corresponding hypotheses added to your context in
>> each case. This is basically the exact same thing as performing
>> case analysis on the sumbool type in options #2,#4. I even name
>> hypotheses in the inductive definition so that they are always
>> introduced with 'predictable' names.
>>
>>  1 subgoal
>>  A : Type
>>  EqA : EqDec A
>>  x : A
>>  y : A
>>  H : equal x y = true
>> ======================
>>  x = y
>>> destruct (eq_dec x y).
>>
>>  2 subgoals
>>  A : Type
>>  EqA : EqDec A
>>  x : A
>>  y : A
>>  H : true = true
>>  Heq : x = y
>> ======================
>>  x = y
>>> assumption.
>>
>>  2 subgoals
>>  A : Type
>>  EqA : EqDec A
>>  x : A
>>  y : A
>>  H : false = true
>>  Hneq : x <> y
>> ======================
>>  x = y
>>> discriminate.
>>
>>  Proof completed.
>>
>> That's it, I've been verbose but I wanted to be as exhaustive and
>> clear as possible. I hope it helps you in deciding how you want
>> to define your decidable types.
>>
>> Stéphane
>>
>>
>> 2010/10/12 Aaron Bohannon 
>>Â <bohannon AT cis.upenn.edu>:
>>> Hi, I found your comment below intriguing, but I don't understand in
>>> what sense that method is "simpler".  What problem is it solving?  Is
>>> the problem specific to type classes?  If it's better, why wasn't it
>>> done this way in the standard library (i.e., in SetoidDec)?  I'm
>>> trying to understand what is the right way to define decidable
>>> equality on a bunch of types, and there seems to be four options now:
>>>
>>> 1) Don't use type classes at all (actually, not too painful, except
>>> for lack of convenient notation).
>>> 2) Use the naive EqDec type class definition that Alexandre described.
>>> 3) Use the EqDec type class definition below.
>>> 4) Use the definition in SetoidDec, applied to the trivial eq_setoid for 
>>> a type.
>>>
>>> Is there any consensus about this issue?
>>>
>>>  - Aaron
>>>
>>> 2010/10/1 Stéphane Lescuyer 
>>>Â <stephane.lescuyer AT polytechnique.org>:
>>>> PS : This is unrelated to your issue, but for the formalization of
>>>> your EqDec class, it's usually simpler to use a boolean test with an
>>>> inductive specification:
>>>> <<<
>>>> Inductive equal_spec {A} (x y : A) : bool -> Prop :=
>>>> | equal_true : x = y -> equal_spec x y true
>>>> | equal_false : x <> y -> equal_spec x y false.
>>>> Class EqDec (A:Type) := {
>>>>  equal : A -> A -> bool;
>>>>  eq_dec : forall x y, equal_spec x y (equal x y)
>>>> }.
>>>> Notation "x == y" := (equal x y) (at level 70, no associativity).
>>>>>>>
>>>> You have a pure equality test and you can perform case analysis for x
>>>> == y by calling "destruct (eq_dec x y)".
>>>
>>
>>
>>
>> --
>> I'm the kind of guy that until it happens, I won't worry about it. -
>> R.H. RoY05, MVP06
>>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06