The Coq mailing list

[Fabian Kunze <fabian.kunze AT cs.uni-saarland.de>]

Hi Richard,

what I always do in that case is to enable the exlicit printing of the used coercions:

Set Printing Coercions. (Or even "Set Printing All.")

My assumption would be that either H0 or H3 does not talk about equality between man, but between object (did you explicetly use "eqobject" somewhere?). If H0 uses coercions, need that ObjMan is actually injective as an explicit assumption. If H3 uses the coercion, "congruence" should just be able to solve the goal.

Best,
Fabian

Am 9/12/2020 um 14:45 schrieb Richard Dapoigny:

Dear Coq users,

I have the following problem.

Using the following inductive type:

Inductive man : Type := | Englishman | Spaniard | Ukrainian | Norwegian | Japanese.

with the following coercion:

Parameter ObjMan : man -> object. Coercion ObjMan  : man >-> object.

with:

Parameter object : Type.
Definition eqobject := @Logic.eq object.

In a demonstration I have the two hypotheses:

H0 : Englishman = Norwegian
H3 : Englishman = Norwegian → False

for which the tactic "contradiction" outputs: No such contradiction

What is the problem here? the coercion?

Thanks for your help.

Richard