<p>To demonstrate Mark's answer, consider the following proof <code>t</code> of your statement, written in Coq. In the proof we assume that a parameter <code>k</code> of type <code>nat</code> is given. We use <code>k</code> as the value of <code>y</code> in case <code>x = 0</code>:</p>

<pre><code>Parameter k : nat.

Theorem t : forall x : nat, { y : nat | x &lt;&gt; 0 -&gt; 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.
</code></pre>

<p>We can prove that <code>t 0</code> is equal to <code>k</code>:</p>

<pre><code>Theorem A: projT1 (t 0) = k.
Proof.
  auto.
Qed.
</code></pre>

<p>The <code>protT1</code> is there because <code>t 0</code> is not just a natural number, but actually a natural number <em>with</em> a proof that <code>0 &lt;&gt; 0 -&gt; 0 = S y</code> and <code>projT1</code> throws away the proof.</p>

<p>The extracted Ocaml code for <code>t</code>, obtained with the command <code>Extraction k</code> is</p>

<pre><code>(** val t : nat -&gt; nat **)

let rec t = function
  | O -&gt; k
  | S n0 -&gt; (match n0 with
              | O -&gt; O
              | S n1 -&gt; S (t n0))
</code></pre>

<p>Again we can see <code>t 0</code> is equal to <code>k</code>, which was an aribtrarily assumed parameter.</p>

CC BY-SA 2.5
2010-12-17T16:35:28.003Z
Thanks for the example in Coq, Andrej, it clarifies more.
day
CC BY-SA 2.5
2010-12-02T21:39:12.937Z
2010-12-02T21:39:12.937Z
Andrej Bauer
<p>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.</p>

CC BY-SA 2.5
2010-11-29T22:32:13.553Z
2010-11-29T22:32:13.553Z
Mark Reitblatt
<p>Given a term <code>t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))</code> in Martin-Lof's type theory, what's the value of <code>w(t(0))</code>, where <code>w</code> is the operator that extracts the witness of a term of existential type?</p>

CC BY-SA 2.5
2010-11-29T21:41:06.393Z
I think you mean $\neg(x=0)$.
Mark Reitblatt
CC BY-SA 2.5
2010-11-29T22:16:22.403Z
Yes, Mark, thanks for pointing out that, fixed.
day
<lo.logic><type-theory><proof-theory>
What happens if we try to extract a witness but it actually does not exist from a term of existential type?
day
# What happens if we try to extract a witness but it actually does not exist from a term of existential type?

(Asked by: username_0 on 2010-11-29)

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?

**Tags:** lo.logic, type-theory, proof-theory
> **Comments:**
> **username_1**: I think you mean $\neg(x=0)$.  
> **username_0**: Yes, Mark, thanks for pointing out that, fixed.  

---

## 2 answers

### Answer by username_1 on 2010-11-29. Score: 12 | Accepted answer

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.


---

### Answer by username_2 on 2010-12-02. Score: 10

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.

> **Comments:**
> **username_0**: Thanks for the example in Coq, Andrej, it clarifies more.  

---

