coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Turn a definition opaque

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Turn a definition opaque
Date: Mon, 22 Apr 2019 19:46:52 +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 relay5-d.mail.gandi.net
Ironport-phdr: 9a23:wvrCoxwOMRTh4qPXCy+O+j09IxM/srCxBDY+r6Qd2uoRIJqq85mqBkHD//Il1AaPAdyCra4awLOP6uigATVGvc/Z9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMq8Uam4RvJ6c+xhfUv3dEZvldyWd0KV6OhRrx6dq88IJ5/yhMp/4t8tNLXLnncag/UbFWFiktPXov5M3suxnDTA+P6WUZX24LjBdGABXL4Q/jUJvpvST0quRy2C+BPc3rVr80Qiit771qSBDzligKMSMy/XzNhcxxiKJbpw+hpwB6zoXJboyZKOZyc6XAdtwdWGRBQ91RVzRfDYygc4sBAe0BPeNCoIn8oVsFsB+yCAaoCe/qzDJDm3340rAg0+k5DA/IwgIgEdINvnraotr6O6UdXvy6wqTT0TXObOlb1Svh5IXGch0sp+yHU7JqccrWzEkiDwLLgU+Mroz5JTyV0PwCvWma7+pkTu2glXQnqx1sqTWoyccjkJfGhp4PxVDC7yl5z4c1JdmjR0Fle96kDIBdtzqZN4p2WcMiQGBouCM/yrIYo563Zi4Kx4o7xxPGbfGMboaG4hXmVOmLIDd4gmpoeL2+hxau8Uig1/bzWtO10FZNqCdOj9rCtmgV2hDN98SKSOFx80W91TqVygze6e9JLVopmaffKZMt2qA8mocdvEjZAyP7mFv6gLWLekgl5OSk8fnrb7riq5KaKoR6kBvxMr40lcy6Gek4MhYBX2yc+emkzr3s40n5T69Kj/A2i6XWrYrWJcEBqa64Bw9ZyIkj5Ay5Dzi70dQUh38HI0xZeB6fjojpPU/BIOzgAPuhnlihki1nyvLaMrH7H5nALXbOnK38cbt56UNQ0A8zwspe55JQBLEBOvXzWkrpudzXFBA2LRC0zPzhCNln2YMeWGaPDbSHP6PIrV+F/fkvI+qMZY8Ouzb9Kv0l5/vwgn8jg1Mde7em3YcPZHCiAvtmO1mZYWbrgtoZDWgKuRM+QPX2h12GTD5cfG2/X7k85zE+EIKpF53PRoGrgLyb3Se0BIdaZm5cCgPELXC9fIKdHvwIdSi6I8l7kzVCW6LyZZUm0ESBvYzmwrxQAevQ8CACqdq329F4++TV0x4z8TZ5Fdi1yGKcVGJ1m2YFXXkw0bwp8h818UuKzaUt268QLtdU/f4cDlZjaMzsitdiAtW3YTrvO9eETFH8H4e8DDU4X490z5kLakd5XdqriBzCmSynH+1Nzu3ZNNkP6qvZmkPJCYN4wnfC2rMmigB4ENBMJHalh6t6+hKVAYPVwRzAy/SaMJ8E1SuIz1+tiHKUtRgGAhVzQL7GXHUaa1GQq9nltBvP

If you can state your expected result as a module interface sure. Otherwise Opaque is as far as it goes.

module interface method:

Module Type T.
Parameter foo : Set.
Parameter thing : foo = nat.
End T.
Module M.
Definition foo := nat. Definition thing := eq_refl.
End M.

Gaëtan Gilbert

On 22/04/2019 19:34, Jason -Zhong Sheng- Hu wrote:

Hi,

I am wondering if there a way to turn a definition entirely opaque, so that the type checker won't unfold it? I guess this question has been raised once a while but I cannot find a solution.

Consider the following two definitions.

Definition foo : Set := nat.

Definition blah : Set.
Proof. exact nat. Qed.

Goal foo = nat.
Proof. reflexivity. Qed.

Goal blah = nat.
Proof. Fail reflexivity. (* this does work as expected *)

Opaque foo.
Goal foo = nat.
Proof. Fail Fail reflexivity. (* this shouldn't work *)

It would be helpful if a definition can be transparent for just a while and become entirely opaque once enough facts are established.

*Thanks,*
*Jason Hu*
*https://hustmphrrr.github.io/*
****

[Coq-Club] Turn a definition opaque, Jason -Zhong Sheng- Hu, 04/22/2019
- Re: [Coq-Club] Turn a definition opaque, Gaëtan Gilbert, 04/22/2019
- Re: [Coq-Club] Turn a definition opaque, Xavier Leroy, 04/22/2019
  - Re: [Coq-Club] Turn a definition opaque, Gert Smolka, 04/24/2019