Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Simplify after elaboration

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simplify after elaboration


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Simplify after elaboration
  • Date: Mon, 23 Mar 2020 22:18:34 -0400
  • Authentication-results: mail3-smtp-sop.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-ed1-f42.google.com
  • Ironport-phdr: 9a23:5VyTcRMwEFVrjl6hqi8l6mtUPXoX/o7sNwtQ0KIMzox0K/r8rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6msZHQy6Pg5oLKyhEYnLys+zyuqa+pvJYgwOiiDrMp1oKxDjjwzKsc9erpFlMb15nhnAuXxOdP5R3ng5DV2Wlhf4oMy3+cgwoGxrp/s9+psYAu3BdKMiQOkAVWV0AyUO/MTu8CL7Y06K73oYXH8Rl0MRUQfA5RD+GJz2t3mj77cv6GyhJcTzCIsMd3Gi4qNsEkK6jS4GM3s0/DiShJAqyq1cpx2lqlp0xIuGONjJZso7RbvUeJYhfUQERtxYDnUTDYa1bo9JBO0Eb75V

You don't need Ltac2 for this.  The trick is to bind x to a different name in Gallina, eg,

Notation "'[SIMPL]' x" := (match x with y => ltac:(let x := eval cbv delta y in y in idtac x; let x := eval simpl in x in exact x) end)
  (only parsing, at level 0, x at level 200).

On Mon, Mar 23, 2020, 21:58 Gregory Malecha <gmalecha AT gmail.com> wrote:
Hello --

I'm trying to write a notation that simplifies its argument. I wrote the following:

Notation "'[SIMPL]' x" := (ltac:(idtac x; let x := eval simpl in x in exact x))
  (only parsing, at level 0, x at level 200).

Definition foo := [SIMPL] 1 + 1.
Print foo. (* := 2 *)

Unfortunately, if there is an unbound identifier in the argument of [SIMPL], I get an error message saying "x not found". What I want to do, is perform the type checking, and get the usual error message if there is an error, and otherwise, reduce the term and exact the result. I was wondering if there is some way that I could do this with Ltac2, but I haven't been able to figure it out.

I know that if I'm defining a term, I can write something like:

Definition foo := Eval simpl in 1 + 1.

but I can't seem to do the same thing at the type level, e.g.

Definition foo : Eval simpl in 1 + 1 = 1 + 1.

Any pointers or suggestions would be greatly appreciated.

Thanks.

--
gregory malecha



Archive powered by MHonArc 2.6.18.

Top of Page