coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Richard Dapoigny <richard.dapoigny AT univ-smb.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Problem with contradiction
Date: Sat, 12 Sep 2020 14:45:32 +0200 (CEST)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout01-ext1.partage.renater.fr

Dear Coq users,

I have the following problem.

Using the following inductive type:

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

[Coq-Club] [CFP] JFLA'2021, Yann Régis-Gianas, 09/11/2020
- [Coq-Club] Problem with contradiction, Richard Dapoigny, 09/12/2020
  - Re: [Coq-Club] Problem with contradiction, Fabian Kunze, 09/12/2020
    - Re: [Coq-Club] Problem with contradiction, Richard Dapoigny, 09/12/2020