coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Sean Wilson <sean.wilson AT ed.ac.uk>
- To: Marko Malikovi� <marko AT ffri.hr>, coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] Intro in Ltac
- Date: Thu, 6 Dec 2007 22:08:05 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: School of Informatics, The University of Edinburgh
On Thursday 06 December 2007 18:51:40 Marko Malikoviæ wrote:
> Greetings,
>
> can somebody give me a reason why first example work, but second not:
>
> Ltac test :=
> intro H1;
> compute in H1;
> assumption.
> Goal 2+3=5 -> 5=5.
> test.
>
>
> Ltac test :=
> try intro H1;
> compute in H1;
> assumption.
> Goal 2+3=5 -> 5=5.
> test.
>
> I need to build Ltac but I don't know how many intros are possible to do
> in particular subgoal. Is it some solution?
This is a hack, but you can do something like this:
(intros x y z H; compute in H ||
intros x y H; compute in H ||
intros x H; compute in H ||
intros H; compute in H ||
fail "Too many variables?")
The first intros will fail if there aren't enough variables, so the second
intros is attempted with one less variable and so on until hopefully one of
the intros works. It will break if you have a subgoal with too many variables
though. Make sure to put in a recognisable error message so you know to add
more intros patterns later if this tactic fails.
I'd like to know if there is a cleaner way to do this, but I find that I need
to use hacks like this in Ltac quite often as it lacks certain fine control.
This is another Ltac hack I use frequently when working with functions when I
don't know the number of parameters needed:
Ltac fun_name t :=
match t with
?f ?a => f
| ?f ?a ?b => f
| ?f ?a ?b ?c => f
| ?f ?a ?b ?c ?d => f
| ?f ?a ?b ?c ?d ?e => f
| _ => fail "fun_name: function has too many parameters!"
end.
Good luck,
Sean
- [Coq-Club] Intro in Ltac, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Edsko de Vries
- Re: [Coq-Club] Intro in Ltac,
Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac - correction, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Edsko de Vries
- Re: [Coq-Club] Intro in Ltac, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac, Sean Wilson
- Re: [Coq-Club] Intro in Ltac, Marko Malikoviæ
- Re: [Coq-Club] Intro in Ltac,
Edsko de Vries
Archive powered by MhonArc 2.6.16.