The Coq mailing list

[David Nowak <David.Nowak AT lineone.net>]

Bonjour,

Comment puis-je filtrer un type dépendant dans une tactique (avec Coq
7.0 d'Avril 2001) ?  La définition

  Tactic Definition MyTactic t :=
    Match t With
      [(x:?1)?2] -> ...

ne fonctionne pas car x serait libre dans ?2.  Il faudrait d'abord
transformer le sous-terme ?2 en un terme de la forme ([x:?1]?3 x), ce
qui permettrait de filtrer comme cela :

  Match t with
   [(x:?1)(?2 x)] -> ...

Je sais faire cette transformation dans un contexte :

  Tactic Definition PatternDepAux id t1 t2 :=
    Match t2 With
      [(?1 id)] -> Generalize id; Clear id; Change (id:t1)(?1 id).

  Tactic Definition PatternDep () :=
    Match Context With
      [|-(id:?1)?] -> Intro id; Pattern id;
                     (Match Context With [|-?2] -> (PatternDepAux id ?1
?2)).


PatternDep () transforme |-(x:nat)x=x en |-(id:nat)([n:nat]n=n id). Mais
je ne vois pas comment je pourrais procéder à la même opération sur un
terme...

Merci,

David.

-- 
David Nowak
Oxford University Computing Laboratory
tel: +44 1865 283527    home: 248014    fax: 273839
http://web.comlab.ox.ac.uk/oucl/people/david.nowak.html