The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Cool!  Thanks for observing that I didn't need "exists" in that
definition.  And I had a suspicion that it is important for the
function arguments to be parameters of the inductive definition.

 - Aaron

2010/10/13 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
>