antaris
Registriertes Mitglied
Ja lean macht das aber excellent und die AI ist höchst schreibfreudig aber natürlich nicht wirklich kreativ, wobei ich das nicht nur schwarz oder weiß sehe. Die Details hat alle die AI -> ChatGPT ausgearbeitet. Das ist das eigentliche und vor allem unermüdliche und Weltbild-agnostische Arbeitstier. Das was tatsächlich fehlt ist vor allem Erfahrung und ja, gleichzeitig auch weitere kreative Köpfe.
Das ist ja nun schon ein "open Project" und es darf sich jeder eingeladen fühlen. Die Möglichkeiten des gesamten Ansatz gehen in meinem Kopf schon viel weiter. Aus meiner Sicht ist das alles nur der Anfang aber ich trage wohlmöglich eine rosarote Brille...klare und kompetente Köpfe sind für die vielen Fragestellungen gefragt.
Ich habe mal nachgeforst. Das ist im Prinzip möglich.
Lean hat ein eigenes Makro-System. Man kann notation, macro und scoped notation fast exakt in deinem Sinne definieren.
Folgende Beispiele:
Code:
/-!
# Lean 4 Notation-Beispiel: Lesbare Makro-Ebene für REALOQS
Dieses Modul zeigt, wie man mit `notation` und `scoped notation`
eine lesbare Schicht über den bestehenden Code legen kann,
ohne die Funktionalität zu ändern.
Der Compiler sieht intern denselben Code wie vorher.
Ein menschlicher Leser sieht mathematische Symbole.
-/
import Mathlib
-- ═══════════════════════════════════════════════════
-- Schritt 1: Die bestehende Definition (wie sie jetzt im Repo steht)
-- ═══════════════════════════════════════════════════
variable {Ω : Type} [Fintype Ω] [DecidableEq Ω]
/-- Quadratische Form: ⟨f, Lf⟩ = Σᵢ Σⱼ f(i) · L(i,j) · f(j) -/
def quadForm (L : Matrix Ω Ω ℝ) (f : Ω → ℝ) : ℝ :=
∑ i : Ω, f i * (∑ j : Ω, L i j * f j)
/-- Bilinearform: ⟨f, Lg⟩ = Σᵢ Σⱼ f(i) · L(i,j) · g(j) -/
def bilinForm (L : Matrix Ω Ω ℝ) (f g : Ω → ℝ) : ℝ :=
∑ i : Ω, f i * (∑ j : Ω, L i j * g j)
-- ═══════════════════════════════════════════════════
-- Schritt 2: Notation definieren
-- ═══════════════════════════════════════════════════
-- `scoped notation` bedeutet: die Notation gilt nur,
-- wenn der Namespace geöffnet ist. Das verhindert Konflikte.
namespace REALOQS
-- Bilinearform: ⟪f, L, g⟫
scoped notation "⟪" f ", " L ", " g "⟫" => bilinForm L f g
-- Quadratische Form ist der Spezialfall f = g,
-- braucht keine eigene Notation: man schreibt einfach ⟪f, L, f⟫
end REALOQS
-- ═══════════════════════════════════════════════════
-- Schritt 3: Verwendung — vorher vs. nachher
-- ═══════════════════════════════════════════════════
section Beispiel
variable (L : Matrix Ω Ω ℝ) (f g : Ω → ℝ)
open REALOQS
-- VORHER (schwer lesbar):
-- ∑ i : Ω, f i * (∑ j : Ω, L i j * f j)
-- = ∑ i : Ω, f i * (∑ j : Ω, L_II i j * f j)
-- NACHHER (sofort verständlich):
-- ⟪f, L, f⟫ = ⟪f, L_II, f⟫
-- Beispiel-Lemma mit der neuen Notation:
example (h : ⟪f, L, f⟫ = 0) : bilinForm L f f = 0 := h
-- Lean weiß, dass ⟪f, L, f⟫ und bilinForm L f f dasselbe sind.
-- Die Notation ist rein syntaktischer Zucker.
end Beispiel
-- ═══════════════════════════════════════════════════
-- Schritt 4: Weitere nützliche Notationen für REALOQS
-- ═══════════════════════════════════════════════════
namespace REALOQS
-- Matrixexponential
scoped notation "exp(" z "·" H ")" => NormedSpace.exp (z • H)
-- Spur
scoped notation "Tr(" A ")" => Matrix.trace A
-- Konjugierte Transponierte
scoped notation A "†" => Matrix.conjTranspose A
end REALOQS
-- ═══════════════════════════════════════════════════
-- Zusammenfassung
-- ═══════════════════════════════════════════════════
/-!
## Was passiert hier?
1. `notation` / `scoped notation` definiert ein neues Symbol
2. `=>` sagt Lean, wie es intern übersetzt wird
3. Der Compiler prüft alles wie vorher
4. Nur die Anzeige für Menschen ändert sich
## Aufwand
- Eine Datei `REALOQS/Notation.lean` mit ~20 Zeilen
- Ein `import REALOQS.Notation` in jedem Modul das sie nutzt
- Null Änderung an bestehenden Beweisen (Die Beweise kompilieren identisch, egal ob die alte oder die neue Schreibweise drinsteht.)
- es muss dann nur mit suchen/ersetzen der Name in den lean-Modulen getauscht werden. alles andere bleibt erhalten
## Effekt
- Code wird lesbar wie Mathematik
- Keine Kommentare nötig für das "Was"
- Kommentare nur noch für das "Warum"
-/