Stream: Coq users

Topic: Error with conj and partial application

Julien Puydt (Aug 13 2021 at 07:17):

I really, really don't get why conj gives me an error, while a similar result works:

Lemma my_conj: forall A B: Prop, A -> B -> A /\ B.
Proof.
  intuition.
Qed.

Variable P: Prop.

Check my_conj. (* forall A B : Prop, A -> B -> A /\ B *)
Check my_conj P. (* forall B : Prop, P -> B -> P /\ B *)

Check conj. (* forall A B : Prop, A -> B -> A /\ B *)
Check conj P. (* The term "P" has type "Prop" while it is expected to have type
"?A" *)

Gaëtan Gilbert (Aug 13 2021 at 08:10):

conj has non-maximal implicit arguments https://coq.github.io/doc/master/refman/language/extensions/implicit-arguments.html#maximal-and-non-maximal-insertion-of-implicit-arguments

Julien Puydt (Aug 13 2021 at 09:54):

Gaëtan Gilbert said:

conj has non-maximal implicit arguments https://coq.github.io/doc/master/refman/language/extensions/implicit-arguments.html#maximal-and-non-maximal-insertion-of-implicit-arguments

Indeed using Check @conj P works ; but honestly the error message is unhelpful : I would never have found it by myself.

Thanks!

Gaëtan Gilbert (Aug 13 2021 at 09:57):

what version of coq are you using? for me the error also says (unable to find a well-typed instantiation for "?A": cannot ensure that "Type" is a subtype of "Prop").

Julien Puydt (Aug 13 2021 at 10:03):

Gaëtan Gilbert said:

what version of coq are you using? for me the error also says (unable to find a well-typed instantiation for "?A": cannot ensure that "Type" is a subtype of "Prop").

I only quoted part of the message ; I have 8.12.0 on the computer and 8.13.2 in jsCoq's scratchpad.

Paolo Giarrusso (Aug 13 2021 at 23:18):

Julien Puydt said:

but honestly the error message is unhelpful : I would never have found it by myself.

Things could be better, but as a trick: beyond Check conj., consider About conj.:

conj : ∀ A B : Prop, A → B → A ∧ B

conj is not universe polymorphic
Arguments conj [A B]%type_scope _ _
Expands to: Constructor Coq.Init.Logic.conj

The output encodes quite some useful information; Arguments conj [A B]... encodes the fact those arguments are non-maximal implicits — using actual Coq syntax! While not easy, learning to read this output is invaluable.

Last updated: Sep 26 2023 at 13:01 UTC