Hvordan arbejder man med eksistenskvantificatorer i Lean?

I matematikken anvender vi ofte kvantifikatorer for at formulere udsagn om eksistens og universelle påstande. Den eksistenskvantifikator, der kan indtastes som \ex i VS Code, bruges til at repræsentere udtrykket "der findes" eller "der eksisterer." For eksempel betyder det formelle udtryk ∃ x : R, 2 < x ∧ x < 3 i Lean, at der findes et reelt tal mellem 2 og 3. I Lean kan vi udnytte kvantifikatoren til at konstruere beviser, som viser eksistensen af objekter med en given egenskab. Denne metode gør det muligt at argumentere præcist og systematisk for, hvorfor et givet udsagn holder.

En typisk måde at bevise et sådant udsagn på er ved at udstille et konkret objekt og vise, at det opfylder de givne betingelser. For eksempel kan tallet 2,5, som vi kan indtaste som 5 / 2 eller (5 : R) / 2 i Lean, nemt vise sig at opfylde betingelsen, og ved hjælp af taktikken norm_num kan vi automatisk bevise, at det møder beskrivelsen. I Lean kan vi opbygge sådanne beviser på forskellige måder afhængigt af den ønskede præsentation.

Når vi står overfor en eksistenskvantifikator, anvender vi ofte taktikken use for at angive den objekt, der opfylder betingelsen. Et eksempel på dette kan ses her:

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

I dette tilfælde anvender vi use til at præsentere objektet 5 / 2 som løsningen på vores mål. Vi beviser derefter, at dette tal opfylder betingelsen ved hjælp af norm_num, som automatisk forenkler og bekræfter, at 2 < 5 / 2 < 3. Hvis vi har flere beviser eller antagelser, kan vi også bruge flere taktikker og definitioner for at udvide vores argumentation.

En anden måde at konstruere et bevis for en eksistenskvantifikator på er ved at bruge Lean’s anonyme konstruktørnotation, som ikke kræver en separat taktik for at udtrække de nødvendige beviser. For eksempel kan vi oprette et bevis for udsagnet om eksistens som følger:

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

Denne notation samler både objektet og beviset for det pågældende udsagn på en mere kompakt og eksplicit måde. I Lean’s syntaks bliver vinkelformede parenteser, som kan indtastes som < og >, brugt til at indikere, at vi eksplicit konstruerer et bevis baseret på de givne data.

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

Her introducerer vi definitioner for øvre og nedre grænser på en funktion, og vi udvider de tidligere beviser for at vise, hvordan en funktion, der har en øvre grænse, også vil have en øvre grænse, når der tilføjes en anden funktion. Ved at anvende teknikker som rcases, som bruges til at pakke ud information fra en eksistenskvantifikator, kan vi udtrække de relevante data fra vores antagelser og bruge dem til at bevise nye resultater.

Eksempelvis kan vi bruge rcases til at udtrække øvre grænseantagelser og derefter bruge dem til at bevise, at summen af to funktioner, der har øvre grænser, også har en øvre grænse:

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

Taktikken rcases bruges til at pakke ud antagelserne i ubf og ubg og tilføje de relevante data til konteksten. På denne måde får vi adgang til de oplysninger, der er nødvendige for at udlede den ønskede konklusion. Dette er en af de mest nyttige teknikker, når man arbejder med eksistensbeviser i Lean.

Det er også muligt at anvende andre metoder som obtain og match til at pakke ud data og skabe beviser. Selvom disse metoder tilbyder lidt forskellig syntaks, kan de alle bruges til at udpakke data og anvende disse til at skabe nye beviser i et matematisk argument. I sidste ende er den grundlæggende ide bag alle disse taktikker den samme: vi udpakker data og anvender dem på en systematisk og præcis måde.

Hvordan definere og evaluere propositonelle formler i Lean

Induktivt definerede typer udgør en central del af formelle beviser i matematik, og en af de mest fundamentale typer er propositonelle formler. I Lean, et formelt bevisværktøj, kan vi definere og manipulere disse formler på en præcis og struktureret måde, der gør det muligt at arbejde med matematik på et logisk niveau.

Propositonelle formler i Lean kan enten være en variabel (repræsenteret som var n), den konstante falskhed (repræsenteret som fls), eller en sammensat formel bestående af konjunktioner, disjunktioner eller implikationer. For eksempel kan en formel som A ∧ B defineres som conj A B, mens A → B defineres som impl A B. Disse definitioner svarer til de klassiske matematiske symboler, hvor ∧ står for konjunktion (og), ∨ for disjunktion (eller), og → for implikation.

Når man arbejder med propositonelle formler i Lean, er en vigtig funktion evnen til at evaluere formlerne i forhold til en tildeling af sandhedsværdier. Dette sker gennem en rekursiv funktion, som kalder på de forskellige komponenter i formlen. Den evaluerer variablerne ved at tildele dem deres respektive sandhedsværdier og bearbejder sammensatte formler ved hjælp af de grundlæggende logiske operationer. Dette er af stor betydning, da det gør det muligt at beregne sandhedsværdien af enhver propositonel formel, givet en tildeling af sandhedsværdier til dens variabler.

Der er også en vigtig funktion, som beregner mængden af variabler, der optræder i en given formel. Ved hjælp af denne funktion kan man f.eks. vise, at to tildelinger, der kun adskiller sig ved værdierne for ikke-tilstedeværende variabler i en formel, vil føre til den samme evaluering. Dette understøtter ideen om, at en formel kun er afhængig af de variabler, der faktisk forekommer i den.

Den rekursive natur af propositonelle formler gør det muligt at definere og evaluere formler på en struktureret og effektiv måde i Lean. Evalueringen af formler afhænger ikke kun af de variabler, der er tilstede, men også af hvordan sammensatte formler interagerer med hinanden. Substitution og evaluering er nøglefunktioner, der muliggør præcise matematiske manipulationer og beviser i systemet.

I praksis kan denne type formeldefinering også anvendes i mere komplekse systemer, hvor vi har at gøre med algebraiske strukturer som grupper eller ringer. Forståelsen af logiske formler og deres evaluering i sådanne systemer er afgørende for at kunne bygge matematiske beviser på en systematisk og korrekt måde.

Hvordan arbejder man med algebraiske strukturer i Lean?

• $R$ med addition er en abelsk gruppe, hvor 0 er den additive identitet og negation fungerer som den inverse operation.

• Multiplikation er associativ, har identitetselementet 1, og distribuerer over addition.

I Lean repræsenteres denne samling af objekter som en type, $R$, og aksionerne, der definerer en ring, er præcist beskrevet som teoremer i Lean's matematikbibliotek, Mathlib. Teoremerne omfatter for eksempel:

• $a + b = b + a$ (commutativitet for addition),

• $(a + b) + c = a + (b + c)$ (associativitet for addition),

• $a \cdot (b + c) = a \cdot b + a \cdot c$ (distributiv lov for multiplikation over addition).

Et af de mest kraftfulde værktøjer i Lean til at arbejde med algebraiske identiteter er brugen af rewriting-teknikker. Her kan vi for eksempel bruge taktikken $rw$ til at omdanne en given udtryk ved at erstatte et element med et andet. Dette kan bruges til at forenkle udtryk og bevise identiteter.

For eksempel, hvis vi ønsker at bevise identiteten

kan vi bruge en række teknikker i Lean til at opnå dette trin for trin. Først kan vi bruge den distributive lov $\text{mul\_add}$ og $\text{add\_mul}$, som er en standardteorem i Lean, til at udvide produktet:

Derefter kan vi anvende $\text{add\_assoc}$ og omarrangere termerne for at få en lettere form:

I Lean kan vi skrive dette bevis som en sekvens af taktikker, hvilket giver os mulighed for at arbejde på en struktureret måde. Her er et eksempel:

lean
Copy code
example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := calc

  (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by rw [mul_add, add_mul, add_mul]
  _ = a * a + (b * a + a * b) + b * b := by rw [← add_assoc, add_assoc (a * a)]
  _ = a * a + 2 * (a * b) + b * b := by rw [mul_comm b a, ← two_mul]

Bemærk, at når vi bruger $calc$-syntaksen, får vi en meget mere læsbar og struktureret måde at arbejde med beviser på, som er lettere at forstå og følge end en simpel sekvens af $rw$-kommandoer. Hver linje i $calc$-udtrykket repræsenterer en ændring i udtrykket, og vi bruger $by$ for at angive den teoretiske begrundelse for hver ændring. Lean tillader også, at vi kan udfylde beviset med $sorry$-kommandoen, indtil vi har en korrekt bevisstruktur. På den måde kan vi koncentrere os om at definere rammerne for vores bevis og derefter udfylde detaljerne.

ved hjælp af $ring$-taktikken:

lean
Copy code
example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring

Denne taktik anvender de grundlæggende ringaksiomer til at omdanne og forenkle udtrykket uden at vi selv skal skrive ud alle de nødvendige manipulationer. Det er en fantastisk metode til at bevise resultater hurtigt i simple algebraiske strukturer.

Der findes også mere avancerede metoder til at håndtere tilfælde, hvor vi kun ønsker at erstatte en specifik forekomst af et udtryk i et bevis. For eksempel, ved at bruge $nth\_rw$, kan vi erstatte den anden forekomst af $a + b$ med et andet udtryk:

lean
Copy code
example (a b c : N) (h : a + b = c) : (a + b) * (a + b) = a * c + b * c := by nth_rw 2 [h] rw [add_mul]

Disse teknikker gør det muligt at arbejde effektivt med algebraiske strukturer i Lean, og de giver os en robust platform til at bevise algebraiske identiteter både på konkrete og abstrakte niveauer.

I arbejdet med Lean og algebraiske strukturer er det vigtigt at forstå, at ikke alle egenskaber, som holder i konkrete strukturer som de reelle tal, nødvendigvis gælder i en vilkårlig ring. For eksempel er multiplikation i de reelle tal kommutativ, men dette er ikke nødvendigvis tilfældet i alle ringe. Derfor skal vi være opmærksomme på, hvilke aksioner og egenskaber der gælder for de strukturer, vi arbejder med.