Jak definovat a formalizovat měřitelné struktury pomocí Hierarchy-Builderu?

V předchozím textu jsme se seznámili s možnostmi formalizace σ-algebr pomocí Hierarchy-Builderu, nástroje pro definici a práci s hierarchiemi v teorii míry. Nyní se zaměříme na proces definice a formalizace měřitelnosti, zejména jakým způsobem je možné pomocí tohoto nástroje definovat a instanciovat různé měřitelné struktury, jako jsou σ-algebra, obsah a měřitelné funkce.

coq
Copy code
Lemma salgebra0 : << G >> set0.
Proof. ... Qed.
Lemma salgebraC : forall A, << G >> A -> << G >> (~` A).
Proof. ... Qed.
Lemma salgebraU : forall A : (set T)^nat, (forall n, << G >> (A n)) -> << G >> (\bigcup_k A k).
Proof. ... Qed.

Po ověření těchto vlastností přistoupíme k instanciaci generátorů σ-algebry pomocí funkce Hierarchy-Builder. Ta nám umožňuje definovat generickou instanci měřitelné struktury pro libovolnou množinu G:

coq
Copy code
HB.instance Definition _ := @isMeasurable.Build (sdisplay G) (salgType G) << G >> (@salgebra0 _ G) (@salgebraC _ G) (@salgebraU _ G).

Tato konstrukce využívá definovaného rozhraní pro měřitelné struktury, které bylo vytvořeno pomocí Hierarchy-Builderu a zaručuje, že pro každou množinu G získáme typ generované σ-algebry. Tento přístup je velmi silný, protože umožňuje definici měřitelných struktur na různých úrovních abstrakce.

coq
Copy code
HB.mixin Record isContent d (T : semiRingOfSetsType d) (R : numFieldType) (mu : set T -> \bar R) := {
    measure_ge0 : forall x, 0 <= mu x;
    measure_semi_additive : semi_additive mu;
}.

coq
Copy code
Definition dirac (A : set T) : \bar R := (\1_A a)%:E.

Po instanciaci měřitelné struktury, včetně Diracovy míry, můžeme začít definovat různé typy měr. Tyto měry mohou být jednoduše generovány pomocí předchozích definic a Hierarchy-Builderu, čímž se usnadňuje celý proces formalizace a práce s měřitelnými funkcemi.

Je důležité si uvědomit, že formalizace teorie míry není pouze otázkou technického přístupu k definicím, ale také závisí na hlubokém porozumění teoretickým základům. Měřitelnost a additivita jsou klíčovými vlastnostmi, které musí být splněny, aby bylo možné pracovat s funkcemi v rámci teorie míry.

Jak používat notace v teoretických formálních systémech

Notace jako „a || b“ je definována jako „orb a b“, což odpovídá logické operaci OR, tedy sjednocení dvou podmínek. Generalizováno, tato notace může být použita v širším formátu jako „[|| b1 , b2 , ... , bn | c]“, což představuje řetězce nebo kombinace několika podmínek, které jsou kombinovány logickými operátory. Podobně, notace „x ∈ A“ znamená, že prvek x je členem množiny A, což je ekvivalentní zápisu „in_mem x (mem A)“. Naopak, „x ∉ A“ vyjadřuje negaci tohoto vztahu, tedy že x není členem množiny A.

Dále je definována notace „negbT“, která vyjadřuje, že pokud je b rovno false, pak platí „~~ b“, což je ekvivalentní negaci b. Tento zápis je velmi užitečný pro práci s logickými operacemi, kde je třeba manipulovat s negacemi. Stejně tak se definují další operátory pro práci s logickými výrazy jako „negbK“ pro involutivitu (kde se negace aplikovaná na negaci vrací k původnímu výrazu) a „contradiction“, která se používá pro formulování důkazů prostřednictvím kontradikce.

Další důležitou notací je „ifP“, která se používá pro zápis podmínek typu „if b then vT else vF“, což je ekvivalentní zápisu větve podmínky. Tato notace je důležitá při formulování větví logických výroků a ulehčuje práci s podmínkami v důkazech. Podobně se používají i další notace jako „andP“, „orP“ a „implyP“ pro zjednodušení zápisu konjunkcí, disjunkcí a implikací.

Pro detailní práci s množinami a jejich členy je určena notace „A =i B“, která vyjadřuje ekvivalenci dvou množin A a B, což znamená, že mají stejné prvky. Tato notace se využívá k vyjádření rovnocennosti množin v rámci formálního dokazování.

Zajímavým rozšířením těchto notací jsou různé varianty logických predikátů, které definují konkrétní způsoby, jakým jsou logické výroky reflektovány na booleovské hodnoty. Například, predikát „reflect“ slouží k reprezentaci pravdivostních hodnot výroků v rámci formálních systémů, kde lze zobrazit pravdivostní hodnotu výroku jako true nebo false, v závislosti na tom, zda daný výrok platí.

Při práci s operacemi nad přirozenými čísly se často setkáváme s notacemi jako „n .+1“ pro inkrementaci a „n .*2“ pro dvojnásobek čísla. Takové zápisy jsou běžné ve formálních důkazech a matematických indukcích, kde se provádí iterace nebo opakované operace na číselných hodnotách.

Při definování vlastností funkcí a operací je důležité chápat vztah mezi těmito operacemi a jejich strukturálními vlastnostmi. Například, „injective“ znamená, že funkce je injektivní, což znamená, že pro každé dvě různé hodnoty v doméně funkce jsou odpovídající hodnoty v oboru hodnot také různé. Podobně „left_id“ a „right_id“ označují identitu pro operace vpravo a vlevo, což je klíčové pro operace s identitními prvky v algebrických strukturách.

Jaký důkaz je tedy možný?

Pokud bychom hledali nějaký příklad důkazu, mohl by vypadat například takto:

coq
Copy code
Check (nat_ind (fun n => add n 0 = n) (erefl 0) (fun n (ih : add n 0 = n) => eq_trans (f_equal (fun f => f (add n 0)) (erefl S)) (f_equal S ih))).

Tento výraz má typ forall n, add n 0 = n, což zřejmě znamená, že pokud chceme dokázat tuto rovnici, budeme muset napsat takto složitý termín. Nicméně, jak asi tušíte, nebude praktické požadovat, aby uživatelé psali takovéto programy jako důkazy. V Coq proof assistantu (stejně jako v většině podobných nástrojů) se důkazy píší postupně, krok za krokem, za pomoci takzvaných taktik. Taktiky jsou příkazy, které proof assistant provádí v určitém pořadí, aby dokázal dané tvrzení.

Pro tento účel by mohl vypadat příslušný skript takto:

coq
Copy code
Lemma addn0 n : add n 0 = n.  

Proof.  
  by elim: n => //= n ->.  
Qed.

Tento skript je ekvivalentní předchozímu důkazu, ale je podstatně stručnější a přehlednější. Taktika elim: n znamená indukci podle čísla n, zatímco //= znamená, že Coq automaticky použije předchozí dokazování, což zjednodušuje proces.

I když je tento skript krátký, stále si zachovává svou technickou složitost, kterou bude třeba objasnit. Ačkoli je to rozhodně kratší než psaní celého termínu, je nutné si uvědomit, že i tak je tento proces stále technický a vyžaduje určitou znalost syntaktických a logických pravidel Coq.

Pokud bychom chtěli dokázat komutativitu sčítání přirozených čísel, potřebovali bychom další mezilemmu:

coq
Copy code
Lemma addnS m n : add m n.+1 = (add m n).+1.  

Proof.  
  by elim: m => //= m ->.  
Qed.

A nakonec, důkaz komutativnosti sčítání přirozených čísel by vypadal takto:

coq
Copy code
Lemma addC m n : add m n = add n m.  
Proof.  
  by elim: m n => [n|m ih n]; rewrite ?addn0 //= ih -addnS.  
Qed.

Tento příklad ukazuje, že k důkazu komutativnosti přirozených čísel musíme mít už dvě mezilemmata: addn0 a addnS. Při vývoji teorie lemmat je důležité promyslet, která lemma by měla být dokázána jako první, jak by měla být organizována v souborech a jak by měla být pojmenována a dokumentována. Při vývoji formální teorie není často problém s samotným důkazem, protože jeho hlavní myšlenka bývá známá, ale spíše s problémy, které jsou podobné těm, které známe ze softwarového inženýrství.

Ve skutečnosti se při práci s formálními teoriemi často ukazuje, že organizace a správa důkazů (a jejich souvisejících souborů a lemmat) může být náročnější než samotné matematické dokazování. Takové úkoly vyžadují pečlivou strukturalizaci a disciplínu při práci s důkazy.

Pokud jde o samotný systém Coq, existuje několik klíčových komponent, které usnadňují tento proces. Jednou z nich je jazyk Coq – Gallina, který je v podstatě variantou typového λ-kalkulu pro konstruktivní uvažování. Gallina umožňuje definovat formální tvrzení a následně je dokazovat pomocí konkrétních termínů a strategií. Tento jazyk zahrnuje nejen základní operace, jako jsou funkce, predikáty a kvantifikátory, ale i složitější konstrukce, které se používají k modelování teoretických matematických struktur.

Co se týče samotného procesu důkazování, důležité je pochopit, že důkaz není něco statického, co si přečteme jednou a hotovo. V Coq je důkaz spíše dynamickým procesem, který se postupně vykonává a udržuje. Důkaz začíná tvrzením, které není ještě dokázáno, a postupně se pomocí taktik rozvíjí až do úplného důkazu. Coq umožňuje tento proces interaktivně řídit, což znamená, že důkaz se tvoří krok za krokem a uživatel může kdykoli upravit nebo přidat nové kroky.

Když pracujeme s formalizovanými důkazy v Coq, musíme mít na paměti, že výsledný důkaz bude často vyžadovat nejen matematické znalosti, ale také technické dovednosti týkající se manipulace s formálním jazykem, správné volby taktiky a organizace samotného důkazu. Tato kombinace matematických a technických dovedností je základem efektivní práce v prostředí Coq.

Jak efektivně organizovat a strukturovat skripty v Coq

Při práci se skripty je zásadní správné označení ukončených taktiky, což umožňuje snadné sledování postupu a rychlé identifikování případných problémů. Taktika exact je příkladem ukončující taktiky, která potvrzuje, že subcíl byl vyřešen, zatímco taktiky jako rewrite nebo apply nejsou ukončující. V těchto případech je doporučeno použít taktiku by, která ukončí skript co nejdříve a obvykle na místě, kde bude oprava problému jednodušší. Tímto způsobem se předchází situacím, kdy skript běží dál, i když již není možné jej správně dokončit.

Dalším klíčovým aspektem je správné odsazení kódu. Odsazení by mělo být prováděno pomocí dvou mezer a musí jasně indikovat úroveň, na které se daný subcíl nachází. To znamená, že na každém místě v skriptu by měla být zřetelně patrná struktura, která ukazuje, kolik subcílů je stále otevřených. Důležité je také použití bodů (například -, +, *), které pomáhají strukturovat skripty podobně jako v organizaci textu pomocí nástroje org-mode.

Při aplikaci taktiky může být generováno více subcílů, což může vyžadovat reorganizaci. Často je užitečné se zaměřit na snazší subcíl, což je běžné například po použití taktiky rewrite. V některých případech může být potřebné použít zjednodušení (například pomocí taktiky simpl). Existuje konvence, že taktika se ukončuje výrazem „; last first“, což umožňuje předefinování pořadí subcílů a práci na těch nejnáročnějších nebo relevantnějších.

Když se zabýváme logikou důkazů v Coq, je důležité si uvědomit, že matematické důkazy se obvykle provádějí pomocí zpětného uvažování, což znamená, že cíl, který chceme dokázat, je postupně upravován. Taktika apply je základním nástrojem pro zpětné uvažování, ale časté používání zpětného uvažování může vést k neefektivnímu postupu. Naopak, taktika have je ideální pro používání dopředného uvažování, kde se nejprve prokáže nějaká mezi-potřeba a poté se pokračuje v dokazování dalšího cíle. Pomocí taktiky have lze také přímo aplikovat lemmata a definice. Tento přístup je efektivní pro důkazy, které vyžadují komplexní meziprocesy.

Pokud jde o argumenty a proměnné v rámci skriptů, používání sekcí pomocí příkazů Section a End je efektivní metodou pro organizaci teorií, které sdílejí společné parametry. Sekce slouží k vytvoření logických bloků, v nichž jsou parametry, hypotézy a kontext definovány na začátku a platí pouze uvnitř sekce. To pomáhá při správě komplexních důkazů, kde jsou některé argumenty a proměnné společné pro více tvrzení a lemmata.

Naproti tomu, pokud jde o knihovnu MathComp, je důležité věnovat pozornost správné deklaraci a používání notací, které jsou základem pro vyjádření matematiky v Coq. MathComp využívá specifické notace pro různé algebraické struktury, což může výrazně zjednodušit vývoj a práci s důkazy. Například notace pro přičítání u přirozených čísel ((_ + _)%N) a u čísel v algebru ((_ + _)%R) je specifická a mění se v závislosti na používaném kontextu.

Důležité je také pochopit význam některých pojmů, jako jsou generické definice a notace. Například definice pravé identity operace je zobrazena pomocí right_id e op, což značí, že element e je neutrální prvek pro binární operaci op z hlediska pravé strany. Tyto generické definice umožňují jednotné a flexibilní vyjádření základních algebraických vlastností a mohou být aplikovány na různé operace.

V neposlední řadě je třeba zdůraznit význam pojmenování v Coq. Pojmenování lemma a taktik musí být stručné, výstižné a snadno zapamatovatelné. To usnadňuje hledání a použití konkrétních lemmat a funkcí, což je klíčové pro efektivní práci v Coq. Systém MathComp klade důraz na jednotný formát pojmenování, který napomáhá organizaci a přehlednosti celého důkazového procesu.