coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Anton Trunov <anton.a.trunov AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why does this apply tactic with a lambda fail?
Date: Thu, 7 Jun 2018 22:09:27 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=anton.a.trunov AT gmail.com; spf=Pass smtp.mailfrom=anton.a.trunov AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f169.google.com
Ironport-phdr: 9a23:MCoKAh/GkJHNn/9uRHKM819IXTAuvvDOBiVQ1KB41+McTK2v8tzYMVDF4r011RmVBdids6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+553ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/0hykIODE37W/ZisJugq1ZoxyvoAdyw5LNYIGQKPZ+fr/Rcc0cSGFcXshRTStBAoakYoYTCeoBIeFYr4/grFUQtxu+GA+sBOTxyjRVgXL5x6s60/gmEQHAxgAvBcgCsGjOrNXoMqcSVv61wbLHzTXGdfxW2DP95JLUfRAmpPGBRLR9etfSx0k3Dw7JkEmcpIj/Mz6W1ukBqXWX4/RjWO61lmIqqgV8riCyysoijoTFnI0Yx1Le+Sh63Io5P8O0RFN9bNW5CpVfrTuaOJFzQs46Q2FnpiI6yroetJ6+ZicKyZAnywfRavydb4SE+xzjWPuQLDp8nn5ld7W/hxG98Uik1OLwTNW70FFPriZdk9nMsG4C1wDL58SZVvdw+l2t1DWP2gzJ9+1IP0M5mbDGJ5MgxrM8jp8Tvl7CHi/ylkX2lqiWdkA89+ey7eTnfrLmppmGO4BukA3+Lr4umtG5AeQ/LAgDRGeb+eGm273i+U31WqlFjvozkqXBqpDVOdwbprKlAw9Syoss9xG/Dy6/3NsEmXkHMUlKdQmcj4npPlHOOOr3Ae2+g1SqijdrxurJMqfvApXXfTD/l+Lqeq844EpBwiIyy8pe7tRaEOIvOvX2D2b3qNveRiMjLgqz3a6zAdNh0YVYUCSTGLKfN736vlqB5+ZpKO6JMtxG8A3hIuQosqa9xUQynkUQKPHwjMknLUugF/EjGH23JH/lg9MPC2AP51NsQ+njiVnEWjlWNS/rA/AMowojAYfjNr/tA5i3ieXYjii+F5xSIGtBDwLUSCq6R8C/Q/4JLRmqDIphnzgDD+bzToYg0VSxrle/xeM5f6zb/SoXsZ+l399wtbXe

Hi Li-yao,

For instance,

pose proof (fun a (b: A -> B) => conj a (b a)) as H; apply H.

works.

So, it looks like a bug to me.

Cheers!
-Anton

> On 7 Jun 2018, at 21:49, Li-yao Xia
> <lysxia AT gmail.com>
> wrote:
>
> 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

[Coq-Club] Why does this apply tactic with a lambda fail?, Li-yao Xia, 06/07/2018
- RE: [Coq-Club] Why does this apply tactic with a lambda fail?, Jason -Zhong Sheng- Hu, 06/07/2018
- Re: [Coq-Club] Why does this apply tactic with a lambda fail?, Anton Trunov, 06/07/2018