DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat: Add dependencies

Browse source
This commit is contained in:
jstoobysmith 2024-09-16 05:32:40 -04:00
parent acef250fe0
commit b50efa91f7
2 changed files with 19 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

22
HepLean/Meta/Informal.lean
View file

@ -15,8 +15,6 @@ open Lean Elab System
/-! TODO: Can likely make this a bona-fide command. -/
/-! TODO: Add expected dependencies. -/
/-- The structure representating an informal definition. -/
structure InformalDefinition where
/-- The name of the informal definition. This is autogenerated. -/
@ -27,6 +25,8 @@ structure InformalDefinition where
physics : String
/-- References. -/
ref : String
/-- The names of top-level commands we expect this definition to depend on. -/
dependencies : List Name
/-- The structure representating an informal proof. -/
structure InformalLemma where
@ -40,6 +40,8 @@ structure InformalLemma where
proof : String
/-- References. -/
ref : String
/-- The names of top-level commands we expect this lemma to depend on. -/
dependencies : List Name
namespace Informal
@ -49,6 +51,8 @@ declare_syntax_cat informalAssignment
/-- The syntax describing an informal assignment of `ident` to a string. -/
syntax (name := informalAssignment) ident ":≈" str : informalAssignment
syntax (name := informalAssignmentDeps) ident ":≈" "[" sepBy(term, ",") "]" : informalAssignment
/-- The syntax for the command informal_definition. -/
syntax (name := informal_definition) "informal_definition " ident
" where " (colGt informalAssignment)* : command
@ -58,6 +62,7 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
let mut math_def? : Option (TSyntax `term) := none
let mut physics_def? : Option (TSyntax `term) := none
let mut ref_def? : Option (TSyntax `term) := none
let mut dep_def? : Option (TSyntax `term) := none
for assignment in assignments do
match assignment with
| `(informalAssignment| physics :≈ $val:str) =>
@ -69,7 +74,9 @@ macro "informal_definition " name:ident " where " assignments:informalAssignment
| `(informalAssignment| ref :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
ref_def? := some (← `($(Lean.quote strVal)))
| _ => Macro.throwError "invalid assignment syntax"
| `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
dep_def? := some (← `([ $deps,* ]))
| _ => Macro.throwError "invalid assignment syntax in informal_definition"
unless math_def?.isSome do
Macro.throwError "A 'math' assignments is required"
`(
@ -78,7 +85,8 @@ def $name : InformalDefinition := {
name := $(Lean.quote name.getId),
physics := $(physics_def?.getD (← `("No physics description provided"))),
math := $(math_def?.getD (panic! "math not assigned")),
ref := $(ref_def?.getD (← `("No references provided")))
ref := $(ref_def?.getD (← `("No references provided"))),
dependencies := $(dep_def?.getD (← `([])))
})
/-- The syntax for the command `informal_lemma`. -/
@ -91,6 +99,7 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
let mut physics_def? : Option (TSyntax `term) := none
let mut proof_def? : Option (TSyntax `term) := none
let mut ref_def? : Option (TSyntax `term) := none
let mut dep_def? : Option (TSyntax `term) := none
for assignment in assignments do
match assignment with
| `(informalAssignment| physics :≈ $val:str) =>
@ -105,6 +114,8 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
| `(informalAssignment| ref :≈ $val:str) =>
let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
ref_def? := some (← `($(Lean.quote strVal)))
| `(informalAssignmentDeps| deps :≈ [ $deps,* ]) =>
dep_def? := some (← `([ $deps,* ]))
| _ => Macro.throwError "invalid assignment syntax"
unless math_def?.isSome do
Macro.throwError "A 'math' assignments is required"
@ -115,7 +126,8 @@ def $name : InformalLemma := {
physics := $(physics_def?.getD (← `("No physics description provided"))),
math := $(math_def?.getD (panic! "math not assigned")),
proof := $(proof_def?.getD (← `("No proof description provided"))),
ref := $(ref_def?.getD (← `("No references provided")))
ref := $(ref_def?.getD (← `("No references provided"))),
dependencies := $(dep_def?.getD (← `([])))
})
end Informal

3
HepLean/SpaceTime/WeylFermion/Basic.lean
View file

@ -39,14 +39,15 @@ informal_definition altRightHandedWeylFermion where
## Equivalences between Weyl fermion vector spaces.
-/
informal_definition leftHandedWeylFermionAltEquiv where
math :≈ "The linear equiv between leftHandedWeylFermion and altLeftHandedWeylFermion given
by multiplying an element of rightHandedWeylFermion by the matrix εᵃ⁰ᵃ¹ ={{0, 1}, {-1, 0}}."
deps :≈ [`leftHandedWeylFermion, `altLeftHandedWeylFermion]
informal_lemma leftHandedWeylFermionAltEquiv_equivariant where
math :≈ "The linear equiv leftHandedWeylFermionAltEquiv is equivariant with respect to the
action of SL(2,C) on leftHandedWeylFermion and altLeftHandedWeylFermion."
deps :≈ [`leftHandedWeylFermionAltEquiv]
informal_definition rightHandedWeylFermionAltEquiv where
math :≈ "The linear equiv between rightHandedWeylFermion and altRightHandedWeylFermion given