The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think if you wanted to pick out an efficient primitive to make available in Ltac2/OCaml, the primitive would be:

Given a term t and a tactic k:

for every subterm t' of t in topdown order:

  invoke k on (t', the type of t', the set of context variables t' depends on, the set of de Bruijn indices used but not bound in t' or its type)

To be completely efficient, this would have to be interwoven with the retyping algorithm and either be cached or else implemented in CPS, 

On Thu, Oct 15, 2020 at 6:39 PM Jason Gross <jasongross9 AT gmail.com> wrote:

Inductive marker := mark.
Ltac norm T :=
  let check_and_change v :=
      assert_fails has_evar v;
      let T' := type of v in
      unify T T';
      let v' := (eval vm_compute in v) in
      progress ( change v with v' in * ) in
  pose proof mark;
  repeat match goal with H : _ |- _ => revert H end;
  repeat match goal with
         | [ |- context[?e] ] => check_and_change e
         end;
  repeat lazymatch goal with
         | [ |- marker -> _ ] => fail
         | _ => intro
         end;
  intros _.

Goal forall a b c, a + (5 + 6) + c = 1 + 1 + b.
  intros a b.
  norm nat.

Note that this may not play well with section variables.

On Thu, Oct 15, 2020 at 5:56 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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/