The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

I guess it would be hard to guess what b should be, wouldn't it? Would eapply make it through?

Thanks,

Jason Hu

-------- Original message --------

From: Li-yao Xia <lysxia AT gmail.com>

Date: 6/7/18 15:50 (GMT-05:00)

To: coq-club AT inria.fr

Subject: [Coq-Club] Why does this apply tactic with a lambda fail?

Hello Coq-club

Say the goal is a conjunction (A /\ B).


Variables A B : Prop.
Goal A /\ B.


and I want to prove A, then B under hypothesis A. One way I found is to
apply some function (A -> (A -> B) -> A /\ B) which is trivial to concoct:


apply (fun a b => conj a (b a)).


Alas, Coq then complains somehow:


Error: Cannot refine with term "conj ?M158 ((?M159 : A -> B) ?M158)"
because a metavariable has several occurrences.


Suprisingly, it is happy with this version matching on a dummy parameter:


apply (fun 'I a b => conj a (b a)).


Or with another version using "refine":


refine ((fun a b => conj a (b a)) _ _).


What is going on?

I am also curious about other solutions for the original task, that also
don't need to explicitly name the two conjuncts A and B.

Li-yao