coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Inversion - Error, cannot solve a unification problem
Date: Tue, 31 Jan 2017 09:08:23 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx03.uni-tuebingen.de
Ironport-phdr: 9a23:JJpz/RSTeiIe+Y0p4D80l8iuh9psv+yvbD5Q0YIujvd0So/mwa67bBON2/xhgRfzUJnB7Loc0qyN4vymBzBLuMza+DBaKdoXCE9D0Z1X1yUbQ+e7SmTDZMbwaCI7GMkQHHRExFqcdXZvJcDlelfJqWez5zNBUj/2NA5yO/inUtWK15f/hKiO/MjYZBwNjz6ga5tzKg+3pEPfrJo4m4xnf4U1wwbS6lxTZ+lMwGpuIxrHnBL1+9z2+4V//j5VsvQn39NGUODmYqkyTLpXATJgP21jt56jjgXKUQbavihUaW4RiBcdWwU=

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

[Coq-Club] Inversion - Error, cannot solve a unification problem, Klaus Ostermann, 01/31/2017