The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-smb.fr>]

Thanks a lot Fabian. Yes, it was a coercion problem and declaring the fonction ObjMan injective and modifying uniq_man as follows solves the problem:

Lemma uniq_man : ~(ObjMan Englishman = ObjMan Norwegian).
Proof.
unfold not;intro H. assert (H':Injective ObjMan).
- apply ObManInjective.
- unfold Injective in H';apply H' in H;change ((fun m:man => match m with | Englishman => True | _ => False end) Norwegian);rewrite <-H;trivial.
Qed.

---

From: "Fabian Kunze" <fabian.kunze AT cs.uni-saarland.de>
To: "coq-club" <coq-club AT inria.fr>
Sent: Samedi 12 Septembre 2020 15:23:20
Subject: Re: [Coq-Club] Problem with contradiction

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:

963504905.2848484.1599914732326.JavaMail.zimbra AT univ-smb.fr">

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