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.