Hvordan bevise logiske udsagn i Lean: Conjunction, Bi-implication og Disjunction

I Lean er logiske operationer som konjunktion, bi-implication og disjunktion essentielle for formuleringen og beviset af matematiske udsagn. Disse operationer er ikke kun teoretiske begreber, men bruges aktivt i praksis for at skabe strukturerede, formelle beviser. At forstå, hvordan man arbejder med dem i Lean, er en grundlæggende færdighed for dem, der ønsker at bruge Lean som et værktøj til matematik.

For bi-implication, som er den logiske operation "hvis og kun hvis", bruger man både konstruktion og vekslen mellem de to retninger af udsagnet. I Lean behandles bi-implication ikke blot som to separate implikationer, men også som en relation mellem udsagn, der er både refleksiv, symmetrisk og transitiv. Når man arbejder med bi-implication i Lean, er det ofte praktisk at anvende taktikker som constructor eller rintro for at håndtere de forskellige tilfælde. Et klassisk eksempel på en bi-implication er at vise, at $x \leq y \land \neg y \leq x \leftrightarrow x \leq y \land x \neq y$, hvor man kan anvende rw og linarith for at simplificere udtryk og udlede nødvendige resultater.

Disjunktion, eller "eller"-operationen, er en anden væsentlig logisk konstruktion. I Lean er det kanoniske mål for at bevise en disjunktion $A \lor B$ at bevise enten $A$ eller $B$. Dette gøres gennem taktikker som left og right, som eksplicit vælger, hvilket af de to udsagn man beviser. Det er vigtigt at bemærke, at man ikke kan bruge en anonym konstruktor til at skabe et bevis for en disjunktion, da Lean skal kunne vælge den rigtige disjunkt, og derfor kræves det, at man specifikt angiver, hvilken del af disjunktionen man arbejder med.

I praktisk anvendelse af Lean er det ikke kun de grundlæggende operationer som konjunktion, bi-implication og disjunktion, man arbejder med. Det er også ofte nødvendigt at anvende metoder som redefinitioner og simplifikation af udtryk. For eksempel kan man bruge metoder som rw for at omskrive udtryk til ækvivalente former, eller simp til at forenkle udtryk baseret på givne definitioner. Dette gør det muligt at håndtere selv de mest komplekse matematiske udsagn i en formel og struktureret tilgang.

Der er en vigtig ting, man skal være opmærksom på, når man arbejder med bi-implication og disjunktion i Lean. Selvom det er muligt at bruge konstruktører og taktikker som constructor, rw, og linarith, er det afgørende at forstå, hvordan Lean internt repræsenterer og arbejder med disse logiske operationer. Bi-implicationen $A \leftrightarrow B$ opfører sig som en sammensætning af to implikationer, men det er stadig en relation, der kan bruges til at skabe forenklinger i udtryk og beregninger. På samme måde kan disjunktioner opdeles i separate tilfælde, hvor man beviser $A$ eller $B$ afhængigt af situationen.

Hvordan opbygger man lineære afbildninger og arbejder med vektorrum i Lean?

I matematik kan man opbygge lineære afbildninger ved at bruge allerede definerede objekter i Lean-biblioteket (Mathlib) sammen med forskellige kombinatorer. For eksempel er LinearMap.lsmul en allerede velkendt lineær afbildning, der viser, hvordan man arbejder med skalarer i et givet vektorrum. En af de mest interessante egenskaber ved lineære afbildninger som LinearMap.lsmul K V er, at de er K-lineære afbildninger fra K (som ses som et vektorrum over sig selv) til mængden af K-lineære afbildninger fra V til V. Denne type afbildning er således en nøglekomponent i forståelsen af lineære transformationer i vektorrum.

Det er vigtigt at bemærke, at argumenterne K og V i LinearMap.lsmul er nødvendige for at kunne bruge Lean effektivt, da systemet ellers ikke ville være i stand til at udlede disse typer automatisk. Desuden kan begreber som LinearEquiv bruges til at definere lineære isomorfier, som er bijektive lineære afbildninger mellem to vektorrum. For eksempel kan man bruge LinearEquiv.ofBijective til at oprette en isomorfi fra en bijektiv afbildning, hvilket åbner op for mere komplekse manipulationer af vektorrum og deres strukturer.

I forbindelse med produkterne og summen af vektorrum er der adskillige metoder til at bygge nye vektorrum ud af eksisterende. For to vektorrum er der ikke nogen forskel mellem sum og produkt, og man kan derfor bruge produkttypen for at definere et kombineret vektorrum. I Lean kan man få strukturerne af afbildningerne (inklusions- og projektionafbildningerne) som lineære afbildninger. Eksempler på lineære afbildninger som LinearMap.fst og LinearMap.snd viser, hvordan man projicerer elementer fra et produkt af to vektorrum ind i de enkelte komponenter. Universal egenskab for produkter og summen af vektorrum gør det muligt at bygge afbildninger ind i et produkt eller ud af en sum ved at bruge kombinerede map-funktioner.

Når vi taler om familie af vektorrum, kan man bruge direkte summer og direkte produkter til at samle en familie af vektorrum. Universal-egenskaben for direkte summer gør det muligt at sammensætte afbildninger fra de enkelte summands rum til en afbildning fra den direkte sum af disse rum til et andet vektorrum. Ligeledes kan man bruge den universelle egenskab for direkte produkter til at samle afbildninger fra en familie af vektorrum til en afbildning i et direkte produkt af disse rum.

Afslutningsvis er det væsentligt at forstå, hvordan man arbejder med subrum og kvotientrum i den lineære algebra, som Lean understøtter. Et subrum er et lineært rum, som opfylder de nødvendige lukningsegenskaber for addition og skalarmultiplikation. På samme måde som lineære afbildninger er subrum i Lean bundet som en struktur med et tilknyttet mængde, og to subrum er lige, hvis de indeholder de samme elementer. Denne tilgang gør det muligt at arbejde med subrum på en systematisk måde, og giver værktøjer til at manipulere med subrum og deres relationer til andre lineære objekter.

Det er også vigtigt at forstå, at manipulationsværktøjer som ext taktik i Lean gør det muligt at bevise ligheder mellem subrum på samme måde som man beviser, at to mængder er lige. Når man konstruerer subrum, skal man være opmærksom på, at det kræver præcise angivelser af de lukkende egenskaber, og at det er nødvendigt at bruge strukturer som Submodule til at definere de lineære subrum og deres operationer.