Stream: Coq users

Topic: Type inference with predicates

Tiara Sinlo (May 18 2024 at 20:56):

Hi, can someone explain what is going on here?

From Coq.Classes Require Import RelationClasses.

Fail Goal forall A (P Q : A -> Prop),
    predicate_equivalence P Q.

Goal forall A (P Q : A -> Prop),
    @predicate_equivalence (Tcons A Tnil) P Q.
Abort.

I would have thought A -> Prop is the simplest predicate there is? Ideally, I wanted to have some rewriting support for the predicates in functions like Forall:

Lemma Forall_wdP A (l : list A) :
  Proper (@predicate_equivalence (Tcons A Tnil) ==> iff) (fun P => Forall P l).

Gregory Malecha (May 23 2024 at 14:58):

You didn't say exactly what is going on. If you want to be able to rewrite under the binder of forall, you probably want an instance like the following:

Instance Forall_proper {T} : Proper (pointwise_relation T Basics.impl ==> eq ==> Basics.impl) (@Forall T).

(might be a typo).

Tiara Sinlo (May 23 2024 at 15:05):

The "inner" problem I was facing was that Coq doesn't recognize A -> Prop as a predicate:

In environment:
A : Type
P : A -> Prop
Q : A -> Prop
The term "P" has type "A -> Prop" while it is expected to have type "predicate ?l".

where P does have type predicate ?l with ?l = Tcons A Tnil
Which was strange to me since A -> Prop is what I think of first when I think about a "predicate". So I was wondering if I misunderstood what predicate is used for and how Coq type inference works.

I'm still a beginner at this, so sorry for the confusion.

Gregory Malecha (May 23 2024 at 15:21):

This is a pretty common issue in Coq. predicate is defined as a function so solving that problem requires Coq's unification algorithm to invert that function which it doesn't do well/does not try to do. I would suggest avoiding uses of predicate.

Last updated: Oct 13 2024 at 01:02 UTC