coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Doubt about eexists

From: Eric Mullen <emullen AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Doubt about eexists
Date: Wed, 20 Jan 2016 00:10:01 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=emullen AT cs.washington.edu; spf=Pass smtp.mailfrom=sliverdragon37 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ob0-f180.google.com
Ironport-phdr: 9a23:Ep+7cBTLeyVTKi9r7c1I1YdnE9psv+yvbD5Q0YIujvd0So/mwa64YBaN2/xhgRfzUJnB7Loc0qyN4/6mADRYqs/Q+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpq8OVOl0Qz2PsKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxzdSAgONyQz+Wpr3+n/3s/d53CScFcbtC689QjSj6ah3TxmuhSsaYW1quFrLg9B92foI6CmqoAZyltbZ

Try making sure that d11 and d10 come into scope before ?1179. Likely what happened is that ?1179 can't unify with whatever you have on the right side, because it has to unify in the context that existed when it was created (not the current context).

I believe that what I've said is true for 8.4, and I think it has changed in 8.5.

Eric

On Tue, Jan 19, 2016 at 3:54 PM Saulo Araujo <saulo2 AT gmail.com> wrote:

Hi,

After using eexists and performing some manipulation, I need to proove a goal of the form

Some ?1179 = Some (coeficient d11 d10)

Which tactic could I use to make Coq understand that there exists a value for ?1179 (i.e. coeficient d11 d10) that makes Some ?1179 = Some (coeficient d11 d10) true?

In other similar situation, reflexivity did the tricky...

I really appreciate any help you can provide,
Saulo Araujo

[Coq-Club] Doubt about eexists, Saulo Araujo, 01/20/2016
- Re: [Coq-Club] Doubt about eexists, Eric Mullen, 01/20/2016
  - Re: [Coq-Club] Doubt about eexists, Saulo Araujo, 01/20/2016
  - Re: [Coq-Club] Doubt about eexists, Jonathan Leivent, 01/20/2016