coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A question about Derive

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] A question about Derive
Date: Thu, 17 May 2018 08:07:09 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.casteran AT labri.fr; spf=None smtp.mailfrom=pierre.casteran AT labri.fr; spf=None smtp.helo=postmaster AT v-zimmta02.u-bordeaux.fr
Ironport-phdr: 9a23:dJkdhB3TJRdtq7ulsmDT+DRfVm0co7zxezQtwd8Zse0QL/ad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfMQA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7S60/Vza/4KdxUBLmlicJOSM6/m/ZhMN/g75Urh26qhxjwIPZep2ZOOZwc67fe94RWGpPXtxWVyxEGo6ydYoPAPQbPeZCsYb2ukUDogGlBQmwGuzv0CVHhnnr1qA9y+QhEB/J3BY6H90QqnjbsM/6NLwOUe+r1qnH1zPDYuhS2Tjn84fIaBEhreuCXbJqaMfcz1QkGQDdjliItIDoMDGY2v4Tv2SG8+ZsT/yjh3Mnpg1rvDSj2t8ghpTGi48X0FzI6zh1zJovKdC7UkJ2bt2pHZ1NvC+ALYR2WNktQ2RwtSY61LIGvZm7cTAUyJg+xh/favmHc42U4h35SOqdPy10hG98dL2kgBay61WvxfPmWcmp31dGtCRFksPUunAM0Rzc9NSHR+Ng8kqu2zuDzR7f5vxYLUwui6bXNp4szqQumpYPqUjDGzX5mETyjK+YbEUk/e2o5vz/YrXnuJCcLZV0hR/kPqsygMO/Gvg4PRYUX2eB/+Sxz7nj8lfiT7VQj/06iKfZsIrCKcQBuqG5GxNV0pok6xunEzim180YkWAbI1JBZRKIlJPkO0rOIfD9FfewmU6gkDZtx/DcP73uGI/BLnbZkOSpQbEo4ElFjQE30NoXs5lTE/QKJO/5ck73rt3RSBEjZV+a2eHiXe1825kEVCqkC7SFPbnbtxfc/uMiOfOBIoQcoyrwMfEjz/rnh2U431EHK/r6laALYWy1S6w1a36SZmDh149YQDU6+zEmRemvs2WsFDtaZnK8RaU5v2lpDIusF4aFSJr/2OXdjhf+JYVfYyV9Mn7JCW3hLt3WX/4GciPULNUzymVZB4jkcJco0FSVjCG/y7djKbCKqDNdp5Pm0cR8v7eViFQ48iZ4As2AwyeDVTMskw==

Hi,

I'm not sure whether Derive can be used in a simple example, probably because of scope problems with the variable ?Goal.

Here is a first version without Derive:

Section essai.
Variable n : nat.
Hypothesis Hn : 0 < n.

   Definition pred : {q : nat | S q = n}.
   Proof.
     destruct n.
     - now destruct (Nat.lt_irrefl 0).
     - eexists; reflexivity.
   Defined.

I would like to re-write my definition like that:

Derive q SuchThat (S q = n) As h.
   Proof.
     destruct n.
     - now destruct (Nat.lt_irrefl 0).
     - subst q; reflexivity.

But it fails because the variable n0 created by the case analysis on n is not in the scope of ?Goal.

Is there a way to write definitions like that using Derive ?

Regards,

Pierre

[Coq-Club] A question about Derive, Pierre Casteran, 05/17/2018