From a3988a49d4d6db3eb7d13d32c278ccf3a86c48c6 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 16 Aug 2024 16:15:39 -0400 Subject: [PATCH] refactor: Lint --- HepLean/SpaceTime/LorentzTensor/Basic.lean | 2 +- .../LorentzTensor/EinsteinNotation/Basic.lean | 4 +- .../EinsteinNotation/IndexNotation.lean | 6 ++- .../EinsteinNotation/lemmas.lean | 25 +------------ .../LorentzTensor/IndexNotation/Basic.lean | 5 ++- .../IndexNotation/Contraction.lean | 37 +++++++++---------- .../IndexNotation/IndexString.lean | 8 ++-- .../IndexNotation/Relations.lean | 7 ---- .../IndexNotation/TensorIndex.lean | 1 - .../LorentzTensor/Real/IndexNotation.lean | 2 +- .../LorentzTensor/RisingLowering.lean | 1 + 11 files changed, 35 insertions(+), 63 deletions(-) diff --git a/HepLean/SpaceTime/LorentzTensor/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Basic.lean index 12f3721..b7fbffc 100644 --- a/HepLean/SpaceTime/LorentzTensor/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/Basic.lean @@ -308,7 +308,7 @@ def mapIso {c : ๐“ฃ.ColorMap X} {d : ๐“ฃ.ColorMap Y} (e : X โ‰ƒ Y) (h : c.MapI (PiTensorProduct.reindex R _ e) โ‰ชโ‰ซโ‚— (PiTensorProduct.congr (fun y => ๐“ฃ.colorModuleCast (by rw [h]; simp))) -lemma mapIso_ext {c : ๐“ฃ.ColorMap X} {d : ๐“ฃ.ColorMap Y} (e e' : X โ‰ƒ Y) (h : c.MapIso e d) +lemma mapIso_ext {c : ๐“ฃ.ColorMap X} {d : ๐“ฃ.ColorMap Y} (e e' : X โ‰ƒ Y) (h : c.MapIso e d) (h' : c.MapIso e' d) (he : e = e') : ๐“ฃ.mapIso e h = ๐“ฃ.mapIso e' h' := by simp [he] diff --git a/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Basic.lean index 48d48df..285af2b 100644 --- a/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/Basic.lean @@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith -/ import Mathlib.LinearAlgebra.StdBasis import HepLean.SpaceTime.LorentzTensor.Basic -import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic import Mathlib.LinearAlgebra.DirectSum.Finsupp import Mathlib.LinearAlgebra.Finsupp /-! @@ -30,7 +29,6 @@ instance : Fintype einsteinTensorColor.Color := Unit.fintype instance : DecidableEq einsteinTensorColor.Color := instDecidableEqPUnit - variable {R : Type} [CommSemiring R] /-- The `TensorStructure` associated with `n`-dimensional tensors. -/ @@ -98,7 +96,7 @@ def toVec : (einsteinTensor R n).Tensor ![Unit.unit] โ‰ƒโ‚—[R] Fin n โ†’ R := /-- A matrix from an Einstein tensor with two indices. -/ def toMatrix : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit] โ‰ƒโ‚—[R] Matrix (Fin n) (Fin n) R := ((einsteinTensor R n).mapIso ((Fin.castOrderIso - (by rfl : (Nat.succ 0).succ = Nat.succ 0 + Nat.succ 0)).toEquiv.trans + (by rfl : (Nat.succ 0).succ = Nat.succ 0 + Nat.succ 0)).toEquiv.trans finSumFinEquiv.symm) (by funext x; fin_cases x; rfl; rfl)).trans <| ((einsteinTensor R n).tensoratorEquiv ![0] ![0]).symm.trans <| (TensorProduct.congr ((PiTensorProduct.subsingletonEquiv 0)) diff --git a/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean index 6d367b7..4a56855 100644 --- a/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean +++ b/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/IndexNotation.lean @@ -59,7 +59,8 @@ lemma toTensorColor_eq : (einsteinTensor R n).toTensorColor = einsteinTensorColo /-- The construction of a tensor index from a tensor and a string satisfying conditions which can be automatically checked. This is a modified version of `TensorStructure.TensorIndex.mkDualMap` specific to real Lorentz tensors. -/ -noncomputable def fromIndexStringColor {R : Type} [CommSemiring R] {cn : Fin n โ†’ einsteinTensorColor.Color} +noncomputable def fromIndexStringColor {R : Type} [CommSemiring R] + {cn : Fin n โ†’ einsteinTensorColor.Color} (T : (einsteinTensor R m).Tensor cn) (s : String) (hs : listCharIsIndexString einsteinTensorColor.Color s.toList = true) (hn : n = (toIndexList' s hs).length) @@ -73,7 +74,8 @@ noncomputable def fromIndexStringColor {R : Type} [CommSemiring R] {cn : Fin n (TensorColor.ColorMap.DualMap.boolFin'_DualMap hd) @[simp] -lemma fromIndexStringColor_indexList {R : Type} [CommSemiring R] {cn : Fin n โ†’ einsteinTensorColor.Color} +lemma fromIndexStringColor_indexList {R : Type} [CommSemiring R] + {cn : Fin n โ†’ einsteinTensorColor.Color} (T : (einsteinTensor R m).Tensor cn) (s : String) (hs : listCharIsIndexString einsteinTensorColor.Color s.toList = true) (hn : n = (toIndexList' s hs).length) diff --git a/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/lemmas.lean b/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/lemmas.lean index 0bdda67..776b757 100644 --- a/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/lemmas.lean +++ b/HepLean/SpaceTime/LorentzTensor/EinsteinNotation/lemmas.lean @@ -11,36 +11,15 @@ import HepLean.SpaceTime.LorentzTensor.EinsteinNotation.IndexNotation -/ -set_option profiler true namespace einsteinTensor open einsteinTensorColor open IndexNotation IndexString open TensorStructure TensorIndex -variable {R : Type} [CommSemiring R] {n m : โ„•} - -/-! TODO: Fix notation here. -/ -set_option maxHeartbeats 0 +variable {R : Type} [CommSemiring R] {n m : โ„•}/- lemma swap_eq_transpose (T : (einsteinTensor R n).Tensor ![Unit.unit, Unit.unit]) : (T|"แตขโ‚แตขโ‚‚") โ‰ˆ ((toMatrix.symm (toMatrix T).transpose)|"แตขโ‚‚แตขโ‚") := by - apply And.intro - apply And.intro - ยท simp only [toTensorColor_eq, indexNotation_eq_color, ColorIndexList.contr, - fromIndexStringColor_indexList, IndexList.contrIndexList_length] - decide - apply And.intro - ยท simp only [toTensorColor_eq, indexNotation_eq_color, ColorIndexList.contr, - fromIndexStringColor_indexList, IndexList.contrIndexList_length] - rw [IndexList.withUniqueDualInOther_eq_univ_iff_forall] - intro x - have h1 : (toIndexList' "แตขโ‚แตขโ‚‚" (by decide) : IndexList einsteinTensorColor.Color).contrIndexList.length - = 2 := by - decide - sorry - - - - sorry + sorry-/ end einsteinTensor diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean index 2b557a7..cdc3654 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean @@ -192,6 +192,7 @@ lemma ext (h : l.val = l2.val) : l = l2 := by cases l2 simp_all +/-- The index list constructed by prepending an index to the list. -/ def cons (i : Index X) : IndexList X := {val := i :: l.val} @[simp] @@ -202,9 +203,9 @@ lemma cons_val (i : Index X) : (l.cons i).val = i :: l.val := by lemma cons_length (i : Index X) : (l.cons i).length = l.length + 1 := by rfl -def induction {P : IndexList X โ†’ Prop } (h_nil : P {val := โˆ…}) +lemma induction {P : IndexList X โ†’ Prop } (h_nil : P {val := โˆ…}) (h_cons : โˆ€ (x : Index X) (xs : IndexList X), P xs โ†’ P (xs.cons x)) (l : IndexList X) : P l := by - cases' l with val + cases' l with val induction val with | nil => exact h_nil | cons x xs ih => diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean index 15a7486..1ab220d 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean @@ -69,7 +69,7 @@ lemma withDual_union_withoutDual : l.withDual โˆช l.withoutDual = Finset.univ := ยท simp at h simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h] -lemma mem_withoutDual_iff_count : +lemma mem_withoutDual_iff_count : fun i => i โˆˆ l.withoutDual = (fun (i : Index X) => l.val.countP (fun j => i.id = j.id) = 1) โˆ˜ l.val.get := by funext x @@ -90,18 +90,18 @@ lemma mem_withoutDual_iff_count : subst hi hj simp at h1 subst hi - exact h5 (by exact fun a => hj (id (Eq.symm a))) (congrArg Index.id h3) + exact h5 (fun a => hj (id (Eq.symm a))) (congrArg Index.id h3) subst hj - exact h4 (by exact fun a => hi (id (Eq.symm a))) (congrArg Index.id h2) - exact h5 (by exact fun a => hj (id (Eq.symm a))) (congrArg Index.id h3) - rw [List.duplicate_iff_two_le_count] at h1 + exact h4 (fun a => hi (id (Eq.symm a))) (congrArg Index.id h2) + exact h5 (fun a => hj (id (Eq.symm a))) (congrArg Index.id h3) + rw [List.duplicate_iff_two_le_count] at h1 simp at h1 by_cases hx : List.count l.val[โ†‘x] l.val = 0 rw [@List.count_eq_zero] at hx - have hl : l.val[โ†‘x] โˆˆ l.val := by - simp + have hl : l.val[โ†‘x] โˆˆ l.val := by + simp only [Fin.getElem_fin] exact List.getElem_mem l.val (โ†‘x) (Fin.val_lt_of_le x (le_refl l.length)) - exact False.elim (h x (fun a => hx hl) rfl) + exact False.elim (h x (fun _ => hx hl) rfl) have hln : List.count l.val[โ†‘x] l.val = 1 := by rw [@Nat.lt_succ] at h1 rw [@Nat.le_one_iff_eq_zero_or_eq_one] at h1 @@ -114,14 +114,14 @@ lemma mem_withoutDual_iff_count : have h2 := List.indexOf_lt_length.mpr hxt have h3 : xt = l.val.get โŸจxid, h2โŸฉ := by exact Eq.symm (List.indexOf_get h2) - simp - by_cases hxtx : โŸจxid, h2โŸฉ = x + simp only [decide_eq_true_eq, Fin.getElem_fin, beq_iff_eq] + by_cases hxtx : โŸจxid, h2โŸฉ = x rw [h3, hxtx] - simp + simp only [List.get_eq_getElem] apply Iff.intro intro h' - have hn := h โŸจxid, h2โŸฉ (by exact fun a => hxtx (id (Eq.symm a)) ) (by rw [h3] at h'; exact h') - exact False.elim (h x (fun a => hn) rfl) + have hn := h โŸจxid, h2โŸฉ (fun a => hxtx (id (Eq.symm a))) (by rw [h3] at h'; exact h') + exact False.elim (h x (fun _ => hn) rfl) intro h' rw [h'] ยท intro h @@ -207,7 +207,7 @@ def contrIndexList : IndexList X where /-! TODO: Prove that `contrIndexList'` and `contrIndexList` are equivalent. -/ /-- An alternative form of the contracted index list. -/ def contrIndexList' : IndexList X where - val := l.val.filter (fun i => l.val.countP (fun j => i.id = j.id) = 1) + val := l.val.filter (fun i => l.val.countP (fun j => i.id = j.id) = 1) @[simp] lemma contrIndexList_length : l.contrIndexList.length = l.withoutDual.card := by @@ -529,17 +529,14 @@ lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Fins exact Eq.symm (Option.eq_some_of_isSome hs) lemma withUniqueDualInOther_eq_univ_iff_forall : - l.withUniqueDualInOther l2 = Finset.univ โ†” - โˆ€ (x : Fin l.length), - l.getDual? x = none โˆง - (l.getDualInOther? l2 x).isSome = true โˆง - โˆ€ (j : Fin l2.length), l.AreDualInOther l2 x j โ†’ some j = l.getDualInOther? l2 x := by + l.withUniqueDualInOther l2 = Finset.univ โ†” + โˆ€ (x : Fin l.length), l.getDual? x = none โˆง (l.getDualInOther? l2 x).isSome = true โˆง + โˆ€ (j : Fin l2.length), l.AreDualInOther l2 x j โ†’ some j = l.getDualInOther? l2 x := by rw [Finset.eq_univ_iff_forall] simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ, true_and] - end IndexList end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean index a63476e..6966180 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean @@ -22,19 +22,22 @@ namespace IndexNotation variable (X : Type) [IndexNotation X] [Fintype X] [DecidableEq X] - /-! ## The definition of an index string -/ +/-- Takes in a list of characters and splits it into a list of characters at those characters + which are notation characters e.g. `'แต˜'`. -/ def stringToPreIndexList (l : List Char) : List (List Char) := let indexHeads := l.filter (fun c => isNotationChar X c) let indexTails := l.splitOnP (fun c => isNotationChar X c) let l' := List.zip indexHeads indexTails.tail l'.map fun x => x.1 :: x.2 +/-- A bool which is true given a list of characters if and only if everl element + of the corresponding `stringToPreIndexList` correspondings to an index. -/ def listCharIsIndexString (l : List Char) : Bool := (stringToPreIndexList X l).all fun l => (listCharIndex X l && l โ‰  []) @@ -55,6 +58,7 @@ variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] def toCharList (s : IndexString X) : List Char := s.val.toList /-! TODO: Move. -/ +/-- Takes a list of characters to the correpsonding index if it exists else to `none`. -/ def charListToOptionIndex (l : List Char) : Option (Index X) := if h : listCharIndex X l && l โ‰  [] then some (Index.ofCharList l (by simpa using h)) @@ -66,8 +70,6 @@ def toIndexList (s : IndexString X) : IndexList X := {val := (stringToPreIndexList X s.toCharList).filterMap fun l => charListToOptionIndex l} - - /-- The formation of an index list from a string `s` statisfying `listCharIndexStringBool`. -/ def toIndexList' (s : String) (hs : listCharIsIndexString X s.toList = true) : IndexList X := toIndexList โŸจs, hsโŸฉ diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean index 73ad27b..0c6ed8e 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean @@ -62,13 +62,6 @@ namespace ContrPerm variable {l l' l2 l3 : ColorIndexList ๐“’} -lemma of_perm (h : l.contr.val.Perm l'.contr.val) : l.ContrPerm l' := by - apply And.intro - exact List.Perm.length_eq h - apply And.intro - sorry - sorry - @[symm] lemma symm (h : ContrPerm l l') : ContrPerm l' l := by rw [ContrPerm] at h โŠข diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean index 570a2e7..93e701f 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean @@ -480,7 +480,6 @@ lemma add_assoc' {Tโ‚ Tโ‚‚ Tโ‚ƒ : ๐“ฃ.TensorIndex} {h' : AddCond Tโ‚‚ Tโ‚ƒ} (h contrPermEquiv_trans, contrPermEquiv_trans] rfl - open AddCond in lemma add_assoc {Tโ‚ Tโ‚‚ Tโ‚ƒ : ๐“ฃ.TensorIndex} {h' : AddCond Tโ‚ Tโ‚‚} (h : AddCond (Tโ‚ +[h'] Tโ‚‚) Tโ‚ƒ) : Tโ‚ +[h'] Tโ‚‚ +[h] Tโ‚ƒ = Tโ‚ +[h'.add_right_of_add_left h] (Tโ‚‚ +[h'.of_add_left h] Tโ‚ƒ) := by diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean index 02f4479..33f58e0 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean @@ -76,7 +76,7 @@ lemma toTensorColor_eq : (realLorentzTensor d).toTensorColor = realTensorColor : `TensorStructure.TensorIndex.mkDualMap` specific to real Lorentz tensors. -/ noncomputable def fromIndexStringColor {cn : Fin n โ†’ realTensorColor.Color} (T : (realLorentzTensor d).Tensor cn) (s : String) - (hs : listCharIndexStringBool realTensorColor.Color s.toList = true) + (hs : listCharIsIndexString realTensorColor.Color s.toList = true) (hn : n = (toIndexList' s hs).length) (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual) (hC : IndexList.ColorCond.bool (toIndexList' s hs)) diff --git a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean index 3a54c76..817bc45 100644 --- a/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean +++ b/HepLean/SpaceTime/LorentzTensor/RisingLowering.lean @@ -68,6 +68,7 @@ lemma boolFin_DualMap {cโ‚ cโ‚‚ : ๐“’.ColorMap (Fin n)} (h : boolFin cโ‚ cโ‚‚ apply List.getElem_mem exact h x (h2 _) +/-- The bool which is ture if `๐“’.colorQuot (cโ‚ i) = ๐“’.colorQuot (cโ‚‚ i)` is true for all `i`. -/ def boolFin' (cโ‚ cโ‚‚ : ๐“’.ColorMap (Fin n)) : Bool := โˆ€ (i : Fin n), ๐“’.colorQuot (cโ‚ i) = ๐“’.colorQuot (cโ‚‚ i)