coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inversion - Error, cannot solve a unification problem

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Inversion - Error, cannot solve a unification problem
Date: Wed, 01 Feb 2017 11:31:48 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f172.google.com
Ironport-phdr: 9a23:btG1aR0pumFE2Y+OsmDT+DRfVm0co7zxezQtwd8Zse0XIvad9pjvdHbS+e9qxAeQG96Kt7Qa1KGM7ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fdbghMizexe7J/IRe5oQnPtsQdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnYhcx+jq1VoByvqR9izYDKfI6YL+Bxcr/HcN4AWWZNQsRcWipcCY28dYsPCO8BMP5foYbnu1sOsRu+BQiyC+Py1zRGm3j23Kwk3Os7DAHNwQstH9cUv3TIsNX6LqISXPuwzKbS0TXDc+lZ2TLn5IjPaBAhruiBULRtesTS0UkiDx3JgkmUpID/PD6Y1v4Bv3aF4+Z8T+6jlmwqpx93rzOy3MkjkJPJiZgQyl3c9SV23oI1JdqgRU5+e9GkEZ9QuziDN4t1Xs8uWm9otDs4x7EYo5K7cy8KyJMoxx7bdfOLaZSH4hXmVOqJIDd4gmxqeK6nihqs7UStzvfwW8q03VpQsCZJjMXAumoQ2xHR9MSLUv598V2g2TaL2QDT8OZEIUUsmKreMZEh3qIwlpoSsUvdAy/6gl72jKiXd0o64Oeo9v/qYrrjppCGNo90jhvyPbgpmsy6Geg4KBQBX3CH+eSg073u5VH2QLJTjvEvjqbZtI3aKt8Aq66iAw5V154j5AylAzen1tQYh3gHI0hfdBKJlYi6c23Jdfv/FLK0h0mmuDZt3fHPeLP7UbvXKX2Wtb79YbZ85lMU8w0hwNlCr8ZRA60dKffbX0btqNXdSBgjPFrnkK7cFNxh29ZGCiq0CaiDPfaKvA==

Hi,

Maybe you can show us the goal and the definition of the inductive type you're trying

to do inversion on?

Best,

-- Matthieu

On Tue, Jan 31, 2017 at 9:08 AM Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de> wrote:

During a proof I try to apply the inversion tactic to a hypothesis with
an inductive type.

The reply from Coq 8.6 is "Error: Cannot solve a unification problem".

I assume this has something to do with my definitions using dependent
types, but I have
no clue whatsoever what I can do about this error. I also apologize
for not having a minimal example to demonstrate the error, but
the lack of any clue about the cause makes it difficult.

Any ideas what causes such an error and how to get the desired
inversion of the hypothesis?

Klaus

Re: [Coq-Club] Inversion - Error, cannot solve a unification problem, Matthieu Sozeau, 02/01/2017