coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A couple of simple proofs.

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] A couple of simple proofs.
Date: Tue, 28 Aug 2018 16:00:04 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-CO1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:PrvcpByROkWyN+/XCy+O+j09IxM/srCxBDY+r6Qd1O0SIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMNsg61WuwiuqwBjz4POfI2ZKOdyc6XAdt0aX2pBWcNRWjREDIyiaYsPCfQOPfpYr4Lgu1UOqgWxDhSrCePs1DBIgGL53bc90+s/CgzG3AsgH84LsHvOrdX1ML0eXvyyzKnN1DjOae5d1zTl6IXQfR0tveuAULZufcbLy0QjDQfIg1uIpYzrITyY1fgBvm2e4uduSe2ijm0qpBxvrjexw8ohhIbEi4ELxV3B+ih23ps6KN2+RUVme9CrCoFQuDufN4ZuQsMtXWVouCEix7MepZO1ezQGxZo+yxPBcvKLbpGE4hX4W+mPOzt4g29leK6kiBa17EigzPDzWtOs0FZQqSpFjsfDuWwR1xzS7ciHTOFx/kC82TaT0wDT7eZEIUMumaXHLJ4hx6Y8lpsVsUvdAi/7gEr7gLOMekgg5OSk8ebqbq/iq5KSL4N0jxvxMqUqmsyxG+Q4NQ0OUnCY+eui0r3s4Ff5QLJUgfAtkqnZt4zaJcEBqa64Bw9ZyJos6xG6Dzu+ytQXgWEHLE5ZeBKAl4XmJ1bOIOnhAfijh1SsjSxkyuvdPrzhB5XNNmLMnK3gfbZ78U5cyRA8wcpR55JOWfk9J6fYXVa0n9jFBFdtOAuthu3jFd9V14UEWGvJDLXPY43Itlrdxe8pJeSQZMcvvzu1f/so4fL0inIRmVgBeKCo2d0cb3XuTacuGFmQfXe52oRJKmwNpAdrFLW72m3HaiZaYjOJZ4x54zg6DIy8CoKaHdKth6CE1Sa/WJZRYzIfUwzeITLTb4yBHsw0RmeKOMY4yW4EUqSkQo4lkxqpsV2ikuc1Hq/v4iQd8Knb+p116unUyU5g0xVRV5/Y+EbUCmZ+kyUPWiM82715rQpl0FCf3KNkgvteU9tO+/dOVQR8PpnZnbV3

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

[Coq-Club] A couple of simple proofs., Kenneth Roe, 08/28/2018
- Re: [Coq-Club] A couple of simple proofs., Gaëtan Gilbert, 08/28/2018
  - Re: [Coq-Club] A couple of simple proofs., Kenneth Roe, 08/28/2018
    - Re: [Coq-Club] A couple of simple proofs., Kazuhiko Sakaguchi, 08/30/2018