Форум за въпроси

Типове в Coq на предикатните съждения в законите на de Morgan

Типове в Coq на предикатните съждения в законите на de Morgan

от Александър Гудев -
Number of replies: 1

Здравейте!

В задачата за доказване на законите на де Морган квантифицираните формули са дадени така:

¬ (∀x A) ↔ ∃x ¬A

Тъй като 'А' по някакъв начин трябва да зависи от 'x', то ако 'А' е просто от тип Prop, то задачата не би имала много смисъл.

В тези закони не даваме никакви ограничения за 'х' - достатъчно ли да приемем, че "x : nat", а А - "nat → Prop", и тогава това ли е формулата, която трябва да докажем?

  Variable A : nat -> Prop.

  Lemma Morgan5: (exists x, ~(A x)) -> ~(forall x, A x).

В противен случай, какъв тип се очаква да дадем на x, и достатъчно ли е доказателството да работи за nat, Set и Type?

Благодаря,

Александър Гудев

In reply to Александър Гудев

Re: Типове в Coq на предикатните съждения в законите на de Morgan

от Трифон Трифонов -

Здравей, Александър,

Абсолютно си прав, за да има смисъл задачата, би трябвало A да е (поне) едноаргументен предикат. Когато доказвахме формулата на пияниците използвахме едноместен предикат d(x), тук се има предвид същото нещо. Задачата е записана "като за дъска", където A е метапроменлива за произволна формула, която може да съдържа свободни променливи, като е ясно, че същественият случай е този, в който x се среща свободно в A. За да се формализира това в Coq е необходимо тази зависимост да е експлицитно изразена, вместо имплицитно.

Ако направиш x да е nat не би трябвало да използваш нито една аксиома на естествените числа, освен това че множеството е непразно.

За да е доказателството в произволна общност, можеш да приемеш, че имаш домейн Variable D : Set и тогава Variable A : D -> Prop. Тогава обаче в Coq ти трябва допълнително допускане: inhabited T (прочети раздела "Being inhabited" в тази страница).

Можеш да си дефинираш собствен предикат:

Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A.

и да добавиш допускането inhabited D към теоремата за пияниците. Тогава доказателството пак би трябвало да работи.

Но да се докаже за естествените числа би трябвало да е достатъчно.