Given a term t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))
in Martin-Lof's type theory, what's the value of w(t(0))
, where w
is the operator that extracts the witness of a term of existential type?
-
$\begingroup$ I think you mean $\neg(x=0)$. $\endgroup$– Mark ReitblattNov 29, 2010 at 21:41
-
$\begingroup$ Yes, Mark, thanks for pointing out that, fixed. $\endgroup$– dayNov 29, 2010 at 22:16
2 Answers
Any value. It depends upon which $t$ you are given. A term of type $\exists y.(\neg(0 = 0) \Rightarrow 0 = S(y))$ is a pair of an int $y$ and a function that takes a proof of $\neg(0=0)$ and gives you a proof of $0 = S(y)$. You can use a term of type $\neg(0 = 0)$ and type $0 = 0$ (from reflexivity) to derive a term of any type you want. This includes a term of type $0 = S(0)$, $0 = S(1)$, $\ldots$. So, you can make $y$ any integer you want.
To demonstrate Mark's answer, consider the following proof t
of your statement, written in Coq. In the proof we assume that a parameter k
of type nat
is given. We use k
as the value of y
in case x = 0
:
Parameter k : nat.
Theorem t : forall x : nat, { y : nat | x <> 0 -> x = S y}.
Proof.
induction x.
exists k; tauto.
induction x.
exists 0; auto.
destruct IHx as [z G].
exists (S z).
intro H.
elim G; auto.
Defined.
We can prove that t 0
is equal to k
:
Theorem A: projT1 (t 0) = k.
Proof.
auto.
Qed.
The protT1
is there because t 0
is not just a natural number, but actually a natural number with a proof that 0 <> 0 -> 0 = S y
and projT1
throws away the proof.
The extracted Ocaml code for t
, obtained with the command Extraction k
is
(** val t : nat -> nat **)
let rec t = function
| O -> k
| S n0 -> (match n0 with
| O -> O
| S n1 -> S (t n0))
Again we can see t 0
is equal to k
, which was an aribtrarily assumed parameter.
-
$\begingroup$ Thanks for the example in Coq, Andrej, it clarifies more. $\endgroup$– dayDec 17, 2010 at 16:35