coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Pattern Matching on False

From: Miroslav Dobsicek <m.dobsicek AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about Pattern Matching on False
Date: Thu, 13 Apr 2017 10:40:40 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=m.dobsicek AT gmail.com; spf=Pass smtp.mailfrom=m.dobsicek AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f47.google.com
Ironport-phdr: 9a23:dzN3chIZCA5jGnI2INmcpTZWNBhigK39O0sv0rFitYgRKfTxwZ3uMQTl6Ol3ixeRBMOAuq4C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwpFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNxzJXZYJ2XOfdkYq/RYd0XSGhHU81MVyJBGIS8b44XAuQGPOZYtY79p0AKrRSkGwmnGe3hyjhTiX/t3K01z/ouEQLb1wEnGtICqmnbrNLuO6cJUOC60LfHzTbYYvNZ3Dfy8onIchQ7rf6QWrJwdNPcxE8yHA3GllWdsY7oMjyP2ugQrWSW7/BsWOGxh2I9pAx8oCCjytovh4TKnI4Z107I+TljzIorONG1SVR3bcO5HJZWqiqULZF5Qtk4TGFtoCs6yqMJuZq8fCUSzZQo3R/fa/ief4mG5xLvSP+dITl3iX9nYr6/iBGy8U+vyu34SMa4ykpFri1AktXUt3AN0QLc6tSfR/Z/8UqtwyuD2x7T5+1eIk04i7DXJpEjz7Iok5ocq0XDHiv4mEXsi6+Wc10p+u2y5+v6ZbXpvYScN45ohQ7gMaQjgcO/AeEiPQgPW2iX4/iz1Lrm/UHhWrVFkuU2krXFsJDdPckUuqm5AxZM3ok/7xa/Eiyp3c8DnXgHKVJFYAiIg5LoO1HIOvD4DO2wj06ikDdxlLj6OejqBYyIJXzemp/ge6x84ghS0lkd19dasrdVELYaJPvtEmP2vsfZBRI6e1ixhergAs583Y4dcW2KC66ddqjVtAnbtaoUP+CQadpN637GIP8/6qu2gA==

Hi Zheng,

you have probably heard that "if you happen to have f:False then anything follows".
In the same vein, f:False can be matched with anything.

Definition test_False_match (f:False) :=
match f with
| _ => true
end.

Check test_False_match.

Best,
Miroslav

On 2017-04-13 09:01, zheng yang wrote:

Hi all,

I am a fresh user of Coq, and I have a question.
I find that the following definition typecheck in Coq:

Parameter x : Set.
Definition false_rect (n : nat) (f : False) : nat :=
match f return nat with | x => O end.

And it is allowed in Coq. However, False does not has any constructor.
Why does it work?

[Coq-Club] Question about Pattern Matching on False, zheng yang, 04/13/2017
- Re: [Coq-Club] Question about Pattern Matching on False, Anton Trunov, 04/13/2017
  - Re: [Coq-Club] Question about Pattern Matching on False, zheng yang, 04/14/2017
- Re: [Coq-Club] Question about Pattern Matching on False, Théo Zimmermann, 04/13/2017
  - Re: [Coq-Club] Question about Pattern Matching on False, zheng yang, 04/14/2017
- Re: [Coq-Club] Question about Pattern Matching on False, Miroslav Dobsicek, 04/13/2017
  - Re: [Coq-Club] Question about Pattern Matching on False, zheng yang, 04/14/2017