diff --git a/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean b/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean index 382c70b..695ce7b 100644 --- a/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean +++ b/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean @@ -17,27 +17,30 @@ This file currently contains informal-results about the Georgi-Glashow group. namespace GeorgiGlashow +/-- The gauge group of the Georgi-Glashow model, i.e., `SU(5)`. -/ informal_definition GaugeGroupI where - math :≈ "The group `SU(5)`." - physics :≈ "The gauge group of the Georgi-Glashow model." + deps := [] +/-- The homomorphism of the Standard Model gauge group into the Georgi-Glashow gauge group, i.e., +the group homomorphism `SU(3) × SU(2) × U(1) → SU(5)` taking `(h, g, α)` to +`blockdiag (α ^ 3 g, α ^ (-2) h)`. + +See page 34 of https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition inclSM where - physics :≈ "The homomorphism of the Standard Model gauge group into the - Georgi-Glashow gauge group." - math :≈ "The group homomorphism `SU(3) x SU(2) x U(1) -> SU(5)` - taking (h, g, α) to (blockdiag (α ^ 3 g, α ^ (-2) h)." - ref :≈ "Page 34 of https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``StandardModel.GaugeGroupI] + deps := [``GaugeGroupI, ``StandardModel.GaugeGroupI] +/-- The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₆SubGroup`. + +See page 34 of https://math.ucr.edu/home/baez/guts.pdf +-/ informal_lemma inclSM_ker where - math :≈ "The kernel of the map ``inclSM is equal to the subgroup - ``StandardModel.gaugeGroupℤ₆SubGroup." - ref :≈ "Page 34 of https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup] + deps := [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup] +/-- The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by +quotienting by the kernal `inclSM_ker`. +-/ informal_definition embedSMℤ₆ where - math :≈ "The group embedding from ``StandardModel.GaugeGroupℤ₆ to ``GaugeGroupI - induced by ``inclSM by quotienting by the kernal ``inclSM_ker." - deps :≈ [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupI, ``inclSM_ker] + deps := [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupI, ``inclSM_ker] end GeorgiGlashow diff --git a/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean b/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean index 8ee2bb3..6cb7c9e 100644 --- a/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean +++ b/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean @@ -22,54 +22,62 @@ namespace PatiSalam -/ +/-- The gauge group of the Pati-Salam model (unquotiented by ℤ₂), i.e., `SU(4) × SU(2) × SU(2)`. -/ informal_definition GaugeGroupI where - math :≈ "The group `SU(4) x SU(2) x SU(2)`." - physics :≈ "The gauge group of the Pati-Salam model (unquotiented by ℤ₂)." + deps := [] +/-- The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group, i.e., the +group homomorphism `SU(3) × SU(2) × U(1) → SU(4) × SU(2) × SU(2)` taking `(h, g, α)` to +`(blockdiag (α h, α ^ (-3)), g, diag (α ^ 3, α ^(-3))`. + +See page 54 of https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition inclSM where - physics :≈ "The homomorphism of the Standard Model gauge group into the Pati-Salam gauge group." - math :≈ "The group homomorphism `SU(3) x SU(2) x U(1) -> SU(4) x SU(2) x SU(2)` - taking (h, g, α) to (blockdiag (α h, α ^ (-3)), g, diag(α ^ (3), α ^(-3)))." - ref :≈ "Page 54 of https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``StandardModel.GaugeGroupI] + deps := [``GaugeGroupI, ``StandardModel.GaugeGroupI] +/-- The kernel of the map `inclSM` is equal to the subgroup `StandardModel.gaugeGroupℤ₃SubGroup`. + +See footnote 10 of https://arxiv.org/pdf/2201.07245 +-/ informal_lemma inclSM_ker where - math :≈ "The kernel of the map ``inclSM is equal to the subgroup - ``StandardModel.gaugeGroupℤ₃SubGroup." - ref :≈ "Footnote 10 of https://arxiv.org/pdf/2201.07245" - deps :≈ [``inclSM, ``StandardModel.gaugeGroupℤ₃SubGroup] + deps := [``inclSM, ``StandardModel.gaugeGroupℤ₃SubGroup] +/-- The group embedding from `StandardModel.GaugeGroupℤ₃` to `GaugeGroupI` induced by `inclSM` by +quotienting by the kernal `inclSM_ker`. +-/ informal_definition embedSMℤ₃ where - math :≈ "The group embedding from ``StandardModel.GaugeGroupℤ₃ to ``GaugeGroupI - induced by ``inclSM by quotienting by the kernal ``inclSM_ker." - deps :≈ [``inclSM, ``StandardModel.GaugeGroupℤ₃, ``GaugeGroupI, ``inclSM_ker] + deps := [``inclSM, ``StandardModel.GaugeGroupℤ₃, ``GaugeGroupI, ``inclSM_ker] +/-- The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`. -/ informal_definition gaugeGroupISpinEquiv where - math :≈ "The equivalence between `GaugeGroupI` and `Spin(6) × Spin(4)`." - deps :≈ [``GaugeGroupI] + deps := [``GaugeGroupI] +/-- The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on all particles in the +standard model, i.e., the ℤ₂-subgroup of `GaugeGroupI` with the non-trivial element `(-1, -1, -1)`. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition gaugeGroupℤ₂SubGroup where - physics :≈ "The ℤ₂-subgroup of the un-quotiented gauge group which acts trivially on - all particles in the standard model." - math :≈ "The ℤ₂-subgroup of ``GaugeGroupI with the non-trivial element (-1, -1, -1)." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI] + deps := [``GaugeGroupI] +/-- The gauge group of the Pati-Salam model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` +by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition GaugeGroupℤ₂ where - physics :≈ "The gauge group of the Pati-Salam model with a ℤ₂ quotient." - math :≈ "The quotient of ``GaugeGroupI by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``gaugeGroupℤ₂SubGroup] + deps := [``GaugeGroupI, ``gaugeGroupℤ₂SubGroup] +/-- The group `StandardModel.gaugeGroupℤ₆SubGroup` under the homomorphism `embedSM` factors through +the subgroup `gaugeGroupℤ₂SubGroup`. +-/ informal_lemma sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup where - math :≈ "The group ``StandardModel.gaugeGroupℤ₆SubGroup under the homomorphism ``embedSM factors - through the subgroup ``gaugeGroupℤ₂SubGroup." - deps :≈ [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup] + deps := [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup] +/-- The group homomorphism from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupℤ₂` induced by `embedSM`. +-/ informal_definition embedSMℤ₆Toℤ₂ where - math :≈ "The group homomorphism from ``StandardModel.GaugeGroupℤ₆ to ``GaugeGroupℤ₂ - induced by ``embedSM." - deps :≈ [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupℤ₂, + deps := [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupℤ₂, ``sm_ℤ₆_factor_through_gaugeGroupℤ₂SubGroup] end PatiSalam diff --git a/HepLean/BeyondTheStandardModel/Spin10/Basic.lean b/HepLean/BeyondTheStandardModel/Spin10/Basic.lean index a57d7c9..c44a80a 100644 --- a/HepLean/BeyondTheStandardModel/Spin10/Basic.lean +++ b/HepLean/BeyondTheStandardModel/Spin10/Basic.lean @@ -16,37 +16,42 @@ is Spin(10). namespace Spin10Model +/-- The gauge group of the Spin(10) model, i.e., the group `Spin(10)`. -/ informal_definition GaugeGroupI where - math :≈ "The group `Spin(10)`." - physics :≈ "The gauge group of the Spin(10) model (aka SO(10)-model.)" + deps := [] +/-- The inclusion of the Pati-Salam gauge group into Spin(10), i.e., the lift of the embedding +`SO(6) × SO(4) → SO(10)` to universal covers, giving a homomorphism `Spin(6) × Spin(4) → Spin(10)`. +Precomposed with the isomorphism, `PatiSalam.gaugeGroupISpinEquiv`, between `SU(4) × SU(2) × SU(2)` +and `Spin(6) × Spin(4)`. + +See page 56 of https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition inclPatiSalam where - physics :≈ "The inclusion of the Pati-Salam gauge group into Spin(10)." - math :≈ "The lift of the embedding `SO(6) x SO(4) → SO(10)` to universal covers, - giving a homomorphism `Spin(6) x Spin(4) → Spin(10)`. Precomposed with the isomorphism, - ``PatiSalam.gaugeGroupISpinEquiv, between `SU(4) x SU(2) x SU(2)` and `Spin(6) x Spin(4)`." - ref :≈ "Page 56 of https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``PatiSalam.GaugeGroupI, ``PatiSalam.gaugeGroupISpinEquiv] + deps := [``GaugeGroupI, ``PatiSalam.GaugeGroupI, ``PatiSalam.gaugeGroupISpinEquiv] +/-- The inclusion of the Standard Model gauge group into Spin(10), i.e., the compoisiton of +`embedPatiSalam` and `PatiSalam.inclSM`. + +See page 56 of https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition inclSM where - physics :≈ "The inclusion of the Standard Model gauge group into Spin(10)." - math :≈ "The compoisiton of ``embedPatiSalam and ``PatiSalam.inclSM." - ref :≈ "Page 56 of https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``inclPatiSalam, ``PatiSalam.inclSM] + deps := [``inclPatiSalam, ``PatiSalam.inclSM] +/-- The inclusion of the Georgi-Glashow gauge group into Spin(10), i.e., the Lie group homomorphism +from `SU(n) → Spin(2n)` discussed on page 46 of https://math.ucr.edu/home/baez/guts.pdf for `n = 5`. +-/ informal_definition inclGeorgiGlashow where - physics :≈ "The inclusion of the Georgi-Glashow gauge group into Spin(10)." - math :≈ "The Lie group homomorphism from SU(n) → Spin(2n) dicussed on page 46 of - https://math.ucr.edu/home/baez/guts.pdf for n = 5." - deps :≈ [``GaugeGroupI, ``GeorgiGlashow.GaugeGroupI] + deps := [``GaugeGroupI, ``GeorgiGlashow.GaugeGroupI] +/-- The inclusion of the Standard Model gauge group into Spin(10), i.e., the composition of +`inclGeorgiGlashow` and `GeorgiGlashow.inclSM`. +-/ informal_definition inclSMThruGeorgiGlashow where - physics :≈ "The inclusion of the Standard Model gauge group into Spin(10)." - math :≈ "The composition of ``inclGeorgiGlashow and ``GeorgiGlashow.inclSM." - deps :≈ [``inclGeorgiGlashow, ``GeorgiGlashow.inclSM] + deps := [``inclGeorgiGlashow, ``GeorgiGlashow.inclSM] +/-- The inclusion `inclSM` is equal to the inclusion `inclSMThruGeorgiGlashow`. -/ informal_lemma inclSM_eq_inclSMThruGeorgiGlashow where - math :≈ "The inclusion ``inclSM is equal to the inclusion ``inclSMThruGeorgiGlashow." - deps :≈ [``inclSM, ``inclSMThruGeorgiGlashow] + deps := [``inclSM, ``inclSMThruGeorgiGlashow] end Spin10Model diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean index 63c4453..aff69e8 100644 --- a/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean +++ b/HepLean/BeyondTheStandardModel/TwoHDM/GaugeOrbits.lean @@ -84,17 +84,19 @@ lemma prodMatrix_smooth (Φ1 Φ2 : HiggsField) : simpa only [prodMatrix, Fin.zero_eta, Fin.isValue, of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one] using smooth_innerProd _ _ +/-- The map `prodMatrix` is invariant under the simultanous action of `gaugeAction` on the two Higgs +fields. -/ informal_lemma prodMatrix_invariant where - math :≈ "The map ``prodMatrix is invariant under the simultanous action of ``gaugeAction - on the two Higgs fields." - deps :≈ [``prodMatrix, ``gaugeAction] + deps := [``prodMatrix, ``gaugeAction] +/-- Given any smooth map `f` from spacetime to 2-by-2 complex matrices landing on positive +semi-definite matrices, there exist smooth Higgs fields `Φ1` and `Φ2` such that `f` is equal to +`prodMatrix Φ1 Φ2`. + +See https://arxiv.org/pdf/hep-ph/0605184 +-/ informal_lemma prodMatrix_to_higgsField where - math :≈ "Given any smooth map ``f from spacetime to 2 x 2 complex matrices landing on positive - semi-definite matrices, there exist smooth Higgs fields ``Φ1 and ``Φ2 such that - ``f is equal to ``prodMatrix Φ1 Φ2." - deps :≈ [``prodMatrix, ``HiggsField, ``prodMatrix_smooth] - ref :≈ "https://arxiv.org/pdf/hep-ph/0605184" + deps := [``prodMatrix, ``HiggsField, ``prodMatrix_smooth] end end TwoHDM diff --git a/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean b/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean index af0cde5..1a1dd2f 100644 --- a/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean +++ b/HepLean/Lorentz/ComplexTensor/Bispinors/Basic.lean @@ -80,15 +80,19 @@ lemma tensorNode_coBispinorDown (p : complexCo) : -/ -informal_lemma contrBispinorUp_eq_metric_contr_contrBispinorDown where - math :≈ "{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ" - proof :≈ "Expand `contrBispinorDown` and use fact that metrics contract to the identity." - deps :≈ [``contrBispinorUp, ``contrBispinorDown, ``leftMetric, ``rightMetric] +/-- `{contrBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ contrBispinorDown p | α' β' }ᵀ`. +Proof: expand `contrBispinorDown` and use fact that metrics contract to the identity. +-/ +informal_lemma contrBispinorUp_eq_metric_contr_contrBispinorDown where + deps := [``contrBispinorUp, ``contrBispinorDown, ``leftMetric, ``rightMetric] + +/-- `{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ`. + +proof: expand `coBispinorDown` and use fact that metrics contract to the identity. +-/ informal_lemma coBispinorUp_eq_metric_contr_coBispinorDown where - math :≈ "{coBispinorUp p | α β = εL | α α' ⊗ εR | β β'⊗ coBispinorDown p | α' β' }ᵀ" - proof :≈ "Expand `coBispinorDown` and use fact that metrics contract to the identity." - deps :≈ [``coBispinorUp, ``coBispinorDown, ``leftMetric, ``rightMetric] + deps := [``coBispinorUp, ``coBispinorDown, ``leftMetric, ``rightMetric] lemma contrBispinorDown_expand (p : complexContr) : {contrBispinorDown p | α β}ᵀ.tensor = diff --git a/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean b/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean index dea01b0..ca848d0 100644 --- a/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean +++ b/HepLean/Lorentz/ComplexTensor/Metrics/Lemmas.lean @@ -31,29 +31,29 @@ namespace complexLorentzTensor -/ +/-- The covariant metric is symmetric `{η' | μ ν = η' | ν μ}ᵀ`. -/ informal_lemma coMetric_symm where - math :≈ "The covariant metric is symmetric {η' | μ ν = η' | ν μ}ᵀ" - deps :≈ [``coMetric] + deps := [``coMetric] +/-- The contravariant metric is symmetric `{η | μ ν = η | ν μ}ᵀ`. -/ informal_lemma contrMetric_symm where - math :≈ "The contravariant metric is symmetric {η | μ ν = η | ν μ}ᵀ" - deps :≈ [``contrMetric] + deps := [``contrMetric] +/-- The left metric is antisymmetric `{εL | α α' = - εL | α' α}ᵀ`. -/ informal_lemma leftMetric_antisymm where - math :≈ "The left metric is antisymmetric {εL | α α' = - εL | α' α}ᵀ" - deps :≈ [``leftMetric] + deps := [``leftMetric] +/-- The right metric is antisymmetric `{εR | β β' = - εR | β' β}ᵀ`. -/ informal_lemma rightMetric_antisymm where - math :≈ "The right metric is antisymmetric {εR | β β' = - εR | β' β}ᵀ" - deps :≈ [``rightMetric] + deps := [``rightMetric] +/-- The alt-left metric is antisymmetric `{εL' | α α' = - εL' | α' α}ᵀ`. -/ informal_lemma altLeftMetric_antisymm where - math :≈ "The alt-left metric is antisymmetric {εL' | α α' = - εL' | α' α}ᵀ" - deps :≈ [``altLeftMetric] + deps := [``altLeftMetric] +/-- The alt-right metric is antisymmetric `{εR' | β β' = - εR' | β' β}ᵀ`. -/ informal_lemma altRightMetric_antisymm where - math :≈ "The alt-right metric is antisymmetric {εR' | β β' = - εR' | β' β}ᵀ" - deps :≈ [``altRightMetric] + deps := [``altRightMetric] /-! @@ -61,35 +61,41 @@ informal_lemma altRightMetric_antisymm where -/ +/-- The contraction of the covariant metric with the contravariant metric is the unit +`{η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ`. +-/ informal_lemma coMetric_contr_contrMetric where - math :≈ "The contraction of the covariant metric with the contravariant metric is the unit - {η' | μ ρ ⊗ η | ρ ν = δ' | μ ν}ᵀ" - deps :≈ [``coMetric, ``contrMetric, ``coContrUnit] + deps := [``coMetric, ``contrMetric, ``coContrUnit] +/-- The contraction of the contravariant metric with the covariant metric is the unit +`{η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ`. +-/ informal_lemma contrMetric_contr_coMetric where - math :≈ "The contraction of the contravariant metric with the covariant metric is the unit - {η | μ ρ ⊗ η' | ρ ν = δ | μ ν}ᵀ" - deps :≈ [``contrMetric, ``coMetric, ``contrCoUnit] + deps := [``contrMetric, ``coMetric, ``contrCoUnit] +/-- The contraction of the left metric with the alt-left metric is the unit +`{εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ`. +-/ informal_lemma leftMetric_contr_altLeftMetric where - math :≈ "The contraction of the left metric with the alt-left metric is the unit - {εL | α β ⊗ εL' | β γ = δL | α γ}ᵀ" - deps :≈ [``leftMetric, ``altLeftMetric, ``leftAltLeftUnit] + deps := [``leftMetric, ``altLeftMetric, ``leftAltLeftUnit] +/-- The contraction of the right metric with the alt-right metric is the unit +`{εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ`. +-/ informal_lemma rightMetric_contr_altRightMetric where - math :≈ "The contraction of the right metric with the alt-right metric is the unit - {εR | α β ⊗ εR' | β γ = δR | α γ}ᵀ" - deps :≈ [``rightMetric, ``altRightMetric, ``rightAltRightUnit] + deps := [``rightMetric, ``altRightMetric, ``rightAltRightUnit] +/-- The contraction of the alt-left metric with the left metric is the unit +`{εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ`. +-/ informal_lemma altLeftMetric_contr_leftMetric where - math :≈ "The contraction of the alt-left metric with the left metric is the unit - {εL' | α β ⊗ εL | β γ = δL' | α γ}ᵀ" - deps :≈ [``altLeftMetric, ``leftMetric, ``altLeftLeftUnit] + deps := [``altLeftMetric, ``leftMetric, ``altLeftLeftUnit] +/-- The contraction of the alt-right metric with the right metric is the unit +`{εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ`. +-/ informal_lemma altRightMetric_contr_rightMetric where - math :≈ "The contraction of the alt-right metric with the right metric is the unit - {εR' | α β ⊗ εR | β γ = δR' | α γ}ᵀ" - deps :≈ [``altRightMetric, ``rightMetric, ``altRightRightUnit] + deps := [``altRightMetric, ``rightMetric, ``altRightRightUnit] /-! diff --git a/HepLean/Lorentz/ComplexTensor/Units/Symm.lean b/HepLean/Lorentz/ComplexTensor/Units/Symm.lean index 541a097..a58aef7 100644 --- a/HepLean/Lorentz/ComplexTensor/Units/Symm.lean +++ b/HepLean/Lorentz/ComplexTensor/Units/Symm.lean @@ -31,32 +31,32 @@ namespace complexLorentzTensor -/ +/-- Swapping indices of `coContrUnit` returns `contrCoUnit`: `{δ' | μ ν = δ | ν μ}ᵀ`. -/ informal_lemma coContrUnit_symm where - math :≈ "Swapping indices of coContrUnit returns contrCoUnit, i.e. {δ' | μ ν = δ | ν μ}.ᵀ" - deps :≈ [``coContrUnit, ``contrCoUnit] + deps := [``coContrUnit, ``contrCoUnit] +/-- Swapping indices of `contrCoUnit` returns `coContrUnit`: `{δ | μ ν = δ' | ν μ}ᵀ`. -/ informal_lemma contrCoUnit_symm where - math :≈ "Swapping indices of contrCoUnit returns coContrUnit, i.e. {δ | μ ν = δ' | ν μ}ᵀ" - deps :≈ [``contrCoUnit, ``coContrUnit] + deps := [``contrCoUnit, ``coContrUnit] +/-- Swapping indices of `altLeftLeftUnit` returns `leftAltLeftUnit`: `{δL' | α α' = δL | α' α}ᵀ`. -/ informal_lemma altLeftLeftUnit_symm where - math :≈ "Swapping indices of altLeftLeftUnit returns leftAltLeftUnit, i.e. - {δL' | α α' = δL | α' α}ᵀ" - deps :≈ [``altLeftLeftUnit, ``leftAltLeftUnit] + deps := [``altLeftLeftUnit, ``leftAltLeftUnit] +/-- Swapping indices of `leftAltLeftUnit` returns `altLeftLeftUnit`: `{δL | α α' = δL' | α' α}ᵀ`. -/ informal_lemma leftAltLeftUnit_symm where - math :≈ "Swapping indices of leftAltLeftUnit returns altLeftLeftUnit, i.e. - {δL | α α' = δL' | α' α}ᵀ" - deps :≈ [``leftAltLeftUnit, ``altLeftLeftUnit] + deps := [``leftAltLeftUnit, ``altLeftLeftUnit] +/-- Swapping indices of `altRightRightUnit` returns `rightAltRightUnit`: +`{δR' | β β' = δR | β' β}ᵀ`. +-/ informal_lemma altRightRightUnit_symm where - math :≈ "Swapping indices of altRightRightUnit returns rightAltRightUnit, i.e. - {δR' | β β' = δR | β' β}ᵀ" - deps :≈ [``altRightRightUnit, ``rightAltRightUnit] + deps := [``altRightRightUnit, ``rightAltRightUnit] +/-- Swapping indices of `rightAltRightUnit` returns `altRightRightUnit`: +`{δR | β β' = δR' | β' β}ᵀ`. +-/ informal_lemma rightAltRightUnit_symm where - math :≈ "Swapping indices of rightAltRightUnit returns altRightRightUnit, i.e. - {δR | β β' = δR' | β' β}ᵀ" - deps :≈ [``rightAltRightUnit, ``altRightRightUnit] + deps := [``rightAltRightUnit, ``altRightRightUnit] end complexLorentzTensor diff --git a/HepLean/Lorentz/Group/Restricted.lean b/HepLean/Lorentz/Group/Restricted.lean index 7a806b6..082db08 100644 --- a/HepLean/Lorentz/Group/Restricted.lean +++ b/HepLean/Lorentz/Group/Restricted.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import HepLean.Lorentz.Group.Orthochronous +import HepLean.Meta.Informal.Basic /-! # The Restricted Lorentz Group @@ -16,17 +17,10 @@ TODO "Prove that every member of the restricted Lorentz group is TODO "Prove restricted Lorentz group equivalent to connected component of identity of the Lorentz group." -noncomputable section - -open Matrix -open Complex -open ComplexConjugate - namespace LorentzGroup +/-- The subgroup of the Lorentz group consisting of elements which are proper and orthochronous. -/ informal_definition Restricted where - math :≈ "The subgroup of the Lorentz group consisting of elements which - are proper and orthochronous." - deps :≈ [``LorentzGroup, ``IsProper, ``IsOrthochronous] + deps := [``LorentzGroup, ``IsProper, ``IsOrthochronous] end LorentzGroup diff --git a/HepLean/Lorentz/RealVector/Modules.lean b/HepLean/Lorentz/RealVector/Modules.lean index 2652df7..bc38c7c 100644 --- a/HepLean/Lorentz/RealVector/Modules.lean +++ b/HepLean/Lorentz/RealVector/Modules.lean @@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ -import HepLean.Meta.Informal.Basic import HepLean.Lorentz.PauliMatrices.SelfAdjoint /-! diff --git a/HepLean/Lorentz/SL2C/Basic.lean b/HepLean/Lorentz/SL2C/Basic.lean index 58df051..8152aef 100644 --- a/HepLean/Lorentz/SL2C/Basic.lean +++ b/HepLean/Lorentz/SL2C/Basic.lean @@ -307,9 +307,9 @@ lemma toLorentzGroup_det_one (M : SL(2, ℂ)) : det (toLorentzGroup M).val = 1 : _ = M.val.det := congrArg det h.symm _ = 1 := M.property +/-- The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/ informal_lemma toRestrictedLorentzGroup where - math :≈ "The homomorphism from `SL(2, ℂ)` to the restricted Lorentz group." - deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_isOrthochronous, + deps := [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_isOrthochronous, ``LorentzGroup.Restricted] TODO "Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group." diff --git a/HepLean/Lorentz/Weyl/Basic.lean b/HepLean/Lorentz/Weyl/Basic.lean index 218b820..6c04b99 100644 --- a/HepLean/Lorentz/Weyl/Basic.lean +++ b/HepLean/Lorentz/Weyl/Basic.lean @@ -284,15 +284,17 @@ lemma leftHandedAltEquiv_inv_hom_apply (ψ : altLeftHanded) : leftHandedAltEquiv.inv.hom ψ = LeftHandedModule.toFin2ℂEquiv.symm (!![0, -1; 1, 0] *ᵥ ψ.toFin2ℂ) := rfl +/-- The linear equivalence between `rightHandedWeyl` and `altRightHandedWeyl` given by multiplying +an element of `rightHandedWeyl` by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`. +-/ informal_definition rightHandedWeylAltEquiv where - math :≈ "The linear equiv between rightHandedWeyl and altRightHandedWeyl given - by multiplying an element of rightHandedWeyl by the matrix `εᵃ⁰ᵃ¹ = !![0, 1; -1, 0]]`" - deps :≈ [``rightHanded, ``altRightHanded] + deps := [``rightHanded, ``altRightHanded] +/-- The linear equivalence `rightHandedWeylAltEquiv` is equivariant with respect to the action of +`SL(2,C)` on `rightHandedWeyl` and `altRightHandedWeyl`. +-/ informal_lemma rightHandedWeylAltEquiv_equivariant where - math :≈ "The linear equiv rightHandedWeylAltEquiv is equivariant with respect to the - action of SL(2,C) on rightHandedWeyl and altRightHandedWeyl." - deps :≈ [``rightHandedWeylAltEquiv] + deps := [``rightHandedWeylAltEquiv] end diff --git a/HepLean/Meta/AllFilePaths.lean b/HepLean/Meta/AllFilePaths.lean index 9c26efe..d27cdd8 100644 --- a/HepLean/Meta/AllFilePaths.lean +++ b/HepLean/Meta/AllFilePaths.lean @@ -3,7 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Lean import HepLean.Meta.TODO.Basic /-! @@ -11,7 +10,7 @@ import HepLean.Meta.TODO.Basic -/ -open Lean Elab System +open System TODO "Make this definition more functional in style. In other words, remove the for loop." diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean index 7e2bf36..3fc53fd 100644 --- a/HepLean/Meta/Basic.lean +++ b/HepLean/Meta/Basic.lean @@ -3,19 +3,23 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Batteries.Lean.HashSet import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.CoreM import ImportGraph.RequiredModules -import HepLean.Meta.Informal.Basic /-! ## Basic Lean meta programming commands -/ -namespace HepLean -open Lean System Meta +/-- The size of a flattened array of arrays. -/ +def Array.flatSize {α} : Array (Array α) → Nat := + foldl (init := 0) fun sizeAcc as => sizeAcc + as.size + +/-- The size of a flattened array of arrays after applying an element-wise filter. -/ +def Array.flatFilterSizeM {α m} [Monad m] (p : α → m Bool) : Array (Array α) → m Nat := + foldlM (init := 0) fun sizeAcc as => return sizeAcc + (← as.filterM p).size + +open Lean /-! @@ -24,194 +28,166 @@ open Lean System Meta -/ /-- Gets all imports within HepLean. -/ -def allImports : IO (Array Import) := do +def HepLean.allImports : IO (Array Import) := do initSearchPath (← findSysroot) - let mods : Name := `HepLean - let imp : Import := {module := mods} - let mFile ← findOLean imp.module - unless (← mFile.pathExists) do - throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist" + let mods := `HepLean + let mFile ← findOLean mods + unless ← mFile.pathExists do + throw <| IO.userError s!"object file '{mFile}' of module {mods} does not exist" let (hepLeanMod, _) ← readModuleData mFile - let imports := hepLeanMod.imports.filter (fun c => c.module ≠ `Init) - return imports + hepLeanMod.imports.filterM fun c => return c.module != `Init /-- Number of files within HepLean. -/ -def noImports : IO Nat := do +def HepLean.noImports : IO Nat := do let imports ← allImports - pure imports.size + return imports.size /-- Gets all constants from an import. -/ -def Imports.getConsts (imp : Import) : IO (Array ConstantInfo) := do +def HepLean.Imports.getConsts (imp : Import) : IO (Array ConstantInfo) := do let mFile ← findOLean imp.module let (modData, _) ← readModuleData mFile - pure modData.constants + return modData.constants /-- Gets all user defined constants from an import. -/ -def Imports.getUserConsts (imp : Import) : MetaM (Array ConstantInfo) := do +def HepLean.Imports.getUserConsts (imp : Import) : CoreM (Array ConstantInfo) := do let env ← getEnv - let x := (← Imports.getConsts imp).filter (fun c => ¬ c.name.isInternal) - let x := x.filter (fun c => ¬ Lean.isCasesOnRecursor env c.name) - let x := x.filter (fun c => ¬ Lean.isRecOnRecursor env c.name) - let x := x.filter (fun c => ¬ Lean.isNoConfusion env c.name) - let x := x.filter (fun c => ¬ Lean.isBRecOnRecursor env c.name) - let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.binductionOnSuffix) - let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.belowSuffix) - let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.ibelowSuffix) - /- Removing syntax category declarations. -/ - let x := x.filter (fun c => ¬ c.name.toString = "Informal.informalAssignment.quot") - let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.indexExpr.quot") - let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.tensorExpr.quot") - pure x + let consts ← Imports.getConsts imp + consts.filterM fun c => + let name := c.name + return !name.isInternal + && !isCasesOnRecursor env name + && !isRecOnRecursor env name + && !isNoConfusion env name + && !isBRecOnRecursor env name + && !isAuxRecursorWithSuffix env name binductionOnSuffix + && !isAuxRecursorWithSuffix env name belowSuffix + && !isAuxRecursorWithSuffix env name ibelowSuffix + /- Removing syntax category declarations. -/ + && name.toString != "TensorTree.indexExpr.quot" + && name.toString != "TensorTree.tensorExpr.quot" + +/-- Turns a name into a system file path. -/ +def Lean.Name.toFilePath (c : Name) : System.FilePath := + System.mkFilePath (c.toString.splitOn ".") |>.addExtension "lean" /-- Lines from import. -/ -def Imports.getLines (imp : Import) : IO (Array String) := do - let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean" - let lines ← IO.FS.lines filePath - return lines +def HepLean.Imports.getLines (imp : Import) : IO (Array String) := do + IO.FS.lines imp.module.toFilePath +namespace Lean.Name /-! ## Name -/ +variable {m} [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] + /-- Turns a name into a Lean file. -/ -def Name.toFile (c : Name) : MetaM String := do - return s!"./{c.toString.replace "." "/" ++ ".lean"}" +def toRelativeFilePath (c : Name) : System.FilePath := + System.FilePath.join "." c.toFilePath /-- Turns a name, which represents a module, into a link to github. -/ -def Name.toGitHubLink (c : Name) (l : Nat := 0) : MetaM String := do - let headerLink := "https://github.com/HEPLean/HepLean/blob/master/" - let filePart := (c.toString.replace "." "/") ++ ".lean" - let linePart := "#L" ++ toString l - return headerLink ++ filePart ++ linePart +def toGitHubLink (c : Name) (line : Nat) : String := + s!"https://github.com/HEPLean/HepLean/blob/master/{c.toFilePath}#L{line}" /-- Given a name, returns the line number. -/ -def Name.lineNumber (c : Name) : MetaM Nat := do +def lineNumber (c : Name) : m Nat := do match ← findDeclarationRanges? c with - | some decl => pure decl.range.pos.line + | some decl => return decl.range.pos.line | none => panic! s!"{c} is a declaration without position" /-- Given a name, returns the file name corresponding to that declaration. -/ -def Name.fileName (c : Name) : MetaM Name := do +def fileName (c : Name) : m Name := do let env ← getEnv - let x := env.getModuleFor? c - match x with - | some c => pure c + match env.getModuleFor? c with + | some decl => return decl | none => panic! s!"{c} is a declaration without position" /-- Returns the location of a name. -/ -def Name.location (c : Name) : MetaM String := do +def location (c : Name) : m String := do let env ← getEnv - let x := env.getModuleFor? c - match x with - | some decl => pure ((← Name.toFile decl) ++ ":" ++ toString (← Name.lineNumber c) ++ " " - ++ c.toString) + match env.getModuleFor? c with + | some decl => return s!"{decl.toRelativeFilePath}:{← c.lineNumber} {c}" | none => panic! s!"{c} is a declaration without position" /-- Determines if a name has a location. -/ -def Name.hasPos (c : Name) : MetaM Bool := do - match ← findDeclarationRanges? c with - | some _ => pure true - | none => pure false +def hasPos (c : Name) : m Bool := do + let ranges? ← findDeclarationRanges? c + return ranges?.isSome /-- Determines if a name has a doc string. -/ -def Name.hasDocString (c : Name) : MetaM Bool := do +def hasDocString (c : Name) : CoreM Bool := do let env ← getEnv - let doc ← Lean.findDocString? env c - match doc with - | some _ => pure true - | none => pure false + let doc? ← findDocString? env c + return doc?.isSome /-- The doc string from a name. -/ -def Name.getDocString (c : Name) : MetaM String := do +def getDocString (c : Name) : CoreM String := do let env ← getEnv - let doc ← Lean.findDocString? env c - match doc with - | some doc => pure doc - | none => pure "" + let doc? ← findDocString? env c + return doc?.getD "" /-- Given a name, returns the source code defining that name. -/ -def Name.getDeclString (name : Name) : MetaM String := do +def getDeclString (name : Name) : CoreM String := do let env ← getEnv - let decl ← findDeclarationRanges? name - match decl with - | some decl => - let startLine := decl.range.pos - let endLine := decl.range.endPos - let fileName? := env.getModuleFor? name - match fileName? with + match ← findDeclarationRanges? name with + | some { range := { pos, endPos, .. }, .. } => + match env.getModuleFor? name with | some fileName => - let fileContent ← IO.FS.readFile { toString := (← Name.toFile fileName)} + let fileContent ← IO.FS.readFile fileName.toRelativeFilePath let fileMap := fileContent.toFileMap - let startPos := fileMap.ofPosition startLine - let endPos := fileMap.ofPosition endLine - let text := fileMap.source.extract startPos endPos - pure text - | none => - pure "" - | none => pure "" + return fileMap.source.extract (fileMap.ofPosition pos) (fileMap.ofPosition endPos) + | none => return "" + | none => return "" + +end Lean.Name + +namespace HepLean /-- Number of definitions. -/ -def noDefs : MetaM Nat := do - let imports ← allImports - let x ← imports.mapM Imports.getUserConsts - let x := x.flatten - let x := x.filter (fun c => c.isDef) - let x ← x.filterM (fun c => (Name.hasPos c.name)) - pure x.toList.length +def noDefs : CoreM Nat := do + let imports ← HepLean.allImports + let x ← imports.mapM HepLean.Imports.getUserConsts + x.flatFilterSizeM fun c => return c.isDef && (← c.name.hasPos) /-- Number of definitions. -/ -def noLemmas : MetaM Nat := do - let imports ← allImports - let x ← imports.mapM Imports.getUserConsts - let x := x.flatten - let x := x.filter (fun c => ¬ c.isDef) - let x ← x.filterM (fun c => (Name.hasPos c.name)) - pure x.toList.length +def noLemmas : CoreM Nat := do + let imports ← HepLean.allImports + let x ← imports.mapM HepLean.Imports.getUserConsts + x.flatFilterSizeM fun c => return !c.isDef && (← c.name.hasPos) /-- Number of definitions without a doc-string. -/ -def noDefsNoDocString : MetaM Nat := do - let imports ← allImports - let x ← imports.mapM Imports.getUserConsts - let x := x.flatten - let x := x.filter (fun c => c.isDef) - let x ← x.filterM (fun c => (Name.hasPos c.name)) - let x ← x.filterM (fun c => do - return Bool.not (← (Name.hasDocString c.name))) - pure x.toList.length +def noDefsNoDocString : CoreM Nat := do + let imports ← HepLean.allImports + let x ← imports.mapM HepLean.Imports.getUserConsts + x.flatFilterSizeM fun c => + return c.isDef && (← c.name.hasPos) && !(← c.name.hasDocString) /-- Number of definitions without a doc-string. -/ -def noLemmasNoDocString : MetaM Nat := do - let imports ← allImports - let x ← imports.mapM Imports.getUserConsts - let x := x.flatten - let x := x.filter (fun c => ¬ c.isDef) - let x ← x.filterM (fun c => (Name.hasPos c.name)) - let x ← x.filterM (fun c => do - return Bool.not (← (Name.hasDocString c.name))) - pure x.toList.length +def noLemmasNoDocString : CoreM Nat := do + let imports ← HepLean.allImports + let x ← imports.mapM HepLean.Imports.getUserConsts + x.flatFilterSizeM fun c => + return !c.isDef && (← c.name.hasPos) && !(← c.name.hasDocString) /-- The number of lines in HepLean. -/ def noLines : IO Nat := do let imports ← HepLean.allImports let x ← imports.mapM HepLean.Imports.getLines - let x := x.flatten - pure x.toList.length + return x.flatSize /-- The number of TODO items. -/ def noTODOs : IO Nat := do let imports ← HepLean.allImports let x ← imports.mapM HepLean.Imports.getLines - let x := x.flatten - let x := x.filter fun l => l.startsWith "TODO " - pure x.size + x.flatFilterSizeM fun l => return l.startsWith "TODO " /-- The number of files with a TODO item. -/ def noFilesWithTODOs : IO Nat := do let imports ← HepLean.allImports let x ← imports.mapM HepLean.Imports.getLines - let x := x.filter (fun M => M.any fun l => l.startsWith "TODO ") - pure x.size + let x := x.filter fun bs => bs.any fun l => l.startsWith "TODO " + return x.size end HepLean diff --git a/HepLean/Meta/Informal/Basic.lean b/HepLean/Meta/Informal/Basic.lean index 027f72c..414630c 100644 --- a/HepLean/Meta/Informal/Basic.lean +++ b/HepLean/Meta/Informal/Basic.lean @@ -3,245 +3,57 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Lean -import HepLean.Meta.TODO.Basic +import Lean.Parser.Term /-! ## Informal definitions and lemmas -This file contains the necessary structures that must be imported into a file -for it to contain informal definitions and lemmas. +This file contains the necessary structures that must be imported into a file for it to contain +informal definitions and lemmas. Everything else about informal definitions and lemmas are in the `Informal.Post` module. -/ -open Lean Elab System - -TODO "Can likely make this a bona-fide command." /-- The structure representing an informal definition. -/ structure InformalDefinition where - /-- The name of the informal definition. This is autogenerated. -/ - name : Name - /-- The mathematical description of the definition. -/ - math : String - /-- The physics description of the definition. -/ - physics : String - /-- References. -/ - ref : String /-- The names of top-level commands we expect this definition to depend on. -/ - dependencies : List Name + deps : List Lean.Name -/-- The structure representing an informal proof. -/ +/-- The structure representing an informal lemma. -/ structure InformalLemma where - /-- The name of the informal lemma. This is autogenerated. -/ - name : Name - /-- The mathematical description of the lemma. -/ - math : String - /-- The physics description of the lemma. -/ - physics : String - /-- A description of the proof. -/ - proof : String - /-- References. -/ - ref : String /-- The names of top-level commands we expect this lemma to depend on. -/ - dependencies : List Name + deps : List Lean.Name namespace Informal -/-- The Parser.Category we will use for assignments. -/ -declare_syntax_cat informalAssignment - -/-- The syntax describing an informal assignment of `ident` to a string. -/ -syntax (name := informalAssignment) ident ":≈" str : informalAssignment - -/-- The syntax describing an informal assignment of `ident` to a list. -/ -syntax (name := informalAssignmentDeps) ident ":≈" "[" sepBy(term, ",") "]" : informalAssignment - /-! ## Syntax +Using macros for syntax rewriting works better with the language server compared to +`Lake.DSL.LeanLibDecl`. Hovering over any definition of `informal_definition` or `informal_lemma` +gives a proper type hint like any proper definition using `def` whereas definitions of `lake_lib` +and `lake_exe` don't show docstrings and infer the type `Lean.Name`. + -/ -/-- The syntax for the command informal_definition. -/ -syntax (name := informal_definition) "informal_definition " ident - " where " (colGt informalAssignment)* : command -/-- An informal definition is a definition which is not type checked, and is written - as a string literal. It can be used to plan out sections for future formalization, or to - include results which the formalization is not immediately known. - Each informal definition must included a - `math :≈ "..."` - entry, but can also include the following entries - `physics :≈ "..."`, `ref :≈ "..."`, and `deps :≈ [...]`. -/ -macro "informal_definition " name:ident " where " assignments:informalAssignment* : command => do - 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) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics" - physics_def? := some (← `($(Lean.quote strVal))) - | `(informalAssignment| math :≈ $val:str) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math" - math_def? := some (← `($(Lean.quote strVal))) - | `(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 in informal_definition" - unless math_def?.isSome do - Macro.throwError "A 'math' assignments is required" - `( -/-- An informal definition. -/ -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"))), - dependencies := $(dep_def?.getD (← `([]))) - }) +open Lean.Parser.Term -/-- The syntax for the command informal_definition. -/ -syntax (name := informal_definition_note) "informal_definition_note " ident - " where " (colGt informalAssignment)* : command +/-- A placeholder for definitions to be formalized in the future. Docstrings of informal definitions +should outline its mathematical or physical content and specify useful references. Use the attribute +`note_attr_informal` from `HepLean.Meta.Notes.Basic` to mark the informal definition as a note. +-/ +macro (name := informalDefinitionDecl) +doc?:(docComment)? attrs?:(attributes)? "informal_definition " name:ident body:declVal : command => + `($[$doc?]? $[$attrs?]? def $name : InformalDefinition $body:declVal) -/-- An informal definition is a definition which is not type checked, and is written - as a string literal. It can be used to plan out sections for future formalization, or to - include results which the formalization is not immediately known. - Each informal definition must included a - `math :≈ "..."` - entry, but can also include the following entries - `physics :≈ "..."`, `ref :≈ "..."`, and `deps :≈ [...]`. -/ -macro "informal_definition_note " name:ident " where " assignments:informalAssignment* : - command => do - 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) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics" - physics_def? := some (← `($(Lean.quote strVal))) - | `(informalAssignment| math :≈ $val:str) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math" - math_def? := some (← `($(Lean.quote strVal))) - | `(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 in informal_definition" - unless math_def?.isSome do - Macro.throwError "A 'math' assignments is required" - `( -/-- An informal definition. -/ -@[note_attr_informal] -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"))), - dependencies := $(dep_def?.getD (← `([]))) - }) - -/-- The syntax for the command `informal_lemma`. -/ -syntax (name := informal_lemma) "informal_lemma " ident " where " - (colGt informalAssignment)* : command - -/-- An informal lemma is a lemma which is not type checked, and is written - as a string literal. It can be used to plan out sections for future formalization, or to - include results which the formalization is not immediately known. - Every informal lemma must included a - `math :≈ "..."` - entry, but can also include the following entries - `physics :≈ "..."`, `proof :≈ "..."`, `ref :≈ "..."`, and `deps :≈ [...]`. -/ -macro "informal_lemma " name:ident " where " assignments:informalAssignment* : command => do - let mut math_def? : Option (TSyntax `term) := none - 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) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics" - physics_def? := some (← `($(Lean.quote strVal))) - | `(informalAssignment| math :≈ $val:str) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math" - math_def? := some (← `($(Lean.quote strVal))) - | `(informalAssignment| proof :≈ $val:str) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for proof" - proof_def? := some (← `($(Lean.quote strVal))) - | `(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" - `( -/-- An informal lemma. -/ -def $name : InformalLemma := { - name := $(Lean.quote name.getId), - 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"))), - dependencies := $(dep_def?.getD (← `([]))) - }) - -/-- The syntax for the command `informal_lemma`. -/ -syntax (name := informal_lemma_note) "informal_lemma_note " ident " where " - (colGt informalAssignment)* : command - -/-- An informal lemma is a lemma which is not type checked, and is written - as a string literal. It can be used to plan out sections for future formalization, or to - include results which the formalization is not immediately known. - Every informal lemma must included a - `math :≈ "..."` - entry, but can also include the following entries - `physics :≈ "..."`, `proof :≈ "..."`, `ref :≈ "..."`, and `deps :≈ [...]`. -/ -macro "informal_lemma_note " name:ident " where " assignments:informalAssignment* : command => do - let mut math_def? : Option (TSyntax `term) := none - 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) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics" - physics_def? := some (← `($(Lean.quote strVal))) - | `(informalAssignment| math :≈ $val:str) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math" - math_def? := some (← `($(Lean.quote strVal))) - | `(informalAssignment| proof :≈ $val:str) => - let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for proof" - proof_def? := some (← `($(Lean.quote strVal))) - | `(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" - `( -/-- An informal lemma. -/ -@[note_attr_informal] -def $name : InformalLemma := { - name := $(Lean.quote name.getId), - 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"))), - dependencies := $(dep_def?.getD (← `([]))) - }) +/-- A placeholder for lemmas to be formalized in the future. Docstrings of informal lemmas +should outline its mathematical or physical content and specify useful references. Use the attribute +`note_attr_informal` from `HepLean.Meta.Notes.Basic` to mark the informal definition as a note. +-/ +macro (name := informalLemmaDecl) +doc?:(docComment)? attrs?:(attributes)? "informal_lemma " name:ident body:declVal : command => + `($[$doc?]? $[$attrs?]? def $name : InformalLemma $body:declVal) end Informal diff --git a/HepLean/Meta/Informal/Post.lean b/HepLean/Meta/Informal/Post.lean index 80103e8..8504395 100644 --- a/HepLean/Meta/Informal/Post.lean +++ b/HepLean/Meta/Informal/Post.lean @@ -4,74 +4,61 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.Meta.Basic +import HepLean.Meta.Informal.Basic /-! ## Informal definitions and lemmas -/ -open Lean Elab System +open Lean namespace Informal /-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma` or a `InformalDefinition`. -/ -def isInformal (c : ConstantInfo) : Bool := - match c with - | ConstantInfo.defnInfo c => - if c.type.isAppOf ``InformalDefinition ∨ c.type.isAppOf ``InformalLemma then true else false +def isInformal : ConstantInfo → Bool + | .defnInfo c => c.type.isConstOf ``InformalDefinition ∨ c.type.isConstOf ``InformalLemma | _ => false /-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma`. -/ -def isInformalLemma (c : ConstantInfo) : Bool := - match c with - | ConstantInfo.defnInfo c => - if c.type.isAppOf ``InformalLemma then true else false +def isInformalLemma : ConstantInfo → Bool + | .defnInfo c => c.type.isConstOf ``InformalLemma | _ => false /-- Is true if and only if a `ConstantInfo` corresponds to an `InformalDefinition`. -/ -def isInformalDef (c : ConstantInfo) : Bool := - match c with - | ConstantInfo.defnInfo c => - if c.type.isAppOf ``InformalDefinition then true else false +def isInformalDef : ConstantInfo → Bool + | .defnInfo c => c.type.isConstOf ``InformalDefinition | _ => false /-- Takes a `ConstantInfo` corresponding to a `InformalLemma` and returns the corresponding `InformalLemma`. -/ -unsafe def constantInfoToInformalLemma (c : ConstantInfo) : MetaM InformalLemma := do +unsafe def constantInfoToInformalLemma (c : ConstantInfo) : CoreM InformalLemma := do match c with - | ConstantInfo.defnInfo c => - Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value + | .defnInfo c => evalConstCheck InformalLemma ``InformalLemma c.name | _ => panic! "Passed constantInfoToInformalLemma a `ConstantInfo` that is not a `InformalLemma`" /-- Takes a `ConstantInfo` corresponding to a `InformalDefinition` and returns the corresponding `InformalDefinition`. -/ -unsafe def constantInfoToInformalDefinition (c : ConstantInfo) : MetaM InformalDefinition := do +unsafe def constantInfoToInformalDefinition (c : ConstantInfo) : CoreM InformalDefinition := do match c with - | ConstantInfo.defnInfo c => - Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value - | _ => panic! "Passed constantInfoToInformalDefinition a - `ConstantInfo` that is not a `InformalDefinition`" + | .defnInfo c => evalConstCheck InformalDefinition ``InformalDefinition c.name + | _ => panic! + "Passed constantInfoToInformalDefinition a `ConstantInfo` that is not a `InformalDefinition`" end Informal namespace HepLean /-- The number of informal lemmas in HepLean. -/ -def noInformalLemmas : MetaM Nat := do +def noInformalLemmas : CoreM Nat := do let imports ← allImports let x ← imports.mapM Imports.getUserConsts - let x := x.flatten - let x := x.filter (Informal.isInformal) - let x := x.filter (Informal.isInformalLemma) - pure x.toList.length + x.flatFilterSizeM fun c => return Informal.isInformalLemma c /-- The number of informal definitions in HepLean. -/ -def noInformalDefs : MetaM Nat := do +def noInformalDefs : CoreM Nat := do let imports ← allImports let x ← imports.mapM Imports.getUserConsts - let x := x.flatten - let x := x.filter (Informal.isInformal) - let x := x.filter (Informal.isInformalDef) - pure x.toList.length + x.flatFilterSizeM fun c => return Informal.isInformalDef c end HepLean diff --git a/HepLean/Meta/Notes/Basic.lean b/HepLean/Meta/Notes/Basic.lean index 3626475..321a86d 100644 --- a/HepLean/Meta/Notes/Basic.lean +++ b/HepLean/Meta/Notes/Basic.lean @@ -3,10 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Batteries.Lean.HashSet import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.CoreM -import ImportGraph.RequiredModules /-! ## Underlying structure for notes @@ -24,7 +21,7 @@ Other results relating to notes are in other files. -/ namespace HepLean -open Lean System Meta +open Lean /-- The information from a `note ...` command. To be used in a note file-/ structure NoteInfo where diff --git a/HepLean/Meta/Notes/HTMLNote.lean b/HepLean/Meta/Notes/HTMLNote.lean index 807e9e0..3f08699 100644 --- a/HepLean/Meta/Notes/HTMLNote.lean +++ b/HepLean/Meta/Notes/HTMLNote.lean @@ -3,8 +3,9 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import HepLean.Meta.Notes.NoteFile +-- import DocGen4.Output.DocString import HepLean.Meta.Informal.Post +import HepLean.Meta.Notes.NoteFile /-! ## Turns a delaration into a html note structure. @@ -12,7 +13,7 @@ import HepLean.Meta.Informal.Post -/ namespace HepLean -open Lean System Meta +open Lean /-- A `HTMLNote` is a structure containing the html information from individual contributions (commands, informal commands, note ..) etc. to a note file. -/ @@ -25,47 +26,52 @@ structure HTMLNote where line : Nat /-- Converts a note infor into a HTMLNote. -/ -def HTMLNote.ofNodeInfo (ni : NoteInfo) : MetaM HTMLNote := do - let line := ni.line - let decl := ni.content - let fileName := ni.fileName - pure { content := decl, fileName := fileName, line := line } +def HTMLNote.ofNodeInfo (ni : NoteInfo) : HTMLNote := + { ni with } /-- An formal definition or lemma to html for a note. -/ -def HTMLNote.ofFormal (name : Name) : MetaM HTMLNote := do - let line ← Name.lineNumber name - let decl ← Name.getDeclString name - let fileName ← Name.fileName name - let webAddress : String ← Name.toGitHubLink fileName line - let content := - "
" - ++ "View/Improve" - ++"
"
-    ++ decl ++
-    "
" - pure { content := content, fileName := fileName, line := line } +def HTMLNote.ofFormal (name : Name) : CoreM HTMLNote := do + let line ← name.lineNumber + let fileName ← name.fileName + return { + fileName, line, + content := s!" +
+ View/Improve + 
{← name.getDeclString}
+
" + } /-- An informal definition or lemma to html for a note. -/ -unsafe def HTMLNote.ofInformal (name : Name) : MetaM HTMLNote := do - let line ← Name.lineNumber name - let fileName ← Name.fileName name - let constInfo ← getConstInfo name - let webAddress : String ← Name.toGitHubLink fileName line +unsafe def HTMLNote.ofInformal (name : Name) : CoreM HTMLNote := do + let line ← name.lineNumber + let fileName ← name.fileName + let constInfo ← getConstInfoDefn name + let webAddress := fileName.toGitHubLink line let mut content := "" - if Informal.isInformalDef constInfo then - let X ← Informal.constantInfoToInformalDefinition constInfo - content := "
" - ++ "Improve/Formalize" - ++"Informal definition: " ++ name.toString ++ "
" - ++ X.math.replace "\n" "
" - ++ "
" - else if Informal.isInformalLemma constInfo then - let X ← Informal.constantInfoToInformalLemma constInfo - content := "
" - ++ "Improve/Formalize" - ++"Informal lemma: " ++ name.toString ++ "
" - ++ X.math.replace "\n" "
" - ++ "
" - pure { content := content, fileName := fileName, line := line } + if constInfo.type.isConstOf ``InformalDefinition then + let doc ← name.getDocString + -- let html ← DocGen4.Output.docStringToHtml doc name.toString + -- let X ← Informal.constantInfoToInformalDefinition constInfo + -- let fragment := X.math.replace "\n" "
" + let fragment := doc.replace "\n" "
" + content := s!" +
+ Improve/Formalize + Informal definition: {name}
+ {fragment} +
" + else if constInfo.type.isConstOf ``InformalLemma then + -- let X ← Informal.constantInfoToInformalLemma constInfo + -- let fragment := X.math.replace "\n" "
" + let doc ← name.getDocString + let fragment := doc.replace "\n" "
" + content := s!" +
+ Improve/Formalize + Informal lemma: {name}
+ {fragment} +
" + return { content, fileName, line } end HepLean diff --git a/HepLean/Meta/Notes/NoteFile.lean b/HepLean/Meta/Notes/NoteFile.lean index 511108c..3b275f1 100644 --- a/HepLean/Meta/Notes/NoteFile.lean +++ b/HepLean/Meta/Notes/NoteFile.lean @@ -13,7 +13,7 @@ A note file is a structure which contains the information to go into a note. -/ namespace HepLean -open Lean System Meta +open Lean /-- A note consists of a title and a list of Lean files which make up the note. -/ structure NoteFile where diff --git a/HepLean/Meta/Notes/ToHTML.lean b/HepLean/Meta/Notes/ToHTML.lean index c64b3c9..e88d7c7 100644 --- a/HepLean/Meta/Notes/ToHTML.lean +++ b/HepLean/Meta/Notes/ToHTML.lean @@ -24,12 +24,12 @@ def sortLE (ni1 ni2 : HTMLNote) : Bool := ni1.line ≤ ni2.line /-- Returns a sorted list of NodeInfos for a file system. -/ -unsafe def getNodeInfo : MetaM (List HTMLNote) := do +unsafe def getNodeInfo : CoreM (List HTMLNote) := do let env ← getEnv let allNotes := (noteExtension.getState env) let allDecl := (noteDeclExtension.getState env) let allInformalDecl := noteInformalDeclExtension.getState env - let allNoteInfo := (← allNotes.mapM HTMLNote.ofNodeInfo) ++ (← allDecl.mapM HTMLNote.ofFormal) + let allNoteInfo := allNotes.map HTMLNote.ofNodeInfo ++ (← allDecl.mapM HTMLNote.ofFormal) ++ (← allInformalDecl.mapM HTMLNote.ofInformal) let noteInfo := allNoteInfo.filter (fun x => x.fileName ∈ N.files) let noteInfoSort := noteInfo.toList.mergeSort N.sortLE diff --git a/HepLean/Meta/Remark/Basic.lean b/HepLean/Meta/Remark/Basic.lean index 56b193b..22199b3 100644 --- a/HepLean/Meta/Remark/Basic.lean +++ b/HepLean/Meta/Remark/Basic.lean @@ -3,17 +3,14 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Batteries.Lean.HashSet -import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.CoreM -import ImportGraph.RequiredModules +import Lean.Elab.Command /-! ## Underlying structure for remarks -/ namespace HepLean -open Lean System Meta +open Lean /-- The information from a `remark ...` command. To be used in a note file-/ structure RemarkInfo where @@ -41,7 +38,7 @@ syntax (name := remark_syntax) "remark " ident ":=" str : command /-- Elaborator for the `note ...` command -/ @[command_elab remark_syntax] -def elabRemark : Lean.Elab.Command.CommandElab := fun stx => +def elabRemark : Elab.Command.CommandElab := fun stx => match stx with | `(remark $n := $s) => do let str : String := s.getString diff --git a/HepLean/Meta/Remark/Properties.lean b/HepLean/Meta/Remark/Properties.lean index 0ab3d11..374d24f 100644 --- a/HepLean/Meta/Remark/Properties.lean +++ b/HepLean/Meta/Remark/Properties.lean @@ -10,35 +10,32 @@ import HepLean.Meta.Remark.Basic -/ namespace HepLean -open Lean System Meta +open Lean +variable {m} [Monad m] [MonadEnv m] [MonadError m] /-- All remarks in the enviroment. -/ -def Name.allRemarkInfo : MetaM (List RemarkInfo) := do +def allRemarkInfo : m (Array RemarkInfo) := do let env ← getEnv - let allRemarks := (remarkExtension.getState env) - pure allRemarks.toList + return remarkExtension.getState env /-- The full name of a remark (name and namespace). -/ def RemarkInfo.toFullName (r : RemarkInfo) : Name := if r.nameSpace != .anonymous then - (r.nameSpace.toString ++ "." ++ r.name.toString).toName + .str r.nameSpace r.name.toString else r.name /-- A Bool which is true if a name correponds to a remark. -/ -def RemarkInfo.IsRemark (n : Name) : MetaM Bool := do - let allRemarks ← Name.allRemarkInfo - let r := allRemarks.find? (fun r => r.toFullName = n) - match r with - | some _ => pure true - | none => pure false +def RemarkInfo.IsRemark (n : Name) : m Bool := do + let allRemarks ← allRemarkInfo + let r := allRemarks.find? fun r => r.toFullName == n + return r.isSome /-- Gets the remarkInfo from a name corresponding to a remark.. -/ -def RemarkInfo.getRemarkInfo (n : Name) : MetaM RemarkInfo := do - let allRemarks ← Name.allRemarkInfo - let r := allRemarks.find? (fun r => r.toFullName = n) - match r with - | some r => pure r +def RemarkInfo.getRemarkInfo (n : Name) : m RemarkInfo := do + let allRemarks ← allRemarkInfo + match allRemarks.find? fun r => r.toFullName == n with + | some r => return r | none => throwError s!"No remark named {n}" end HepLean diff --git a/HepLean/Meta/TODO/Basic.lean b/HepLean/Meta/TODO/Basic.lean index 6718270..d393293 100644 --- a/HepLean/Meta/TODO/Basic.lean +++ b/HepLean/Meta/TODO/Basic.lean @@ -3,10 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Batteries.Lean.HashSet -import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.CoreM -import ImportGraph.RequiredModules +import Lean.Elab.Command /-! # Basic underlying structure for TODOs. @@ -14,7 +11,7 @@ import ImportGraph.RequiredModules -/ namespace HepLean -open Lean System Meta +open Lean /-- The information from a `TODO ...` command. -/ structure todoInfo where @@ -38,7 +35,7 @@ syntax (name := todo_comment) "TODO " str : command /-- Elaborator for the `TODO ...` command -/ @[command_elab todo_comment] -def elabTODO : Lean.Elab.Command.CommandElab := fun stx => +def elabTODO : Elab.Command.CommandElab := fun stx => match stx with | `(TODO $s) => do let str : String := s.getString diff --git a/HepLean/StandardModel/Basic.lean b/HepLean/StandardModel/Basic.lean index 4be77b6..8951e88 100644 --- a/HepLean/StandardModel/Basic.lean +++ b/HepLean/StandardModel/Basic.lean @@ -26,45 +26,56 @@ open ComplexConjugate abbrev GaugeGroupI : Type := specialUnitaryGroup (Fin 3) ℂ × specialUnitaryGroup (Fin 2) ℂ × unitary ℂ +/-- The subgroup of the un-quotiented gauge group which acts trivially on all particles in the +standard model, i.e., the ℤ₆-subgroup of `GaugeGroupI` with elements `(α^2 * I₃, α^(-3) * I₂, α)`, +where `α` is a sixth complex root of unity. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition gaugeGroupℤ₆SubGroup where - physics :≈ "The subgroup of the un-quotiented gauge group which acts trivially on - all particles in the standard model. " - math :≈ "The ℤ₆-subgroup of ``GaugeGroupI with elements (α^2 * I₃, α^(-3) * I₂, α), where `α` - is a sixth complex root of unity." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI] + deps := [``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 - physics :≈ "The smallest possible gauge group of the Standard Model." - math :≈ "The quotient of ``GaugeGroupI by the ℤ₆-subgroup `gaugeGroupℤ₆SubGroup`." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup] + deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup] +/-- 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 +`gaugeGroupℤ₆SubGroup`. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition gaugeGroupℤ₂SubGroup where - physics :≈ "The ℤ₂subgroup of the un-quotiented gauge group which acts trivially on - all particles in the standard model. " - math :≈ "The ℤ₂-subgroup of ``GaugeGroupI derived from the ℤ₂ subgroup of `gaugeGroupℤ₆SubGroup`." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup] + deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup] +/-- The guage group of the Standard Model with a ℤ₂ quotient, i.e., the quotient of `GaugeGroupI` by +the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition GaugeGroupℤ₂ where - physics :≈ "The guage group of the Standard Model with a ℤ₂ quotient." - math :≈ "The quotient of ``GaugeGroupI by the ℤ₂-subgroup `gaugeGroupℤ₂SubGroup`." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₂SubGroup] + deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₂SubGroup] +/-- 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 +`gaugeGroupℤ₆SubGroup`. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition gaugeGroupℤ₃SubGroup where - physics :≈ "The ℤ₃-subgroup of the un-quotiented gauge group which acts trivially on - all particles in the standard model. " - math :≈ "The ℤ₃-subgroup of ``GaugeGroupI derived from the ℤ₃ subgroup of `gaugeGroupℤ₆SubGroup`." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup] + deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₆SubGroup] +/-- The guage group of the Standard Model with a ℤ₃-quotient, i.e., the quotient of `GaugeGroupI` by +the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition GaugeGroupℤ₃ where - physics :≈ "The guage group of the Standard Model with a ℤ₃-quotient." - math :≈ "The quotient of ``GaugeGroupI by the ℤ₃-subgroup `gaugeGroupℤ₃SubGroup`." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₃SubGroup] + deps := [``GaugeGroupI, ``StandardModel.gaugeGroupℤ₃SubGroup] /-- Specifies the allowed quotients of `SU(3) x SU(2) x U(1)` which give a valid gauge group of the Standard Model. -/ @@ -81,12 +92,14 @@ inductive GaugeGroupQuot : Type /-- The element of `GaugeGroupQuot` corresponding to the full SM gauge group. -/ | I : GaugeGroupQuot +/-- The (global) gauge group of the Standard Model given a choice of quotient, i.e., the map from +`GaugeGroupQuot` to `Type` which gives the gauge group of the Standard Model for a given choice of +quotient. + +See https://math.ucr.edu/home/baez/guts.pdf +-/ informal_definition GaugeGroup where - physics :≈ "The (global) gauge group of the Standard Model given a choice of quotient." - math :≈ "The map from `GaugeGroupQuot` to `Type` which gives the gauge group of the Standard Model - for a given choice of quotient." - ref :≈ "https://math.ucr.edu/home/baez/guts.pdf" - deps :≈ [``GaugeGroupI, ``gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup, ``gaugeGroupℤ₃SubGroup, + deps := [``GaugeGroupI, ``gaugeGroupℤ₆SubGroup, ``gaugeGroupℤ₂SubGroup, ``gaugeGroupℤ₃SubGroup, ``GaugeGroupQuot] /-! @@ -95,20 +108,20 @@ informal_definition GaugeGroup where -/ +/-- The gauge group `GaugeGroupI` is a Lie group. -/ informal_lemma gaugeGroupI_lie where - math :≈ "The gauge group `GaugeGroupI` is a Lie group.." - deps :≈ [``GaugeGroupI] + deps := [``GaugeGroupI] +/-- For every `q` in `GaugeGroupQuot` the group `GaugeGroup q` is a Lie group. -/ informal_lemma gaugeGroup_lie where - math :≈ "For every q in ``GaugeGroupQuot the group ``GaugeGroup q is a Lie group." - deps :≈ [``GaugeGroup] + deps := [``GaugeGroup] +/-- The trivial principal bundle over SpaceTime with structure group `GaugeGroupI`. -/ informal_definition gaugeBundleI where - math :≈ "The trivial principal bundle over SpaceTime with structure group ``GaugeGroupI." - deps :≈ [``GaugeGroupI, ``SpaceTime] + deps := [``GaugeGroupI, ``SpaceTime] +/-- A global section of `gaugeBundleI`. -/ informal_definition gaugeTransformI where - math :≈ "A global section of ``gaugeBundleI." - deps :≈ [``gaugeBundleI] + deps := [``gaugeBundleI] end StandardModel diff --git a/HepLean/StandardModel/HiggsBoson/Basic.lean b/HepLean/StandardModel/HiggsBoson/Basic.lean index 29bb3b2..872ad50 100644 --- a/HepLean/StandardModel/HiggsBoson/Basic.lean +++ b/HepLean/StandardModel/HiggsBoson/Basic.lean @@ -171,11 +171,11 @@ def ofReal (a : ℝ) : HiggsField := (HiggsVec.ofReal a).toField /-- The higgs field which is all zero. -/ def zero : HiggsField := ofReal 0 +/-- The zero Higgs field is the zero section of the Higgs bundle, i.e., the HiggsField `zero` +defined by `ofReal 0` is the constant zero-section of the bundle `HiggsBundle`. +-/ informal_lemma zero_is_zero_section where - physics :≈ "The zero Higgs field is the zero section of the Higgs bundle." - math :≈ "The HiggsField `zero` defined by `ofReal 0` - is the constant zero-section of the bundle `HiggsBundle`." - deps :≈ [`StandardModel.HiggsField.zero] + deps := [`StandardModel.HiggsField.zero] end HiggsField diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean index 09da58e..7afa652 100644 --- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean +++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean @@ -215,25 +215,24 @@ theorem rotate_fst_real_snd_zero (φ : HiggsVec) : · simp only [Fin.mk_one, Fin.isValue, Pi.smul_apply, Function.comp_apply, cons_val_one, head_cons, tail_cons, smul_zero] +/-- There exists a `g` in `GaugeGroupI` such that `rep g φ = φ'` iff `‖φ‖ = ‖φ'‖`. -/ informal_lemma guage_orbit where - math :≈ "There exists a `g` in ``GaugeGroupI such that `rep g φ = φ'` if and only if - ‖φ‖ = ‖φ'‖." - deps :≈ [``rotate_fst_zero_snd_real] + deps := [``rotate_fst_zero_snd_real] +/-- The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the +stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the +`SU(3) × U(1)` subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` with the embedding given by +`(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`. +-/ informal_lemma stability_group_single where - physics :≈ "The Higgs boson breaks electroweak symmetry down to the electromagnetic force." - math :≈ "The stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, - for non-zero `‖φ‖` is the `SU(3) x U(1)` subgroup of - `gaugeGroup := SU(3) x SU(2) x U(1)` with the embedding given by - `(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`." - deps :≈ [``StandardModel.HiggsVec, ``StandardModel.HiggsVec.rep] + deps := [``StandardModel.HiggsVec, ``StandardModel.HiggsVec.rep] +/-- The subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` which preserves every `HiggsVec` by the +action of `StandardModel.HiggsVec.rep` is given by `SU(3) × ℤ₆` where `ℤ₆` is the subgroup of +`SU(2) × U(1)` with elements `(α^(-3) * I₂, α)` where `α` is a sixth root of unity. +-/ informal_lemma stability_group where - math :≈ "The subgroup of `gaugeGroup := SU(3) x SU(2) x U(1)` which preserves every `HiggsVec` - by the action of ``StandardModel.HiggsVec.rep is given by `SU(3) x ℤ₆` where ℤ₆ - is the subgroup of `SU(2) x U(1)` with elements `(α^(-3) * I₂, α)` where - α is a sixth root of unity." - deps :≈ [``HiggsVec, ``rep] + deps := [``HiggsVec, ``rep] end HiggsVec @@ -249,20 +248,21 @@ namespace HiggsField -/ +/-- The action of `gaugeTransformI` on `HiggsField` acting pointwise through `HiggsVec.rep`. -/ informal_definition gaugeAction where - math :≈ "The action of ``gaugeTransformI on ``HiggsField acting pointwise through - ``HiggsVec.rep." - deps :≈ [``HiggsVec.rep, ``gaugeTransformI] + deps := [``HiggsVec.rep, ``gaugeTransformI] +/-- There exists a `g` in `gaugeTransformI` such that `gaugeAction g φ = φ'` iff +`φ(x)^† φ(x) = φ'(x)^† φ'(x)`. +-/ informal_lemma guage_orbit where - math :≈ "There exists a `g` in ``gaugeTransformI such that `gaugeAction g φ = φ'` if and only if - φ(x)^† φ(x) = φ'(x)^† φ'(x)." - deps :≈ [``gaugeAction] + deps := [``gaugeAction] +/-- For every smooth map `f` from `SpaceTime` to `ℝ` such that `f` is positive semidefinite, there +exists a Higgs field `φ` such that `f = φ^† φ`. +-/ informal_lemma gauge_orbit_surject where - math :≈ "For every smooth map f from ``SpaceTime to ℝ such that `f` is positive semidefinite, - there exists a Higgs field φ such that `f = φ^† φ`." - deps :≈ [``HiggsField, ``SpaceTime] + deps := [``HiggsField, ``SpaceTime] end HiggsField diff --git a/HepLean/StandardModel/HiggsBoson/Potential.lean b/HepLean/StandardModel/HiggsBoson/Potential.lean index 96764af..ef4e3fc 100644 --- a/HepLean/StandardModel/HiggsBoson/Potential.lean +++ b/HepLean/StandardModel/HiggsBoson/Potential.lean @@ -323,12 +323,12 @@ lemma isBounded_of_𝓵_pos (h : 0 < P.𝓵) : P.IsBounded := by have h2' := h2 φ x linarith +/-- When there is no quartic coupling, the potential is bounded iff the mass squared is +non-positive, i.e., for `P : Potential` then `P.IsBounded` iff `P.μ2 ≤ 0`. That is to say +`- P.μ2 * ‖φ‖_H^2 x` is bounded below ifff `P.μ2 ≤ 0`.-/ informal_lemma isBounded_iff_of_𝓵_zero where - physics :≈ "When there is no quartic coupling, the potential is bounded iff the mass squared is - non-positive." - math :≈ "For `P : Potential` then P.IsBounded if and only if P.μ2 ≤ 0. - That is to say `- P.μ2 * ‖φ‖_H^2 x` is bounded below if and only if `P.μ2 ≤ 0`." - deps :≈ [`StandardModel.HiggsField.Potential.IsBounded, `StandardModel.HiggsField.Potential] + deps := [`StandardModel.HiggsField.Potential.IsBounded, `StandardModel.HiggsField.Potential] + /-! ## Minimum and maximum diff --git a/HepLean/Tensors/OverColor/Lift.lean b/HepLean/Tensors/OverColor/Lift.lean index 0c2488e..0c1e121 100644 --- a/HepLean/Tensors/OverColor/Lift.lean +++ b/HepLean/Tensors/OverColor/Lift.lean @@ -895,10 +895,11 @@ lemma forgetLiftAppCon_naturality_eqToHom_apply (c c1 : C) (h : c = c1) rw [forgetLiftAppCon_naturality_eqToHom] rfl +/-- The natural isomorphism between `lift (C := C) ⋙ forget` and +`Functor.id (Discrete C ⥤ Rep k G)`. +-/ informal_definition forgetLift where - math :≈ "The natural isomorphism between `lift (C := C) ⋙ forget` and - `Functor.id (Discrete C ⥤ Rep k G)`." - deps :≈ [``forget, ``lift] + deps := [``forget, ``lift] end end OverColor diff --git a/HepLean/Tensors/TensorSpecies/Contractions/Basic.lean b/HepLean/Tensors/TensorSpecies/Contractions/Basic.lean index 7d507bf..8016ba1 100644 --- a/HepLean/Tensors/TensorSpecies/Contractions/Basic.lean +++ b/HepLean/Tensors/TensorSpecies/Contractions/Basic.lean @@ -48,17 +48,19 @@ lemma contractSelfField_equivariant {S : TensorSpecies} {c : S.C} {g : S.G} simpa using congrFun (congrArg (fun x => x.hom.toFun) ((S.contractSelfHom c).comm g)) (ψ ⊗ₜ[S.k] φ) -informal_lemma contractSelfField_non_degenerate where - math :≈ "The contraction of two vectors of the same color is non-degenerate. - I.e. ⟪ψ, φ⟫ₜₛ = 0 for all φ implies ψ = 0." - proof :≈ "The basic idea is that being degenerate contradicts the assumption of having a unit - in the tensor species." - deps :≈ [``contractSelfField] +/-- The contraction of two vectors of the same color is non-degenerate, i.e., `⟪ψ, φ⟫ₜₛ = 0` for all +`φ` implies `ψ = 0`. +Proof: the basic idea is that being degenerate contradicts the assumption of having a +unit in the tensor species. +-/ +informal_lemma contractSelfField_non_degenerate where + deps := [``contractSelfField] + +/-- The contraction `⟪ψ, φ⟫ₜₛ` is related to the tensor tree +`{ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ`. -/ informal_lemma contractSelfField_tensorTree where - math :≈ "The contraction ⟪ψ, φ⟫ₜₛ is related to the tensor tree - {ψ | μ ⊗ (S.dualRepIsoDiscrete c).hom φ | μ}ᵀ " - deps :≈ [``contractSelfField, ``TensorTree] + deps := [``contractSelfField, ``TensorTree] /-! diff --git a/HepLean/Tensors/TensorSpecies/DualRepIso.lean b/HepLean/Tensors/TensorSpecies/DualRepIso.lean index 47a85ef..78595f9 100644 --- a/HepLean/Tensors/TensorSpecies/DualRepIso.lean +++ b/HepLean/Tensors/TensorSpecies/DualRepIso.lean @@ -241,27 +241,28 @@ def dualRepIsoDiscrete (c : S.C) : S.FD.obj (Discrete.mk c) ≅ S.FD.obj (Discre ext x exact S.fromDualRep_toDualRep_eq_self c x +/-- Given a `i : Fin n` the isomorphism between `S.F.obj (OverColor.mk c)` and +`S.F.obj (OverColor.mk (Function.update c i (S.τ (c i))))` induced by `dualRepIsoDiscrete` acting on +the `i`-th component of the color. +-/ informal_definition dualRepIso where - math :≈ "Given a `i : Fin n` the isomorphism between `S.F.obj (OverColor.mk c)` and - `S.F.obj (OverColor.mk (Function.update c i (S.τ (c i))))` induced by `dualRepIsoDiscrete` - acting on the `i`-th component of the color." - deps :≈ [``dualRepIsoDiscrete] + deps := [``dualRepIsoDiscrete] +/-- Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric. -/ informal_lemma dualRepIso_unitTensor_fst where - math :≈ "Acting with `dualRepIso` on the fst component of a `unitTensor` returns a metric." - deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor] + deps := [``dualRepIso, ``unitTensor, ``metricTensor] +/-- Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric. -/ informal_lemma dualRepIso_unitTensor_snd where - math :≈ "Acting with `dualRepIso` on the snd component of a `unitTensor` returns a metric." - deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor] + deps := [``dualRepIso, ``unitTensor, ``metricTensor] +/-- Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor. -/ informal_lemma dualRepIso_metricTensor_fst where - math :≈ "Acting with `dualRepIso` on the fst component of a `metricTensor` returns a unitTensor." - deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor] + deps := [``dualRepIso, ``unitTensor, ``metricTensor] +/-- Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor. -/ informal_lemma dualRepIso_metricTensor_snd where - math :≈ "Acting with `dualRepIso` on the snd component of a `metricTensor` returns a unitTensor." - deps :≈ [``dualRepIso, ``unitTensor, ``metricTensor] + deps := [``dualRepIso, ``unitTensor, ``metricTensor] end TensorSpecies diff --git a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean index 0dad90d..e1dc129 100644 --- a/HepLean/Tensors/Tree/NodeIdentities/Basic.lean +++ b/HepLean/Tensors/Tree/NodeIdentities/Basic.lean @@ -30,13 +30,13 @@ variable {S : TensorSpecies} -/ +/-- A `constVecNode` has equal tensor to the `vecNode` with the map evaluated at 1. -/ informal_lemma constVecNode_eq_vecNode where - math :≈ "A constVecNode has equal tensor to the vecNode with the map evaluated at 1." - deps :≈ [``constVecNode, ``vecNode] + deps := [``constVecNode, ``vecNode] +/-- A `constTwoNode` has equal tensor to the `twoNode` with the map evaluated at 1. -/ informal_lemma constTwoNode_eq_twoNode where - math :≈ "A constTwoNode has equal tensor to the twoNode with the map evaluated at 1." - deps :≈ [``constTwoNode, ``twoNode] + deps := [``constTwoNode, ``twoNode] /-! diff --git a/scripts/MetaPrograms/informal.lean b/scripts/MetaPrograms/informal.lean index 1939326..8ce0d67 100644 --- a/scripts/MetaPrograms/informal.lean +++ b/scripts/MetaPrograms/informal.lean @@ -3,12 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Batteries.Lean.HashSet -import Lean -import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.CoreM import HepLean.Meta.Informal.Post -import ImportGraph.RequiredModules +import Mathlib.Lean.CoreM /-! # Extracting information about informal definitions and lemmas @@ -19,125 +15,101 @@ To make the dot file for the dependency graph run: - or dot -Tpng -Gdpi=300 -o ./Docs/graph.png ./Docs/InformalDot.dot -/ -open Lean System Meta +open Lean -def getConst (imp : Import) : IO (Array (Import × ConstantInfo)) := do - let mFile ← findOLean imp.module - let (modData, _) ← readModuleData mFile - pure (modData.constants.map (fun c => (imp, c))) +/- To make private definitions completely invisible, place them in a separate importable file. -/ -def getLineNumber (c : Name) : MetaM Nat := do - match ← findDeclarationRanges? c with - | some decl => pure decl.range.pos.line - | none => panic! s!"{c} is a declaration without position" +structure Decl where + name : Name + module : Name + lineNo : Nat + docString : String -def getModule (c : Name) : MetaM Name := do - match Lean.Environment.getModuleFor? (← getEnv) c with - | some mod => pure mod - | none => panic! s!"{c} is a declaration without position" +inductive InformalDeclKind + | def | lemma -def getConstInfo (n : Name) : MetaM ConstantInfo := do - match (← getEnv).find? n with - | some c => pure c - | none => panic! s!"{n} is not a constant" +instance : ToString InformalDeclKind where + toString + | .def => "def" + | .lemma => "lemma" -/-- Gets the docstring from a name, if it exists, otherwise the string "No docstring."-/ -def getDocString (n : Name) : MetaM String := do - match ← Lean.findDocString? (← getEnv) n with - | some doc => pure doc - | none => pure "No docstring." +structure InformalDecl extends Decl where + kind : InformalDeclKind + deps : Array Decl -def depToString (d : Name) : MetaM String := do - let lineNo ← getLineNumber d - let mod ← getModule d - pure s!" * {d}: ./{mod.toString.replace "." "/" ++ ".lean"}:{lineNo}" +structure DepDecls where + private mk:: + private decls : Std.HashMap Name Decl + formalDecls : Array Decl + /-- Pairs of informal declarations and their enclosing modules. -/ + informalModuleMap : Array (Name × Array InformalDecl) -def depToWebString (d : Name) : MetaM String := do - let lineNo ← getLineNumber d - let mod ← getModule d - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (mod.toString.replace "." "/") ++ ".lean" - pure s!" * [{d}]({webPath}#L{lineNo})" +private abbrev DeclsM := StateRefT (Std.HashMap Name Decl) CoreM -unsafe def informalDependencies (c : ConstantInfo) : MetaM (Array Name) := do - if Informal.isInformalLemma c then - let informal ← Informal.constantInfoToInformalLemma c - pure informal.dependencies.toArray - else if Informal.isInformalDef c then - let informal ← Informal.constantInfoToInformalDefinition c - pure informal.dependencies.toArray - else - pure #[] +private def Decl.ofName (name : Name) (module : Option Name := none) : DeclsM Decl := do + if let some decl := (← get).get? name then + return decl + let env ← getEnv + let decl : Decl := { + name + module := module.getD (env.getModuleFor? name).get! + lineNo := (← findDeclarationRanges? name).get!.range.pos.line + docString := (← findDocString? env name).getD "No docstring." + } + modifyGet fun decls => (decl, decls.insert name decl) -unsafe def informalLemmaToString (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let informalLemma ← Informal.constantInfoToInformalLemma c.2 - let dep ← informalLemma.dependencies.mapM fun d => depToString d - pure s!" -Informal lemma: {informalLemma.name} -- ./{c.1.module.toString.replace "." "/" ++ ".lean"}:{lineNo} -- Math description: {informalLemma.math} -- Physics description: {informalLemma.physics} -- Proof description: {informalLemma.proof} -- References: {informalLemma.ref} -- Dependencies:\n{String.intercalate "\n" dep}" +private unsafe def InformalDecl.ofName? (name module : Name) : DeclsM (Option InformalDecl) := do + unless name.isInternalDetail do + if let some const := (← getEnv).find? name then + if Informal.isInformalDef const then + return ← ofName .def (← evalConst InformalDefinition name).deps + else if Informal.isInformalLemma const then + return ← ofName .lemma (← evalConst InformalLemma name).deps + return none +where + ofName (kind : InformalDeclKind) (deps : List Name) : DeclsM InformalDecl := + return {← Decl.ofName name module with kind, deps := ← deps.toArray.mapM Decl.ofName} -unsafe def informalLemmaToWebString (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let informalLemma ← Informal.constantInfoToInformalLemma c.2 - let dep ← informalLemma.dependencies.mapM fun d => depToWebString d - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (c.1.module.toString.replace "." "/") ++ ".lean" - pure s!" -**Informal lemma**: [{informalLemma.name}]({webPath}#L{lineNo}) := - *{informalLemma.math}* -- Physics description: {informalLemma.physics} -- Proof description: {informalLemma.proof} -- References: {informalLemma.ref} -- Dependencies:\n{String.intercalate "\n" dep}" +unsafe def DepDecls.ofRootModule (rootModule : Name) : CoreM DepDecls := do + let (informalModuleMap, decls) ← getAllDecls.run ∅ -unsafe def informalDefToString (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let informalDef ← Informal.constantInfoToInformalDefinition c.2 - let dep ← informalDef.dependencies.mapM fun d => depToString d - pure s!" -Informal def: {informalDef.name} -- ./{c.1.module.toString.replace "." "/" ++ ".lean"}:{lineNo} -- Math description: {informalDef.math} -- Physics description: {informalDef.physics} -- References: {informalDef.ref} -- Dependencies:\n{String.intercalate "\n" dep}" + let mut informalNames : Std.HashSet Name := ∅ + for (_, informalDecls) in informalModuleMap do + for {name, ..} in informalDecls do + informalNames := informalNames.insert name -unsafe def informalDefToWebString (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let informalDef ← Informal.constantInfoToInformalDefinition c.2 - let dep ← informalDef.dependencies.mapM fun d => depToWebString d - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (c.1.module.toString.replace "." "/") ++ ".lean" - pure s!" -**Informal def**: [{informalDef.name}]({webPath}#L{lineNo}) := - *{informalDef.math}* -- Physics description: {informalDef.physics} -- References: {informalDef.ref} -- Dependencies:\n{String.intercalate "\n" dep}" + let mut formalDecls : Array Decl := #[] + for (name, decl) in decls do + unless informalNames.contains name do + formalDecls := formalDecls.push decl -unsafe def informalToString (c : Import × ConstantInfo) : MetaM String := do - if Informal.isInformalLemma c.2 then - informalLemmaToString c - else if Informal.isInformalDef c.2 then - informalDefToString c - else - pure "" + return {decls, formalDecls, informalModuleMap} +where + getAllDecls : DeclsM (Array (Name × Array InformalDecl)) := do + let ({imports, ..}, _) ← readModuleData (← findOLean rootModule) + imports.filterMapM fun {module, ..} => do + if module.getRoot == rootModule then + let ({constNames, ..}, _) ← readModuleData (← findOLean module) + let informalDecls ← constNames.filterMapM fun name => InformalDecl.ofName? name module + unless informalDecls.isEmpty do + let informalDecls := informalDecls.qsort fun a b => a.lineNo < b.lineNo + printInformalDecls module informalDecls + return (module, informalDecls) + return none + printInformalDecls (module : Name) (informalDecls : Array InformalDecl) : CoreM Unit := do + println! module + for {kind, name, lineNo, docString, deps, ..} in informalDecls do + println! s!" +Informal {kind}: {name} +- {module.toRelativeFilePath}:{lineNo} +- Description: {docString} +- Dependencies:" + for {name, module, lineNo, ..} in deps do + println! s!" * {name}: {module.toRelativeFilePath}:{lineNo}" -unsafe def informalToWebString (c : Import × ConstantInfo) : MetaM String := do - if Informal.isInformalLemma c.2 then - informalLemmaToWebString c - else if Informal.isInformalDef c.2 then - informalDefToWebString c - else - pure "" - -def informalFileHeader : String := s!" +/-- Making the Markdown file for dependency graph. -/ +def mkMarkdown (depDecls : DepDecls) : IO Unit := do + println! " # Informal definitions and lemmas See [informal definitions and lemmas as a dependency graph](https://heplean.github.io/HepLean/graph.svg). @@ -151,143 +123,19 @@ There is an implicit invitation to the reader to contribute to the formalization background in Lean. " -open Informal -/-- Takes an import and outputs the list of `ConstantInfo` corresponding - to an informal definition or lemma in that import, sorted by line number. -/ -def importToInformal (i : Import) : MetaM (Array (Import × ConstantInfo)) := do - let constants ← getConst i - let constants := constants.filter (fun c => ¬ Lean.Name.isInternalDetail c.2.name) - let informalConst := constants.filter fun c => Informal.isInformal c.2 - let informalConstLineNo ← informalConst.mapM fun c => getLineNumber c.2.name - let informalConstWithLineNo := informalConst.zip informalConstLineNo - let informalConstWithLineNoSort := informalConstWithLineNo.qsort (fun a b => a.2 < b.2) - return informalConstWithLineNoSort.map (fun c => c.1) + for (module, informalDecls) in depDecls.informalModuleMap do + println! s!"## {module}" + for {kind, name, lineNo, docString, deps, ..} in informalDecls do + println! s!" +**Informal {kind}**: [{name}]({module.toGitHubLink lineNo}) := + *{docString}* +- Dependencies:" + for {name, module, lineNo, ..} in deps do + println! s!" * {name}: {module.toRelativeFilePath}:{lineNo}" -unsafe def importToString (i : Import) : MetaM String := do - let informalConst ← importToInformal i - let informalPrint ← (informalConst.mapM informalToString).run' - if informalPrint.isEmpty then - pure "" - else - pure ("\n\n" ++ i.module.toString ++ "\n" ++ String.intercalate "\n\n" informalPrint.toList) - -unsafe def importToWebString (i : Import) : MetaM String := do - let informalConst ← importToInformal i - let informalPrint ← (informalConst.mapM informalToWebString).run' - if informalPrint.isEmpty then - pure "" - else - pure ("\n\n## " ++ i.module.toString ++ "\n" ++ String.intercalate "\n\n" informalPrint.toList) - -section dotFile -/-! - -## Making the dot file for dependency graph. - --/ - -/-- Turns a formal definition or lemma into a node of a dot graph. -/ -def formalToNode (nameSpaces : Array Name) (d : Name) : MetaM String := do - let lineNo ← getLineNumber d - let mod ← getModule d - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (mod.toString.replace "." "/") ++ ".lean" - let docstring ← getDocString d - let prefixName := if nameSpaces.contains d then d else - d.getPrefix - let nodeStr := s!"\"{d}\"[label=\"{d}\", shape=box, style=filled, fillcolor=steelblue, - tooltip=\"{docstring}\"]" - if prefixName = Lean.Name.anonymous then - pure nodeStr - else - pure ("subgraph cluster_" ++ prefixName.toString.replace "." "_" ++ " { " ++ nodeStr ++ "; }") - -unsafe def informalLemmaToNode (nameSpaces : Array Name) (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (c.1.module.toString.replace "." "/") ++ ".lean" - let informalLemma ← (Informal.constantInfoToInformalLemma c.2) - let prefixName := if nameSpaces.contains c.2.name then c.2.name else - c.2.name.getPrefix - let nodeStr := s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=ellipse, style=filled, fillcolor=lightgray, - tooltip=\"{informalLemma.math}\"]" - if prefixName = Lean.Name.anonymous then - pure nodeStr - else - pure ("subgraph cluster_" ++ prefixName.toString.replace "." "_" ++ " { " ++ nodeStr ++ "; }") - -unsafe def informalDefToNode (nameSpaces : Array Name) (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (c.1.module.toString.replace "." "/") ++ ".lean" - let informalDef ← (constantInfoToInformalDefinition c.2) - let prefixName := if nameSpaces.contains c.2.name then c.2.name else - c.2.name.getPrefix - let nodeStr := s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=box, style=filled, fillcolor=lightgray, - tooltip=\"{informalDef.math}\"]" - if prefixName = Lean.Name.anonymous then - pure nodeStr - else - pure ("subgraph cluster_" ++ prefixName.toString.replace "." "_" ++ " { " ++ nodeStr ++ "; }") - - -unsafe def informalToNode (nameSpaces : Array Name) (c : Import × ConstantInfo) : MetaM String := do - if Informal.isInformalLemma c.2 then - informalLemmaToNode nameSpaces c - else if Informal.isInformalDef c.2 then - informalDefToNode nameSpaces c - else - pure "" - -unsafe def informalLemmaToEdges (c : Import × ConstantInfo) : MetaM (String) := do - let informalLemma ← constantInfoToInformalLemma c.2 - let deps := informalLemma.dependencies - let edge := deps.map (fun d => s!"\"{d}\" -> \"{c.2.name}\"") - pure (String.intercalate "\n" edge) - -unsafe def informalDefToEdges (c : Import × ConstantInfo) : MetaM (String) := do - let informalDef ← constantInfoToInformalDefinition c.2 - let deps := informalDef.dependencies - let edge := deps.map (fun d => s!"\"{d}\" -> \"{c.2.name}\"") - pure (String.intercalate "\n" edge) - -unsafe def informalToEdges (c : Import × ConstantInfo) : MetaM (String) := do - if Informal.isInformalLemma c.2 then - informalLemmaToEdges c - else if Informal.isInformalDef c.2 then - informalDefToEdges c - else - pure "" - -unsafe def namespaceToCluster (name : Name) : MetaM String := do - let nameUnder := name.toString.replace "." "_" - if name = Lean.Name.anonymous then - pure "" - else - pure ("subgraph cluster_" ++ nameUnder ++ " - { - label=\"" ++ name.toString ++ "\"; - color=steelblue; - }") - -unsafe def mkDot (imports : Array Import) : MetaM String := do - let informal ← imports.mapM importToInformal - let informal := informal.flatten - let deps ← (informal.map (fun c => c.2)).mapM informalDependencies - let deps := deps.flatten - let informal_name := informal.map (fun c => c.2.name) - let informalNameSpaces := informal.map fun c => c.2.name.getPrefix - let clusters ← informalNameSpaces.mapM fun c => namespaceToCluster c - let clusters := String.intercalate "\n" clusters.toList.eraseDups - let formal_deps := deps.filter (fun d => d ∉ informal_name) - let formal_nodes ← formal_deps.mapM (formalToNode informalNameSpaces) - let nodes := String.intercalate "\n" formal_nodes.toList - - let informalNodes ← informal.mapM (informalToNode informalNameSpaces) - let informalNodes := String.intercalate "\n" informalNodes.toList - let edges ← informal.mapM informalToEdges - let edges := String.intercalate "\n" edges.toList - let header := "strict digraph G { +/-- Making the DOT file for dependency graph. -/ +def mkDOT (depDecls : DepDecls) : IO Unit := do + IO.println "strict digraph G { graph [ pack=true; packmode=\"array1\"; @@ -298,77 +146,48 @@ unsafe def mkDot (imports : Array Import) : MetaM String := do labelloc=\"t\"; labeljust=\"l\"; edge [arrowhead=vee];" - let footer := "}" - pure (header ++ "\n" ++clusters ++ "\n" ++ nodes ++ "\n" ++ - informalNodes ++ "\n" ++ edges ++ "\n" ++ footer) -end dotFile + let mut clusters : Std.HashSet Name := ∅ + for (_, informalDecls) in depDecls.informalModuleMap do + for {name, ..} in informalDecls do + let cluster := name.getPrefix + unless cluster.isAnonymous do + clusters := clusters.insert cluster + println! s!"subgraph cluster_{cluster.toString.replace "." "_"}" ++ " + { + label=\"" ++ cluster.toString ++ "\"; + color=steelblue; + }" -section htmlFile + for decl in depDecls.formalDecls do + println! toNode clusters decl "box" "steelblue" -/-! + for (_, informalDecls) in depDecls.informalModuleMap do + for {toDecl := decl, kind, ..} in informalDecls do + match kind with + | .def => println! toNode clusters decl "box" "lightgray" + | .lemma => println! toNode clusters decl "ellipse" "lightgray" -## Making the html file for dependency graph. + for (_, informalDecls) in depDecls.informalModuleMap do + for informalDecl in informalDecls do + for dep in informalDecl.deps do + println! s!"\"{dep.name}\" -> \"{informalDecl.name}\"" --/ + println! "}" +where + toNode (clusters : Std.HashSet Name) (decl : Decl) (shape color : String) : String := + let {name, docString, ..} := decl + let prefixName := if clusters.contains name then name else name.getPrefix + let nodeStr := s!"\"{name}\"[label=\"{name}\", shape={shape}, style=filled, fillcolor={color}, + tooltip=\"{docString}\"]" + if prefixName.isAnonymous then + nodeStr + else + s!"subgraph cluster_{prefixName.toString.replace "." "_"} \{ {nodeStr}; }" -def formalToHTML (d : Name) : MetaM String := do - let lineNo ← getLineNumber d - let mod ← getModule d - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (mod.toString.replace "." "/") ++ ".lean" - let docstring ← getDocString d - pure s!" -
-{d}
-Docstring: {docstring} - -
" - -unsafe def informalLemmaToHTML (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (c.1.module.toString.replace "." "/") ++ ".lean" - let informalLemma ← (constantInfoToInformalLemma c.2) - pure s!" -
-{c.2.name}
-Math description: {informalLemma.math}
-Physics description: {informalLemma.physics}
-
" - -unsafe def informalDefToHTML (c : Import × ConstantInfo) : MetaM String := do - let lineNo ← getLineNumber c.2.name - let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++ - (c.1.module.toString.replace "." "/") ++ ".lean" - let informalDef ← (constantInfoToInformalDefinition c.2) - pure s!" -
-{c.2.name}
-Math description: {informalDef.math}
-Physics description: {informalDef.physics}
-
" - -unsafe def informalToHTML (c : Import × ConstantInfo) : MetaM String := do - if Informal.isInformalLemma c.2 then - informalLemmaToHTML c - else if Informal.isInformalDef c.2 then - informalDefToHTML c - else - pure "" - -unsafe def toHTML (imports : Array Import) : MetaM String := do - let informal ← imports.mapM importToInformal - let informal := informal.flatten - let deps ← (informal.map (fun c => c.2)).mapM informalDependencies - let deps := deps.flatten - let informal_name := informal.map (fun c => c.2.name) - let formal_deps := deps.filter (fun d => d ∉ informal_name) - let formal_nodes ← formal_deps.mapM (formalToHTML) - let nodes := String.intercalate "\n" formal_nodes.toList - let informalNodes ← informal.mapM (informalToHTML) - let informalNodes := String.intercalate "\n" informalNodes.toList - let header := "--- +/-- Making the HTML file for dependency graph. -/ +def mkHTML (depDecls : DepDecls) : IO Unit := do + IO.println "--- layout: default --- @@ -412,7 +231,15 @@ layout: default
" - let footer := " + + for decl in depDecls.formalDecls do + println! toHTML decl + + for (_, informalDecls) in depDecls.informalModuleMap do + for {toDecl := decl, ..} in informalDecls do + println! toHTML decl + + IO.println "