coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Cannot satisfy constraint" error using subset types

From: Jan Bessai <jan.bessai AT tu-dortmund.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] "Cannot satisfy constraint" error using subset types
Date: Sat, 29 Apr 2017 11:59:13 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=Neutral smtp.pra=jan.bessai AT tu-dortmund.de; spf=Pass smtp.mailfrom=jan.bessai AT tu-dortmund.de; spf=None smtp.helo=postmaster AT unimail.uni-dortmund.de
Ironport-phdr: 9a23:L0VBDhRGxpfzfAGWLktYU35fE9psv+yvbD5Q0YIujvd0So/mwa69YBKN2/xhgRfzUJnB7Loc0qyN4vymATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbx/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/nzJhMx+jKxVoxyvqBJwzIHWfI6bO+Fzfr/fcN4AWWZNQshcWi5HD4ihb4UPFe0BPeNAoof5vVQOqwa1CBSyC+P00T9HnH721rA93uQjCw7G2hYsEMkQv3TPt9X6LqYSXPupzKnV1DnMcvRW2S3h6IjNbxAhp+yDUahtfsXP0EQiER7OgFaIqYH9Ij+ZyOAAv3KF4+Z9V++jkXMrpx9yrzS1xsogl5HFi4EVx1ze6yl13pw5KN+6RUJhfNKpH5tduieHPIVsWMwiWXtnuCMix70Gp5G7eC8KxYw6xx7ZavyHdpKH4hPnVOqLPDd4gnNldKuiiBa160ig1uj8VtSy0FlXtCZKj8fDumgM1xzV9MeHVuNw8lq/1TuLzQzf9PxILEIumabGNZIswaQ8m5oOvUjbGy/5gkT2jKuYdkU+/eio7vzqYrf8qZ+aLYN7kR/xMr81msOlAOQ1KRQOX3WC9euh073j51H5QLBXjv0wj6bVqo3VKtoDqq6jHwBVypoj6wq4Dzq+zNsYmmAHIEtZdxKDkojmIErDIOv4DPe6m1Sjii1nx/HAPr37A5XCNGLPkLn7feU110kJww0qiNtb+ph8C7cbIfu1VFWimsbfC0obOgr86ev8E9x8ntccUGTJCKKCK6rTmUOVo+4oOfWJeYkZ/jrwfat2r8XyhGM0zAdONZKi2oEaPSi1

Hi,

The term "fds" has type "id -> id -> {n : nat & eqn n}"
while it is expected to have type "id -> id -> {n : nat & eqn n}" (cannot
satisfy constraint
"eqn (length tys1)" == "(fun n : nat => eqn n) (projT1 (fds f c))").

The types that it wants to be identical are identical, and they are also
identical if all implicit arguments, universe levels etc. are printed.

I came across issues like that when porting a proof from Coq 8.5 to 8.6. My guess is reduction during unification got less intelligent but more predictable. I usually get around these cases doing something like

assert (x_eq: x = f y). {
unfold f; destruct y; simpl; reflexivity.
}
rewrite x_eq.

potentially using "rewrite in" or simpler proofs for x_eq.

This is a bit explicit and brittle, but I tend to prefer it over overly intelligent magic.
Hope this helps.

Bests,
Jan

[Coq-Club] "Cannot satisfy constraint" error using subset types, Klaus Ostermann, 04/29/2017
- Re: [Coq-Club] "Cannot satisfy constraint" error using subset types, Jan Bessai, 04/29/2017
  - Re: [Coq-Club] "Cannot satisfy constraint" error using subset types, Klaus Ostermann, 04/29/2017
    - Re: [Coq-Club] "Cannot satisfy constraint" error using subset types, Jan Bessai, 04/30/2017