Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg 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 22:41:19 -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-il1-f178.google.com
  • Ironport-phdr: 9a23:Lnji6hN9SCcr07+ba7ol6mtUPXoX/o7sNwtQ0KIMzox0IvXzrarrMEGX3/hxlliBBdydt6sbzbSM+PG/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oLRi6swrdu80UjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksN/jKxZrxyhqRJxwJPabp+JO/dlZKzRYckXSHBdUspNVSFMBJ63YYsVD+oGOOZVt5XwqEAOrRu/HgmsBP3gyjxVjXLq2601yeIhHhzb1wEnBd0Bq3TUrNTuNKcST++1z7PEwi/Fb/xM3zfy9ZLEchEgofGQUrJ9asXRyUw1GAPEilWcs5DqPzSQ1ukUtWWQ8uVvW/61hWE9twFxviagxt0qioTRgo8YykzI+DtnzIg7K9C2SE92bcC4HJdNty+UN4t4Tt0sTmx0pCs3xKAKtIOlcCUI1Jkq2x/SZfOIfoWI/x/uVeCcKip2inJifbKwnRey8U64x+LgUcm0ylBKoTRBktnIrHwCyQHc6tWBR/Bg/UmhwS6C2x7P5uxAO0w5lqrWJ4Q8zrMxl5cfq1nPEy31lUjwkaSYbF8r+vKy5OTierjmpoGTN4tzigzmN6QhgM2/AeAhPggPW2iX5P2w1LP+8UD7Q7hGlPI2kq7esJDVIcQUuLS1DBNS0oYm8xq/DjGm38oEnXQfMl5JZBaKg5LqNlzOOvz0EPayjlW2nDt2xf3LPaXtApDXIXjClLfhc6x960lZyAcr199Q/JJUCrAaIPLzREDxt8bUAQU/MwOuxeboFc9x1oIfWWKTDa+UK6zSsVqS6eIuJ+mAfpMauDH4K/Q9/f7hkWc5mUMBfamuxZYYdHe4Hu1/L0qFZXrsn8wOHHwRvgs+SezqkEeNXSRSZ3a0RaI85ys0BJioDYfZFciRh+mK2z7+FZlLbCgSAVeVVHzsao+sWvEWaSvULNU3wRIeUr30YoUh1AquuQyy4rxuKOacriQStZP41NV2oeTVnBc+sz11E8u13GSETmUylWQNEWxllJtjqFBwnw/QmZNzhOZVQIQKtqF5FzwiPJuZ9NRUTtX7WwbPZNCMEQ/0TdCvADV3RdU0kYZXPhRNXu66hxWG5BKERr8Yk7vRWs4x+6PYmnn1foNzkimWkqYmiFYiT41EMmj03vcjpTiWPJbAlgCir4jvbb4VhXef+2KKzG7It0ZdAlZ9

Sorry, I was not clear. I want to only strongly normalize closed subterms of the type and leave the rest unchanged.



On Wed, Oct 14, 2020 at 6:54 PM Jason Gross <jasongross9 AT gmail.com> wrote:
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.... ?




Archive powered by MHonArc 2.6.19+.

Top of Page