[Coq-Club] A couple of simple proofs.

[Kenneth Roe]

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

[Gaëtan Gilbert]

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

  forall (x y :Prop), (x <-> y) -> x=y.
Proof.
  ...
Qed.
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

[Kenneth Roe]

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-***@inria.fr <coq-club-***@inria.fr> on behalf of Gaëtan Gilbert <***@skyskimmer.net>
Sent: Tuesday, August 28, 2018 9:06:57 AM
To: coq-***@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

Post by Kenneth Roe
forall (x y :Prop), (x <-> y) -> x=y.
Proof.
...
Qed.
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

[Kazuhiko Sakaguchi]

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

Kazuhiko

Post by Kenneth Roe
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
________________________________
Sent: Tuesday, August 28, 2018 9:06:57 AM
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.
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

Post by Kenneth Roe
forall (x y :Prop), (x <-> y) -> x=y.
Proof.
...
Qed.
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