clean up, skip transitive import, unuse Vector.lean

Author: m4lvin

Pdl.lean

@@ -15,7 +15,6 @@ import Pdl.LocalTableau
 import Pdl.Tableau
 import Pdl.TableauExamples
 import Pdl.TableauPath
-import Pdl.Vector
 import Pdl.Soundness
 import Pdl.Game
 import Pdl.Completeness

Pdl/Distance.lean

@@ -434,14 +434,8 @@ theorem relateSeq_existsH_dist (v_αγ_w : relateSeq M (α :: γ) v w)
     rw [αγ_eq_α_γ, ← δ_eq_α]
     simp [distance_list_append]
     apply iInf_le
-  have two : distance_list M v w (α :: γ) ≤ distance_list M v w (δ ++ γ) := by
-    have := fun u => @relateSeq_H_imp_relate α W M v u _ _ in_H v_X
-    have : ∀ (u : W), relateSeq M  (δ ++ γ) v u → relateSeq M (α :: γ) v u := by
-      intro u
-      rw [relateSeq_append]
-      rw [relateSeq_cons]
-      aesop
-    exact distList_le_of_Hsat M v _ α γ in_H v_X -- use (e)
+  have two : distance_list M v w (α :: γ) ≤ distance_list M v w (δ ++ γ) :=
+    distList_le_of_Hsat M v _ α γ in_H v_X -- use (e)
   exact ⟨in_H, v_X, eq_of_le_of_le one two⟩
 
 /-- 7.47 (h)

Pdl/PartInterpolation.lean

@@ -1,7 +1,6 @@
 import Mathlib.Data.Finset.Basic
 
 import Pdl.Completeness
-import Pdl.Distance
 
 /-! # Interpolants for Partitions (big part of Section 7) -/
 

Pdl/Soundness.lean

@@ -5,9 +5,8 @@ import Mathlib.Data.Prod.Lex
 import Mathlib.Data.Vector.Defs
 import Pdl.TableauPath
 import Mathlib.Data.ENat.Defs
+
 import Pdl.LocalSoundness
-import Pdl.Distance
-import Pdl.Measures
 
 /-! # Soundness (Section 6) -/
 
@@ -164,9 +163,6 @@ theorem nodeAt_companionOf_multisetEq {tab : Tableau .nil X} (s : PathIn tab) lp
   convert k_same
   simp only [List.get_eq_getElem]
   have := PathIn.toHistory_eq_Hist s
-  have : (tabAt_fst_length_eq_toHistory_length s ▸ k).val = k.val := by
-    apply Fin.val_eq_val_of_heq
-    simp
   simp_all
 
 /-- Any repeat and companion are both loaded. -/
@@ -465,41 +461,34 @@ theorem ePropB.b {tab : Tableau .nil X} (s t : PathIn tab) :
     exact Relation.ReflTransGen.single comp
 
 theorem c_claim {a : Sequent} {tab : Tableau [] a} (t l c : PathIn tab) :
-  (nodeAt t).isFree → t < l → l ♥ c → t < c := by
-intro t_free t_above_l l_hearts_c
-have ⟨lpr, tabAt_l_def, c_def⟩ := l_hearts_c
-by_contra hyp
-have c_above_l : c < l := companion_lt l_hearts_c
-have comp_leq_t : c ≤ t := by
-  rcases path_revEuclidean _ _ _ t_above_l c_above_l with h|h|h
-  · exact False.elim (hyp h)
-  · exact Relation.TransGen.to_reflTransGen h
-  · rw [h]
-    exact Relation.ReflTransGen.refl
-have comp_lt_t : c < t := by
-  apply Relation.TransGen_of_ReflTransGen comp_leq_t
-  intro c_eq_t
-  have c_loaded := (companion_loaded l_hearts_c).2
+    (nodeAt t).isFree → t < l → l ♥ c → t < c := by
+  intro t_free t_above_l l_hearts_c
+  have ⟨lpr, tabAt_l_def, c_def⟩ := l_hearts_c
+  by_contra hyp
+  have c_above_l : c < l := companion_lt l_hearts_c
+  have comp_leq_t : c ≤ t := by
+    rcases path_revEuclidean _ _ _ t_above_l c_above_l with h|h|h
+    · exact False.elim (hyp h)
+    · exact Relation.TransGen.to_reflTransGen h
+    · rw [h]
+      exact Relation.ReflTransGen.refl
+  have ⟨k, k', def_c, def_t, k'_le_k⟩ := exists_rewinds_middle comp_leq_t (Relation.TransGen.to_reflTransGen t_above_l)
+  have t_loaded : (nodeAt t).isLoaded := by
+    rw [←def_t]
+    apply companion_to_repeat_all_loaded lpr tabAt_l_def c_def k'
+    apply Fin.le_def.1 at k'_le_k
+    have k_is_lpr_succ : k.1 = lpr.1.1.succ := by
+      have ⟨k_val, k_def⟩ := k
+      have ⟨⟨lpr_len, lpr_len_pf⟩, ⟨eq_con, loaded_con⟩⟩ := lpr
+      unfold companionOf at c_def
+      rw [c_def] at def_c
+      have := rewind_is_inj def_c
+      simp [Fin.cast] at this
+      exact this
+    simp_all
   simp [Sequent.isFree] at t_free
-  rw [←c_eq_t, c_loaded] at t_free
-  contradiction
-have ⟨k, k', def_c, def_t, k'_le_k⟩ := exists_rewinds_middle comp_leq_t (Relation.TransGen.to_reflTransGen t_above_l)
-have t_loaded : (nodeAt t).isLoaded := by
-  rw [←def_t]
-  apply companion_to_repeat_all_loaded lpr tabAt_l_def c_def k'
-  apply Fin.le_def.1 at k'_le_k
-  have k_is_lpr_succ : k.1 = lpr.1.1.succ := by
-    have ⟨k_val, k_def⟩ := k
-    have ⟨⟨lpr_len, lpr_len_pf⟩, ⟨eq_con, loaded_con⟩⟩ := lpr
-    unfold companionOf at c_def
-    rw [c_def] at def_c
-    have := rewind_is_inj def_c
-    simp [Fin.cast] at this
-    exact this
-  simp_all
-simp [Sequent.isFree] at t_free
-rw [t_loaded] at t_free
-contradiction
+  rw [t_loaded] at t_free
+  cases t_free
 
 theorem ePropB.c {X} {tab : Tableau .nil X} (s t : PathIn tab) :
     (nodeAt s).isFree → s < t → s <ᶜ t := by
@@ -546,7 +535,6 @@ theorem not_cEquiv_of_free_loaded (s t : PathIn tab)
         have l_s : l ◃* s := Relation.ReflTransGen.trans l_t t_s
         cases eq_or_ne l s
         case inl les =>
-          have := edge_is_strict_ordering sel
           simp_all
         case inr lnes => exact Relation.TransGen_of_ReflTransGen l_s lnes
       case inr shl =>

Pdl/TableauPath.lean

@@ -2,7 +2,6 @@ import Mathlib.Data.Finset.Lattice.Fold
 import Mathlib.Logic.Relation
 
 import Pdl.Tableau
-import Pdl.Vector
 
 /-! # Navigating through tableaux with PathIn
 

Pdl/Vector.lean renamed to Unused/Vector.lean

@@ -3,7 +3,7 @@ import Mathlib.Tactic.Linarith
 
 /-! # Helper Lemmas about Vector
 
-These are used in `Soundness.lean`.
+These were previously used in `Soundness.lean`.
 -/
 
 lemma List.nonempty_drop_sub_succ (δ_not_empty : δ ≠ []) (k : Fin δ.length) :