3

Given any programming language, whenever a standard library function exists, we should most likely use it rather than write our own code. One would think that this advice applies equally to Coq. However, I recently forced myself to use the same_relation predicate of the Relation module, and I am left with the feeling of being worse off. So I must be missing something, hence my question. To illustrate what I mean let us consider to possible relations:

Require Import Relations.      (* same_relation *)
Require Import Setoids.Setoid. (* seems to be needed for rewrite *)

Inductive rel1 {A:Type} : A -> A -> Prop :=
  | rel1_refl : forall x:A, rel1 x x.   (* for example *)

Inductive rel2 {A:Type} : A -> A -> Prop :=
  | rel2_refl : forall x:A, rel2 x x.   (* for example *)

The specific details of these relations do not matter here, as long as rel1 and rel2 are equivalent. Now, if I want to ignore the Coq library, I could simply state:

Lemma L1: forall (A:Type)(x y:A), rel1 x y <-> rel2 x y.
Proof.
  (* some proof *)
Qed.

and if I want to follow my instinct and use the Coq library:

Lemma L2: forall (A:Type), same_relation A rel1 rel2.
Proof.
  (* some proof *)
Qed.

In the simplest of cases, it seems that having proven lemma L1 or Lemma L2 is equally beneficial:

Lemma application1: forall (A:Type) (x y:A), 
  rel1 x y -> rel2 x y (* for example *)
Proof.
  intros A x y H. apply L1 (* or L2 *) . exact H.
Qed.

Whether I decide to use apply L1 or apply L2 makes no difference...

However in practice, we are likely to be faced with a more complicated goal:

Lemma application2: forall (A:Type) (x y:A) (p:Prop),
  p /\ rel1 x y -> p /\ rel2 x y.
Proof.
  intros A x y p H. rewrite <- L1. exact H.
Qed.

My point here is that replacing rewrite <- L1 by rewrite <- L2 will fail. This is also true of the previous example, but at least I was able to use apply rather than rewrite. I cannot use apply in this case (unless I go through the trouble of splitting my goal). So it seems that I have lost the convenience of using rewrite, if I only have Lemma L2.

Using rewrite on results which are an equivalence (not just an equality) is very convenient. It seems that wrapping an equivalence into the predicate same_relation takes away this convenience. Was I right to follow my instinct and force myself to use same_relation? More generally, is it so true that if a construct is defined in the standard Coq library, I should use it, rather than define my own version of it?

1 Answer 1

4

You pose two questions, I try to answer separately:

  • Regarding your rewrite problem, this problem is natural as the definition of same_relation goes as double inclusion. I agree that maybe a definition using iff would be more convenient. It would really depend on the kind of goals you have. A possible solution for your problem is to define a view:

    Lemma L1 {A:Type} {x y:A} : rel1 x y <-> rel2 x y.
    Proof.
    Admitted.
    
    Lemma L2 {A:Type} : same_relation A rel1 rel2.
    Proof.
    Admitted.
    
    Lemma U {T} {R1 R2 : relation T} :
      same_relation _ R1 R2 -> forall x y, R1 x y <-> R2 x y.
    Proof. now destruct 1; intros x y; split; auto. Qed.
    
    Lemma application2 {A:Type} {x y:A} {p:Prop} :
       p /\ rel1 x y -> p /\ rel2 x y.
    Proof. now rewrite (U L2). Qed.
    

    Note also that rewriting with a <-> relation is not really based on equality, but on "setoid rewriting". In fact, the following doesn't hold in Coq A <-> B -> A = B.

  • Regarding your second question, whether to use the Coq standard library is a highly subjective topic. I personally rarely use it, I prefer a different library called math-comp, but YMMV. Regarding relations, mathcomp is mostly specialized into boolean relations rel x y = x -> y -> bool, thus, equivalence is simply defined as equality, typically, given r1 r2 you'd write r1 =2 r2.

    IMHO in the end, such choices are highly dependent on your application domain.

[edit]: Note that the Relation library is dated:

Naive set theory in Coq. Coq V6.1. This work was started in July 1993 by F. Prost.

So indeed, it may not be the best modern base to build Coq developments on.

3
  • 1
    Thanks very much !! Jun 18, 2016 at 16:08
  • The Sets library (which contains Relation with capital R) was started in 1993. But the OP refers to the Relations library that contains relation (I don't know when it was started, though). Jun 19, 2016 at 13:52
  • I think Relations are a direct descendant of Sets but the svn history doesn't go as far in an easy way.
    – ejgallego
    Jun 19, 2016 at 18:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.