coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Li-yao Xia <lysxia AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Why does this apply tactic with a lambda fail?
Date: Thu, 7 Jun 2018 15:49:08 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lysxia AT gmail.com; spf=Pass smtp.mailfrom=lysxia AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
Ironport-phdr: 9a23:0D5CZhf8GODmoZG8z9ue+73dlGMj4u6mDksu8pMizoh2WeGdxcu+Yx7h7PlgxGXEQZ/co6odzbaO7ua4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYb5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37mHZhNFzgqxVrh2uqABwzYHPbYGJNvdzZL/Rcc8USGdDWMtaSixPApm7b4sKF+cPO+dYo5D9plQUqhu1GAijBOL1xTRVgXL22a070/8uEAHHxgMtBN0OsHHOo9X0MKceS/y6zK7NzTjaaf5dxDTz6JDQfxw/vf2BWah8fMnRxEU1CQ/Jk1SdpZb4Mz6WyOgBq3aX4ut8We+tjmMnpQ58rzqzysopi4TEg40YxkzY+SV3xYs6Oce3SEB5bNOhHpZduS+aN4VzT8MsXW5npDw1x7gdtpO5ZycHzJIqzAPFZfOdaYiH+BfjWf6RIThmgHJlf6qyhxOo/kihzu3wT9C00EpWoiZcnNnAq3MA2wLJ5siITft9+Uih2TKR2AzJ9u5EJkU0mbLaK54n3LEwioIevVrfEiLygkn7j6+bel869uS16unreKjqq5yCO4NsjwHxKKUumsixAeQiNQgOWnCW+eC81b348kz5Qa9Fg+Y5kqncqp/aJMAbqrSlDA9S14Yv8wy/ACu+0NQEgXkHK0pIdw6Aj4jwIl3BPPT4DeqkjFm3izdqx/XGPqX7DZnXL3jDlq3hfbdn5EJGxgoz14MX25UBAbYYZfn3R0XZtdrCDxZ/PRbn7fzgDYBZ18YPUGXHMq6QePfWoESY5+sHLOyFZYtTszH4fat2r8XyhGM0zAdONZKi2oEaPSjhT6ZWZn6BaH+pue8vVGIDvw4wVuvv0QTQXjtaZnL0VKU5tGhiVNCWSLzbT4Xou4SvmT+hF8QPNG9DA1GIV3zvctfcAqpeWGepOsZk1wc8e/2hRosmj0/8sQb7z/9+MrKR9HRI79Ts09964+CVnhY3p2R5

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