coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Canonical structure inference gets lost with application

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Canonical structure inference gets lost with application
Date: Sat, 23 Nov 2019 19:37:30 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=arthur.aa AT gmail.com; spf=Pass smtp.mailfrom=arthur.aa AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f180.google.com
Ironport-phdr: 9a23:ugwqFh282nTfNshWsmDT+DRfVm0co7zxezQtwd8Zse0fKvad9pjvdHbS+e9qxAeQG9mCsLQd1rWd6fyocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbalvIBi2rwjdudcajIR/Iast1xXFpWdFdf5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALMTRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTlkzkMOSIn/27Li8xwlKNbrwynpxxj2I7ffYWZOONjcq/BYd8WQGxMVdtTWSNcGIOxd4QAAeoPM+hbsofzuUcBoACiBQWwHu7j1iNEimP00KA8zu8vERvG3AslH98WrHnUtsn1NKcPUeCv0aLF0TTCYO1I2Tjj9YfIdQ0qruySUrltbcfRzE4vFxnEjlWVtIfoOCma1v4Rs2ib8upgT/ijhHQ9pAxqrTivw90jiojNho4P1l/E8iB5zZ8zKNalS0B7ecapHIVMuyyeLYd7QcMvT3t2tCok1LEKo4O3cSsWxJkh2hXRceaIc5KS7RLmTOuRISl3hHZieL+ngha960mgyunlWsmt01ZGszNJktfRun0OyxDf8MeHSvx6/keu3TaAyRrf5f1DIUAxjabbKpghzaAslpcLr0jPAiv7lF/1gaKWbEko5Pak5/r9brn7pZKQK5d4igTkPaQvnsy/D/44Mg8LX2WD4+u8zqHj/U3kQLVQlPE5iLPWvYvVJcQevKG5AgtV3pw/5Ba4CjeqyM4YkmUfLFJZZBKHiJDkNE3JIPDhFPuwn1CskCpwyP3dJb3gApDNLmDZn7v7fLZ97VRcyAspwtxF6ZJUEOJJHPWmcUjo/PfcExVxZwez2qPsDMh3/oIYQ2OGRKGDZvD8q1iNs8s1P+mRfsc8qjvjJvQir/LjxVY8nkUceOH91IELaG2iWP1vC0qcaHvoxNwGFDFZ7UIFUOX2hQjaAnZobHGoUvd5v2ljUd/0PcL4XomoxYe58mK7E5lRPD4UD1mNFTLxdNzBVa5cMGSdJchuljFCXr+kGdd4hEOe8TTiwr8iFdL6vygRtJbtzt9wvrSBmhQ79DgyBMOYgTjUEzNE21gQTjpz55hR5FRnww7ag6d9iv1cU9dU4qERXw==

Hi everyone,

I am trying to use canonical structures for an inference task, and I
am having trouble getting the unification engine to cooperate:

From Coq Require Import ssreflect ssrfun.
Set Implicit Arguments.

Record box T := Box { unbox : T }.
Canonical box_def T x := @Box T x.

(* I want Coq to try unify "unbox f ~ S" and "x ~ 0" and to conclude
that "f" must be "box_def S",
since "box_def" is canonical. But the inference does not work... Maybe the
first unification problem "unbox f x ~ 1" is triggering the
canonical structure inference directly? *)
Fail Definition infer :=
(fun (f : box (nat -> nat)) (x : nat) & phant_id (unbox f x) 1 =>
(f, x)) _ _ id.

(* If "unbox" does not appear in head position, unification works just fine.
*)
Definition infer :=
(fun (f : nat -> nat) (x : box nat) & phant_id (f (unbox x)) 1 =>
(f, x)) _ _ id.

Is this behavior intentional? Can it be circumvented?

--
Arthur Azevedo de Amorim

[Coq-Club] Canonical structure inference gets lost with application, Arthur Azevedo de Amorim, 11/24/2019
- Re: [Coq-Club] Canonical structure inference gets lost with application, Beta Ziliani, 11/24/2019