feat: More computable form of contracting indices

HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean

@@ -70,8 +70,8 @@ lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ :=
     simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h]
 
 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
+    (fun i => (i ∈ l.withoutDual : Bool)) =
+    (fun (i : Index X) => (l.val.countP (fun j => i.id = j.id) = 1 : Bool)) ∘ l.val.get := by
   funext x
   simp [withoutDual, getDual?]
   rw [Fin.find_eq_none_iff]
@@ -181,11 +181,62 @@ lemma mem_withoutDual_iff_count :
     simp at h1
     simp [idMap] at hn
     simp [hn]
+
 /-- An equivalence from `Fin l.withoutDual.card` to `l.withoutDual` determined by
   the order on `l.withoutDual` inherted from `Fin`. -/
 def withoutDualEquiv : Fin l.withoutDual.card ≃ l.withoutDual :=
   (Finset.orderIsoOfFin l.withoutDual (by rfl)).toEquiv
 
+lemma list_ofFn_withoutDualEquiv_eq_sort :
+    List.ofFn (Subtype.val ∘ l.withoutDualEquiv) = l.withoutDual.sort (fun i j => i ≤ j) := by
+  rw [@List.ext_get_iff]
+  apply And.intro
+  simp only [List.length_ofFn, Finset.length_sort]
+  intro n h1 h2
+  simp only [List.get_eq_getElem, List.getElem_ofFn, Function.comp_apply]
+  rfl
+
+lemma withoutDual_sort_eq_filter : l.withoutDual.sort (fun i j => i ≤ j) =
+    (List.finRange l.length).filter (fun i => i ∈ l.withoutDual) := by
+  have h1 {n : ℕ} (s : Finset (Fin n)) (p : Fin n → Prop) [DecidablePred p] :
+      List.filter p (Finset.sort (fun i j => i ≤ j) s) =
+      Finset.sort (fun i j => i ≤ j) (Finset.filter p s) := by
+    simp [Finset.filter, Finset.sort]
+    have : ∀ (m : Multiset (Fin n)), List.filter p (Multiset.sort (fun i j => i ≤ j) m) =
+        Multiset.sort (fun i j => i ≤ j) (Multiset.filter p m) := by
+      apply Quot.ind
+      intro m
+      simp [List.mergeSort]
+      have h1 : List.Sorted (fun i j => i ≤ j) (List.filter (fun b => decide (p b))
+          (List.mergeSort (fun i j => i ≤ j) m)) := by
+        simp [List.Sorted]
+        rw [List.pairwise_filter]
+        rw [@List.pairwise_iff_get]
+        intro i j h1 _ _
+        have hs : List.Sorted (fun i j => i ≤ j) (List.mergeSort (fun i j => i ≤ j) m) := by
+          exact List.sorted_mergeSort (fun i j => i ≤ j) m
+        simp [List.Sorted] at hs
+        rw [List.pairwise_iff_get] at hs
+        exact hs i j h1
+      have hp1 : (List.mergeSort (fun i j => i ≤ j) m).Perm m := by
+        exact List.perm_mergeSort (fun i j => i ≤ j) m
+      have hp2 : (List.filter (fun b => decide (p b)) ((List.mergeSort (fun i j => i ≤ j) m))).Perm
+          (List.filter (fun b => decide (p b)) m) := by
+        exact List.Perm.filter (fun b => decide (p b)) hp1
+      have hp3 : (List.filter (fun b => decide (p b)) m).Perm
+        (List.mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)) := by
+        exact List.Perm.symm (List.perm_mergeSort (fun i j => i ≤ j)
+        (List.filter (fun b => decide (p b)) m))
+      have hp4 := hp2.trans hp3
+      refine List.eq_of_perm_of_sorted hp4 h1 ?_
+      exact List.sorted_mergeSort (fun i j => i ≤ j) (List.filter (fun b => decide (p b)) m)
+    exact this s.val
+  rw [withoutDual]
+  rw [← h1]
+  simp only [Option.isNone_iff_eq_none, Finset.mem_filter, Finset.mem_univ, true_and]
+  apply congrArg
+  exact Fin.sort_univ l.length
+
 /-- An equivalence splitting the indices of an index list `l` into those indices
   which have a dual in `l` and those which do not have a dual in `l`. -/
 def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length :=
@@ -202,27 +253,44 @@ def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length :=
 /-- The index list formed from `l` by selecting only those indices in `l` which
   do not have a dual. -/
 def contrIndexList : IndexList X where
+  val := l.val.filter (fun i => l.val.countP (fun j => i.id = j.id) = 1)
+
+/-- An alternative form of the contracted index list. -/
+@[simp]
+def contrIndexList' : IndexList X where
   val := List.ofFn (l.val.get ∘ Subtype.val ∘ l.withoutDualEquiv)
 
-/-! 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)
+lemma contrIndexList_eq_contrIndexList' : l.contrIndexList = l.contrIndexList' := by
+  apply ext
+  simp only [contrIndexList']
+  trans List.map l.val.get (List.ofFn (Subtype.val ∘ ⇑l.withoutDualEquiv))
+  swap
+  simp only [List.map_ofFn]
+  rw [list_ofFn_withoutDualEquiv_eq_sort, withoutDual_sort_eq_filter]
+  simp [contrIndexList]
+  let f1 : Index X → Bool := fun (i : Index X) => l.val.countP (fun j => i.id = j.id) = 1
+  let f2 : (Fin l.length) → Bool := fun i => i ∈ l.withoutDual
+  change List.filter f1 l.val = List.map l.val.get (List.filter f2 (List.finRange l.length))
+  have hf : f2 = f1 ∘ l.val.get := mem_withoutDual_iff_count l
+  rw [hf]
+  rw [← List.filter_map]
+  apply congrArg
+  simp [length]
 
 @[simp]
 lemma contrIndexList_length : l.contrIndexList.length = l.withoutDual.card := by
-  simp [contrIndexList, withoutDual, length]
+  simp [contrIndexList_eq_contrIndexList', withoutDual, length]
 
 @[simp]
 lemma contrIndexList_idMap (i : Fin l.contrIndexList.length) : l.contrIndexList.idMap i
     = l.idMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
-  simp [contrIndexList, idMap]
+  simp [contrIndexList_eq_contrIndexList', idMap]
   rfl
 
 @[simp]
 lemma contrIndexList_colorMap (i : Fin l.contrIndexList.length) : l.contrIndexList.colorMap i
     = l.colorMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
-  simp [contrIndexList, colorMap]
+  simp [contrIndexList_eq_contrIndexList', colorMap]
   rfl
 
 lemma contrIndexList_areDualInSelf (i j : Fin l.contrIndexList.length) :
@@ -273,7 +341,7 @@ lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList
   rw [contrIndexList_length, h1]
   simp only [Finset.card_univ, Fintype.card_fin, List.get_eq_getElem, true_and]
   intro n h1' h2
-  simp [contrIndexList]
+  simp [contrIndexList_eq_contrIndexList']
   congr
   simp [withoutDualEquiv]
   simp [h1]