O que instanciar variáveis ​​existenciais com variável fora do escopo implica?

7

Tenho a seguinte prova inacabada de um lema:

Goal forall (P : Type -> Prop) (Q : Prop),
  ((forall x, (P x)) -> Q) -> (exists x, P x -> Q).
Proof.
  intros. 
  eapply ex_intro. intros. apply H. intros. eapply H0.

O problema é a última eapplyfalha, com a mensagem

Error:
In environment
P : Type -> Prop
Q : Prop
H : (forall x : Type, P x) -> Q
H0 : P ?x
x : Type
Unable to unify "?x" with "x" (cannot instantiate "?x" because "x" is not in
its scope: available 
arguments are "P" "Q" "H").

As etapas da prova já parecem muito fraudulentas. A prova constrói uma variável existencial para ficar no lugar de na segunda metade e, em seguida, tenta instanciar usando o obtido como premissa após a aplicação da hipótese . As etapas da prova parecem uma prova cíclica para mim.xx(forall x, (P x)) -> Q

O que em geral esta mensagem implica? Que tipos de erros lógicos essa mensagem indica aqui?


Há um problema recente no Github da Coq, na verdade, indica que instâncias instáveis ​​fora do escopo PODEM provar falsidade, exceto pelo fato de serem bloqueadas pelo QED.

https://github.com/coq/coq/issues/8215

Jason Hu
fonte
2
Você não será capaz de provar isso construtivamente. Você pode, se você assumir algum axioma adequado da lógica clássica.
Derek Elkins saiu de SE
2
@DerekElkins eu aprendi isso. mas a instanciação fora do escopo revela a razão pela qual isso não funcionará na lógica construtiva?
Jason Hu
11
Eu não diria isso, embora comece a sugerir. Existem várias maneiras de não conseguir provar isso de forma construtiva e, obviamente, todas as abordagens precisam falhar para que isso não seja possível. A prova construtiva de um existencial requer a produção de uma testemunha. Nesse caso, precisamos criar um valor arbitrário de um tipo arbitrário que seja impossível e nenhuma das suposições nos fornece um valor do tipo. A lei do meio excluído, por outro lado, permite-nos extrair valores do nada.
Derek Elkins saiu de SE
11
A prova padrão do LEM no cálculo sequencial clássico é de fato "uma variável que foge do seu escopo". Ainda não olhou muito de perto, mas pode ser que você tenha uma situação semelhante.
Gallais
Você realmente quis dizer (P : Type -> Prop)? E não (A : Type) (P : A -> Prop)? Se você quis dizer o último, poderá provar a negação do seu lema .
Anton Trunov 22/09

Respostas:

8

Quando você faz uma introdução existencial, você está dizendo que há algum termo , que é representado pela variável de unificação , de tal forma que . Em seguida, tenta aplicar a . Ele tenta generalizar , porque se puder mostrar que para uma constante nova (representada pela saída Coq), então seguirá. Ele tenta unificar essa constante nova , com a variável de unificação , mas isso não é permitido. De uma perspectiva lógica, representa um termot?xP(t)QP(t)H:(x.P(x))QP ?xP(c)cxx.P(x)x?x?xte que prazo é, por definição frescura, distinto do fresco (ie ), que é só para dizer não estava no escopo quando introduzimos , então não pode ter dependesse disso.cxctt

Como um cenário mais simples, não podemos provar usando introdução existencial com . não está no escopo nesse ponto.x.y.x=yyy

Derek Elkins deixou o SE
fonte