Jak udowodnić istnienie obiektów i wykorzystywać kwantyfikatory egzystencjalne w matematyce?

Kwantyfikator egzystencjalny, który w systemie Lean zapisuje się jako \ex, jest jednym z najważniejszych narzędzi w matematyce formalnej. Pozwala on na wyrażenie twierdzenia w formie „istnieje element, który spełnia pewną właściwość”. W praktyce matematycznej oznacza to, że istnieje obiekt, który można znaleźć, aby zaspokajał określony warunek.

Weźmy na przykład wyrażenie ∃ x : R, 2 < x ∧ x < 3. Formalnie oznacza to, że istnieje liczba rzeczywista, która jest większa od 2, a jednocześnie mniejsza od 3. Aby udowodnić takie twierdzenie, musimy pokazać, jaki element spełnia te warunki. Liczba 2,5 jest takim przykładem. W systemie Lean możemy zapisać to jako 5 / 2, ponieważ Lean będzie w stanie wywnioskować, że chodzi o liczbę rzeczywistą. Ponadto, dzięki użyciu taktyki norm_num, system automatycznie udowodni, że ta liczba spełnia wymagania twierdzenia.

lean
Copy code
example : ∃ x : R, 2 < x ∧ x < 3 := by use 5 / 2 norm_num

Dzięki tej taktyce wskazujemy, że liczba 5/2 spełnia wymagane warunki. Następnie, za pomocą taktyki norm_num, Lean automatycznie przeprowadzi dowód, że ta liczba rzeczywiście leży pomiędzy 2 a 3.

Warto zauważyć, że w Lean istnieje również możliwość konstrukcji dowodu za pomocą notacji anonimowych konstruktorów. Przykład:

lean
Copy code
example : ∃ x : R, 2 < x ∧ x < 3 := 〈5 / 2, by norm_num〉

Zauważ, że w tym przypadku nie używamy słowa by, a całość dowodu jest zawarta w jednym wyrażeniu. Takie podejście jest stosowane, gdy chcemy wyrazić dowód w bardziej zwięzły sposób. Warto również zauważyć, że notacja z użyciem nawiasów ostrych, 〈 i 〉, pozwala na efektywne zorganizowanie dowodów w formalny sposób.

lean
Copy code
def FnUb (f : R → R) (a : R) : Prop := ∀ x, f x ≤ a
def FnHasUb (f : R → R) := ∃ a, FnUb f a

Takie podejście pozwala na wprowadzenie ogólnych twierdzeń, które nie muszą od razu wskazywać konkretnego obiektu (czyli konkretnego górnego ograniczenia). W tym przypadku, twierdzenie FnHasUb mówi, że istnieje liczba a, która jest górnym ograniczeniem funkcji f.

Z kolei, aby przejść do bardziej złożonych twierdzeń, które wiążą dwa funkcje (np. dodawanie dwóch funkcji o ograniczeniach górnych), Lean pozwala na skuteczne łączenie takich założeń. Na przykład:

lean
Copy code
example (ubf : FnHasUb f) (ubg : FnHasUb g) : FnHasUb fun x 7→ f x + g x := by rcases ubf with 〈a, ubfa〉 rcases ubg with 〈b, ubgb〉 use a + b apply fnUb_add ubfa ubgb

Taktyka rcases pozwala na rozpakowanie informacji zawartych w kwantyfikatorze egzystencjalnym. Dzięki temu możemy dostarczyć nowe zmienne i hipotezy, które będą użyteczne w dalszym dowodzie.

Warto również zaznaczyć, że oprócz rcases, Lean oferuje inne narzędzia do manipulacji z kwantyfikatorami egzystencjalnymi, takie jak rintro, które łączy elementy intro i rcases, oraz obtain, które automatycznie rozpakowuje informacje w sposób sugerujący typy danych. Takie narzędzia znacznie upraszczają proces manipulacji dowodami, gdzie musimy wykorzystywać istniejące założenia i udowodnić nowe tezy na ich podstawie.

Doświadczenie pracy z kwantyfikatorami egzystencjalnymi pokazuje, jak ważne jest precyzyjne rozumowanie i skuteczne stosowanie technik logicznych, które pozwalają na udowodnienie istnienia obiektów spełniających określone warunki. Poprzez zastosowanie takich narzędzi jak use, rcases, rintro, czy obtain, matematycy formalni mogą efektywnie pracować z dowodami w systemach takich jak Lean. Dzięki tym narzędziom, możemy nie tylko udowadniać istnienie różnych obiektów, ale także wykorzystywać je w szerszym kontekście matematycznym, łącząc różne twierdzenia i uzyskując nowe rezultaty w sposób systematyczny i formalny.

Jak w Lean definiować i łączyć struktury algebraiczne, takie jak grupy i monoidy

Pierwszym krokiem jest zrozumienie, jak działa mechanizm rozszerzania klas w Lean. Przykład klasy Semigroup2 pokazuje, jak poprzez rozszerzenie klasy Dia1 można zdefiniować strukturę, która spełnia właściwość łączności dla operacji dwuargumentowych. Takie rozszerzenie pozwala na definiowanie operacji, w których zachowanie łączności będzie kluczowe:

lean
Copy code
class Semigroup2 (α : Type) extends Dia1 α where

  dia_assoc : ∀ a b c : α, a  b  c = a  (b  c)

Ta konstrukcja pozwala Lean na rozpoznanie, że typ α ma już zdefiniowaną operację dia, która jest łączna.

W kolejnych krokach Lean umożliwia tworzenie nowych struktur, które zawierają zarówno elementy semigroupu, jak i dodatkowe właściwości. Klasa DiaOneClass1 jest rozszerzeniem zarówno klasy One1, jak i Dia1, wprowadzając element neutralny, który jest neutralny po obu stronach operacji. Zatem każda instancja tej klasy posiada dwie ważne właściwości: neutralność po lewej stronie i po prawej stronie operacji.

lean
Copy code
class DiaOneClass1 (α : Type) extends One1 α, Dia1 α where
  one_dia : ∀ a : α, 1  a = a
  dia_one : ∀ a : α, a  1 = a

Warto zwrócić uwagę na to, jak Lean radzi sobie z automatycznym tworzeniem instancji klas, co widać po przykładzie, w którym Lean samodzielnie łączy instancje klas Semigroup1 oraz DiaOneClass1 do jednej struktury Monoid1. Działanie to jest możliwe dzięki mechanizmowi rozszerzania, który pozwala na uniknięcie dublowania operacji (takich jak dia), co mogłoby prowadzić do błędów.

lean
Copy code
class Monoid1 (α : Type) extends Semigroup1 α, DiaOneClass1 α

Kiedy próbujemy połączyć te dwie klasy, Lean automatycznie zajmuje się nadmiarowymi operacjami, zapewniając, że wszystkie operacje są spójne i nie prowadzą do konfliktów. Dzięki temu struktura Monoid1 zawiera wszystkie niezbędne właściwości semigroupu, w tym operację dia, i nie generuje dwóch niezależnych instancji tej samej operacji, jak miałoby to miejsce w przypadku ręcznego połączenia klas.

lean
Copy code
class Inv1 (α : Type) where
  inv : α → α
class Group1 (G : Type) extends Monoid1 G, Inv1 G where
  inv_dia : ∀ a : G, a ¹  a = 1

W przypadku grupy w Lean nie jest wymagane, aby odwrotność była definiowana po obu stronach operacji — wystarczy, że będzie spełniać prawo lewej inwersji, a prawo prawej inwersji jest automatycznie wynikiem. Jednak aby wykazać, że lewa inwersja jest również prawą, trzeba posłużyć się odpowiednią lemmą. Dodatkowo, aby uprościć kod i zwiększyć czytelność, można użyć komendy export, która pozwala na przeniesienie definicji zagnieżdżonych w przestrzeni nazw do przestrzeni głównej.

lean
Copy code
export DiaOneClass1 (one_dia dia_one)

export Semigroup1 (dia_assoc)
export Group1 (inv_dia)

Przy takiej organizacji kodu, definicje stają się bardziej zwięzłe, a dostęp do wszystkich wymaganych funkcji jest prostszy. Jest to kluczowe w przypadku dużych projektów matematycznych, gdzie istnieje wiele zależności między różnymi strukturami algebraicznymi.

Na tym etapie Lean zaczyna także wspierać definicje dla bardziej zaawansowanych struktur, jak pierścienie. Definicje tych struktur wymagają jednak zastosowania specjalnych technik, ponieważ pierścień łączy zarówno grupę addytywną, jak i monoidę multiplikatywną, co rodzi trudności związane z używaniem różnych notacji dla operacji dodawania i mnożenia.

lean
Copy code
class AddSemigroup3 (α : Type) extends Add α where
  add_assoc3 : ∀ a b c : α, a + b + c = a + (b + c) @[to_additive AddSemigroup3]
class Semigroup3 (α : Type) extends Mul α where
  mul_assoc3 : ∀ a b c : α, a * b * c = a * (b * c)

Tego rodzaju mechanizm jest bardzo przydatny przy definiowaniu pierścieni i innych bardziej złożonych struktur algebraicznych, pozwalając na pełną kontrolę nad tym, jakie operacje i w jakiej formie są dostępne w danej strukturze.

Warto zauważyć, że Lean, dzięki swojemu systemowi klas i rozszerzeń, pozwala na tworzenie bardzo elastycznych i skalowalnych definicji struktur algebraicznych, które mogą być używane w szerokim zakresie zastosowań matematycznych.