The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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/