coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] normalize all closed terms of a given type

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] normalize all closed terms of a given type
Date: Wed, 14 Oct 2020 20:53:49 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f52.google.com
Ironport-phdr: 9a23:n9bkth2g66p8CVcismDT+DRfVm0co7zxezQtwd8ZseISKfad9pjvdHbS+e9qxAeQG9mCtLQa0aGM7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhjexe7J/IAu5oQnPtsQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnYhcx+jq1VoByvqR9izYDKfI6YL+Bxcr/HcN4AWWZNQsRcWipcCY28dYsPCO8BMP5coYbnvFsOqh2+DhStCuP1zT9InWT21rA93uQjCw7GxwsgH9QBsHTOq9X1L7wSXOSuwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesXe1UchDRnKjkmMqYP7JTOV0PwAvmyV4edgSe6ihHIqpgFxrDSxyMohiZfFi5wJxl3K6Sh0wYI4KNK3RkJnf9OqEJlduiCaOYZ5Xs4sTGJltigkx7AApJW1ci8KyJE9yB7ebfyKa5SH4hX5VOaXPzh4gHZldKihiBmv7EitzPD3WMqs0FtSsCZJjt3BumoO2hHT8MSLVOdx80S71TuPyQze7PxPL1oumqrBMZEhx6Y9lpoNvkTHGS/7gED2g7WXdkUg4+Sn9fnobqj/qp+SN4J4lBvyMqspmsy4DuQ4NhYBU3KH9uS70b3v5Uz5QLNUgf0qiqTVrozWKMABqqO6AwJZyJgv5wq8Aju80NkUg2ELLFdfdxKGi4jpNUvOIPf9DfqngVSjiixrx/fAPr3uGJXNKWPDkKzlcLtm5E5czRA8zdFb555OFr4BJ/fzVlfrtNPEFh85LxC0w+H/Bdph0YMeQHuDDbOdMKPPqlCF/fkvIumJZI8NojnxMfkl5/j0jX84g1ARZ6ep3YFEIEy/S/9hOgCSZWfmyoMKFn5PtQ4jRsTrjkeDWHhdfSDhcbg742QZAZmhC8/sXIe2m/TV3i6gGZtZfGddEQGkHnLhdoHCUPAJPnHBavR9myAJAODyA7Qq0guj4VejluhXa9HM8yhdjqrNkdh44+qJyEM3/D1wSsmRiiSDEjsykWQPSDs7mqt4pB4lkwbR4e1Dm/VdUOdrybZMWwY+O4TbyrUjWd/3UwPFONyOTQT/G4n0MXQKVts0huQ2TQNlAdz710LM2iOrB/kekLnZXJE=

Here is a slow tactic to do this:

Ltac norm T :=

repeat match goal with

| [ |- context [?e] ] => let e' := eval vm_compute in (e : T) in progress change e with e'

end.

You may want a different typing check if you don't want coercion insertion or only want to check up to syntactic typing rather than unification.

On Wed, Oct 14, 2020, 20:20 Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a tactic to strongly normalize all closed terms of a given type in the Coq goal and context?
Is there a way to write such a tactic in Ltac/Ltac2/Mtac2.... ?

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

[Coq-Club] normalize all closed terms of a given type, Abhishek Anand, 10/15/2020
- Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/15/2020
  - Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/15/2020
    - Re: [Coq-Club] normalize all closed terms of a given type, Abhishek Anand, 10/15/2020
      - Re: [Coq-Club] normalize all closed terms of a given type, Fabian Kunze, 10/15/2020
        
        Re: [Coq-Club] normalize all closed terms of a given type, Beta Ziliani, 10/15/2020
        
        Re: [Coq-Club] normalize all closed terms of a given type, Abhishek Anand, 10/15/2020
        
        Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/16/2020
        Re: [Coq-Club] normalize all closed terms of a given type, Jason Gross, 10/16/2020