coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Turn a definition opaque

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Turn a definition opaque
Date: Mon, 22 Apr 2019 17:34:13 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-SN1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:WmeiXh293kJ3o1/+smDT+DRfVm0co7zxezQtwd8ZseMTL/ad9pjvdHbS+e9qxAeQG9mCsrQY1aGP6/CoGTRZp8rY6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq9QajZFtJ6swxRfFv2dEdudLzm9sOV6fggzw68it8JJ/6Shcp+4t+8tdWqjmYqo0SqBVAi47OG4v/s3rshfDTQqL5nQCV2gdjwRFDQvY4hzkR5n9qiT1uPZz1ymcJs32UKs7WS++4KdxSR/nkzkIOjgk+2zKkMNwjaZboBW8pxxjxoPffY+YOOZicq7bYNgVQndPXttKVyxZHIyzc5cPAeQGPeZdtYb9pl0Opga6CQSjAO7jzzlFjWL006InyeQsCQHI0hI9EdISvnrar8n6O6gJXO+v0KXE0S/OY+9K1Tvg7oXDbxAvoeuLXbJ1acffzVMgFxjCjlWWtIfpJjCa1uQKs2id4OprSP+hi245pAF3rTij39onhIvUhokIzV3E+zh2wIY0JN2jVkJ3fcOoHIdLuiGaMIt2XsYiTHtpuCY+0LEJpZm7fC0TxZkh2hXRZfuHc42S7RLiUuacOTh4hHN5eLK/mha96lKsyuz7VsSyzV1ErTJFn8HDu3wRzRDe7taLRuF980u71juC1hjf6u9aLk03iabWLpsszqMsmpodrUvOGy/7lFj2gaKUc0gr4fSn5ur6bbjju5OQKox5hwX4P68zgMKwG/44PRILX2WD+eSzyrnj/UrhTbtSkvA4lbXVvI7DKcoGvqC1HhZZ0oE45BmhFTum18kYnWUcI1JCZRKHiZXmN0vWIPDiCve/n0qjnyt3x/DHOb3hBI/BLn/ekLf9ebZ97ElcyAkpwd9D4JJUD6kNIPP1WkDvqNzVFhA0PxCuz+vjFtlxzIMTVXiAD6KYKK/StEWH5uMrI+mCfo8VvzP9JuAr5/HzjX84mEQdcbe10ZcKdHy1BfRmI0KFYXrpmNgBEGMKshAiQ+ztjV2OSSRTaGqqX6Ig+jE7D5qrApvERoC0mbCOwCO7HoBNaW1dEVCNEXLod52eVPsWaSKSJNVhkj0eWrS7RY8hz0LmiAivgbFgN6/f/jASnZPlztl8oePJ31lm/jttSs+ZzmulTmdun2pOSSVgj45lpkko6F6Y1q4wxs5YEtpcr8hJXwE1cNb80qQuBdzySBmbJo7RYFahXtCvADV3RdU0lYxdK31hEsmv20iQlxGhBKUYwuDaXcFmwufnx3H0Yv1F5TPG2a0m0wZ0ZOJqbTfjvYgmsg/ZCsjOjlmTkLuseeIExinR+WyfzG2I+kZFTAp3VqaDVncaNBKP/IbJo3jaRrrrMowJdw5IyMqMMKxPM4a7jVJaQf7iPJLVZGfjwj7sVybN/auFac/RQ0tYxD/UURNWkwcP+H+HMU41ASLz+28=

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