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:54:11 -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-ej1-f41.google.com
Ironport-phdr: 9a23:68ewpBalPOx9hyitcD54wzj/LSx+4OfEezUN459isYplN5qZr8i5bnLW6fgltlLVR4KTs6sC17OJ9f66EjZdqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5wIRmsrAjdqMYajZViJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lK1UoByjqBJ/zYDaY5ybOuRica7GZ9wWWXBMU9xNWyBdAI6xaZYEAeobPeZfqonwv18AogGlBQmrAuPk1z5GhmXx3a0hyOQqDAbL3A46ENIVt3TUqtr1NL0VUeCu16nFyS7Ob/xT2Tjn6YjIdgotru2LXbJ1aMfcz1QkGAzZgFuKs4PlIy+V2foXs2id9+dtUeyhhm47pwx+vjWixscihpfHi48W1FzJ6zl1zYgpKNC5TEN2btGqHIdOui+aNYZ7Q8MsTm50tSg1ybAIt4C2cS4Xw5opwB7fbuaIc4mO4h/7SOmRJi14hHR7d7K7gxa+61avxfDhVsSyzV1ErTJFn8HSunwR0xHf8MuKR/tn8ku/xDqC1Brf5+5ZLU0yiKHVMYQuwqQqmZoWqUnDHjH5mEHxjKKOc0Ur4Omo6+D+brr4pJ+QKpZ4ig/xP6gzgMC/DuM4Mg8BX2if5+uwzqHs/Ur8QLlSj/02lLfWsIzCKMgFuqK0BxVZ34Uj5hqlETuqzdcVkWMIIV5YYB6HipLmO1DKIPD2F/e/hFGsnS9px//cJb3hBZPNLnfZkLfmZrZ98EpRxRE8zdBa/Z1UC7UBLOjvVU/2sdzUFgU5PBCsw+b7FNV90ZsTVn6IAq+AKa/drVuI5v80LOSXf48UuDP9K+A/6PL0jH85n0Udfaiz0pcNZnC4BKcuH0LMan31x9wFDG1C6gE5VanhjECIeT9VfXe7GawmsGIVEoWjWKXKXYeryJOb2zygVslUb3tBDF+WFmzzJq2LXv4NbGSZJco3wW9MbqSoV4J0jULmjwT90bcydrOFqB1djorq0Z1O38OWkBgz8TJuCMHEijOCSmh1miUDQDpkhfkj83w48U+K1O1Du9IdDcZavqobXQIzNJqaxOt/WYirB1DxO+yRQVPjee2IRDE8StVrno0Lakd5Xtig11XNg3PsDLgSmLiGQpcz9/CE0g==

Sorry, that only does goal, but doing the context isn't much different

On Wed, Oct 14, 2020, 20:53 Jason Gross <jasongross9 AT gmail.com> wrote:

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