coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] A unification problem

From: Qinshi Wang <qinshiw AT cs.princeton.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] A unification problem
Date: Sun, 2 Jan 2022 22:30:49 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=qinshiw AT cs.princeton.edu; spf=Pass smtp.mailfrom=qinshiw AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT violeteyes.cs.princeton.edu
Ironport-data: A9a23:wTHLvKMLaJxV5NfvrR3flsFynXyQoLVcMsFnjC/WdVHohzJxgzQOnzMbXjqHPfyOYGSmf4ggPIq2oBwPvZbSv4NqS1BcGVNFHysb85KdbTi6Bh6tZH3KdpWroHqKXqzyU/GYRCwPZiKa9kfF3oTJ9yEmj/nRHuCkUoYoBwgoLeNaYHd54f5cs7Vh6mJYqYDR7zKl4bsekeWHULOW82Ic3lYv1k62gEgHUMIeF98vlgdWifhj5DcynpSOZX4VDfnZw3DQGuG4EgMmLtsvwo1V/kuBl/ssIs2klbL2bkAbT6WUNhPIkmBXXaOvnh9E4CE+z87XNtJFMxcR0mzT2YkqlpMQ6PRcSi9xVkHIsP0cVQJYEj5WNrYA4KXGJ3OyrcuViUDKbhMAxt03UBtvYdJFkgpwKTwepKdAdVjhdCurjOWvhbm/V+NEndUmNMCtPYUFu3gmwyuxMBqMaYSbFv+MussBiW923tQUSK6YPJFENC40OUyGPgkQb34JLr4+uvPx3iynN2VMwL6OjbQ25Gze0AFg3aOrO8GTYsaLQ85YgkGe4G/K4gzE7tghHIT34VK4HriE34cjXB8XWb7+0JWm9/lujUGe12EIThYNE0OhoP+yh1K5XZRSJ1F8Fu8Gs/0p7ELyJjXid0TQnZJGlkd0txls/ykS4xrL0rDV5Q2UGm8CCDNNdbTKcecoECcy2Abhc8zBXFRSXX78dZ5Z3ryP6yuoOC4eIHMFY2kJQRZtDxzLyG0spkqnc+uP25JZQjE49f8cDtxKQOUDa20vsPM2
Ironport-hdrordr: A9a23:K0GCB64fERYPsGbDeQPXwPzXdLJyesId70hD6qkRc20zTiX2raCTdZggtCMc6wx+ZJhDo6HjBEDoexq1nvRICOIqTNKftWfdyQ+VxUJZgLfK8nnPHyX/86p6zqdvc693DZnVAUJhhcj3pCmUeuxQo+VvPJrFuQ4W9RhQcT0=
Ironport-phdr: A9a23:D0mL8BI9fHV7hRqPWdmcuKJmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvLM01weCANqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yf2+94fObwhGmDaxbrN/IRerpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIOD43/m/UhMJtkqxUvAmspxljz4POeoyZKOZyc6HbcNgHRWRBRMFRVylZD42nbosPCfEBPeZZr4Lgp1QBtx2+BQaxD+7o0z9Ih3n23bY60+QgHwDLxxAvH8kUvHTMttX1NaESXvyrw6nUyjXDaela1ing54jVax0sp+yHUr1sf8TL00YvCx/FgUuKqYzjJz6YyOQAvmqf4uZ8SO6iiG0qph9srjWtycohi4nEi58bx13G9ih0wok4KNylRUJnY9OpH4ZcuiWGOoZ4Tc0uX39ltSAnwbMFoZ62ZDUGxIokyhLFdvCLbpaE7gj+WOufIDp0nnJodbKnixqs7UStzvfwW8q03VpQsCZJjMTAumoN2hHc7MWMV+Fz8V272TmV0gDe8uFELl4wlarcM5Mh3L8wlp0XsUvdAi/5hkX3g7GNdkk+5ueo8P7rYq38pp+dMY97lh/xMrgpmsy5G+g3LBUBX3WD9eS90r3s41H5Ta1XgvEokaTVqo3WKdkFqqKjHgNY3Icu5wy/AjqmyNgYmGMILFNBeBKJlYjpPFTOLejhDfe+hVSsizdrx/HIP7D6HprNNWLPkK/7fbZ87U5T1BQ8zcxY55JSEL0OPu/8WlLpuNzCEhA5KxC0w/rgCNhlyoweXnuPDraFP6PWrF+H/fkiI/KMZY8QoDbyMeIp5//ojX8jmF8SZ7Ol3ZUNaCPwIvMzKEKAJHHon90pEGEQvwN4Qva5pkeFVGtqZnCpX6N02Tg9B8ryFIbFXYCsn5SKx2GjBJxQbW1aDVbKHHv1IdbXE8wQYT6fd5cy2gcPUqKsHtdJPf6GvxS806BmKOHZ5ioe85/vyYosjwUyvQ8z8jh5E8mM3nrLRHoyhnkJQTQ7wKd550Fx1wXauUCdq/dDU8RJ5vVCXxs9M9jRw/EoU7jP

Dear Coq folks,

I encountered a unification problem with the "apply" tactics and couldn't figure out the reason. In particular,

"eapply (register_write_spec)" failed with (Unable to unify "@object ?Goal1 ?Goal2" with "let (extern_env_object, extern_env, extern_object, extern_state) := target in extern_object".), while the right hand side was reduced to (@object Info (_expression_ Info)) by cbv.
None of eapply (register_write_spec), eapply (register_write_spec _) or simple eapply (register_write_spec) worked. But eapply (register_write_spec _ _ _) and simple eapply (register_write_spec _) worked. It's strange that the placeholders changed the behavior, and that simple eapply is stronger than eapply.
The result was changed by changing some seemingly irrelevant parts.

A minimal working example is attached. It's encouraged to debug the file with "display implicit arguments" on.

Many thanks for any kind of help.

Thanks,

Qinshi

Attachment: verif.v
Description: Binary data

[Coq-Club] A unification problem, Qinshi Wang, 01/03/2022