The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Mon, 10 May 2010 11:09:42 +0200, Marko Maliković <marko AT ffri.hr> a  
écrit:

> Dear Coq users and contributors,
>
> 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.

How could Coq do it automatically when

apply A with (Q := True) in H.
apply A with (Q := False) in H.
apply A with (Q := x = 1 -> y = 2) in H.
...

also work?

> Thanks a lot,
>
> -----------------------
> Dr. Sc. Marko Maliković
> Filozofski fakultet
> Sveučilište u Rijeci
> ---------------------
> Ph.D. Marko Maliković
> Faculty of Arts and Sciences
> University of Rijeka, Croatia
> -----------------------------


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay