coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] notation to put an open term in a specific closing context

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] notation to put an open term in a specific closing context
Date: Fri, 13 Sep 2019 13:42:57 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f45.google.com
Ironport-phdr: 9a23:v6+GlRK+OcfXmdV+IdmcpTZWNBhigK39O0sv0rFitYgeKfXxwZ3uMQTl6Ol3ixeRBMOHsqkC07Wd6v25ESxYuNDd6SpEKMQNHzY+yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twrcutQYjId4Nqo8yBTFrmZIduhL2GhkIU6fkwvm6sq/4ZJv7T5ct+49+8JFTK73Y7k2QbtEATo8Lms7/tfrtR7NTQuO4nsTTGAbmQdWDgbG8R/3QI7/vjP1ueRh1iaaO9b2Ta0vVjS586hrUh7ohzwZODM/7Wral9Z/jKNfoBKmuhx/34vZa5ybOfZiYq/Qe84RSGxcVchTSiNBGJuxYIQPAeQPPuhWspfzqEcVoBSkGQWhHvnixiNUinL026AxzuQvERvB3AwlB98DrG/brNX0NKcJUeC60qrIxijfYvNQwzj97pXHeQ0mrP6WRr1wccvRyVIvFwzbjVWcs5bqPzWP2eQLrmeX9etgVeOzi24osAxxrT2vyd0tionNnI4a1lfE9SBgzYszONa2Rkl7Ydu+H5tRsSGXL5d5QsQ4Q2Fupik6zrkGtYSlcycX1ZQqwQPUZf+fc4WQ/B7vSOKcLS17iX9lYr6zmhe//Em6xuDzVsS51ktBoDBfndnWrH8N0gTe6siZRft5+UeswTOP2BrS6uFAOEw0lK3bJ4M4zr4+mZcesV7PHiDxmEXxg6+Wclsr9vK05OTgZ7Xqvp6cN4lqhQHiKqkihNCzDOAiPgUNX2WX4/mw2bzi8EHjT7hHjuU6kqzDv5DbIcQbqLS5AwhQ0os78RmwFDem0NUDnXkHMl1FewiLgJLvO17UJvD3EO2zg1WtkDd3yPDLJbLhApDXIXjClLftZ6py60lZyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiioynkZYdq2019NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/oVeCUCVTanX6dqQ14D1zXIusDYbYRo2uxrWH1SG3WJxXem9uBVWFEHOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEn36V3KjoF/J++RwRU28JLu0N8vur/WnBA2sD1zVoGTjzzLQGZzkWcFATQx2fIn+BAv+hK4yaF9xsdgO5lL/foQC1U1MJfdy6pxDNWgAluQLOfMc06vR5CdOR90S9swx9EUZEMkQoetixnC22yhBLpHzrE=

Coq surprisingly accepts this notation:

Notation "'withThis' x" := (fun this:nat => x) (at level 50).

But it is what I hoped it would be:

Definition try : nat -> nat := withThis this.

(* Error: The reference this was not found in the current
environment. *)

The following works, though:

Definition try : nat -> nat := withThis 2.

Is there some other trickery in Coq that allows one to write a term in a separate file and the context in a separate file? In our use case, we want something like the following:

contexts.v:

Notation "'f1 x" := (fun a:nat b:nat c:nat => x) (at level 50).

Notation "'f2 x" := (fun c:nat d:nat e:nat => x) (at level 50).

termsInsideContexts.v:

Require Import contexts.

Definition ff1 := f1 (a + b+ c).

Definition ff2 :=f2 (c+d+e).

We want this file-level separation because contexts.v is autogenerated.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] notation to put an open term in a specific closing context, Abhishek Anand, 09/13/2019