Pourquoi Coq n'accepte-t-il pas ce lemme comme indice?Le lemme ne peut pas être utilisé comme indice
Lemma contr : forall p1 : Prop, False -> p1.
Proof. tauto. Qed.
Hint Resolve contr : Hints.
Ou d'autres lemmes qui se terminent par une variable Prop?
Regarder la documentation Hint Resolve (http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@command232):
term cannot be used as a hint
The type of term contains products over variables which do not appear in the conclusion. A typical example is a transitivity axiom. In that case the apply tactic fails, and thus is useless.
Cependant, il ne semble pas (me) d'être le cas ici, comme le seul produit est plus p1 qui apparaît dans la conclusion .
Le problème ici semble être que votre conclusion n'a absolument aucune forme du tout. auto semble fonctionner en faisant correspondre la forme de votre objectif avec la forme du type de retour de la base de données d'indices. Ici, il pourrait être contrarié par le fait que votre objectif est juste une variable quantifiée. Je ne suis pas sûr si c'est une chose raisonnable à trébucher, mais cette instance particulière pourrait être le seul cas où vous pourriez avoir un type de retour sans forme (avec évidemment le même cas pour Set et Type), donc ce n'est pas une grosse affaire .
Donc, vous ne avez probablement pas besoin de cela comme un soupçon? ... il suffit d'utiliser des tactiques telles que tauto, intuition ou effectuer tout type d'élimination/destruction/inversion sur la valeur de type False dans votre environnement ... pas très satisfaisant mais eh: \