Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] matching variables in Ltac

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] matching variables in Ltac


chronological Thread 
  • From: AUGER <Cedric.Auger AT lri.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] matching variables in Ltac
  • Date: Wed, 05 May 2010 12:55:25 +0200
  • Organization: ProVal

Le Wed, 05 May 2010 11:49:30 +0200, Loic Pottier <loic.pottier AT sophia.inria.fr> a écrit:

Hi,

with Ltac, can we match names of variables in a pattern, to use them in right-hand side? e.g:

Ltac tac:=
  match goal with
   |- forall ?x:?E, ?P => idtac x
end.

(but this does not work :-(  )

or, if not, associate a character to a type so that intro will use it by default?

Loïc


I think it is not satisfactory, but you can do something like:


Ltac tac:=
 let x := fresh "forced_var" in
 intro x; revert x; idtac x.

Goal forall P, P /\ False.
tac.

It will change the name of your binder so you can chose it.

To get the name of your binder, it seems to require either an extension of the match rule, either to make your own tactic in caml.
the intro tactic is defined in [trunk]/tactics/tactics.mli

There is a function called find_intro_names of signature:
val find_intro_names : rel_context -> goal sigma -> identifier list

so your function should look like:

let print_universal_first_binder ctx gl =
 match Tactics.find_intro_names ctx gl with
 | [] -> tclFAIL
 | id::_ -> tclIDTAC_MESSAGE (Pp.str (Names.string_of_id id))

I am not sure of the result as I have never written plugins/tactics in Ocaml





--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay




Archive powered by MhonArc 2.6.16.

Top of Page