coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Logical implication between two identical forall

From: richard Dapoigny <richard.dapoigny AT univ-smb.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Logical implication between two identical forall
Date: Tue, 1 Oct 2019 00:14:59 +0200
Authentication-results: mail3-smtp-sop.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,

Assuming classical logic, i have the following goal:

∀ X0 Y0 : N,
(eta X0 Balls ∧ eta Y0 Balls ∧ eta B (el X0) ∧ eta X0 (ext A) ∧ eta B (el Y0) ∧ eta Y0 (ext A) → eta X0 (el Y0) ∨ eta Y0 (el X0))
→ ∀ X'0 Y'0 : N,
eta X'0 Balls ∧ eta Y'0 Balls ∧ eta B (el X'0) ∧ eta X'0 (ext A) ∧ eta B (el Y'0) ∧ eta Y'0 (ext A) → eta X'0 (el Y'0) ∨ eta Y'0 (el X'0)

since variables are dummy, I expect to solve it with classical tactics such as eauto, tauto, etc. However none of these seems to work. Is anybody has some hints?

Thanks for your help,

Richard

--
Richard Dapoigny
Associate Professor - LISTIC Laboratory
University Savoie Mont-Blanc
5, chemin de Bellevue
Po. Box 80439
Annecy-le-Vieux 74940
FRANCE
https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/

****** People who don't know history are condemned to repeat it. ******

[Coq-Club] Logical implication between two identical forall, richard Dapoigny, 10/01/2019
- Re: [Coq-Club] Logical implication between two identical forall, Gaëtan Gilbert, 10/01/2019
  - Re: [Coq-Club] Logical implication between two identical forall, richard Dapoigny, 10/01/2019
    - Re: [Coq-Club] Logical implication between two identical forall, Gaëtan Gilbert, 10/01/2019