The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> can someone explain to me why in such case, apply tactic cannot determine
> variable Q automatically (example is only "demo"):
> 
> Coq < Section Demo.
> 
> Coq < Axiom A : forall P Q : Prop, (P -> Q) -> P -> Q.
> A is assumed
> 
> Coq < Parameter x y : nat.
> x is assumed
> y is assumed
> 
> Coq < Hypothesis H : x = 1 -> y = 2.
> H is assumed
> 
> Coq <
> Coq < Goal True.
> 1 subgoal
> 
>   H : x = 1 -> y = 2
>   ============================
>    True
> 
> Unnamed_thm <
> Unnamed_thm < apply A in H.
> Toplevel input, characters 1-13:
> > apply A in H.
> > ^^^^^^^^^^^^
> Error: Unable to find an instance for the variable Q.
> 
> OK, "apply A with (Q := (y=2)) in H" help, but I don't want to know what
> is value of Q. I want to do it automatically.

You could have said as well "apply A with (Q := (y=3)) in H" and it
would have worked, what shows that there is indeed no instance for Q
that Coq could infer.

Hope it helps.

Hugo Herbelin