O que acontece se tentarmos extrair uma testemunha, mas ela realmente não existe a partir de um termo do tipo existencial?

12

Dado um termo t : ∀x.∃y.(¬(x = 0) ⇒ x = S(y))na teoria de tipos de Martin-Lof, qual é o valor de w(t(0)), onde westá o operador que extrai a testemunha de um termo de tipo existencial?

dia
fonte
Eu acho que você quer dizer . ¬(x=0)
Re: Reitblatt #
Sim, Mark, obrigado por apontar isso, corrigido.
day

Respostas:

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
fonte
10

Para demonstrar a resposta de Mark, considere a seguinte prova tde sua declaração, escrita em Coq. Na prova, assumimos que um parâmetro kdo tipo naté fornecido. Usamos kcomo valor de ycaso 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 provar que t 0é igual a k:

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

O protT1está lá porque t 0não é apenas um número natural, mas na verdade um número natural com uma prova de que 0 <> 0 -> 0 = S ye projT1joga fora a prova.

O código Ocaml extraído para t, obtido com o comando Extraction ké

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

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

Novamente, podemos ver que t 0é igual a k, que era um parâmetro assumido arbitrariamente.

Andrej Bauer
fonte
Obrigado pelo exemplo em Coq, Andrej, esclarece mais.
Dia