coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Doubt about eexists

From: Saulo Araujo <saulo2 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Doubt about eexists
Date: Tue, 19 Jan 2016 20:54:18 -0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=saulo2 AT gmail.com; spf=Pass smtp.mailfrom=saulo2 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
Ironport-phdr: 9a23:n6nwgxGEST6RKlj9jXSmvZ1GYnF86YWxBRYc798ds5kLTJ75pMiwAkXT6L1XgUPTWs2DsrQf27SQ6vi4EjVeqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh770osWLKFwWzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB14fjx5PSyHf5Qz4Wd+lqSLnsu0n8CafNMzyC7szXGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

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