The Coq mailing list

[Kazuhiko Sakaguchi <pi8027 AT gmail.com>]

The first one is propositional extensionality:
https://coq.inria.fr/library/Coq.Logic.PropExtensionality.html

Kazuhiko
2018年8月29日(水) 2:15 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
> >