coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Define a function using tactics without a type

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Define a function using tactics without a type
Date: Sat, 14 Apr 2018 02:14:47 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay10.mail.gandi.net
Ironport-phdr: 9a23:W/qIaxGnJka4EyYUqfWCnJ1GYnF86YWxBRYc798ds5kLTJ7zpMqwAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934Hab5qYNOZ9c67HYd8WWWRMU8RXWidcAo28dYwPD+8ZMOhZtYb6u0cOogG4BQa0Be3vyztIiWTo0q0gz+QqDAbL3AM6EN0QrHTbttP1OL0dUeC0yKnH1ivMb+lK2Trm84jIcRAgoeqPXbJxdMrRzFcgFxnfglWWt4PlIyqY2+IQuGaV6OpgUPigi28hqwxpoDivwd0jhZXJhoIUz1DI7D52wJwrKt25VE57Z8CrEIFKuy6HKYR7RN4pTWJwuCsi1LEKpJy2cDIIxZg73RLTdv6KfouS7h79WuudPS90iXN7dL6lmhq+7VasxvfhWsS701tGtDdJn9rMu30Lyhfd8NKISuFn8UekwTuP1x7c6uVDIU0sj6rUNZohzaQwl5YOrUjPBCr2l1/3jK+SbEkk9fKn6+L6bbXnvJOcMZF7ih3mPqQvnMywH/g4PxAQU2SG++mwzr/u8VHjTLlXjPA7kbPVvI7UKMgHvqK5BhVa0ocn6xaxFTem19EYkGEILF1fZh2Hk5LmO1fULPD3DPe/h0+jnylxx/DaJbDhGZbNL3jYkLfifLZ97ktcxxQpzdxF4ZJbFK0BLOrpWkDtrNzYEgM5Mwuszun7D9V9z5oSVn6LAq+EK6zfqkSI5+IqI+mUfoAZojf9K/4/5/7vl3A1g1EdfbP6lacQPXu/B7FtJ1iTSXvqmNYIV2kQ7SQkS+m/p1QBTTdVUFmzW6gx/C1zXI2vAJvKQMaigbiL0T2nNoZVd3tFC1WJHG2ucYiYDaRfIBmOK9Nsx2RXHYOqTJUsgEn35V3KjoF/J++RwRU28Jfq1dx7/erWzE9g7j9lFMec1mSAVSdyk39aHmZqjpA6mlR0zxK46YY9m+ZRTIIB/PBYSQQ7MJvR1ap8BsygAlucLOfMc06vR5CdOR90Tt81xIVSMVxwH9yz10iF2iOrB/kanrqHBdoy/76Oh3U=

You can do something like

Lemma foo : {T : Type & T}.
Proof.
eexists.
exact (1+0).
Defined.

Definition bar := Eval lazy beta match delta [projT2 foo] in projT2 foo.

(tweak the Eval according to your desires)

Gaëtan Gilbert

On 14/04/2018 01:41, Joachim Breitner wrote:

Hi,

I can write

Definition foo1 : type := body.
Definition foo2 := body.
Definition foo3 : type. exact body. Defined.

but it seems I cannot write

Definition foo4. exact body. Defined.

Is there a way of doing so? I.e. a way of using tactics to define a
function without having to specify the type before?

What I do now is something like this

Definition foo4_type : Type.
let ty := type of body in exact ty. Defined.
Definition foo4 : foo4_type exact body. Defined.

but it is a bit clunky.

(The actual tactic is a bit larger and does some interesting stuff
before calling [exact]; namely; getting the body of a local let out of
a complex function).

Thanks,
Joachim

--
Joachim “nomeata” Breitner

mail AT joachim-breitner.de
https://www.joachim-breitner.de/

[Coq-Club] Define a function using tactics without a type, Joachim Breitner, 04/14/2018
- Re: [Coq-Club] Define a function using tactics without a type, Gaëtan Gilbert, 04/14/2018
- Re: [Coq-Club] Define a function using tactics without a type, Emilio Jesús Gallego Arias, 04/16/2018
  - Re: [Coq-Club] Define a function using tactics without a type, ikdc, 04/17/2018
    - Re: [Coq-Club] Define a function using tactics without a type, Pierre Courtieu, 04/17/2018