Hoe gebruik je verzamelingen en functies in Lean voor bewijsvoering en wiskundige identiteiten?

In de Lean wiskundige omgeving worden verzamelingen en functies op een gestructureerde manier gedefinieerd, waarbij veel van de gebruikelijke wiskundige concepten worden vertaald naar formele beweringen die geautomatiseerd kunnen worden gecontroleerd. De interactie tussen verzamelingen, hun bewerkingen, en de eigenschappen van functies speelt hierbij een belangrijke rol. Het doel van dit hoofdstuk is om enkele van deze concepten in detail te verkennen, met name binnen de context van het werken met geïnitialiseerde verzamelingen, hun operaties en de verschillende eigenschappen van functies zoals afbeelding en prebeeld.

De operaties zoals unie, doorsnede en het nemen van de prebeelden en afbeeldingen van verzamelingen vormen een fundamenteel onderdeel van de interactie tussen wiskundige objecten in Lean. Het bewijs van identiteiten die gebruik maken van deze operaties kan eenvoudig worden uitgevoerd door het toepassen van Lean's tactieken, zoals ext, simp, en rintro, wat helpt bij het decomposeren van complexe beweringen en het genereren van de vereiste stappen in een bewijs.

Een voorbeeld hiervan is het bewijzen van de identiteit van verzamelingen in Lean, zoals het bewijs dat de doorsnede van de unie van twee verzamelingen gelijk is aan de unie van de doorsneden van die verzamelingen. Dit kan worden gedaan door de juiste tactieken toe te passen en de ext en simp commando’s te gebruiken, die respectievelijk een opstelling van de bewering en de simplificatie van de voorwaarden voor lidmaatschap mogelijk maken.

Lean maakt het ook mogelijk om de concepten van "prebeeld" en "afbeelding" van functies uit te werken. Het prebeeld van een functie f over een verzameling p wordt gedefinieerd als de verzameling van alle elementen x waarvoor geldt dat f x in p ligt. Dit wordt in Lean geschreven als f ¹' p. Evenzo wordt de afbeelding van een verzameling s door de functie f gedefinieerd als de verzameling van alle elementen die het beeld van een element uit s zijn, genoteerd als f '' s.

Bijvoorbeeld, voor een injectieve functie f geldt dat de afbeelding van de doorsnede van twee verzamelingen s en t gelijk is aan de doorsnede van de afbeeldingen van s en t, oftewel f '' (s ∩ t) = f '' s ∩ f '' t. Dit kan worden bewezen door gebruik te maken van de definities van de afbeelding en het prebeeld, evenals door de geschikte Lean tactieken toe te passen om de gewenste bewering af te leiden.

Wanneer we werken met de verzameling van priemgetallen en de operaties van unie en doorsnede, komen de specifieke eigenschappen van deze operaties goed naar voren. Bijvoorbeeld, de identiteit waarbij de doorsnede van een verzameling priemgetallen gelijk is aan de verzameling die alleen het getal 1 bevat, kan eenvoudig worden bewezen door gebruik te maken van het principe van contrapositie en de eigenschappen van priemgetallen. In Lean kan dit worden uitgevoerd met behulp van de contrapose! en simp tactieken.

Verder is het belangrijk om te begrijpen dat sommige van de wiskundige operaties die in Lean worden gedefinieerd, zoals de verzameling van prebeelden en afbeeldingen van functies, vaak kunnen worden gezien als toepassingen van de zogenaamde Galois-verbindingen tussen verzamelingen. Dit concept houdt in dat er een relatie bestaat tussen de afbeelding van een functie en het prebeeld ervan, die in de meeste gevallen kan worden uitgedrukt als een logische implicatie tussen de twee verzamelingen. Het gebruik van de mem_image_of_mem en de image_subset_iff theorema’s maakt het makkelijker om dergelijke relaties te begrijpen en toe te passen in bewijsvoering.

Een ander belangrijk aspect van het werken met functies in Lean is de mogelijkheid om de inverse van een functie te definiëren, zelfs wanneer de functie mogelijk niet surjectief is. Dit vereist een extra niveau van abstractie, aangezien we mogelijk moeten werken met een standaardwaarde voor de elementen die geen prebeeld hebben in de functie. Dit kan worden bereikt door de notatie [Inhabited α] in te voeren, waarmee we aannemen dat het type α een "standaard" element heeft.

Naast deze kernconcepten is het ook belangrijk om bekend te raken met de techniek van het werken met verzamelingen van verzamelingen, ook wel aangeduid als Set (Set α). Deze verzamelingen vereisen een ander soort bewerking en vormen een nuttige uitbreiding van de traditionele concepten van unie en doorsnede, aangezien de unie van een verzameling van verzamelingen bijvoorbeeld wordt gedefinieerd als de verzameling van alle elementen die behoren tot minstens één van de verzamelingen in die verzameling.

Het gebruik van de juiste tactieken en kennis van de definities in de Lean-bibliotheek stelt ons in staat om snel en effectief wiskundige identiteiten en eigenschappen te bewijzen. Door Lean’s vermogen om formules en bewijzen te structureren, kunnen we complexe wiskundige concepten op een formele en geautomatiseerde manier verkennen, wat het een krachtig hulpmiddel maakt voor iedereen die zich bezighoudt met formele wiskunde en bewijsvoering.

Hoe Algebraïsche Structuren en Groepen worden Geformaliseerd in Lean

In de wereld van formele wiskunde en programmeertalen zoals Lean, is het van groot belang dat we algebraïsche structuren op een systematische en gestandaardiseerde manier kunnen definiëren en gebruiken. Een van de fundamentele concepten die hierin centraal staat, is het begrip groep, dat wordt geformaliseerd via de structuur Group1 in Lean. In dit hoofdstuk onderzoeken we hoe een groep in Lean wordt geconstrueerd, welke notaties hierbij worden gebruikt, en hoe we algebraïsche eigenschappen kunnen vastleggen in deze formele taal.

Bijvoorbeeld, in Lean wordt een groep gedefinieerd door vier componenten: een binaire operatie (meestal vermenigvuldigen of optellen), een identiteitselement, een inverse functie en de associativiteit van de operatie. Voor een willekeurige groep $G$ zou dit kunnen betekenen dat we werken met elementen die we vermenigvuldigen, waarbij het product van twee elementen voldoet aan de groepsaxioma's.

De bijectie wordt in Lean voorgesteld door vier componenten: een functie $f.toFun$ van $\alpha$ naar $\beta$, de inverse functie $f.invFun$ van $\beta$ naar $\alpha$, en twee eigenschappen die garanderen dat deze functies inderdaad elkaars inverses zijn. Het gebruik van notaties zoals $f.toFun$ en $f.invFun$ maakt het expliciet dat we hier werken met functies en niet met algemene relaties.

De definitie van de groep van permutaties in Lean is als volgt:

lean
Copy code
def permGroup {α : Type*} : Group1 (Equiv.Perm α) where
  mul f g := Equiv.trans g f
  one := Equiv.refl α
  inv := Equiv.symm
  mul_assoc f g h := (Equiv.trans_assoc _ _ _).symm
  one_mul := Equiv.trans_refl
  mul_one := Equiv.refl_trans
  inv_mul_cancel := Equiv.self_trans_symm

De kracht van Lean wordt verder duidelijk wanneer we de structuur van groepen uitbreiden naar andere algebraïsche structuren. Bijvoorbeeld, in plaats van multiplicatieve groepen, kunnen we additieve groepen definiëren die gebruik maken van een andere notatiestructuur. De componenten van een additieve groep worden aangeduid met add, zero en neg. Dit laat zien hoe flexibel Lean is in het omgaan met verschillende algebraïsche structuren, terwijl de onderliggende principes consistent blijven.

Een belangrijk aspect van werken met Lean is de manier waarop notatie en structuur samenhangen. Terwijl we in traditionele wiskunde notaties vaak onafhankelijk beschouwen van de onderliggende structuur, wordt in Lean de notatie strikt gekoppeld aan de gedefinieerde structuur. Dit betekent dat de gebruikelijke symbolen voor groepen (zoals $+$ voor optellen) automatisch worden geïnterpreteerd op basis van de context, afhankelijk van de structuur die we hebben gedefinieerd.

Wanneer we werken met permutaties in Lean, zoals gedefinieerd in Equiv.Perm α, kunnen we gebruik maken van de notatie voor vermenigvuldiging, identiteit en inverse, zonder expliciet te hoeven verwijzen naar de onderliggende functies. Dit maakt de interactie met algebraïsche structuren uiterst intuïtief en krachtig. Bijvoorbeeld, bij het werken met de permutatiegroep, kunnen we de associativiteit en de inverses eenvoudig bewijzen door gebruik te maken van standaardtheorema's zoals mul_assoc en inv_mul_cancel.

Het is essentieel voor de lezer om te begrijpen dat de kracht van Lean niet alleen ligt in de formele definitie van algebraïsche structuren, maar ook in de manier waarop we deze structuren combineren met automatische afleidingen en impliciete argumenten. Dit vermindert de complexiteit van de formele wiskunde aanzienlijk, terwijl het ons tegelijkertijd in staat stelt om zeer rigoureuze en gedetailleerde bewijsvoering te voeren.

Hoe algebraïsche structuren werken met betrekking tot deelbaarheid en ordening

Bij het bestuderen van deelbaarheid en de concepten van de grootste gemeenschappelijke deler (gcd) en het kleinste gemeenschappelijke veelvoud (lcm) wordt het duidelijk dat deze operaties op een bepaalde manier analogieën vertonen met de minimum- en maximumfuncties. Een belangrijk aspect van deelbaarheid is bijvoorbeeld dat elk getal 0 deelt, wat betekent dat 0 het grootste element is in termen van deelbaarheid. Dit idee kan verder worden verkend door de bijbehorende theorema's en eigenschappen van de gcd en lcm te bestuderen.

In Lean, een wiskundige proof assistant, kunnen we een aantal definities en theorema's formuleren met betrekking tot gcd en lcm. Bijvoorbeeld, we kunnen de eigenschappen van gcd en lcm in Lean onderzoeken met de volgende uitspraken:

• Nat.gcd_zero_right n : Nat.gcd n 0 = n

• Nat.gcd_zero_left n : Nat.gcd 0 n = n

• Nat.lcm_zero_right n : Nat.lcm n 0 = 0

• Nat.lcm_zero_left n : Nat.lcm 0 n = 0

Deze stellingen tonen aan dat het gcd van een getal en 0 altijd gelijk is aan het getal zelf, terwijl het lcm van een getal en 0 altijd 0 is. Het begrijpen van deze eigenschappen is essentieel voor het verder onderzoeken van de relaties tussen getallen binnen verschillende algebraïsche structuren.

In Lean kunnen we werken met partiële ordeningen door bijvoorbeeld de volgende variabelen te definiëren:

• variable {α : Type*} [PartialOrder α]

• variable (x y z : α)

Hier kunnen we gebruik maken van axioma's zoals le_refl, le_trans en le_antisymm, die de basiseigenschappen van een partiële orde definiëren. Het belangrijkste is te begrijpen dat deze ordening de basis legt voor complexere structuren zoals een lattice.

• ⊓ is de grootste lagere grens, ook wel infimum of meet genoemd.

• ⊔ is de kleinste bovenste grens, ook wel supremum of join genoemd.

Enkele voorbeelden van lattices zijn:

• min en max op een totale orde zoals de gehele getallen of de reële getallen met ≤

• ∩ en ∪ op de verzameling van deelverzamelingen van een domein met de ordenering ⊆

• ∧ en ∨ op booleaanse waarheidswaarden, waarbij de ordenering wordt gedefinieerd door "x ≤ y als x onwaar is of y waar is"

• gcd en lcm op de natuurlijke getallen (of positieve natuurlijke getallen), met de deelbaarheidsordening (|)

Het is belangrijk om in gedachten te houden dat de commutativiteit en associativiteit van de infimum- en supremumoperaties kunnen worden bewezen met behulp van hun karakteristieke axioma's, samen met le_refl en le_trans. Dit betekent dat, net als bij de min/max of gcd/lcm, deze operaties enkele fundamentele eigenschappen vertonen die wiskundig te verantwoorden zijn.

Naast het begrijpen van de basisoperaties zoals infimum en supremum, komt er bij het werken met lattices ook het concept van distributiviteit kijken. Een distributieve lattice voldoet aan specifieke identiteiten zoals:

• x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)

• x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)

Het is een interessante oefening om te laten zien dat niet elke lattice distributief is. Er zijn voorbeelden van niet-distributieve lattices met eindig veel elementen, die illustreren dat distributiviteit niet vanzelfsprekend is.

Bij het verkennen van deze algebraïsche structuren en hun interacties is het van cruciaal belang om verder te gaan dan de basisprincipes en in staat te zijn om de implicaties van axioma’s en de onderlinge verbanden tussen verschillende operaties en structuren te begrijpen.