The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Yeah, closed means no evars and no local variables.

For example, in the proof below, I want 2^64 to be normalized and leave everything else unchanged.

I can use the tactic `norm` below to manually pick terms to normalize. But I wish there was an automatic way to pick all closed terms of a given type.

Require Import ZArith.
Open Scope Z_scope.
Ltac norm T :=
  match goal with
    [ |- context[T] ] => let Tc := eval vm_compute in T in
                       change T with Tc
  end.

Lemma xx (x:Z) : (2^64)*x=1.
  norm (2^64).

-- Abhishek

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

On Thu, Oct 15, 2020 at 5:44 AM Beta Ziliani <beta AT mpi-sws.org> wrote:

I was going to ask the same question. Perhaps an example could help?

On Thu, Oct 15, 2020 at 3:08 AM Fabian Kunze <fabian.kunze AT cs.uni-saarland.de> wrote:

By closed, do you mean no evars, or no local variables?

15 Oct 2020 07:42:39 Abhishek Anand <abhishek.anand.iitg AT gmail.com>:

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

-- Abhishek

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

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.... ?

-- Abhishek

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