From ec2e1e7df953ce056d6692d6299b21b932eb314d Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 27 Jan 2025 11:26:02 +0000 Subject: [PATCH] refactor: Lint --- HepLean.lean | 1 + .../Algebras/CrAnAlgebra/Basic.lean | 2 +- .../Algebras/CrAnAlgebra/SuperCommute.lean | 1 - .../Algebras/CrAnAlgebra/TimeOrder.lean | 3 +- .../Algebras/FieldOpAlgebra/Basic.lean | 1 + .../FieldSpecification/Basic.lean | 2 + .../FieldSpecification/CrAnSection.lean | 10 +-- .../FieldSpecification/TimeOrder.lean | 89 +++++++++---------- scripts/MetaPrograms/notes.lean | 3 - 9 files changed, 56 insertions(+), 56 deletions(-) diff --git a/HepLean.lean b/HepLean.lean index e500505..9492019 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -124,6 +124,7 @@ import HepLean.Meta.TransverseTactics import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute +import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.TimeOrder import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.NormalOrder import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean index da2c81d..255d288 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean @@ -113,7 +113,7 @@ lemma ofStateList_sum (φs : List 𝓕.States) : /-- The algebra map taking an element of the free-state algbra to the part of it in the creation and annihlation free algebra spanned by creation operators. -/ -def crPart : 𝓕.States → 𝓕.CrAnAlgebra := fun φ => +def crPart : 𝓕.States → 𝓕.CrAnAlgebra := fun φ => match φ with | States.inAsymp φ => ofCrAnState ⟨States.inAsymp φ, ()⟩ | States.position φ => ofCrAnState ⟨States.position φ, CreateAnnihilate.create⟩ diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean index 25cdfe0..292dc30 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean @@ -14,7 +14,6 @@ variable {𝓕 : FieldSpecification} namespace CrAnAlgebra - /-! ## The super commutor on the CrAnAlgebra. diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean index 69d410d..fbd28ce 100644 --- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean +++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean @@ -46,7 +46,7 @@ lemma timeOrder_ofStateList (φs : List 𝓕.States) : rw [ofStateList_sum, map_sum] enter [2, x] rw [timeOrder_ofCrAnList] - simp + simp only [crAnTimeOrderSign_crAnSection] rw [← Finset.smul_sum] congr rw [ofStateList_sum, sum_crAnSections_timeOrder] @@ -155,6 +155,7 @@ lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.S ## Norm-time order -/ +/-- The normal-time ordering on `CrAnAlgebra`. -/ def normTimeOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 := Basis.constr ofCrAnListBasis ℂ fun φs => normTimeOrderSign φs • ofCrAnList (normTimeOrderList φs) diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean index ffbdce0..033436f 100644 --- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean +++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean @@ -42,6 +42,7 @@ abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCo namespace FieldOpAlgebra variable {𝓕 : FieldSpecification} +/-- The instance of a setoid on `CrAnAlgebra` from the ideal `TwoSidedIdeal`. -/ instance : Setoid (CrAnAlgebra 𝓕) := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.toSetoid lemma equiv_iff_sub_mem_ideal (x y : CrAnAlgebra 𝓕) : diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean index c9ef3cf..cbe795f 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean @@ -66,9 +66,11 @@ def statesToField : 𝓕.States → 𝓕.Fields | States.position φ => φ.1 | States.outAsymp φ => φ.1 +/-- The bool on `States` which is true only for position states. -/ def statesIsPosition : 𝓕.States → Bool | States.position _ => true | _ => false + /-- The statistics associated to a state. -/ def statesStatistic : 𝓕.States → FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean index 49042e4..e251ffe 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean @@ -160,23 +160,23 @@ lemma card_cons_eq {φ : 𝓕.States} {φs : List 𝓕.States} : rw [Fintype.ofEquiv_card consEquiv.symm] simp -lemma card_eq_mul : {φs : List 𝓕.States} → Fintype.card (CrAnSection φs) = +lemma card_eq_mul : {φs : List 𝓕.States} → Fintype.card (CrAnSection φs) = 2 ^ (List.countP 𝓕.statesIsPosition φs) | [] => by simp | States.position _ :: φs => by - simp [statesIsPosition] + simp only [statesIsPosition, List.countP_cons_of_pos] rw [card_cons_eq] rw [card_eq_mul] - simp [statesToCrAnType] + simp only [statesToCrAnType, CreateAnnihilate.CreateAnnihilate_card_eq_two] ring | States.inAsymp x_ :: φs => by - simp [statesIsPosition] + simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg] rw [card_cons_eq] rw [card_eq_mul] simp [statesToCrAnType] | States.outAsymp _ :: φs => by - simp [statesIsPosition] + simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg] rw [card_cons_eq] rw [card_eq_mul] simp [statesToCrAnType] diff --git a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean index 6736e4c..ea74d71 100644 --- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean +++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean @@ -203,7 +203,7 @@ noncomputable instance (φ φ' : 𝓕.CrAnStates) : Decidable (crAnTimeOrderRel instance : IsTotal 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where total a b := IsTotal.total (r := 𝓕.timeOrderRel) a.1 b.1 -/-- Time ordering of `CrAnStates` is transitive. -/ +/-- Time ordering of `CrAnStates` is transitive. -/ instance : IsTrans 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where trans a b c := IsTrans.trans (r := 𝓕.timeOrderRel) a.1 b.1 c.1 @@ -231,7 +231,6 @@ lemma crAnTimeOrderList_nil : crAnTimeOrderList (𝓕 := 𝓕) [] = [] := by ## Relationship to sections -/ - lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : 𝓕.CrAnStates} (h : ψ.1 = φ) : {φs : List 𝓕.States} → (ψs : CrAnSection φs) → Wick.koszulSignInsert 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel ψ ψs.1 = @@ -239,15 +238,15 @@ lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : | [], ⟨[], h⟩ => by simp [Wick.koszulSignInsert] | φ' :: φs, ⟨ψ' :: ψs, h1⟩ => by - simp [Wick.koszulSignInsert, crAnTimeOrderRel, h] - simp at h1 + simp only [Wick.koszulSignInsert, crAnTimeOrderRel, h] + simp only [List.map_cons, List.cons.injEq] at h1 have hi := koszulSignInsert_crAnTimeOrderRel_crAnSection h (φs := φs) ⟨ψs, h1.2⟩ rw [hi] congr · exact h1.1 - · simp [crAnStatistics, crAnStatesToStates, h1.1 ] + · simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply] congr - · simp [crAnStatistics, crAnStatesToStates, h1.1 ] + · simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply] congr exact h1.1 @@ -265,24 +264,24 @@ lemma crAnTimeOrderSign_crAnSection : {φs : List 𝓕.States} → (ψs : CrAnSe lemma orderedInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : 𝓕.CrAnStates} (h : ψ.1 = φ) : {φs : List 𝓕.States} → (ψs : CrAnSection φs) → - (List.orderedInsert 𝓕.crAnTimeOrderRel ψ ψs.1).map 𝓕.crAnStatesToStates = + (List.orderedInsert 𝓕.crAnTimeOrderRel ψ ψs.1).map 𝓕.crAnStatesToStates = List.orderedInsert 𝓕.timeOrderRel φ φs | [], ⟨[], _⟩ => by - simp [Wick.koszulSignInsert] + simp only [List.orderedInsert, List.map_cons, List.map_nil, List.cons.injEq, and_true] exact h | φ' :: φs, ⟨ψ' :: ψs, h1⟩ => by - simp [Wick.koszulSignInsert, crAnTimeOrderRel, h] - simp at h1 + simp only [List.orderedInsert, crAnTimeOrderRel, h] + simp only [List.map_cons, List.cons.injEq] at h1 by_cases hr : timeOrderRel φ φ' - · simp [hr] + · simp only [hr, ↓reduceIte] rw [← h1.1] at hr - simp [crAnStatesToStates] at hr - simp [hr] + simp only [crAnStatesToStates] at hr + simp only [hr, ↓reduceIte, List.map_cons, List.cons.injEq] exact And.intro h (And.intro h1.1 h1.2) - · simp [hr] + · simp only [hr, ↓reduceIte] rw [← h1.1] at hr - simp [crAnStatesToStates] at hr - simp [hr] + simp only [crAnStatesToStates] at hr + simp only [hr, ↓reduceIte, List.map_cons, List.cons.injEq] apply And.intro h1.1 exact orderedInsert_crAnTimeOrderRel_crAnSection h ⟨ψs, h1.2⟩ @@ -291,65 +290,65 @@ lemma crAnTimeOrderList_crAnSection_is_crAnSection : {φs : List 𝓕.States} | [], ⟨[], h⟩ => by simp | φ :: φs, ⟨ψ :: ψs, h⟩ => by - simp [timeOrderList, crAnTimeOrderList] - simp at h + simp only [crAnTimeOrderList, List.insertionSort, timeOrderList] + simp only [List.map_cons, List.cons.injEq] at h exact orderedInsert_crAnTimeOrderRel_crAnSection h.1 ⟨(List.insertionSort crAnTimeOrderRel ψs), crAnTimeOrderList_crAnSection_is_crAnSection ⟨ψs, h.2⟩⟩ +/-- Time ordering of sections of a list of states. -/ def crAnSectionTimeOrder (φs : List 𝓕.States) (ψs : CrAnSection φs) : CrAnSection (timeOrderList φs) := ⟨crAnTimeOrderList ψs.1, crAnTimeOrderList_crAnSection_is_crAnSection ψs⟩ lemma orderedInsert_crAnTimeOrderRel_injective {ψ ψ' : 𝓕.CrAnStates} (h : ψ.1 = ψ'.1) : - {φs : List 𝓕.States} → (ψs ψs' : 𝓕.CrAnSection φs) → - (ho : List.orderedInsert crAnTimeOrderRel ψ ψs.1 = List.orderedInsert crAnTimeOrderRel ψ' ψs'.1) → - ψ = ψ' ∧ ψs = ψs' + {φs : List 𝓕.States} → (ψs ψs' : 𝓕.CrAnSection φs) → + (ho : List.orderedInsert crAnTimeOrderRel ψ ψs.1 = + List.orderedInsert crAnTimeOrderRel ψ' ψs'.1) → ψ = ψ' ∧ ψs = ψs' | [], ⟨[], _⟩, ⟨[], _⟩, h => by - simp at h + simp only [List.orderedInsert, List.cons.injEq, and_true] at h simpa using h | φ :: φs, ⟨ψ1 :: ψs, h1⟩, ⟨ψ1' :: ψs', h1'⟩, ho => by - simp at h1 h1' + simp only [List.map_cons, List.cons.injEq] at h1 h1' have ih := orderedInsert_crAnTimeOrderRel_injective h ⟨ψs, h1.2⟩ ⟨ψs', h1'.2⟩ - simp at ho + simp only [List.orderedInsert] at ho by_cases hr : crAnTimeOrderRel ψ ψ1 - · simp_all + · simp_all only [ite_true] by_cases hr2 : crAnTimeOrderRel ψ' ψ1' · simp_all - · simp [crAnTimeOrderRel] at hr hr2 - simp_all + · simp only [crAnTimeOrderRel] at hr hr2 + simp_all only rw [crAnStatesToStates] at h1 h1' rw [h1.1] at hr rw [h1'.1] at hr2 exact False.elim (hr2 hr) - · simp_all + · simp_all only [ite_false] by_cases hr2 : crAnTimeOrderRel ψ' ψ1' - · simp [crAnTimeOrderRel] at hr hr2 - simp_all + · simp only [crAnTimeOrderRel] at hr hr2 + simp_all only rw [crAnStatesToStates] at h1 h1' rw [h1.1] at hr rw [h1'.1] at hr2 exact False.elim (hr hr2) - · simp [hr2] at ho + · simp only [hr2, ↓reduceIte, List.cons.injEq] at ho have ih' := ih ho.2 - simp_all + simp_all only [and_self, implies_true, not_false_eq_true, true_and] apply Subtype.ext - simp + simp only [List.cons.injEq, true_and] rw [Subtype.eq_iff] at ih' exact ih'.2 -lemma crAnSectionTimeOrder_injective : {φs : List 𝓕.States} → +lemma crAnSectionTimeOrder_injective : {φs : List 𝓕.States} → Function.Injective (𝓕.crAnSectionTimeOrder φs) | [], ⟨[], _⟩, ⟨[], _⟩ => by simp | φ :: φs, ⟨ψ :: ψs, h⟩, ⟨ψ' :: ψs', h'⟩ => by intro h1 apply Subtype.ext - simp - simp [crAnSectionTimeOrder] at h1 + simp only [List.cons.injEq] + simp only [crAnSectionTimeOrder] at h1 rw [Subtype.eq_iff] at h1 - simp [crAnTimeOrderList] at h1 - simp at h h' - have hi := crAnSectionTimeOrder_injective (φs := φs) (a₁ := ⟨ψs, h.2⟩) (a₂ := ⟨ψs', h'.2⟩) + simp only [crAnTimeOrderList, List.insertionSort] at h1 + simp only [List.map_cons, List.cons.injEq] at h h' rw [crAnStatesToStates] at h h' have hin := orderedInsert_crAnTimeOrderRel_injective (by rw [h.1, h'.1]) (𝓕.crAnSectionTimeOrder φs ⟨ψs, h.2⟩) @@ -364,7 +363,7 @@ lemma crAnSectionTimeOrder_bijective (φs : List 𝓕.States) : rw [Fintype.bijective_iff_injective_and_card] apply And.intro crAnSectionTimeOrder_injective apply CrAnSection.card_perm_eq - simp [timeOrderList] + simp only [timeOrderList] exact List.Perm.symm (List.perm_insertionSort timeOrderRel φs) lemma sum_crAnSections_timeOrder {φs : List 𝓕.States} [AddCommMonoid M] @@ -392,15 +391,15 @@ instance : IsTotal 𝓕.CrAnStates 𝓕.normTimeOrderRel where total a b := by simp only [normTimeOrderRel] match IsTotal.total (r := 𝓕.crAnTimeOrderRel) a b, - IsTotal.total (r := 𝓕.normalOrderRel) a b with + IsTotal.total (r := 𝓕.normalOrderRel) a b with | Or.inl h1, Or.inl h2 => simp [h1, h2] - | Or.inr h1, Or.inl h2 => - simp [h1, h2] + | Or.inr h1, Or.inl h2 => + simp only [h1, h2, imp_self, and_true, true_and] by_cases hn : crAnTimeOrderRel a b · simp [hn] · simp [hn] | Or.inl h1, Or.inr h2 => - simp [h1, h2] + simp only [h1, true_and, h2, imp_self, and_true] by_cases hn : crAnTimeOrderRel b a · simp [hn] · simp [hn] @@ -410,7 +409,7 @@ instance : IsTotal 𝓕.CrAnStates 𝓕.normTimeOrderRel where instance : IsTrans 𝓕.CrAnStates 𝓕.normTimeOrderRel where trans a b c := by intro h1 h2 - simp_all [normTimeOrderRel] + simp_all only [normTimeOrderRel] apply And.intro · exact IsTrans.trans _ _ _ h1.1 h2.1 · intro hc diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean index 64c4ad4..b708f07 100644 --- a/scripts/MetaPrograms/notes.lean +++ b/scripts/MetaPrograms/notes.lean @@ -144,12 +144,9 @@ def perturbationTheory : Note where .p "We will want to consider all three of these types of states simultanously so we define and inductive type `States` which is the disjoint union of these three types of states.", .name `FieldSpecification.States, - .name `FieldSpecification.StateAlgebra, .h2 "Time ordering", .name `FieldSpecification.timeOrderRel, .name `FieldSpecification.timeOrderSign, - .name `FieldSpecification.StateAlgebra.timeOrder, - .name `FieldSpecification.StateAlgebra.timeOrder_eq_maxTimeField_mul_finset, .h2 "Creation and annihilation states", .h2 "Normal ordering", .h2 "Proto-operator algebra",