The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

For the first proof, there seemed to be a number of equivalences in Coq.Logic.ClassicalFacts.  Is there a standard axiom to add for classical logic?

           - Ken

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
Sent: Tuesday, August 28, 2018 9:06:57 AM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] A couple of simple proofs.

 

The first one can't be proven, either add it as an axiom or live without it.

For the second one:

Theorem xverif: (forall q, q+1=3->q+1=4)<->False.
Proof.
   split.
   (* get rid of the False -> ... goal *)
   2:intros [].

   intros H.
   specialize H with 2. (* or pose proof (H 2) as H' then work with H' *)
   discriminate H.
   reflexivity.
Qed.

for instance

I don't know why you're trying with (q:=0), that won't give anything
interesting.

Gaëtan Gilbert

On 28/08/2018 18:00, Kenneth Roe wrote:
> How can I complete the following two proofs:
>
>
> Theorem bicond:
>
>    forall (x y :Prop), (x <-> y) -> x=y.
>
> Proof.
>
>    ...
>
> Qed.
>
>
> And the second proof:
>
>
> Theorem xverif: (forall q, q+1=3->q+1=4)=False.
>
> Proof.
>
>    eapply bicond.
>
>    split. intros.
>
>
>    elim H with (q := 0).
>
>    generalize H.
>
>    intros.
>
>    ...
>
> Qed.
>
>
> What gets filled in for the "..." in each of the above proofs?
>
>
>                    - Ken
>