Skip to Content.
Sympa Menu

coq-club - [Coq-Club] "exists" Extraction

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "exists" Extraction


Chronological Thread 
  • From: Morgan Sinclaire <morgansinclaire AT boisestate.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] "exists" Extraction
  • Date: Wed, 10 Apr 2019 15:31:15 -0600
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=morgansinclaire AT boisestate.edu; spf=Pass smtp.mailfrom=morgansinclaire AT boisestate.edu; spf=None smtp.helo=postmaster AT mail-wm1-f54.google.com
  • Ironport-phdr: 9a23:kBbKQhS1LGqUHNmXfE5lIEymL9psv+yvbD5Q0YIujvd0So/mwa6yYBWN2/xhgRfzUJnB7Loc0qyK6vmmADNLuMjY+DBaKdoQDkdD0Z1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrssxhfTv3dFeetayX5pKF6Ogh3w4tu88IN5/ylfpv4t69RMXbnmc6g9ULdVECkoP2cp6cPxqBLNVxGP5nwSUmUXlhpHHQ3I5wzkU5nyryX3qPNz1DGVMsPqQ780Xy+i77pwRx/zlCgHLT85/3rJhcF2kalWvQiupx17w47TfYGVKP9zdb7TcN8GWWZMWNtaWipcCY2+coQPFfIMMulYoYfzpFUAsAWwChW3Cez11jNFnGX70bEm3+kjFwzNwQwuH8gJsHTRtNj7M6ASUfq6zKbSyzXIcu5Y2Tb76IfUdhAuu/CMXahufsHMzkQvEgTFjk+fqYP/OTOVzeUNs26H4OpkT+2vinQnpB9qrze0wccsi5LJiZwOylDY7yp53Jg6KcemR0FmfN6pCZ1dvDyUOYtxR8MtWWBouCAix7IauZ67eCkKyIw9yB7bcfOLaY6I7Qz/VOuXPDx2h2pldaqhixqu9UWs0O7xW8mu3FpXsCZIkcPAu3AC2hHV98OJUOFy/l271jaKzw3T6v9LIUQzlafDLp4u2L8wlp4KvUXNGy/6hVz6jKGWe0gr4OSo5OPnYrLppp+YKYB4kB3xMqMrmsCnAOQ4NBYBX3SD9OiiyLHu+Vf1TbZKg/Esj6XVrpPXKd4bq6O2GwNV15ws6xe7DzeoytQYmnwHIUpAeBKAlYjpNEvBIPbjDfe+hVSjjDNryOrHPr37HJrANWPMkLDgfbZm9UFc0xYzwspD551KEL0OPu/8WlLpuNzCEhA5KxC0w/rgCNhlyoweXnuPDraFP6PWrF+H/fkiI/KMZY8QoDbyMeIp5//ojX8jmF8SZ7Ol3ZUNaCPwIvMzKEKAJHHon90pEGEQvwN4Qva5pkeFVGt2YGy9VqR03TA9A4avDJ3ODtSoh6aO1SGgH5tdYmlHEF2kG3DpbIifR/4QZWSfLtI3wW9MbqSoV4J0jULmjwT90bcydrOFqB1djorq0Z1O38OWkBgz8TJuCMHEjTOHSGBvk3gUTiM7mq1zvB4kkwvR4e1Dm/VdUOdrybZRSA5ja8zWyO1hBsvuUx7MONqFVQT+G4j0MXQKVts0huQ2TQN9FtGl1E2R2iOrB/oKkuXOCsFotK3b2Hf1KoB2zHOUjKQ=

I'm having trouble with extracting information from Prop, and specifically with the Prop/Type and ex/sig distinction which I wasn't aware of before. What I have is this definition:

Fixpoint valid (P : ftree) : Prop := ...

Where "ftree" is a certain infinitely-branching tree structure I've defined, and for this reason "valid" is undecidable in general.

Now I'm in the middle of a proof, where I have a hypothesis that looks like:

H : forall m : nat, exists t : ftree, valid t /\ [stuff about t]

And to complete my proof I need to produce a function of the form:

nat -> ftree

And by Curry-Howard, H should be such a function, but Coq doesn't believe so, because I can't extract computational information from "exists" (as discussed here, section 12.2).

Now, I know Coq does this because it wants to limit the amount of program extraction one can do, but in my case I want full Curry-Howard. So my first question is:

1) Can I "toggle" this feature in Coq so I can get full program extraction from "exists"?

If not, I don't know much about Sigma types, but I don't think I can just convert this "ex" into "sig" since the predicate "valid" is undecidable? I haven't worked with Type at all, so my other question:

2) Is there an easy way to convert a Prop to a Type?

If so, I can change my definition of "valid" to be of type Type. Currently that definition is 63 lines and involves some Prop syntax such as "forall" and "/\", so any reference on how to do that in Type would be helpful so I can understand what I'm doing.

Thanks!




Archive powered by MHonArc 2.6.18.

Top of Page