Search code examples
coqcoq-tactic

Applying a dependent type to an arguement to assert a goal in Coq?

If I have a general setup like the following, how can I prove I assert (f a)? 

A : Type
f : A -> Prop
a : A
...
============================
f a

Specifically, why can't I use any of these tactics, and what do the errors mean?

specialize (f a).
Error: Cannot change f, it is used in conclusion.

apply (f a).
Unable to unify "Prop" with "f a".
Solution

  • You cannot specialise f because it is used in the conclusion, that is in the goal. specalize (f a) replaces your hypothesis f by its applied version. If we forget about the goal that would get you f : Prop afterwards. However since f appears in the goal you are not allowed to change its meaning.

    Also f a is a proposition, and certainly not a proof of f a itself! The fact that it is named f doesn't mean it's not a predicate.