coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about Pattern Matching on False
Date: Thu, 13 Apr 2017 08:12:27 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
Ironport-phdr: 9a23:Kc5JeR14tMTgk3j8smDT+DRfVm0co7zxezQtwd8Zse0WIvad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLnhykHODw5/m/ZicJ+kbxVrw66qhNl34LZepuYOOZicq7fe94RWGpPXtxWVyxEGo6ycYsPCPAGPelArIb9pl4OrR6gCgm2AePg0DlIhnnr1qA9z+QhER/J3As6E9MPsXTUqdD1NKYJXOC6yanH1zTDb/dM1Tjh74jIdwksrPeRVrxzacrc0VcjGx/Bg1mKqoHoPymZ2voQv2Wa9eZsSOGih3AhpgpsuDag3N0shZPMho8NylDL6yF5wIEtKN29UkF7YNqkHIJJtyGGK4d6W80iT3xrtSok0LEGtpm7fC8FyJQj2RHTceCIc4+N4h77VeaRJyl3hG59db6hmxq/9VKsx+78W8WuzlpGsytInsPRun0OyRDf8s2HReF8/kel1zaPzQfT6uRcLEAolarUNZkhzqQxl5oStETDGy72lV75jK+TbEok++yo5/77bbXho5+QL5V0hR3mMqQyhsy/Bvw1PRQJX2iC4OizyLnj/VDiT7hRlf03kqzZsIjAKsgBp665BRVV0oc55BqlATemyodQoX5SJ1VcPRmDkoLBOlfUIfm+A+3srU6rlWJXx3HBCY/gB5DANH3KlrGpKap95kka2gs2yNF36JddC7VHK/X2DByi/OfEBwM0ZlTni93sD89wg9sT

Hi Zheng Yang,

You should not get confused by your first line:

Parameter x : Set.

It has no impact on the pattern-matching where x is just a pattern which can bound anything to x.

Since you don't use x, it is equivalent to writing

Definition false_rect (n : nat) (f : False) : nat :=

match f return nat with | _ => O end.

For the rest of the explanation, Anton Trunov has been faster than me ;-)

Best,

Théo

Le jeu. 13 avr. 2017 à 09:02, zheng yang <zyang.uestc AT gmail.com> a écrit :

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