Skip to Content.
Sympa Menu

coq-club - [Coq-Club] What problem does an extracted function solve?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] What problem does an extracted function solve?


Chronological Thread 
  • From: "Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] What problem does an extracted function solve?
  • Date: Mon, 4 Nov 2013 10:11:54 +0000
  • Accept-language: en-GB, en-US

It's easy to show that

T =
fun (x : nat) (H : x > 0) => exist (fun y : nat => y > 0) x H
: forall x : nat, x > 0 -> {y : nat | y > 0}

Clearly, T cannot produce an output unless it is given a nat x and a proof
that x > 0. However, I'm not sure what to make of the function extracted from
T, i.e.

let t x =
x

because t can produce an output for all values of x, not only x > 0. On the
face of it, t appears to solve a different problem than T. How should one
view the relationship between t and T?

Regards,
Jeff.


Archive powered by MHonArc 2.6.18.

Top of Page