The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

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