BC1d: Induktywna logika [TODO]

Wiemy, że słowo kluczowe Inductive pozwala nam definiować nowe typy (a nawet rodziny typów, jak w przypadku option). Wiemy też, że zdania są typami. Wobec tego nie powinno nas dziwić, że induktywnie możemy definiować także zdania, spójniki logiczne, predykaty oraz relacje.

Induktywne zdania


Inductive false_prop : Prop := .

Inductive true_prop : Prop :=
| obvious_proof : true_prop
| tricky_proof : true_prop
| weird_proof : true_prop
| magical_proof : true_prop.

Induktywne definicje zdań nie są zbyt ciekawe, gdyż pozwalają definiować jedynie zdania fałszywe (zero konstruktorów) lub prawdziwe (jeden lub więcej konstruktorów). Pierwsze z naszych zdań jest fałszywe (a więc rónoważne z False), drugie zaś jest prawdziwe (czyli równoważne z True) i to na cztery sposoby!

Ćwiczenie (induktywne zdania)


Lemma false_prop_iff_False : false_prop <-> False.

Lemma true_prop_iff_True : true_prop <-> True.

Prawda i fałsz


Module MyConnectives.

Inductive False : Prop := .

Fałsz nie ma żadnych konstruktorów, a zatem nie może zostać w żaden sposób skonstruowany, czyli udowodniony. Jego definicja jest bliźniaczo podobna do czegoś, co już kiedyś widzieliśmy — tym czymś był Empty_set, czyli typ pusty. Nie jest to wcale przypadek. Natknęliśmy się (znowu) na przykład korespondencji Curry'ego-Howarda.
Przypomnijmy, że głosi ona (w sporym uproszczeniu), iż sorty Prop i Set/Type są do siebie bardzo podobne. Jednym z tych podobieństw było to, że dowody implikacji są funkcjami. Kolejnym jest fakt, że False jest odpowiednikiem Empty_set, od którego różni się tym, że żyje w Prop, a nie w Set.
Ta definicja rzuca też trochę światła na sposób wnioskowania "ex falso quodlibet" (z fałszu wynika wszystko), który poznaliśmy w rozdziale pierwszym.
Użycie taktyki destruct lub inversion na termie dowolnego typu induktywnego to sprawdzenie, którym konstruktorem term ten został zrobiony — generują one dokładnie tyle podcelów, ile jest możliwych konstruktorów. Użycie ich na termie typu False generuje zero podcelów, co ma efekt natychmiastowego zakończenia dowodu. Dzięki temu mając dowód False możemy udowodnić cokolwiek.

Inductive True : Prop :=
| I : True.

True jest odpowiednikiem unit, od którego różni się tym, że żyje w Prop, a nie w Set. Ma dokładnie jeden dowód, który w Coqu nazwano, z zupełnie nieznanych powodów (zapewne dla hecy), I.

Induktywne definicje spójników logicznych

W rozdziale pierwszym dowiedzieliśmy się, że produkt zależny (typ, którego termami są funkcje zależne), a więc i implikacja, jest typem podstawowym/wbudowanym oraz że negacja jest zdefiniowana jako implikowanie fałszu. Teraz, gdy wiemy już co nieco o typach induktywnych, nadszedł czas by zapoznać się z definicjami spójników logicznych (i nie tylko).

Inductive and (P Q : Prop) : Prop :=
| conj : P -> Q -> and P Q.

Dowód koniunkcji zdań P i Q to para dowodów: pierwszy element pary jest dowodem P, zaś drugi dowodem Q. Koniunkcja jest odpowiednkiem produktu, od którego różni się tym, że żyje w Prop, a nie w Type.

Inductive or (P Q : Prop) : Prop :=
| or_introl : P -> or P Q
| or_intror : Q -> or P Q.

Dowód dysjunkcji zdań P i Q to dowód P albo dowód Q wraz ze wskazaniem, którego zdania jest to dowód. Dysjunkcja jest odpowiednikiem sumy, od której różni się tym, że żyje w Prop, a nie w Type.

End MyConnectives.