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

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

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.

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: Jun 22 2024 at 16:02 UTC