¿Qué sucede si intentamos extraer un testigo pero en realidad no existe a partir de un término de tipo existencial?

12

Dado un término t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))en la teoría de tipos de Martin-Lof, ¿cuál es el valor de w(t(0)), dónde westá el operador que extrae el testigo de un término de tipo existencial?

día
fuente
Creo que te refieres a . ¬(x=0)
Mark Reitblatt
Sí, Mark, gracias por señalar eso, arreglado.
día

Respuestas:

12

ty.(¬(0=0)0=S(y))y¬(0=0)0=S(y)¬(0=0)0=00=S(0)0=S(1)y

Mark Reitblatt
fuente
10

Para demostrar la respuesta de Mark, considere la siguiente prueba tde su declaración, escrita en Coq. En la prueba asumimos que se da un parámetro kde tipo nat. Usamos kcomo el valor de yen caso 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.

Podemos demostrar que t 0es igual a k:

Theorem A: projT1 (t 0) = k.
Proof.
  auto.
Qed.

El protT1está ahí porque t 0no es sólo un número natural, pero en realidad un número natural con una prueba de que 0 <> 0 -> 0 = S yy projT1desecha la prueba.

El código Ocaml extraído para t, obtenido con el comando Extraction kes

(** val t : nat -> nat **)

let rec t = function
  | O -> k
  | S n0 -> (match n0 with
              | O -> O
              | S n1 -> S (t n0))

De nuevo, podemos ver que t 0es igual a k, que era un parámetro asumido de forma arbitraria.

Andrej Bauer
fuente
Gracias por el ejemplo en Coq, Andrej, aclara más.
día