Início / coding / Perguntas / 79597336
Accepted
Arthur Kexu-Wang
Asked: 2025-04-29 05:54:38 +0800 CST

Em Coq (ou Rocq), um lema com uma conclusão universal não pode ser aplicado a outras premissas?

  • 772

Quando provo com Coq (ou Rocq), descubro que, às vezes, se uma hipótese é "P" e outra é "P -> para todo x, Q x", não consigo fazer de "para todo x, Q x" uma nova premissa pelo modus ponens.

Aqui está um exemplo:

Theorem post_forall: forall (X: Type) (P: Prop) (Q: X -> Prop),
  (P -> forall x, Q x) -> forall x, P -> Q x.
Proof.

(* 
Here is a correct proof:

intros X P Q. 
intros H.
intros y.
intros H1.
generalize dependent y.
apply H.
apply H1. 
Qed.
*)


intros X P Q. 
intros H.
intros y.
intros H1.
generalize dependent y.
apply H in H1.
(** STUCK HERE, 

But Why cannot we do this???

They look the same.
*)
Admitted.

A prova ficará presa na linha "aplicar H em H1" e Coq retornará "Não foi possível encontrar uma instância para a variável x".

Mas "x" precisa ser instanciado? Parece desnecessário. Qual é a diferença entre as duas provas?

Perguntei ao DeepSeek e ao ChatGPT. Nenhum deles conseguiu fornecer uma resposta satisfatória.

Também imaginei que poderia ser o problema da ocorrência de variáveis ​​no antecedente. Mas, se fosse, a tática de "generalizar dependente" deveria ter falhado.

logic

3 respostas

  1. Veja a documentação : uma solução simples é usar eapply H in H1, ou simplesmente concluir a prova com exact (H H1).

    Alternativamente, observe que você realmente não precisa de táticas aqui: toda a prova é apenas fun X P Q H x p => H p x.

    • 0
  2. Best Answer

    O comportamento que você está procurando está disponível , mas você precisa usar a specializetática, e ela substituirá sua implicação em vez de sua consequência [ referência ].

    Exemplo com algum contexto de prova omitido:

    H : P -> (forall x : X, Q x)
H1 : P
______________________________________(1/1)
False

    specialize (H H1)

    H : forall x : X, Q x
H1 : P
______________________________________(1/1)
False

    Eu também estou confuso. Acho que você encontrou uma peculiaridade em "apply". Já vi restrições semelhantes ao raciocínio sobre quantificações internas documentadas em outros recursos de versões mais antigas. (Especificamente no CPDT, se alguém se lembra...)

    • 0

  3. O módulo pones é A => B, aqui você tem (forall x, A -> B x) => (A => forall x, B x). Não é a mesma coisa. Claro que o módulo abre implica isso, mas não se aplica diretamente. Se você quiser usar o módulo pones, precisa introduzir todas as variáveis ​​primeiro.

    Theorem post_forall: forall (X: Type) (P: Prop) (Q: X -> Prop),
  (P -> forall x, Q x) -> forall x, P -> Q x.
Proof.
  intros X P Q Hpq x p. apply Hpq. exact p.
Qed.
    • -1

relate perguntas