feat: Semi-formal results (#440)

* feat: Add tags

* feat: Add tags to YML

* refactor: Lint

* feat: Sort TODOs

* feat: Add semi-formal results

* feat: fix name

* refactor: Lint

PhysLean.lean

@@ -22,6 +22,7 @@ import PhysLean.Meta.AllFilePaths
 import PhysLean.Meta.Basic
 import PhysLean.Meta.Informal.Basic
 import PhysLean.Meta.Informal.Post
+import PhysLean.Meta.Informal.SemiFormal
 import PhysLean.Meta.Notes.Basic
 import PhysLean.Meta.Notes.HTMLNote
 import PhysLean.Meta.Notes.NoteFile

PhysLean/Meta/Informal/SemiFormal.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Lean.Elab.Exception
+import Lean.Elab.Command
+/-!
+
+# Semiformal results
+
+Semiformal results sit inbetween informal and formal results. There type or propsoition is
+defined, by the proof or definition is not.
+
+## Note
+
+The code here is modified from the Util.ProofWanted module of the Battires library.
+Released under the Apache 2.0 license, copyright 2023 Lean FRO, authored by
+David Thrane Christiansen.
+
+-/
+
+
+open Lean Parser Elab Command
+
+/-- The information from a `TODO ...` command. -/
+structure WantedInfo where
+  /-- The content of the note. -/
+  content : String
+  /-- Name of result. -/
+  name : Name
+  /-- The file name where the note came from. -/
+  fileName : Name
+  /-- The line from where the note came from. -/
+  line : Nat
+  /-- The tag of the TODO item -/
+  tag : String
+
+/-- The enviroment extension for semiformal results. -/
+initialize wantedExtension : SimplePersistentEnvExtension WantedInfo (Array WantedInfo) ←
+  registerSimplePersistentEnvExtension {
+    name := `wantedExtension
+    addEntryFn := fun arr todoInfor => arr.push todoInfor
+    addImportedFn := fun es => es.foldl (· ++ ·) #[]
+  }
+
+/-- The parser for semiformal results. -/
+@[command_parser]
+def «semiformal_result» := leading_parser
+    docComment >>  "semiformal_result" >> strLit >> declId >> ppIndent declSig
+
+/-- The elaborator for semiformal results. -/
+@[command_elab «semiformal_result»]
+def elabLemmaWanted : CommandElab := fun stx =>
+  match stx with
+  | `($doc:docComment semiformal_result $s $name $args* : $res) =>
+    let tag : String := s.getString
+    let pos := stx.getPos?
+    let docString : String := doc.getDocString
+    match pos with
+    | some pos => do
+      let env ← getEnv
+      let fileMap ← getFileMap
+      let filePos := fileMap.toPosition pos
+      let line := filePos.line
+      let modName := env.mainModule
+      let wantedInfo : WantedInfo := {
+        content := docString,
+        name := (Lean.Elab.expandDeclIdCore name).1,
+        fileName := modName,
+        line := line,
+        tag := tag }
+      let _ ← modifyEnv fun env => wantedExtension.addEntry env wantedInfo
+      let _ ← withoutModifyingEnv do
+      elabCommand <| ← `(
+        section
+        set_option linter.unusedVariables false
+        axiom helper {α : Sort _} : α
+        $doc:docComment noncomputable def $name $args* : $res := helper
+        end)
+      pure ()
+    | none => throwError "Invalid syntax for `lemma_wanted` command"
+  | _ => throwError "Invalid syntax for `lemma_wanted` command"

PhysLean/Particles/BeyondTheStandardModel/GeorgiGlashow/Basic.lean

@@ -37,14 +37,14 @@ informal_definition inclSM where
 See page 34 of https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_lemma inclSM_ker where
-  deps := [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup]
+  deps := [``inclSM]
   tag := "6V2W2"
 
 /-- The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by
 quotienting by the kernel `inclSM_ker`.
 -/
 informal_definition embedSMℤ₆ where
-  deps := [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupI, ``inclSM_ker]
+  deps := [``inclSM,  ``GaugeGroupI, ``inclSM_ker]
   tag := "6V2XA"
 
 end GeorgiGlashow

PhysLean/Particles/BeyondTheStandardModel/PatiSalam/Basic.lean

@@ -79,13 +79,13 @@ informal_definition GaugeGroupℤ₂ where
 the subgroup `gaugeGroupℤ₂SubGroup`.
 -/
 informal_lemma sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup where
-  deps := [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup]
+  deps := [``inclSM, ``gaugeGroupℤ₂SubGroup]
   tag := "6V2SV"
 
 /-- The group homomorphism from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupℤ₂` induced by `embedSM`.
 -/
 informal_definition embedSMℤ₆Toℤ₂ where
-  deps := [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupℤ₂,
+  deps := [``inclSM,  ``GaugeGroupℤ₂,
     ``sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup]
   tag := "6V2S4"
 

PhysLean/Particles/StandardModel/Basic.lean

@@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Geometry.Manifold.Instances.Real
 import PhysLean.Relativity.SpaceTime.Basic
 import PhysLean.Meta.Informal.Basic
+import PhysLean.Meta.Informal.SemiFormal
 /-!
 # The Standard Model
 
@@ -32,18 +33,14 @@ where `α` is a sixth complex root of unity.
 
 See https://math.ucr.edu/home/baez/guts.pdf
 -/
-informal_definition gaugeGroupℤ₆SubGroup where
-  deps := [``GaugeGroupI]
-  tag := "6V2FZ"
+semiformal_result "6V2FZ" gaugeGroupℤ₆SubGroup [inst : Group GaugeGroupI] : Subgroup GaugeGroupI
 
 /-- The smallest possible gauge group of the Standard Model, i.e., the quotient of `GaugeGroupI` by
 the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`.
 
 See https://math.ucr.edu/home/baez/guts.pdf
 -/
-informal_definition GaugeGroupℤ₆ where
-  deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
-  tag := "6V2GA"
+semiformal_result "6V2GA" GaugeGroupℤ₆ : Type
 
 /-- The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on all particles in the
 standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` derived from the ℤ₂ subgroup of
@@ -52,7 +49,7 @@ standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` derived from the ℤ
 See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition gaugeGroupℤ₂SubGroup where
-  deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
+  deps := [``GaugeGroupI]
   tag := "6V2GH"
 
 /-- The gauge group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by
@@ -71,7 +68,7 @@ standard model, i.e., the ℤ₃-subgroup of `GaugeGroupI` derived from the ℤ
 See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition gaugeGroupℤ₃SubGroup where
-  deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup]
+  deps := [``GaugeGroupI]
   tag := "6V2GV"
 
 /-- The gauge group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by
@@ -105,7 +102,7 @@ quotient.
 See https://math.ucr.edu/home/baez/guts.pdf
 -/
 informal_definition GaugeGroup where
-  deps := [``GaugeGroupI, ``gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup, ``gaugeGroupℤ₃SubGroup,
+  deps := [``GaugeGroupI,  ``gaugeGroupℤ₂SubGroup, ``gaugeGroupℤ₃SubGroup,
     ``GaugeGroupQuot]
   tag := "6V2HF"
 

scripts/MetaPrograms/TODO_to_yml.lean

@@ -7,6 +7,7 @@ import PhysLean.Meta.Basic
 import PhysLean.Meta.TODO.Basic
 import Mathlib.Lean.CoreM
 import PhysLean.Meta.Informal.Post
+import PhysLean.Meta.Informal.SemiFormal
 /-!
 
 # Turning TODOs into YAML
@@ -130,12 +131,14 @@ structure FullTODOInfo where
   line : Nat
   isInformalDef : Bool
   isInformalLemma : Bool
+  isSemiFormalResult : Bool
   category : PhysLeanCategory
   tag : String
 
 def FullTODOInfo.ofTODO (t : todoInfo) : FullTODOInfo :=
   {content := t.content, fileName := t.fileName, line := t.line, name := t.fileName,
-   isInformalDef := false, isInformalLemma := false, category := PhysLeanCategory.ofFileName t.fileName,
+   isInformalDef := false, isInformalLemma := false,
+   isSemiFormalResult := false, category := PhysLeanCategory.ofFileName t.fileName,
    tag := t.tag}
 
 unsafe def getTodoInfo : MetaM (Array FullTODOInfo) := do
@@ -154,13 +157,25 @@ unsafe def informalTODO (x : ConstantInfo) : CoreM FullTODOInfo := do
   let isInformalLemma := Informal.isInformalLemma x
   let category := PhysLeanCategory.ofFileName file
   return {content := docString, fileName := file, line := lineNo, name := name,
-          isInformalDef := isInformalDef, isInformalLemma := isInformalLemma, category := category,
+          isInformalDef := isInformalDef, isInformalLemma := isInformalLemma,
+          isSemiFormalResult := false, category := category,
           tag := tag}
 
 unsafe def allInformalTODO : CoreM (Array FullTODOInfo) := do
   let x ← AllInformal
   x.mapM informalTODO
 
+def FullTODOInfo.ofSemiFormal (t : WantedInfo) : FullTODOInfo :=
+  {content := t.content, fileName := t.fileName, line := t.line, name := t.name,
+   isInformalDef := false, isInformalLemma := false,
+   isSemiFormalResult := true, category := PhysLeanCategory.ofFileName t.fileName,
+   tag := t.tag}
+
+unsafe def allSemiInformal  : CoreM (Array FullTODOInfo) := do
+  let env ← getEnv
+  let semiInformalInfos := (wantedExtension.getState env)
+  pure (semiInformalInfos.map FullTODOInfo.ofSemiFormal)
+
 def FullTODOInfo.toYAML (todo : FullTODOInfo) : MetaM String := do
   let content := todo.content
   let contentIndent := content.replace "\n" "\n      "
@@ -170,6 +185,7 @@ def FullTODOInfo.toYAML (todo : FullTODOInfo) : MetaM String := do
     line: {todo.line}
     isInformalDef: {todo.isInformalDef}
     isInformalLemma: {todo.isInformalLemma}
+    isSemiFormalResult: {todo.isSemiFormalResult}
     category: {todo.category}
     name: {todo.name}
     tag: {todo.tag}
@@ -179,7 +195,8 @@ def FullTODOInfo.toYAML (todo : FullTODOInfo) : MetaM String := do
 unsafe def allTODOs : MetaM (List FullTODOInfo) := do
   let todos ← getTodoInfo
   let informalTODOs ← allInformalTODO
-  let all := todos ++ informalTODOs
+  let semiInformal ← allSemiInformal
+  let all := todos ++ informalTODOs ++ semiInformal
   return  (all.qsort (fun x y => x.fileName.toString < y.fileName.toString
     ∨ (x.fileName.toString = y.fileName.toString ∧ x.line < y.line))).toList