The Coq mailing list

["Andrew McCreight" <continuation AT gmail.com>]

I think the special 'context' pattern does what you want.  You should read about it in the manual, but I think something like this might work:

match goal with
  | [ H : context [7 :: _] |- _ ] => simpl in H
end


- Andrew

2008/10/5 <marko AT ffri.hr>

Dear Coq developers and users,

If I have in context hypothesis about some list, what is the most simple
manner to do pattern matching over those hypothesis to find if those
hypothesis contain some element or not. The problem is: The list increase
during proving some goals but I don't know how long these list is in some
subgoals.
I found these solution (this is example in which I don't know if list
contain number 7 and on what position number 7 is. If list contain number
7 anywhere I have to use one tactic but I have to use another tactic if
list not contain number 7):

Section Example.
Require Import List.
Parameter Lista : list nat.
Hypothesis H_lista : Lista = 3 :: 6 :: 5 :: 7 :: 2 :: nil.
Parameter goal_to_prove : Prop.
Goal goal_to_prove.
pattern 7 in H_lista;
match goal with
 | [ H_lista : (fun _ : nat => ?X) ?Y |- _ ] => simpl in H_lista
 | [ |- _ ] => assert (1=1)
end.

This work but I don't think this manner is "beautiful".

Is there some more simple (or good looking) manner?

Thank you,

Marko Malikoviæ

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club