The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

Quite obviously there are sufficient conditions, for example it'd be enough that F is s.t. (exists y, F) <-> (forall y, F) is provable.

But let us note that in your test'  absolutely anything can be the consequent, including False:

Lemma test' : forall n, (forall m, m=0 /\ m=n) -> False.
Proof.
  intros n H. destruct n.
  - specialize (H 1). destruct H. discriminate.
  - specialize (H 0). destruct H. discriminate.
Qed.

On 12.05.19 18:40, richard Dapoigny wrote:

it seems it not true in general but in some cases, it is true :

Lemma test : forall n m, m=0 /\ m=n -> n=0.
Proof.
intros  n m H;destruct H;rewrite <-H0;assumption.
Qed.

Lemma test' : forall n, (forall m, m=0 /\ m=n) -> n=0.
Proof.
intros n H;specialize (H n);destruct H;assumption.
Qed.

so, is there a way to contain the case in which it true (i.e., a condition)?

Le 12/05/2019 à 17:22, Jeremy Dawson a écrit :

Would you expect it to hold?  Rather, isn't the appropriate equivalence 
in classical logic the following?

(forall x, ((exists y, F) -> G)) <-> forall x y, (F -> G)

Jeremy

On 05/13/2019 01:17 AM, richard Dapoigny wrote:

Dear all,

using classical logic in Coq, is there a way to prove that the following 
equivalence holds?

forall x, ((forall y, F) -> G) <-> forall x y, (F -> G)

in which F depends on x an y while G only depends on x

Thanks for your answer,

Rich

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

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