Início / coding / Perguntas / 77496923
Accepted
Alicia M.
Asked: 2023-11-17 01:34:43 +0800 CST

Compreensão de conjuntos complexos

  • 772

Estou me deparando com um problema e não sei se é a maneira de Isabelle gerenciar a compreensão do conjunto ou se estou tendo um momento muito lento.

Este lema continua muito bem

lemma "{x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}"
  by auto

E este simplesmente não

lemma "{x | x y. (P x y)} ∩ {x | x y z. (Q x y z)} = {x | x y z. (P x y) ∧ (Q x y z)}"

Deve haver uma diferença entre os dois e não vejo isso. Obviamente, preciso do segundo, meu (P x y)e (Q x y z)é bastante complexo e será difícil simplificá-lo.

Como sempre, qualquer ajuda (ou redirecionamento para alguma direção mais saudável) é muito apreciada.

isabelle

1 respostas

  1. Best Answer

    O lado esquerdo {x | x y. P x y} ∩ {x | x y z. Q x y z}contém tudo xo que ele contém (∃y. P x y) ∧ (∃y z. Q x y z).

    O lado direito {x | x y z. P x y ∧ Q x y z}contém tudo xo que vale para isso ∃y z. P x y ∧ Q x y z.

    A diferença é que a primeira restrição é mais fraca, pois o yque faz P x yacontecer e o yque faz Q x y zacontecer não precisam ser iguais.

    A {x | x. P x} ∩ {x | x y. (Q x y)} = {x | x y. (P x) ∧ (Q x y)}situação é diferente, pois a única variável compartilhada é o x, mas o xé um pouco especial.

    Se você reduzir as afirmações acima a quantificadores, talvez fique um pouco mais claro: A primeira diz essencialmente que, para todos x:

    P x ∧ (∃y. Q x y) ⟷ (∃y. P x ∧ Q x y)

    Enquanto o segundo diz que, para todos X:

    (∃y z. P x y) ∧ (∃y z. Q x y z) ⟷ (∃y z. P x y ∧ Q x y z)
    • 2

relate perguntas